*+      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~None  !"23468<HM1An 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 rangeB Z^n. This is a wrapper around the Omega library's Relation type.A relation can be considered as just a set of points in Z^(m+n). However, many routines treat the domain and range differently.VA 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 formula6Test whether two sets or relations have the same arity0Convert a raw pointer to an OmegaSet or OmegaRel The " routine takes a parameter specifying how much effort to put into generating a good result. Higher effort takes more time. It's unspecified what a given effort level does. Create 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's low-level representation directly. This function takes care of data structure traversal and relies on other routines to interpret the data.All three accumulating functions take the set variables as their first parameter, and any existentially quantified variables as their second parameter. The set variables are returned along with a result value.Create an Omega relation. The first two parameters are the number of dimensions of the domain and range, respectively. The third parameter builds a formula defining the relation. Two points are related iff the formula evaluates to True on those points.Inspect a relation's low-level representation directly. This function takes care of data structure traversal and relies on other routines to interpret the data. All three accumulating functions take the relation's input and 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.Get a list of relations, one per output variable, with the same input and output dimensions as the original, but whose constraints mention only one output variable and no existential constraints.NThis function is needed to create a high-level Rel from a low-level OmegaRel.Determine a lower bound on whether the formula is satisfiable. The lower bound is based on treating all UNKNOWN constraints as false.Determine an upper bound on whether the formula is satisfiable. The upper bound is based on treating all UNKNOWN constraints as true.DUse simple, fast tests to decide whether the formula is a tautology.#True if the formula is a tautology./True if the formula has no UNKNOWN constraints.,True if the formula has UNKNOWN constraints.True if the formula is UNKNOWN.YCompute the upper bound of a set or relation by setting all UNKNOWN constraints to true.ZCompute the lower bound of a set or relation by setting all UNKNOWN constraints to false.^Test whether two sets or relations are equal. The sets or relations must have the same arity.,The answer is precise if both arguments are 8. If either argument is inexact, this function returns False.]Compute the union of two sets or relations. The sets or relations must have the same arity.dCompute the intersection of two sets or relations. The sets or relations must have the same arity.Compute the composition of two sets or relations. The first relation's 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. CCompute the difference of two relations or sets. The members of difference x y are the members of x that are not members of y.!UCompute the cross product of two sets. The cross product relates every element of s to every element of y."*Get the gist of a set or relation, given some background truth. The gist operator uses heuristics to make a set or relation simpler, while 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 /x <- intersection given =<< gist effort r givenwe have x == r.#Get the transitive closure of a relation. In some cases, the transitive 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.(rGet the deltas of a relation. The relation's input dimensionality must be the same as its output dimensionality.)Approximate a set or relation by allowing all existentially quantified 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 4 parameter is the variable bound by the quantifier..!Existential quantification. The 4 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.2Falsity.       !"#$%&'()*+,-./ 2Dimensionality of the space that the set inhabits Set members.Accumulating function for equality constraints&Initial value for equality constraints0Accumulating function for inequality constraints(Initial value for inequality constraints#Accumulating function for conjunctsInitial value for conjuncts Set to query0Dimensionality of the domainDimensionality of the range The relation.Accumulating function for equality constraints&Initial value for equality constraints0Accumulating function for inequality constraints(Initial value for inequality constraints#Accumulating function for conjunctsInitial value for conjunctsRelation to query-Input variables, output variables, and result !"#$%&'()*+,-.1/01223456789:;<=>?@A3  !"#$%&'()*+,-./0123  ! "#$%&'()12*+,-./0        !"#$%&'()*+,-./ 0 !"#$%&'()*+,-.1/01223456789:;<=>?@ANone!"234<=KM16$A predicate on an integer expresion.BHA commutative and associative operator with a unit. The type parameter t0 gives the operator's parameter and return type.;+The internal representation of expressions.<FVariables. Variables are represented internally by de Bruijn indices.C5We keep track of whether an expression is simplified.?'Integer and boolean-valued expressions.D1Get an expression, without trying to simplify it.E)Get the simplified form of an expression.@Wrap an expression.A:Wrap an expression that is known to be in simplified form.BFProduce the Nth bound variable. Zero is the innermost variable index.F$Construct a new quantified variable.C^Produce 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 -1L SummationMMultiplicationNLogical negationO ConjunctionP DisjunctionQ ConjunctionRAddSSubtractTMultiplyUMultiply by an integerV*Test whether an integer expression is zeroW1Test whether an integer expression is nonnegativeX Equality testYInequality testZ Greater than[ Less than\Greater than or equal]Less than or equal^'Build a universally quantified formula._*Build an existentially quantified formula.`oReduce an integer expression to a value. Values for free variables are provided explicitly in an environment.anReduce a boolean expression to a value. Values for free variables are provided explicitly in an environment.GUse a fresh variable in an expression. After the expression is constructed, rename/adjust variable indices so that the fresh variable has index 0 and all other free variables' indices are incremented by 1.c#Create a sum of products expressionH+True if the literal is the operator's zero.I+True if the literal is the operator's unit.iqDecide whether two expressions are syntactically equal, modulo commutativity, associativity, and alpha-renaming.JNormalize an expression.KOLook up a variable in a list. The variable's position is its de Bruijn index.j*Convert a boolean expression to a formula.MThe expression must be a Presburger formula. In particular, if an expression involves the product of two non-constant terms, it cannot be converted to a formula. The library internally simplifies expressions to sum-of-products form, so complex expressions are valid as long as each simplified product has at most one variable.LTConvert an integer term to a coefficients for an equality or inequality constraint.k.Substitute a single variable in an expression.lgAdjust bound variable bindings by adding an offset to all bound variable indices beyond a given level.mPTrue if the expression has no more than the specified number of free variables.MNOPQRS345678BTUVW9:;XYZ[\]<^_C`ab=>?cDE@ABFdCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_` summationmultiplicationinteger literal environmente summationmultiplicationinteger literal environmenta  summationmultiplicationinteger literal disjunction conjunctionnegationquantificationan integer predicatetrue false  environmentGbcconstant part of sum product termsdconstant part of sum product termsefghfghijklmHInopqrstuvwxyz{|}~iJKjFree variablesExpression to convertFree variablesExpression to convertLfree variablesexpression to convertkvariable to replaceits replacementexpression to renamerenamed expressionvariable to replaceits replacementexpression to renamerenamed expressionlfirst variable to changeAmount to shift byInput expressionAdjusted expressionfirst variable to changeAmount to shift byInput expressionAdjusted expressionm;3456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklm;?>=<BCDEFGHIJKLMNOPQcRSTUVWXYZ\[]^_`a;:9687354@AbdfgehijklmzMNOPQRS354687BWVUT9:;]\[ZYX<_^C`ab=>?cDE@ABFdCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`eaGbcdefghfghijklmHInopqrstuvwxyz{|}~iJKjLklm QRSTUXYZ[\]None!"M Is equalityBound variablesTerms Constant part ExpressionNone!"Mn+Sets of points in Z^n defined by a formula.the number of variablesa predicate defining the set$low-level representation of this seto6Create a set whose members are defined by a predicate.@The expression should have one free variable for each dimension.2For example, the set of all points on the plane is  set 2 (\[_, _] -> trueE)2The set of all points (x, y, z) where x > y + z is " set 3 (\[x,y,z] -> x |>| y |+| z)p Convert an  to a n. Internal function to convert an  to a ny, when we know the set's dimension. This can avoid actually building the expression when all we want is the dimension.q2Get the dimensionality of the space a set inhabitsr*Get the predicate defining a set's memberss Convert a n to an .tOCompute the upper bound of a set by setting all UNKNOWN constraints to true.uPCompute 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.}JTest 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 z8. 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.CIntersection of two sets. The sets must have the same dimension (dimension s1 == dimension s2), or an error will be raised.ADifference of two sets. The sets must have the same dimension (dimension s1 == dimension s2), or an error will be raised.Get the gist of a set, given some background truth. The 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 .x === gist effort x given `intersection` given!noNumber of dimensionsPredicate defining the setpqrstuvwxyz{|}~ nopqrstuvwxyz{|}~nopsqrvwxyz{|}tu~ nopqrstuvwxyz{|}~None!"MA relation from points in a domain Z^m to points in a range Z^n.A relation can be considered just a set of points in Z^(m+n). However, many functions that operate on relations treat the domain and range differently. number of variables in the input!the function from input to outputfunction 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 mQ variables refer to the domain, and the remaining variables refer to the range.@Create 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 . 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.0True if the relation has no UNKNOWN constraints.-True if the relation has UNKNOWN constraints.)True if the relation is entirely UNKNOWN.TTest whether two relations are equal. The relations must have the same dimension (RinputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2), or an error will be raised.,The answer is precise if both relations are 8. If either relation is inexact, this function returns False.FUnion of two relations. The relations must have the same dimension (RinputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2), or an error will be raised.MIntersection of two relations. The relations must have the same dimension (RinputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2), or an error will be raised.iComposition 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. 9domain (restrictDomain r s) === intersection (domain r) s!Restrict the range of a relation. 6range (restrictRange r s) === intersection (range r) sKDifference of two relations. The relations must have the same dimension (RinputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2), or an error will be raised.Cross product of two sets.5Get 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 re-introducing the background truth. The relations must have the same input dimensions and the same output dimensions.The gist satisfies the property .x === gist effort x given `intersection` givenGet the transitive closure of a relation. In some cases, the transitive closure cannot be computed exactly, in which case a lower bound is returned.1Invert a relation, swapping the domain and range.!Get the complement of a relation.Approximate a relation by allowing all existentially quantified variables to take on rational values. This allows these variables to be eliminated from the formula./Dimensionality of the domainDimensionality of the rangePredicate defining the relationDimensionality of the domain!Function relating domain to range Predicate restricting the domain& & *      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwx !%',.yz{|}~w)* !"#$%&'(+,-.         !"#$%%&'())*+,-./01234567D89:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwsxyz{|}~y Omega-1.0.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 toOmegaReljoinpPtr sameArityfromPtrseparateRelationDimensions unVarHandleFDrunFDrPtrrDomrRngsPtrsDomIteratornextLogicaladd_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_AndFormRelationhsw_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_relationfreeforeach iterateDNFiterateConjVars iterateEqs iterateGeqspeekConstraintVars peekInputVarspeekOutputVars peekSetVarsqueryConstraintwithPresburgerwithPresburger2 wrapOmegaSet wrapOmegaRel addConstraint$fStorableCoefficient$fShowCoefficient$fPresburgerOmegaRel$fShowOmegaRel$fPresburgerOmegaSet$fShowOmegaSet$fIteratorPtrPtr$fIteratorPtrPtr0$fIteratorPtrPtr1$fIteratorPtrPtr2 $fLogicalPtr $fLogicalPtr0 $fLogicalPtr1 $fLogicalPtr2$fConstraintGEQ_Handle$fConstraintEQ_HandleCAUOpExprBoxgetExprgetSimplifiedExpr newQuantifiedwithFreshVariableisZeroOfisUnitOfsimplify lookupVarsumToConstraintShowsEnv showNthVarnumBoundvarNamesTermDisjConjProdSumQuantEVarELitENotEPredECAUE QuantifiedBound isSimplified expression freeVariables foldIntExp'isLitEdeconstructProductrebuildProductdeconstructSum rebuildSumcauEqzerounit evalCAUOpevalPredappPrecmulPrecaddPreccmpPrecandPreclamPrec emptyShowsEnv bindVariable bindVariables showsVarPrecshowsIntshowsIntExprPrecshowsBoolExprPrecshowGEZshowGEZ'showEQZpartitionSumBySignshowSumshowProd showsList showSepByshowQuantifiershowLambdaBoundshowLambdaList expListsEqual findEqualExpr simplifyRecbasicSimplificationscomplexSimplificationsposToSopflattenpevalzuscollect exprToFormulaexpToFormulaError renameExpradjustBindingsExpr $fShowCAUOp $fEqCAUOp $fShowExp $fShowExp0makeLookupFunctionconstraintToExprsetToExpressionrelToExpressionwrapExistentialVarsiterateNsetDimsetExp setOmegaSet omegaSetToSet mkOmegaSetuseSet useSetSetuseSet2 useSet2Set $fShowSet relInpDim relOutDimrelFun relOmegaRel omegaRelToRel mkOmegaRelmkFunctionalOmegaReluseRel useRelReluseRel2 useRel2Rel $fShowRel