t      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~An integer-valued term n*v in a formula. A variable in a formula. %A boolean-valued Presburger formula. A relation from points in a domain Z^m  to points in a range Z^n. + This is a wrapper around the Omega library's Relation type. AA relation can be considered as just a set of points in Z^(m+n). @ However, many routines treat the domain and range differently. A set of points in Z^n. + This is a wrapper around the Omega library's Relation type. +Data types containing Presburger formulae. #Extract the pointer from a formula 7Test whether two sets or relations have the same arity 1Convert a raw pointer to an OmegaSet or OmegaRel  The "9 routine takes a parameter specifying how much effort to D put into generating a good result. Higher effort takes more time.  It'.s unspecified what a given effort level does.       !"#$%&'()*+,-. FCreate an Omega set. The first parameter is the number of dimensions : the set inhabits. The second parameter builds a formula  defining the set's members. The set's members are those points * for which the formula evaluates to True. )Dimensionality of the space that the set  inhabits  Set members  Inspect a set'4s low-level representation directly. This function H takes care of data structure traversal and relies on other routines to  interpret the data. AAll three accumulating functions take the set variables as their @ first parameter, and any existentially quantified variables as D their second parameter. The set variables are returned along with  a result value. /Accumulating function for equality constraints 'Initial value for equality constraints 1Accumulating function for inequality constraints )Initial value for inequality constraints $Accumulating function for conjuncts Initial value for conjuncts  Set to query /CCreate an Omega relation. The first two parameters are the number K of dimensions of the domain and range, respectively. The third parameter I builds a formula defining the relation. Two points are related iff the , formula evaluates to True on those points. Dimensionality of the domain Dimensionality of the range  The relation Inspect a relation'4s low-level representation directly. This function H takes care of data structure traversal and relies on other routines to  interpret the data. 2All three accumulating functions take the relation' s input and F output variables as their first and second parameters, respectively, / and any existentially quantified variables as & their second parameter. The relation'!s input and output variables are % returned along with a result value. /Accumulating function for equality constraints 'Initial value for equality constraints 1Accumulating function for inequality constraints )Initial value for inequality constraints $Accumulating function for conjuncts Initial value for conjuncts Relation to query .Input variables, output variables, and result 0@Get a list of relations, one per output variable, with the same D input and output dimensions as the original, but whose constraints B mention only one output variable and no existential constraints. DThis function is needed to create a high-level Rel from a low-level  OmegaRel. ?Determine a lower bound on whether the formula is satisfiable. H The lower bound is based on treating all UNKNOWN constraints as false. @Determine an upper bound on whether the formula is satisfiable. G The upper bound is based on treating all UNKNOWN constraints as true. EUse simple, fast tests to decide whether the formula is a tautology. $True if the formula is a tautology. 0True if the formula has no UNKNOWN constraints. -True if the formula has UNKNOWN constraints.  True if the formula is UNKNOWN. DCompute the upper bound of a set or relation by setting all UNKNOWN  constraints to true. DCompute the lower bound of a set or relation by setting all UNKNOWN  constraints to false. .Test whether two sets or relations are equal. 1 The sets or relations must have the same arity. ,The answer is precise if both arguments are . 6 If either argument is inexact, this function returns False. CCompute the union of two sets or relations. The sets or relations  must have the same arity. JCompute the intersection of two sets or relations. The sets or relations  must have the same arity. 7Compute the composition of two sets or relations. The  first relation'1s domain must be the same dimension as the second' s range.  !"EGet the gist of a set or relation, given some background truth. The H gist operator uses heuristics to make a set or relation simpler, while F still retaining sufficient information to regenerate the original by = re-introducing the background truth. The sets or relations  must have the same arity. Given x computed by  1 x <- intersection given =<< gist effort r given we have x == r. #IGet the transitive closure of a relation. In some cases, the transitive D closure cannot be computed exactly, in which case a lower bound is  returned. $Get the domain of a relation. %Get the range of a relation. &Get the inverse of a relation. ')Get the complement of a set or relation. (Get the deltas of a relation.  The relation'6s input dimensionality must be the same as its output  dimensionality. )GApproximate a set or relation by allowing all existentially quantified J variables to take on rational values. This allows these variables to be  eliminated from the formula. *Logical conjunction (and). +Logical disjunction (or). ,Logical negation. -Universal quantification. The  parameter is the variable  bound by the quantifier. .!Existential quantification. The  parameter is the variable  bound by the quantifier. 1/$Construct an inequation of the form a*x + b*y + ... + d >= 0. 0"Construct an equation of the form a*x + b*y + ... + d = 0. 1Truth. 2 Falsity. 3  !"#$%&'()*+,-./0123  ! "#$%&'()12*+,-./03   !"#$%&'()*+,-./01223456783456%A predicate on an integer expresion. 7894A commutative and associative operator with a unit.  The type parameter t gives the operator's parameter and return type. :;<=9:;,The internal representation of expressions. >?@ABC<GVariables. Variables are represented internally by de Bruijn indices. DEF6We keep track of whether an expression is simplified. GHI=>?(Integer and boolean-valued expressions. JK2Get an expression, without trying to simplify it. L*Get the simplified form of an expression. @Wrap an expression. A;Wrap an expression that is known to be in simplified form. BGProduce the Nth bound variable. Zero is the innermost variable index. M%Construct a new quantified variable. NCFProduce a set of variables to use as free variables in an expression.  This produces the list "[nthVariable 0, nthVariable 1, ...] DLike C., but produce the expression corresponding to  each variable. EFGHIJKMultiplication by -1 L Summation MMultiplication NLogical negation O Conjunction P Disjunction Q Conjunction RAdd S Subtract T Multiply UMultiply by an integer V+Test whether an integer expression is zero W2Test whether an integer expression is nonnegative XEquality test YInequality test Z Greater than [ Less than \Greater than or equal ]Less than or equal ^(Build a universally quantified formula. _+Build an existentially quantified formula. `DReduce an integer expression to a value. Values for free variables , are provided explicitly in an environment.  summation multiplication integer literal  environment O summation multiplication integer literal  environment aCReduce a boolean expression to a value. Values for free variables , are provided explicitly in an environment.  summation multiplication integer literal  disjunction  conjunction  negation quantification an integer predicate true false  environment P@Use a fresh variable in an expression. After the expression is  constructed, rename/3adjust variable indices so that the fresh variable ) has index 0 and all other free variables' indices are incremented  by 1. bc$Create a sum of products expression constant part of sum product terms dconstant part of sum product terms efghQRSTUVWXY#True if the literal is the operator's zero. Z#True if the literal is the operator's unit. [\]^_`abcdefi?Decide whether two expressions are syntactically equal, modulo 3 commutativity, associativity, and alpha-renaming. ghiNormalize an expression. jklmnopqr+Look up a variable in a list. The variable's position is its  de Bruijn index. j+Convert a boolean expression to a formula. CThe expression must be a Presburger formula. In particular, if an I expression involves the product of two non-constant terms, it cannot be & converted to a formula. The library G internally simplifies expressions to sum-of-products form, so complex F expressions are valid as long as each simplified product has at most  one variable. Free variables Expression to convert sFree variables Expression to convert t=Convert an integer term to a coefficients for an equality or  inequality constraint. free variables expression to convert uk/Substitute a single variable in an expression. variable to replace its replacement expression to rename renamed expression vvariable to replace its replacement expression to rename renamed expression lIAdjust bound variable bindings by adding an offset to all bound variable  indices beyond a given level. first variable to change Amount to shift by Input expression Adjusted expression wfirst variable to change Amount to shift by Input expression Adjusted expression m=True if the expression has no more than the specified number  of free variables. ;3456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklm;?>=<BCDEFGHIJKLMNOPQcRSTUVWXYZ\[]^_`a;:9687354@Abdfgehijklm;35445687789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmxy Is equality Bound variables Terms Constant part  Expression z{xyz{|}xyz{ n,Sets of points in Z^n defined by a formula. ~the number of variables a predicate defining the set %low-level representation of this set o7Create a set whose members are defined by a predicate. AThe expression should have one free variable for each dimension. 3For example, the set of all points on the plane is   set 2 trueE 3The set of all points (x, y, z) where x > y + z is @ set 3 (case takeFreeVariables' 3 of [x,y,z] -> x |>| y |+| z) Number of dimensions Predicate defining the set p Convert an  to a n.  Internal function to convert an  to a n, when we know  the set'>s dimension. This can avoid actually building the expression $ when all we want is the dimension. q3Get the dimensionality of the space a set inhabits r Get the predicate defining a set' s members s Convert a n to an . tuvwxyz{|}!Test whether two sets are equal. ' The sets must have the same dimension  (dimension s1 == dimension s2), or an error will be raised. ,The answer is precise if both relations are z. 6 If either relation is inexact, this function returns False. ~Union of two sets. ' The sets must have the same dimension  (dimension s1 == dimension s2), or an error will be raised. Intersection of two sets. ' The sets must have the same dimension  (dimension s1 == dimension s2), or an error will be raised. Difference of two sets. ' The sets must have the same dimension  (dimension s1 == dimension s2), or an error will be raised. 9Get the gist of a set, given some background truth. The 9 gist operator uses heuristics to simplify the set while @ retaining sufficient information to regenerate the original by > re-introducing the background truth. The sets must have the  same dimension.  The gist satisfies the property 0 x === gist effort x given `intersection` given  nopqrstuvwxyz{|}~nopsqrvwxyz{|}tu~ nopqrstuvwxyz{|}~-A relation from points in a domain Z^m to points in a range Z^n. HA relation can be considered just a set of points in Z^(m+n). However, E many functions that operate on relations treat the domain and range  differently. !number of variables in the input "the function from input to output function defining the relation *low-level representation of this relation <Create a relation whose members are defined by a predicate. The expression should have m+n free variables, where m and n are & the first two parameters. The first m E variables refer to the domain, and the remaining variables refer to  the range. Dimensionality of the domain Dimensionality of the range  Predicate defining the relation ACreate a relation where each output is a function of the inputs. Each expression should have m free variables, where m  is the first parameter. For example, the relation {(x, y) -> (y, x) | x > 0 && y > 0} is # let [x, y] = takeFreeVariables' 2 @ in functionalRel 2 [y, x] (conjE [y |>| intE 0, x |>| intE 0]) Dimensionality of the domain "Function relating domain to range !Predicate restricting the domain  Convert an  to a .  Internal function to convert an  to a , when we know  the relation's dimensions. $Get the dimensionality of a relation' s domain $Get the dimensionality of a relation's range  Convert a  to an . 'Get the predicate defining a relation. &Test whether two relations are equal. , The relations must have the same dimension  ('inputDimension r1 == inputDimension r2 &&) outputDimension r1 == outputDimension r2),  or an error will be raised. ,The answer is precise if both relations are . 6 If either relation is inexact, this function returns False. Union of two relations. , The relations must have the same dimension  ('inputDimension r1 == inputDimension r2 &&) outputDimension r1 == outputDimension r2),  or an error will be raised. Intersection of two relations. , The relations must have the same dimension  ('inputDimension r1 == inputDimension r2 &&) outputDimension r1 == outputDimension r2),  or an error will be raised. Composition of two relations.  The second relation'+s output must be the same size as the first's input  ('outputDimension r2 == inputDimension r1),  or an error will be raised. Same as , with the arguments swapped. Difference of two relations. , The relations must have the same dimension  ('inputDimension r1 == inputDimension r2 &&) outputDimension r1 == outputDimension r2),  or an error will be raised. Cross product of two sets. >Get the gist of a relation, given some background truth. The > gist operator uses heuristics to simplify the relation while @ retaining sufficient information to regenerate the original by C re-introducing the background truth. The relations must have the 7 same input dimensions and the same output dimensions.  The gist satisfies the property 0 x === gist effort x given `intersection` given & & "      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwx !%',.yz{|}~w)* !"#$%&'(+,-.         D !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQsRSTUVWXYZy[\]^_`abcde Omega-0.2.2Data.Presburger.Omega.LowLevelData.Presburger.Omega.ExprData.Presburger.Omega.SetData.Presburger.Omega.RelData.Presburger.Omega.SetRel CoefficientcoeffVar coeffValue VarHandleFormulaOmegaRelOmegaSet PresburgerEffort StrenuousModerateLight newOmegaSet queryDNFSet newOmegaRelqueryDNFRelationlowerBoundSatisfiableupperBoundSatisfiableobviousTautologydefiniteTautologyexactinexactunknown upperBound lowerBoundequalunion intersection compositionrestrictDomain restrictRange difference crossProductgisttransitiveClosuredomainrangeinverse complementdeltas approximate conjunction disjunctionnegationqForallqExists inequalityequalitytruefalse QuantifierExistsForallPredOpIsGEZIsZeroBoolExprIntExprExprVarBoolExpIntExpExpwrapExprwrapSimplifiedExpr nthVariabletakeFreeVariablestakeFreeVariables'varEnthVarEintEboolEtrueEfalseEnegateEsumEprodEnotEconjEdisjE|&&||+||-||*|*|isZeroEisNonnegativeE|==||/=||>||<||>=||<=|forallEexistsE foldIntExp foldBoolExpvarExprsumOfProductsEsumOfProductsExprtestExprconjExprdisjExpr existsExprexpEqual expToFormularenameadjustBindingsvariablesWithinRangeSetset fromOmegaSet dimension predicate toOmegaSetRelrel functionalRel fromOmegaRelinputDimensionoutputDimension toOmegaReljoinhsw_debug_print_geqhsw_debug_print_eqhsw_constr_vars_freehsw_constr_vars_nexthsw_constraint_get_coefficientshsw_constraint_get_consthsw_geq_handle_free hsw_geqs_free hsw_geqs_next hsw_get_geqshsw_eq_handle_free hsw_eqs_free hsw_eqs_next hsw_get_eqshsw_tuple_iterator_freehsw_tuple_iterator_nexthsw_get_conjunct_variableshsw_dnf_iterator_freehsw_dnf_iterator_next hsw_query_dnfseparate_relation_dimensionshsw_add_constrainthsw_formula_to_andhsw_declaration_declarehsw_formula_finalizehsw_formula_add_existshsw_formula_add_forallhsw_formula_add_nothsw_formula_add_orhsw_formula_add_andhsw_relation_finalizehsw_relation_add_existshsw_relation_add_forallhsw_relation_add_nothsw_relation_add_orhsw_relation_add_andhsw_approximate hsw_deltashsw_complement hsw_inverse hsw_range hsw_domainhsw_transitive_closurehsw_gisthsw_cross_producthsw_differencehsw_restrict_rangehsw_restrict_domainhsw_compositionhsw_intersection hsw_union hsw_equalhsw_lower_boundhsw_upper_boundhsw_is_unknownhsw_is_inexact hsw_is_exacthsw_is_definite_tautologyhsw_is_obvious_tautologyhsw_is_upper_bound_satisfiablehsw_is_lower_bound_satisfiable hsw_set_varhsw_output_var hsw_input_varhsw_num_set_varshsw_num_output_varshsw_num_input_varshsw_relation_showptr_to_free_relationhsw_free_relation hsw_new_sethsw_new_relationfree unVarHandleFDrunFDrPtrrDomrRngsPtrsDompPtr sameArityfromPtrIteratornextLogicaladd_andadd_oradd_not add_forall add_existsconvert_to_andfinalizeC_Constr_Vars_Iter C_GEQ_HandleC_GEQ_Iterator C_EQ_Handle C_EQ_IteratorC_Tuple_Iterator C_ConjunctC_DNF_IteratorC_Var C_QuantifierC_AndC_Form C_Relation ConstraintConstr_Vars_Iter GEQ_Handle GEQ_Iterator EQ_Handle EQ_IteratorTuple_IteratorConjunct DNF_IteratorVar_Decl F_DeclarationF_AndFormRelationforeach iterateDNFiterateConjVars iterateEqs iterateGeqspeekConstraintVars peekInputVarspeekOutputVars peekSetVarsqueryConstraintwithPresburgerwithPresburger2 wrapOmegaSet wrapOmegaRelseparateRelationDimensions addConstraintShowsEnv showNthVarnumBoundvarNamesTermCAUOpDisjConjProdSumQuantEVarELitENotEPredECAUE QuantifiedBoundExprBox isSimplified expressiongetExprgetSimplifiedExpr newQuantified freeVariables foldIntExp'withFreshVariableisLitEdeconstructProductrebuildProductdeconstructSum rebuildSumcauEqzerounitisZeroOfisUnitOf evalCAUOpevalPred bindVariable showsVarPrecshowsIntshowsIntExprPrecshowsBoolExprPrecshowGEZshowEQZ showsList showSepByshowQuantifier expListsEqual findEqualExprsimplify simplifyRecbasicSimplificationscomplexSimplificationsposToSopflattenpevalzuscollect lookupVar exprToFormulasumToConstraintexpToFormulaError renameExpradjustBindingsExprmakeLookupFunctionconstraintToExprsetToExpressionrelToExpressionwrapExistentialVarsiterateNsetDimsetExp setOmegaSet mkOmegaSet omegaSetToSetuseSet useSetSetuseSet2 useSet2Set relInpDim relOutDimrelFun relOmegaRelmkFunctionalOmegaRel omegaRelToReluseRel useRelReluseRel2 useRel2Rel