Much of the power of the Omega library lies in the ability to walk through the simplified conjunctions (and their constraints) that define a relation. In this section, we'll describe method to do that.
To perform more detailed queries on a relation, we must tell the Omega Library the desired form of the results, and the amount of effort (time) that should be expended in trying to eliminate redundancies. Currently, the only form of query that is supported is disjunctive normal form, though in the future we may include disjoint disjunctive normal form, or a form that contains only inequality constraints.
To request that a relation be simplified to DNF, use the function query_DNF . This returns a pointer to a DNF (we discuss how to use a DNF below). Several levels of simplification are available. Increased effort levels result in better elimination of redundant information in the formula. You can set this level for both removing redundant constraints within a conjunction, or for removing entire conjuncts that are redundant with some other part of the formula. These levels are given as arguments to query_DNF . If no arguments are given, the levels default to (0,0), the lowest level of effort. The current effort levels are given below:
The best way to traverse the formula is by using a series of iterator classes. The overall method to traversing a simplified formula is:
for each conjunct in the DNF
for each equality constraint in the conjunct
for each variable in the constraint
perform some action
for each GEQ constraint in the conjunct
for each variable in the constraint
perform some action
Most often, you will use the DNF *
returned from query_DNF to initialize a DNF_Iterator , which allows you to traverse a list of Conjuncts , which represent the individual conjunctions in the DNF. Note that if you change the relation destructively after obtaining a simplified DNF from it, neither the result of a previous query_DNF
call nor any iterators constructed from it will remain valid.
You can iterate through the EQs or the GEQs in a Conjunct , or both. To browse the EQs, either give the Conjunct as an argument to the EQ_Iterator constructor, or assign the result of the Conjunct::EQs() function to an existing EQ_Iterator . When you dereference an EQ_Iterator , it returns an EQ_Handle . The analogous techniques apply to GEQ_Iterators , to iterate through the GEQs, or to Constraint_Iterators , to iterate through both the EQs and the GEQs.
We have already seen the use of Constraint_Handle s (and its subtypes EQ_Handle and GEQ_Handle ) to build constraints. In this context, a Constraint_Handle (and its derived types) is used only to examine constraints; you cannot modify the constraints returned from any constraint iterator. The following operations are used to query a constraint.
Here is an example of examining the constraints in a Relation . This loop finds all the GEQs involving v in all Conjunct C from Relation R1 , and ``ands'' them with Relation R2 's formula. The only caveat to doing this is that R2 must have at least as many variables in its tuples as R1 does.
for(DNF_iterator di(R1.query_DNF()); di; di++) for(EQ_Iterator ei = (*di)->EQs(); ei; ei++) if((*ei).get_coef(v) != 0) R2.and_with_GEQ(*ei);
You could also loop through all the variables in each conjunct and check their coefficients in each constraint:
You can also loop through all the variables in the conjunct and check their coefficients in each constraint;
for(DNF_iterator di(R1.query_DNF()); di; di++) for(EQ_Iterator ei = (*di)->EQs(); ei; ei++) for(Variable_Iterator vi = (*di)->variables(); vi; vi++)
Since this is a common thing to do, there's a special iterator class that allows you to walk through all the variables that appear in a particular constraint, and get their coefficients. It's called Constr_Vars_Iter. There's also a version of it that will show you only the existentially quantified variables. (An easy way to check if a constraint involves any existentially quantified variables is to get that kind of iterator and check if it is live.)
For a Constr_Vars_Iter, the return value is a Variable_Info
structure. It contains a Variable_ID and an integer for its coefficient in the constraint. You can also use the special functions Variable_ID curr_var() and int curr_coef() to get that information.
The for loop in Figure 5.3 shows an example of the use of these query functions that is redundant with the existing printing functions, but serves to illustrate the query operations.