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 :
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''.
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:
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.