4.4 Building atomic constraints

Atomic constraints come in three forms: equalities of the form , inequalities of the form , and stride constraints ( is divisible by step).

Atomic constraints are manipulated using the EQ_Handle , GEQ_Handle , and Stride_Handle classes. These are derived from the class Constraint_Handle. They are referred to as ``handles'', because atomic constraints do not exist as independent objects. Instead, they are components of another class that is known only to the implementation; each Constraint_Handle contains information about how to access a particular constraint.

The following functions can be used to add an atomic constraint to an F_And :

EQ_Handle F_And::add_EQ()
Creates an equality constraint as a child of the F_And node and returns a EQ_Handle for this constraint. All variables implicitly have a coefficient of zero in this constraint.

GEQ_Handle F_And::add_GEQ()
Creates an inequality constraint as a child of the F_And node and returns a GEQ_Handle for this constraint. All variables have an implicit coefficient of zero in this constraint.

EQ_Handle F_And::add_stride(int step)
The effect of this function is equivalent to creating an F_Exists

node with a new variable alpha as a child of the F_And node and creating an equality constraint as a child of the F_Exists node. The coefficient of alpha in this constraint is step and the coefficients of all other variables is implicitly zero. This can be used to add constraints like `` y is odd'' or `` x+2y+17 is divisible by 3''.

void F_And::add_unknown()
Adds an unknown constraint as a child of the F_And node, thus making the formula an upper bound (see Section 5.6). You don't need to use this function unless you are creating an inexact relation.

Sometimes you may have a relation (perhaps passed in to a function) that you want to modify by adding some constraints to it, but you don't have any pointers into the formula. In these situations, you can use the functions Relation::and_with_GEQ and Relation::and_with_EQ. The affect of calling these functions without arguments, on a relation R, with formula f, is equivalent to creating a constraint e of the appropriate type, changing R's formula to be an F_And node with f and e as children and returns a Constraint_Handle

of the appropriate type for e. All variables have an implicit coefficient of zero in e. There's another version of this function that allows you to copy constraints between relations. If you call either function with a Constraint_Handle c as an argument, the affect is the same except that the coefficients of e are set to be the same as the coefficients of c. Notice that the latter form allows you to convert EQ's to GEQ's and vice-versa; the coefficients are copied, and the resulting constraint just has the semantics of whatever kind of constraint you asked for. It's a little confusing, but it saves you from copying each coefficient individually.

The coefficients of variables and the constant terms in constraints can be updated by using the following member functions: functions:

void Constraint_Handle::update_coef(Variable_ID, int delta)
Add delta to the coefficient of the variable corresponding to Variable_ID .

void Constraint_Handle::update_const(int delta)
Add delta to the constant term of the constraint.

void Constraint_Handle::multiply(int multiplier)
Multiply each coefficient and the constant term by multiplier .

Warning:

Setting numbers of EQs and GEQs

The library allows you to set the number of EQs and GEQs that are available in each problem. As this increases, the library can handle larger and larger problems, but memory use increases as well. If you need to solve large problems, you may have to increase these values. If you need to have many relations existing at the same time, you may need to decrease these values.

The variables to set are maxGEQs and maxEQs . They default to 70 and 35 respectively. If you set these variables, they must be set before you use the Omega Library. If you create any relations, and then change the value of these variables, you will get crashes.

Web Accessibility