=      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ Safe-Infered-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. 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.  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. 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. 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. ?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. #Restrict the domain of a relation.  If domain r is d, then domain =<< restrictDomain r s  is intersection d s. "Restrict the range of a relation.  If range r is d, then range =<< restrictRange r s  is intersection d s. 1Compute the difference of two relations or sets.  The members of difference x y are the members of x that are not  members of y. !'Compute the cross product of two sets. . The cross product relates every element of s to every element of y. "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. /$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. C )Dimensionality of the space that the set  inhabits  Set members /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 Dimensionality of the domain Dimensionality of the range  The relation /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  !"#$%&'()*+,-./0123  !"#$%&'()*+,-./0123  ! "#$%&'()12*+,-./0=   !"#$%&'()*+,-./012 Safe-Infered&6%A predicate on an integer expresion. ;,The internal representation of expressions. <GVariables. Variables are represented internally by de Bruijn indices. ?(Integer and boolean-valued expressions. @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. CFProduce 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. KMultiplication 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. aCReduce a boolean expression to a value. Values for free variables , are provided explicitly in an environment. c$Create a sum of products expression i?Decide whether two expressions are syntactically equal, modulo 3 commutativity, associativity, and alpha-renaming. 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. k/Substitute a single variable in an expression. lIAdjust bound variable bindings by adding an offset to all bound variable  indices beyond a given level. m=True if the expression has no more than the specified number  of free variables. ?3456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_` summation multiplication integer literal  environment a  summation multiplication integer literal  disjunction  conjunction  negation quantification an integer predicate true false  environment bcconstant part of sum product terms dconstant part of sum product terms efghijFree variables Expression to convert kvariable to replace its replacement expression to rename renamed expression lfirst variable to change Amount to shift by Input expression Adjusted expression m;3456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklm;?>=<BCDEFGHIJKLMNOPQcRSTUVWXYZ\[]^_`a;:9687354@Abdfgehijklm;3546879:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklm Safe-Infered Is equality Bound variables Terms Constant part  Expression  Safe-Inferedn,Sets of points in Z^n defined by a formula. 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) p Convert an  to a n. q3Get the dimensionality of the space a set inhabits r Get the predicate defining a set' s members s Convert a n to an . t8Compute the upper bound of a set by setting all UNKNOWN  constraints to true. u8Compute the lower bound of a set by setting all UNKNOWN  constraints to false. z,True if the set has no UNKNOWN constraints. {)True if the set has UNKNOWN constraints. |'True if the set is completely UNKNOWN. }!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 noNumber of dimensions Predicate defining the set pqrstuvwxyz{|}~ nopqrstuvwxyz{|}~nopsqrvwxyz{|}tu~ nopqrstuvwxyz{|}~ Safe-InferedA 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. <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. 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])  Convert an  to a . $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. 1True if the relation has no UNKNOWN constraints. .True if the relation has UNKNOWN constraints. *True if the relation is entirely UNKNOWN. &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. #Restrict the domain of a relation. ; domain (restrictDomain r s) === intersection (domain r) s "Restrict the range of a relation. 8 range (restrictRange r s) === intersection (range r) s 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 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. 2Invert a relation, swapping the domain and range. "Get the complement of a relation. @Approximate a relation by allowing all existentially quantified J variables to take on rational values. This allows these variables to be  eliminated from the formula. #Dimensionality of the domain Dimensionality of the range  Predicate defining the relation Dimensionality of the domain "Function relating domain to range !Predicate restricting the domain & & #      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwx !%',.yz{|}~w)* !"#$%&'(+,-. Omega-1.0Data.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 toOmegaReljoin$fStorableCoefficient$fShowCoefficient$fPresburgerOmegaRel$fShowOmegaRel$fPresburgerOmegaSet$fShowOmegaSet$fIteratorPtrPtr$fIteratorPtrPtr0$fIteratorPtrPtr1$fIteratorPtrPtr2 $fLogicalPtr $fLogicalPtr0 $fLogicalPtr1 $fLogicalPtr2$fConstraintGEQ_Handle$fConstraintEQ_Handle $fShowCAUOp $fEqCAUOp $fShowExp $fShowExp0makeLookupFunctionconstraintToExprsetToExpressionrelToExpressionwrapExistentialVarsiterateN $fShowSet $fShowRel