h&#w|      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   !!!!!!""""""""""#$$$$$$$$$$$$%%%%%%%%%%%%%%%%%%%%%%%&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&'(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((())))))***+++++++++++++++++++++++++++++++++++++++++++++++++++++++++,,,,,,,,,,,----------------................./////000000000000000011122222222222222222222223333344444444455555555555555556777777788888888888888888899999999999999999999999999::;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;<<<<=>>???@@@@@AAAAAAAAAAAAAABB Safe-Inferred7liquid-fixpointA map with an efficient liquid-fixpoint forall (v, ks) in reversedMap. forall k in ks. (k, v) is in directMapliquid-fixpoint8This are the only keys that can be used in internal mapsKliquid-fixpoint3A HashMap that can share the values of some entries If two keys k1 and k2 are mapped to single v, updating the entry for k1 also updates the entry for k2 and viceversa.The user of the map is responsible for indicating which keys are going to share their values.Keys can be updated with shareMapInsertWith and O.liquid-fixpoint(k, v) pairs in the map.=Contains at least an entry for each key in the values of of .liquid-fixpointIf k1 is mapped to k2<, then both keys are considered associated to the value of k2 in .&Contains an entry for each key in the K.Nliquid-fixpointinsertWith f k v m is the map m plus key k being associated to value v.If k is present in m, then k< and any other key sharing its value will be associated to  f v (m ! k).Oliquid-fixpointmergeKeysWith f k0 k1 m updates the k0 value to f (m ! k0) (m ! k1) and k1 shares the value with k0.If k0 and k1% are already sharing their values in m4, or both keys are missing, this operation returns m unmodified.If only one of the keys is present, the other key is associated with the existing value.KLMNOPKLMNPO Safe-Inferred8VWVW Safe-Inferred"81 XYZ[\]^_`a XYZ[_\]^`aZ9  Safe-Inferred8sbcdebcdeC Safe-Inferred8 Safe-Inferred9<fliquid-fixpointAlso known as  in pretty&, but that clashes with Semigroup's <>  !"#$%&'()*+,-./0123456789:;?=<>D@BCAIEFHGJf  !"#$%&'()*+,-./0123456789:;?=<>D@BCAIEFHGJff6 Safe-Inferred "/;wxliquid-fixpoint:Unique Int -----------------------------------------------yliquid-fixpoint:Edit Distance --------------------------------------------liquid-fixpoint!If loud, write a string to stdoutliquid-fixpoint (v, M.lookupDefault [] v em)sccsWith ef [1,2,3] [[3],[1,2]]ghionmljkpqrstuvwxyz{|}~pqrstuvwxyionmljkz{|}~hg9 9  Safe-InferredCYliquid-fixpoint!Constraint Generation Informationliquid-fixpoint&Input to constraint solving (fixpoint)liquid-fixpoint)Output from constraint solving (fixpoint)liquid-fixpoint(HTML file with inferred type annotationsliquid-fixpointText file with inferred typesliquid-fixpointVim annotation fileliquid-fixpointHaskell sourceliquid-fixpointHaskell sourceliquid-fixpointLiterate Haskell sourceliquid-fixpointJavaScript sourceliquid-fixpointTypescript sourceliquid-fixpoint%Spec file (e.g. include/Prelude.spec)liquid-fixpointLifted-Spec file, containing automatically generated specificationsliquid-fixpoint-Qualifiers file (e.g. include/Prelude.hquals)liquid-fixpointFinal result: SAFE/UNSAFEliquid-fixpointHTML file with templates?liquid-fixpoint8Markdown file (temporarily generated from .Lhs + annots)liquid-fixpoint-JSON file containing result (annots + errors)liquid-fixpoint*Previous source (for incremental checking)liquid-fixpoint*Previous output (for incremental checking)liquid-fixpointConstraint Graphliquid-fixpoint Partitionliquid-fixpoint0SMTLIB2 queries for automatically created proofsliquid-fixpoint$Binary representation of .fq / FInfoliquid-fixpointSMTLIB2 query fileliquid-fixpointHorn query fileliquid-fixpoint#filter constraints with delta debugliquid-fixpoint"filter qualifiers with delta debugliquid-fixpointfilter kvars with delta debugliquid-fixpoint7Hardwired Paths and Files -----------------------------,,  Safe-Inferred6;Qs/liquid-fixpointEliminate describes the number of KVars to eliminate: None = use PA/Quals for ALL k-vars, i.e. no eliminate Some = use PA/Quals for CUT k-vars, i.e. eliminate non-cuts All = eliminate ALL k-vars, solve cut-vars to TRUE Horn = eliminate kvars using the Horn solver Existentials = eliminate kvars and existentialsliquid-fixpoint describes which (Horn) constraints to scrape qualifiers from None = do not scrape, only use the supplied qualifiers Head = scrape only from the constraint heads (i.e. "rhs") All = scrape all concrete predicates (i.e. "rhs" + "lhs")liquid-fixpoint1src file (*.hs, *.ts, *.c, or even *.fq or *.bfq)liquid-fixpoint)number of cores used to solve constraintsliquid-fixpointMinimum size of a partitionliquid-fixpoint2Maximum size of a partition. Overrides minPartSizeliquid-fixpointwhich SMT solver to useliquid-fixpoint not interpret div and mul in SMTliquid-fixpoint&interpretation of string theory by SMTliquid-fixpointdefunctionalize (use apply$ for all uninterpreted applications)liquid-fixpoint3allow higher order binders in the logic environmentliquid-fixpointallow higher order qualifiersliquid-fixpointeliminate non-cut KVarsliquid-fixpoint6configure auto-scraping of qualifiers from constraintsliquid-fixpoint)maximum length of KVar chain to eliminateliquid-fixpointsmt timeout in msecliquid-fixpointprint eliminate statsliquid-fixpointprint solver statsliquid-fixpoint+print meta-data associated with constraintsliquid-fixpointcompute constraint statisticsliquid-fixpoint&partition FInfo into separate fq filesliquid-fixpointsave FInfo as .bfq and .fq fileliquid-fixpoint3min .fq by delta debug (unsat with min constraints)liquid-fixpoint0min .fq by delta debug (sat with min qualifiers)liquid-fixpoint+min .fq by delta debug (sat with min kvars)liquid-fixpointshrink final solution by pruning redundant qualfiers from fixpointliquid-fixpoint"eta eliminate function definitionsliquid-fixpointsolve "gradual" constraintsliquid-fixpointinteractive gradual solvingliquid-fixpointignore given kut variablesliquid-fixpointTreat non-linear vars as cutsliquid-fixpoint!Disable non-concrete KVar slicingliquid-fixpoint'Allow axiom instantiation via rewritingliquid-fixpoint/Unfold invocations with undecided guards in PLEliquid-fixpoint(Do not use the interpreter to assist PLEliquid-fixpointUse old version of PLEliquid-fixpointUse incremental PLEliquid-fixpointDon't use environment reductionliquid-fixpointInline ANF bindings. Sometimes improves performance and sometimes worsens it.liquid-fixpoint%Only check these specific constraintsliquid-fixpoint6Enable extensional interpretation of function equalityliquid-fixpoint)Enable termination checking for rewritingliquid-fixpointRead input query from stdinliquid-fixpointRender output in JSON formatliquid-fixpoint4Maximum PLE "fuel" (unfold depth) (default=infinite)liquid-fixpointTerm ordering for use in RESTliquid-fixpointConfiguration Options -----------------------------------------------------  Safe-Inferred"Skliquid-fixpointImplement either  or liquid-fixpointTop-level pretty printerliquid-fixpointPlease do not alter this.  Safe-InferredTliquid-fixpointExamples   Safe-Inferred6;Xu liquid-fixpointA Reusable SrcSpan Type ------------------------------------------liquid-fixpointStart Positionliquid-fixpoint End Positionliquid-fixpoint?This is a compatibility type synonym for megaparsec vs. parsec.liquid-fixpoint?This is a compatibility type synonym for megaparsec vs. parsec.liquid-fixpoint?This is a compatibility type synonym for megaparsec vs. parsec.liquid-fixpointLocated Values ---------------------------------------------------liquid-fixpoint'Computes, safely, the predecessor of a  value, stopping at 1.liquid-fixpointComputes the successor of a  value.liquid-fixpointCreate, safely, as position. If a non-positive number is given, we use 1.liquid-fixpointCreate a source position from integers, using 1 in case of non-positive numbers.liquid-fixpoint8We need the Binary instances for LH's spec serializationliquid-fixpointRetrofitting instances to SourcePos ------------------------------""  Safe-Inferred"(56;^ liquid-fixpoint$Values that can be viewed as Symbolsliquid-fixpointLocated Symbols -----------------------------------------------------liquid-fixpoint Invariant: a  is made up of: '0'..'9'++ [a...z] ++ [A..Z] ++ ?If the original text has ANY other chars, it is represented as:lq$i+where i is a unique integer (for each text)liquid-fixpointDecoding Symbols -----------------------------------------------------liquid-fixpointEncoding Symbols -----------------------------------------------------liquid-fixpointRJ: We allow the extra  unsafeChars: to allow parsing encoded symbols. e.g. the raw string This#is%$inval!d may get encoded as "enc%12" and serialized as such in the fq/bfq file. We want to allow the parser to then be able to read the above back in.liquid-fixpointUse this **EXCLUSIVELY** when you want to add stuff in front of a Symbolliquid-fixpoint'testSymbol c' creates the `is-c` symbol for the adt-constructor named c.liquid-fixpoint [Map, key, val] That is, ` is used to split a type application into the FTyCon and its args.liquid-fixpointExported Basic Sorts -----------------------------------------------liquid-fixpointExported Basic Sorts -----------------------------------------------liquid-fixpointExported Basic Sorts -----------------------------------------------liquid-fixpointExported Basic Sorts -----------------------------------------------liquid-fixpointExported Basic Sorts -----------------------------------------------liquid-fixpointExported Basic Sorts -----------------------------------------------liquid-fixpoint8We need the Binary instances for LH's spec serialization Safe-Inferred"()*6;qliquid-fixpointClass Predicates for Valid Refinements -----------------------------liquid-fixpointTODO: This doesn't seem to merit a TC ------------------------------liquid-fixpoint'Values that can be viewed as Predicatesliquid-fixpointGeneralizing Symbol, Expression, Predicate into Classes -----------&Values that can be viewed as Constants(Values that can be viewed as Expressionsliquid-fixpointParsed refinement of Symbol as Expr# e.g. in '{v: _ | e }' v is the Symbol and e the Exprliquid-fixpointExpressions ---------------------------------------------------------------Uninterpreted constants that are embedded as "constant symbol : Str"liquid-fixpointSubstitutions -------------------------------------------------------------liquid-fixpointKvars ---------------------------------------------------------------------liquid-fixpointLike DE' but only traverses the nodes of type a or [a].liquid-fixpointEliminates redundant castsliquid-fixpointWrap the enclosed  , in parentheses only if the condition holds.liquid-fixpoint is a fast version of  needed for the ebind testsliquid-fixpoint NOTE: pAnd-SLOW and  are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use 2 which ensures some basic things but is faster.liquid-fixpoint NOTE: pAnd-SLOW and  are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use 2 which ensures some basic things but is faster.liquid-fixpointPredicates ----------------------------------------------------------------liquid-fixpoint:Refinements ----------------------------------------------liquid-fixpoint7Gradual Type Manipulation ----------------------------liquid-fixpoint7Generally Useful Refinements --------------------------liquid-fixpointString Constants ----------------------------------------------------------Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.liquid-fixpoint,The symbol may be an encoding of a SymConst.liquid-fixpoint parameters for Reft, vv + othersliquid-fixpointfree symbols of a9 9  Safe-Inferred8;t Safe-Inferredt Safe-Inferreduliquid-fixpointTODO: Rewrite using visitor -----------------------------------------------   Safe-Inferred"%&6;wliquid-fixpoint# Horn Constraintsliquid-fixpoint# Refine Iterationsliquid-fixpoint # smtBracket calls (push/pop)liquid-fixpoint# smtCheckUnsat callsliquid-fixpoint# times SMT said RHS Validliquid-fixpoint!Returns the Horn clauses checked.liquid-fixpoint*Returns a number which can be used in the Safe constructor of a  FixResult to show "the work done".   Safe-Inferred "(5689:;y liquid-fixpointResult --------------------------------------------------------- liquid-fixpointThe Solver0 statistics, which include also the constraints actually checked. A program will be "trivially safe" in case this number is 0. liquid-fixpointA BareBones Error Type ---------------------------------------------------- liquid-fixpointCatalogue of Errors --------------------------------------------   Safe-Inferred")*689:;{@ liquid-fixpointConstraint Pack Sets ------------------------------------------------------ liquid-fixpoint'Functions for Global Binder Environment liquid-fixpoint&Functions for Indexed Bind Environment< <  Safe-Inferred6;E liquid-fixpointA Refinement of  that describes SMTLIB Sorts liquid-fixpoint / describes the SMT semantics for a given symbol liquid-fixpoint for UDF: len, height, append liquid-fixpointfor ADT constructor and tests: cons, nil liquid-fixpointfor ADT tests : `is$cons` liquid-fixpointfor ADT field: hd, tl liquid-fixpoint for theory ops: mem, cup, select liquid-fixpoint 3 represents the information about each interpreted  liquid-fixpointname liquid-fixpointserialized SMTLIB2 name liquid-fixpointsort liquid-fixpoint>TRUE = defined (interpreted), FALSE = declared (uninterpreted) liquid-fixpoint  is used to resolve the  and   of each  liquid-fixpointSorts of *all* defined symbols liquid-fixpoint)Information about theory-specific Symbols liquid-fixpointUser-defined data-declarations liquid-fixpointDistinct Constant symbols liquid-fixpointTypes at which apply/ was used; see [NOTE:apply-monomorphization] liquid-fixpoint / is the low-level representation for SMT valuesliquid-fixpointThese are "BUILT-in" polymorphic functions which are UNININTERPRETED but POLYMORPHIC, hence need to go through the apply-defunc stuff.liquid-fixpointsmtSorts attempts to compute a list of all the input-output sorts at which applications occur. This is a gross hack; as during unfolding we may create _new_ terms with wierd new sorts. Ideally, we MUST allow for EXTENDING the apply-sorts with those newly created terms. the solution is perhaps to *preface* each VC query of the form-push assert p check-sat pop%with the declarations needed to make p3 well-sorted under SMT, i.e. change the above todeclare apply-sorts push assert p check-sat popsuch a strategy would NUKE the entire apply-sort machinery from the CODE base. [TODO]: dynamic-apply-declaration liquid-fixpointThe poly parameter is True when we are *declaring* sorts, and so we need to leave the top type variables be; it is False when we are declaring variables etc., and there, we serialize them using  (though really, there SHOULD BE NO floating tyVars... 'smtSort True msg t' serializes a sort t using type variables, 'smtSort False msg t' serializes a sort t using  instead of tyvars.' '  Safe-Inferred")*68;) liquid-fixpointname of reflected function liquid-fixpointnames of parameters liquid-fixpointdefinition of body liquid-fixpoint sort of body liquid-fixpointis this a recursive definition liquid-fixpointAxiom Instantiation Information -------------------------------------- liquid-fixpointTop level Solvers ---------------------------------------------------- liquid-fixpointcst id |-> Horn Constraint liquid-fixpoint%Kvar |-> WfC defining its scope/args liquid-fixpointBind |-> (Symbol, SortedReft) liquid-fixpointSubset of existential binders liquid-fixpointGlobal Constant symbols liquid-fixpointDistinct Constant symbols liquid-fixpointSet of KVars *not* to eliminate liquid-fixpointAbstract domain liquid-fixpointMetadata about binders liquid-fixpointUser-defined data declarations liquid-fixpointHigher Order info liquid-fixpointTODO: what is this? liquid-fixpoint)Information about reflected function defs liquid-fixpoint+Allow higher order binds in the environemnt liquid-fixpointAllow higher order quals liquid-fixpointTop-level Queries liquid-fixpointConstraint Cut Sets ------------------------------------------------------- liquid-fixpointmatch everything liquid-fixpointstr . $i i.e. match prefix str with suffix bound to $i liquid-fixpoint$i . str i.e. match suffix str with prefix bound to $i liquid-fixpointstr i.e. exactly match str liquid-fixpointQualifiers ---------------------------------------------------------------- liquid-fixpointName liquid-fixpoint Parameters liquid-fixpoint Predicate liquid-fixpointSource Location liquid-fixpointSolutions and Results liquid-fixpointId of lhs/rhs binder liquid-fixpointConstraints --------------------------------------------------------------- liquid-fixpoint"Smart Constructors" for Constraints --------------------------------- liquid-fixpointconstructing qualifiers liquid-fixpointConstructing Queries liquid-fixpointRendering Queries liquid-fixpoint!Query Conversions: FInfo to SInfo  9  Safe-Inferred] liquid-fixpointCompute the domain of a kvar liquid-fixpointFree variables of a refinement liquid-fixpoint8Split a SortedReft into its concrete and KVar components liquid-fixpointcheckRegular ds0 returns the subset of ds that are _not_ regularliquid-fixpointisRegular [d1,...]1 gets a non-empty list of mut-recursive datadecls liquid-fixpoint  sorts the data declarations such that each declarations only refers to preceding ones.  F Safe-Inferred  Safe-Inferred liquid-fixpoint:String Constants ----------------------------------------- liquid-fixpointCoSub is a map from (coercion) ty-vars represented as 'FObj s' to the ty-vars that they should be substituted with. Note the domain and range are both Symbol and not the Int used for real ty-vars. liquid-fixpointContext ctx8 is built in a "top-down" fashion; not "across" siblings liquid-fixpointTransforms can access current ctx liquid-fixpoint!Accumulations can access current ctx; acc value is monoidal liquid-fixpoint9Specialized and faster version of mapExpr for expressions liquid-fixpointVisitors over Sortliquid-fixpointLike  : but it doesn't substitute on the result of the function. $mapSortOnlyOnce [(a,b), (b,c)] a = bwhereas mapSort [(a,b), (b,c)] a = c# #  Safe-Inferredliquid-fixpoint ignores the actual refinements as they are not relevant in the kvar parameters (as suggested by BLC.)   Safe-Inferred";=a liquid-fixpoint(e, f) asserts that e is a subexpression of f e liquid-fixpointYields the result of rewriting an expression with an autorewrite equation.Yields nothing if:The result of the rewrite is identical to the original expressionAny of the arguments of the autorewrite has a refinement type which is not satisfied in the current context.liquid-fixpointComputes the subexpressions of a list of expressions. Each subexpression comes with a function that rebuilds the context in which the subexpression occurs. %and [ es == f e | (e, f) <- subs es ] liquid-fixpointunify vs template e = Just su yields a substitution su" such that subst su template == e Moreover, su/ is constraint to only substitute variables in vs.Yields Nothing if no substitution exists.   Safe-Inferred   Safe-Inferred"$ liquid-fixpointAST Conversion: Types that can be serialized ------------------------------ liquid-fixpoint4Additional information around the SMT solver backend liquid-fixpointThe high-level interface for interacting with the SMT solver backend. liquid-fixpoint.The close operation of the SMT solver backend. liquid-fixpoint"Responses received from SMT engine liquid-fixpointTypes ---------------------------------------------------------------------Commands issued to SMT engine     Safe-Inferred"( liquid-fixpoint NOTE:Adding-TheoriesTo add new (SMTLIB supported) theories to liquid-fixpoint and upstream, grep for  Map_default and then add your corresponding symbol in all those places. This is currently far more complicated than it needs to be.Theory Symbols ------------------------------------------------------------liquid-fixpoint NOTE:Adding-TheoriesTo add new (SMTLIB supported) theories to liquid-fixpoint and upstream, grep for  Map_default and then add your corresponding symbol in all those places. This is currently far more complicated than it needs to be.Theory Symbols ------------------------------------------------------------liquid-fixpoint NOTE:Adding-TheoriesTo add new (SMTLIB supported) theories to liquid-fixpoint and upstream, grep for  Map_default and then add your corresponding symbol in all those places. This is currently far more complicated than it needs to be.Theory Symbols ------------------------------------------------------------liquid-fixpointExported API --------------------------------------------------------------liquid-fixpointTheory Symbols :  uninterpSEnv should be disjoint from see  interpSEnv) to avoid duplicate SMT definitions.  uninterpSEnv& is for uninterpreted symbols, and  interpSEnv is for interpreted symbols. contains the list of ALL SMT symbols with interpretations, i.e. which are given via `define-fun` (as opposed to `declare-fun`)liquid-fixpoint'Constructors, Selectors and Tests from  arations.liquid-fixpoint('selfSort d' returns the _self-sort_ of d :: %. See [NOTE:DataDecl] for details.liquid-fixpoint)'fldSort d t' returns the _real-sort_ of d if t- is the _self-sort_ and otherwise returns t". See [NOTE:DataDecl] for details.liquid-fixpoint converts the  into a full     Safe-Inferred(liquid-fixpointReplace constant integer and floating point expressions by constant values where possible. Safe-Inferred"<liquid-fixpointAPI for manipulating Sort Substitutions -----------------------------------liquid-fixpointChecking Refinements ------------------------------------------------------Types used throughout checkerliquid-fixpointElaborate: make polymorphic instantiation explicit via casts, make applications monomorphic for SMTLIB. This deals with polymorphism by -ing all refinements except for KVars. THIS IS NOW MANDATORY as sort-variables can be instantiated to ' and bool.liquid-fixpointPredicates on Sorts -------------------------------------------------------liquid-fixpoint: adds "casts" to decorate polymorphic instantiation sites.liquid-fixpoint7 replaces all direct function calls indirect calls via liquid-fixpointSort Inference ------------------------------------------------------------liquid-fixpointChecking Refinements ------------------------------------------------------liquid-fixpointChecking Expressions ------------------------------------------------------liquid-fixpointElaborate expressions with types to make polymorphic instantiation explicit.liquid-fixpoint is to support tests like `testspos undef00.fq`liquid-fixpoint/defuncEApp monomorphizes function applications.liquid-fixpoint NOTE:apply-monomorphizationBecause SMTLIB does not support higher-order functions, all _non-theory_ function applications EApp e1 e2are represented, in SMTLIB, as(Eapp (EApp apply e1) e2)where & is 'ECst (EVar "apply") t' and t is 'FFunc a b' a,b are the sorts of e2 and 'e1 e2' respectively.9Note that *all polymorphism* goes through this machinery.7Just before sending to the SMT solver, we use the cast t to generate a special  apply_at_t symbol.$To let us do the above, we populate  & with the _set_ of all sorts at which  is used, computed by .NOTE:coerce-apply'-- related to [NOTE:apply-monomorphism];Haskell's GADTs cause a peculiar problem illustrated below:```haskell data Field a where FInt :: Field Int FBool :: Field Boolproj :: Field a -> a -> a proj fld x = case fld of FInt -> 1 + x FBool -> not b ```## The Problem-The problem is you cannot encode the body of proj as a well-sorted refinement:```haskell if is$FInt fld then (1 + (coerce (a ~ Int) x)) else (not (coerce (a ~ Bool) x)) ```The catch is that x is being used BOTH as  and as " which is not supported in SMTLIB.$## Approach: Uninterpreted Functions We encode coerce+ as an explicit **uninterpreted function**:7```haskell if is$FInt fld then (1 + (coerce)(a -> int) x)) else (not (coerce(a -> bool) x)) ```1where we define, extra constants in the style of ```haskell constant coerce*(a -> int ) :: a -> int constant coerce(a -> bool) :: a -> int ```$However, it would not let us verify: ```haskell5unwrap :: Field a -> a -> a unwrap fld x = proj fld xtest = unwrap FInt 4 == 5 && unwrap FBool True == False ```because we'd get```haskell unwrap FInt 4 :: { if is$FInt FInt then (1 + coerce_int_int 4) else ... } ```and the UIF nature of coerce_int_int renders the VC invalid.(## Solution: Eliminate Trivial CoercionsHOWEVER, the solution here, may simply be to use UIFs when the coercion is non-trivial (e.g. `a ~ int`) but to eschew them when they are trivial. That is we would encode:| Expr | SMTLIB | |:-----------------------|:-------------------| | `coerce (a ~ int) x` | `coerce_a_int x` | | `coerce (int ~ int) x` | x | a, f :: Maybe (b -> b), x: c |- fromJust f x RJ: The above comment makes no sense to me :(liquid-fixpoint/Helper for checking binary (numeric) operationsliquid-fixpointChecking Predicates -------------------------------------------------------liquid-fixpointChecking Relationsliquid-fixpointSort Unification on Expressionsliquid-fixpointSort Unificationliquid-fixpoint3Fast Unification; `unifyFast True` is just equalityliquid-fixpointApplying a Type Substitution ----------------------------------------------liquid-fixpointDeconstruct a function-sort -----------------------------------------------liquid-fixpointError messages ------------------------------------------------------------##  Safe-Inferred")*56;= "liquid-fixpointA Index is a suitably indexed version of the cosntraints that lets us 1. CREATE a monolithic "background formula" representing all constraints, 2. ASSERT each lhs via bits for the subc-id and formulas for dependent cut KVarsliquid-fixpointBindPred for each BindIdliquid-fixpointDefinition of each liquid-fixpointConstraints defining each liquid-fixpointBinders of each Subcliquid-fixpoint,Transitive closure oof all dependent bindersliquid-fixpointSorts for all symbols , bindPrev :: !(BIndex |-> BIndex) -- ^ "parent" (immediately dominating) binder , kvDeps :: !(CMap [KIndex]) -- ^ List of (Cut) KVars on which a SubC dependsliquid-fixpointEach # corresponds to a conjunction of a  and bpKVarsliquid-fixpointConcrete predicate (PTrue o)liquid-fixpointKVar-Subst pairsliquid-fixpoint7A BIndex is created for each LHS Bind or RHS constraintliquid-fixpointA KIndex uniquely identifies each *use* of a KVar in an (LHS) binderliquid-fixpointInstantiated Qualifiers ---------------------------------------------------liquid-fixpointA - is an association list indexed by predicatesliquid-fixpointBinders from defining Envliquid-fixpointSubstitutions from cstrs Rhsliquid-fixpoint Id of defining Cstrliquid-fixpoint(Tag of defining Cstr (DEBUG)liquid-fixpointA  is a single constraint defining a KVar ---------------------------liquid-fixpointA  contains the various indices needed to compute a solution, in particular, to compute lhsPred for any given constraint.liquid-fixpoint'Environment used to elaborate solutionsliquid-fixpointActual solution (for cut kvar)liquid-fixpointSolution for gradual variablesliquid-fixpoint"Defining cubes (for non-cut kvar)liquid-fixpointSet of allowed binders for kvarliquid-fixpoint$EbindSol for each existential binderliquid-fixpointAn  contains the relevant information for an existential-binder; (See testsposebind-*.fq for examples.) This is either 1. the constraint whose HEAD is a singleton that defines the binder, OR 2. the solved out TERM that we should use in place of the ebind at USES.liquid-fixpoint7The constraint whose HEAD "defines" the Ebind and the Symbol for that EBindliquid-fixpoint0The solved out term that should be used at USES.liquid-fixpointEBinds not to be solved for (because they're currently being solved for)liquid-fixpointThe = data type --------------------------------------------------liquid-fixpointUpdate Solution -----------------------------------------------------------liquid-fixpointCreate a Solution ---------------------------------------------------------liquid-fixpointRead / Write Solution at KVar ---------------------------------------------! Safe-Inferred;|liquid-fixpointThe main data types" Safe-Inferred"( liquid-fixpoint"Environment which has been reducedliquid-fixpointThe original constraintliquid-fixpointId of the constraintliquid-fixpointStrips from all the constraint environments the bindings that are irrelevant for their respective constraints./Environment reduction has the following stages.Stage 1) Compute the binding dependencies of each constraint ignoring KVars.A binding is a dependency of a constraint if it is mentioned in the lhs, or the rhs of the constraint, or in a binding that is a dependency, or in a define or match clause that is mentioned in the lhs or rhs or another binding dependency, or if it appears in the environment of the constraint and can't be discarded as trivial (see ).4Stage 2) Compute the binding dependencies of KVars.A binding is a dependency of a KVar K1 if it is a dependency of a constraint in which the K1 appears, or if it is a dependency of another KVar appearing in a constraint in which K1 appears.Stage 3) Drop from the environment of each constraint the bindings that aren't dependencies of the constraint, or that aren't dependencies of any KVar appearing in the constraint.Note on SInfo:(This function can be changed to work on   rather than  5. However, this causes some tests to fail. At least:liquid-fixpointtestsproof/rewrite.fq testsimportclient/ReflectClient4a.hslhs bindings are numbered with the highest numbers when FInfo is converted to SInfo. Environment reduction, however, rehashes the binding identifiers and lhss could end up with a lower numbering. For most of the tests, this doesn't seem to make a difference, but it causes the two tests referred above to fail.See #473 for more discussion.liquid-fixpoint+Reduces the environments of WF constraints./reduceWFConstraintEnvironments bindEnv (cs, ws) * enlarges the environments in cs with bindings needed by the kvars they use * replaces the environment in ws with reduced environmentsReduction of wf environments gets rid of any bindings not mentioned by 8 or any substitution on the corresponding KVar anywhere.liquid-fixpoint%dropIrrelevantBindings aenvMap ss env drops bindings from env which aren't referenced neither in a refinement type in the environment nor in ss&, and not reachable in definitions of aenv referred from env or ss>, and which can't possibly affect the outcome of verification.)Right now, it drops bindings of the form a : {v | true } and b : {v | v [>=|<=|=|!=|etc] e } whenever a and b% aren't referenced from any formulas.liquid-fixpointFor each Equation and Rewrite, collects the symbols that it needs.liquid-fixpointreachableSymbols x r, computes the set of symbols reachable from x in the graph represented by r . Includes x in the result.liquid-fixpoint/Simplifies bindings in constraint environments.It runs  and ( on the environment of each constraint.,If 'inlineANFBindings cfg' is on, also runs  to inline lq_anf bindings.liquid-fixpointIf the environment contains duplicated bindings, they are combined with conjunctions.This means that 1[ a : {v | P v }, a : {z | Q z }, b : {v | S v} ] is combined into ([ a : {v | P v && Q v }, b : {v | S v} ]If a symbol has two bindings with different sorts, none of the bindings for that symbol are merged.liquid-fixpointInlines some of the bindings whose symbol satisfies a given predicate.-Only works if the bindings don't form cycles.liquid-fixpointLike " but specialized for ANF bindings.6Only bindings with prefix lq_anf$... might be inlined.liquid-fixpointLike  but also inlines VV bindingsThis function is used to produced the prettified output, and the user can request to use it in the verification pipeline with --inline-anf-bindings. However, using it in the verification pipeline causes some tests in liquidhaskell to blow up.Note: This function simplifies.liquid-fixpointLike > but returns only modified bindings and **DOES NOT SIMPLIFY**.liquid-fixpoint%Inlines bindings in env in the given .liquid-fixpointInlines bindings given by srLookup7 in the given expression if they appear in equalities.Given a binding like a : { v | v = e1 && e2 } and an expression ... e0 = a ...), this function produces the expression ... e0 = e1 ... if v does not appear free in e1.... e0 = (a : s) ... is equally transformed to ... e0 = (e1 : s) ...Given a binding like a : { v | v = e1 } and an expression  ... a ...), this function produces the expression  ... e1 ... if v does not appear free in e1.liquid-fixpoint Transforms bindings of the form {v:bool | v && P v} into {v:Bool | v && P true}, and bindings of the form {v:bool | ~v && P v} into {v:bool | ~v && P false}."Only yields the modified bindings.liquid-fixpoint#dropLikelyIrrelevantBindings ss env is like dropIrrelevantBindings but drops bindings that could potentially be necessary to validate a constraint.This function drops any bindings in the reachable set of symbols of ss. See .A constraint might be rendered unverifiable if the verification depends on the environment being inconsistent. For instance, suppose the constraint is a < 0 and we call this function like dropLikelyIrrelevantBindings ["a"] [a : { v | v > 0 }, b : { v | false }] == [a : { v | v > 0 }]The binding for b1 is dropped since it is not otherwise related to a4, making the corresponding constraint unverifiable.Bindings refered only from match or define" clauses will be dropped as well.Symbols starting with a capital letter will be dropped too, as these are usually global identifiers with either uninteresting or known types.liquid-fixpointrelatedSymbols ss env1 is the set of all symbols used transitively by ss in env or used together with it in a refinement type. The output includes ss.For instance, say ss contains a, and the environment is a : { v | v > b }, b : int, c : { v | v >= b && b >= d}, d : inta uses b. Because the predicate of c relates b with d, d5 can also influence the validity of the predicate of a!, and therefore we include both b, c, and d in the set of related symbols.liquid-fixpointEnvironment before reductionliquid-fixpoint(cs, ws): * cs3 are the constraints with reduced environments * ws7 are the wf constraints in which to reduce environments  # Safe-Inferred"liquid-fixpointeraseUnusedBindings ss env prefixes with _' the symbols that aren't refered from ss( or refinement types in the environment.liquid-fixpointShortens the names of refinements types in a given environment and constraintliquid-fixpointGiven a list of symbols with no duplicates, it proposes shorter names to use for them.All proposals preserve the prefix of the original name. A prefix is the longest substring containing the initial character and no separator ## ( symSepName).Suffixes are preserved, except when symbols with a given prefix always use the same suffix.liquid-fixpointIndexes symbols by prefix and then by suffix. If the prefix equals the symbol, then the suffix is the empty symbol. For instance, toPrefixSuffixMap ["a##b##c"] ! "a" ! "c" == ["a##b##c"] toPrefixSuffixMap ["a"] ! "a" ! "" == ["a"] In general, forall ss. Set.fromList ss == Set.fromList $ concat [ xs | m <- elems (toPrefixSuffixMap ss), xs <- elems m ] forall ss. and [ all (pfx `isPrefixOfSym`) xs && all (sfx `isSuffixOfSym`) xs | (pfx, m) <- toList (toPrefixSuffixMap ss) , (sfx, xs) <- toList m ]!TODO: put the above in unit testsliquid-fixpointSuggests renamings for every symbol in a given prefix/suffix map.$ Safe-Inferred",jliquid-fixpointSMTLIB/Z3 don't like "unused" type variables; they get pruned away and cause wierd hassles. See testspos$adt_poly_dead.fq for an example.  adds a junk constructor that "uses" up all the tyvars just to avoid this pruning problem.liquid-fixpointsmt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors like Nil, see `testsposadt_list_1.fq`% Safe-Inferred "%&, liquid-fixpointtype ClosedPred E = {v:Pred | subset (vars v) (keys E) } checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Boolliquid-fixpointIf you already HAVE a context, where all the variables have declared types (e.g. if you want to make MANY repeated Queries)liquid-fixpointSMT IO --------------------------------------------------------------------liquid-fixpointSMT Context ---------------------------------------------------------liquid-fixpoint>Close file handles and release the solver backend's resources.liquid-fixpointSMT Commands -----------------------------------------------------------liquid-fixpointSMT Commands -----------------------------------------------------------liquid-fixpoint returns {0, 1, 2} where: 0 = Theory-Definition, 1 = Theory-Declaration, 2 = Query-Binderliquid-fixpoint is used solely to determine the set of literals (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT, or string literals "cat", "dog", "mouse". These should only include non-function sorted values.6 6  & Safe-Inferred";(Oliquid-fixpointParsing Constraints (.fq files) --------------------------------liquid-fixpoint,An OpTable stores operators by their fixity.3Fixity levels range from 9 (highest) to 0 (lowest).liquid-fixpointThe layout stack tracks columns at which layout blocks have started.liquid-fixpointno layout infoliquid-fixpointin a block not using layoutliquid-fixpointin a block at the given columnliquid-fixpoint past a block at the given columnliquid-fixpointThe parser state.1We keep track of the fixities of infix operators.We also keep track of whether empty list and singleton lists syntax is allowed (and how they are to be interpreted, if they are).We also keep track of an integer counter that can be used to supply unique integers during the parsing process.+Finally, we keep track of the layout stack.liquid-fixpoint'Pop the topmost element from the stack.liquid-fixpoint1Modify the layout stack using the given function.liquid-fixpoint:Start a new layout block at the current indentation level.liquid-fixpointTemporarily reset the layout information, because we enter a block with explicit separators.liquid-fixpoint1Remove the topmost element from the layout stack.liquid-fixpoint/Consumes all whitespace, including LH comments./Should not be used directly, but primarily via .The only "valid" use case for spaces is in top-level parsing function, to consume initial spaces.liquid-fixpointVerify that the current indentation level is in the given relation to the provided reference level, otherwise fail.This is a variant of  indentGuard provided by megaparsec, only that it does not consume whitespace.liquid-fixpointChecks the current indentation level with respect to the current layout stack. May fail. Returns the parser to run after the next token.This function is intended to be used within a layout block to check whether the next token is valid within the current block.liquid-fixpointChecks the current indentation level with respect to the current layout stack. The current indentation level must be strictly greater than the one of the surrounding block. May fail.This function is intended to be used before we establish a new, nested, layout block, which should be indented further than the surrounding blocks.liquid-fixpointIndentation-aware lexeme parser. Before parsing, establishes whether we are in a position permitted by the layout stack. After the token, consume whitespace and potentially change state.liquid-fixpoint(Indentation-aware located lexeme parser.This is defined in such a way that it determines the actual source range covered by the identifier. I.e., it consumes additional whitespace in the end, but that is not part of the source range reported for the identifier.liquid-fixpointMake a parser location-aware.This is at the cost of an imprecise span because we still consume spaces in the end first.liquid-fixpointParse a block delimited by layout. The block must be indented more than the surrounding blocks, otherwise we return an empty list.Assumes that the parser for items does not accept the empty string.liquid-fixpoint5Parse a single line that may be continued via layout.liquid-fixpointParse a block of items which can be delimited either via layout or via explicit delimiters as specified.Assumes that the parser for items does not accept the empty string.liquid-fixpointParse a block of items that are delimited via explicit delimiters. Layout is disabled/reset for the scope of this block.liquid-fixpoint#Symbolic lexeme. Stands on its own.liquid-fixpointLocated variant of .liquid-fixpoint Parser String symbol x = L.symbol spaces (string x)liquid-fixpoint&Parser that consumes the given symbol.The difference with  is that the given symbol is seen as a token of its own, so the next character that follows does not matter.symbol :: String -> Parser String symbol x = L.symbol spaces (string x)liquid-fixpoint&Parser that consumes the given symbol.The difference with  is that the given symbol is seen as a token of its own, so the next character that follows does not matter.symbol :: String -> Parser String symbol x = L.symbol spaces (string x)liquid-fixpoint&Parser that consumes the given symbol.The difference with  is that the given symbol is seen as a token of its own, so the next character that follows does not matter.symbol :: String -> Parser String symbol x = L.symbol spaces (string x)liquid-fixpointParses a string literal as a lexeme. This is based on megaparsec's  charLiteral parser, which claims to handle all the single-character escapes defined by the Haskell grammar.liquid-fixpoint Consumes a float literal lexeme.liquid-fixpointConsumes a natural number literal lexeme, which can be in decimal, octal and hexadecimal representation.This does not parse negative integers. Unary minus is available as an operator in the expression language.liquid-fixpointRaw (non-whitespace) parser for an identifier adhering to certain conditions.'The arguments are as follows, in order:%the parser for the initial character,:a predicate indicating which subsequent characters are ok,;a check for the entire identifier to be applied in the end,5an error message to display if the final check fails.liquid-fixpoint?Raw parser for an identifier starting with an uppercase letter.See Note [symChars].liquid-fixpoint>Raw parser for an identifier starting with a lowercase letter.See Note [symChars].liquid-fixpoint6Raw parser for an identifier starting with any letter.See Note [symChars].liquid-fixpointPredicate version to check if the characer is a valid initial character for .TODO: What is this needed for?liquid-fixpointLexeme version of .liquid-fixpointLexeme version of .liquid-fixpoint.Unconstrained identifier, lower- or uppercase.Must not be a reserved word.Lexeme version of .liquid-fixpointParser for literal numeric constants: floats or integers without sign.liquid-fixpoint#Parser for literal string contants.liquid-fixpoint Parser for "atomic" expressions.(This parser is reused by Liquid Haskell.liquid-fixpoint3Parser for an explicitly type-annotated expression.liquid-fixpoint9Parser for atomic expressions plus function applications.Base parser used in  which adds in other operators.liquid-fixpoint Expressionsliquid-fixpoint4Transform an operator table to the form expected by 7, which wants operators sorted by decreasing priority.liquid-fixpoint%Add an operator to the parsing state.liquid-fixpoint7Add a new numeric FTyCon (symbol) to the parsing state.liquid-fixpoint(Parses any of the known infix operators.liquid-fixpointLocated version of .liquid-fixpointHelper function that turns an associativity into the right constructor for .liquid-fixpoint-Add the given operator to the operator table.liquid-fixpoint:Helper function for computing the priority of an operator.=If no explicit priority is given, a priority of 9 is assumed.liquid-fixpointParser for sorts, parameterised over the parser for arguments.,TODO, Andres: document the parameter better.liquid-fixpointPredicates ----------------------------------------------------------------Parser for "atomic" predicates.(This parser is reused by Liquid Haskell.liquid-fixpoint(Parser for the reserved constant "true".liquid-fixpoint)Parser for the reserved constant "false".liquid-fixpoint:Parses a semicolon-separated bracketed list of predicates.Used as the argument of the prefix-versions of conjunction and disjunction.liquid-fixpointParses a predicate.:Unlike for expressions, there is a built-in operator list.liquid-fixpointParses a relation predicate.4Binary relations connect expressions and predicates.liquid-fixpointParses a relation symbol.1There is a built-in table of available relations.liquid-fixpointBareTypes -----------------------------------------------------------------Refaliquid-fixpoint2(Sorted) Refinements with configurable sub-parsersliquid-fixpointBinder (lowerIdP <* colon)liquid-fixpoint(Sorted) Refinementsliquid-fixpoint((Sorted) Refinements with default binderliquid-fixpointParsing Data Declarations -------------------------------------------------liquid-fixpointParsing Qualifiers -------------------------------------------------------- Qualifiersliquid-fixpointAxioms for Symbolic Evaluation ---------------------------------liquid-fixpointInteracting with Fixpoint --------------------------------------liquid-fixpointParse via the given parser, and obtain the rest of the input as well as the final source position.liquid-fixpointInitial parser state.liquid-fixpoint%Entry point for parsing, for testing.Take the top-level parser, the source file name, and the input as a string. Fails with an exception on a parse error.liquid-fixpoint'Function to test parsers interactively.liquid-fixpoint2Obtain a fresh integer during the parsing process.  ' Safe-Inferred"/*( Safe-Inferred"689:;.liquid-fixpoint;Tag each query with a possible string denoting "provenance"liquid-fixpointQuery is an NNF Horn Constraint.liquid-fixpoint$qualifiers over which to solve cstrsliquid-fixpointkvars, with parameter-sortsliquid-fixpointlist of constraintsliquid-fixpoint*list of constants (uninterpreted functionsliquid-fixpoint*list of constants (uninterpreted functionsliquid-fixpointlist of equationsliquid-fixpointlist of match-esliquid-fixpointlist of data-declarationsliquid-fixpointpliquid-fixpointc1  ...  cnliquid-fixpointall x:t. p => cliquid-fixpoint(exi x:t. p / c or is it exi x:t. p => c?liquid-fixpointCst is an NNF Horn Constraint.liquid-fixpointHPred is a Horn predicate that appears as LHS (body) or RHS (head) of constraintsliquid-fixpointrliquid-fixpoint $k(y1..yn)liquid-fixpointp1  ... pnliquid-fixpointHVar is a Horn variableliquid-fixpoint"name of the variable $k1, $k2 etc.liquid-fixpoint, so both fields need to express the exact same dependencies.liquid-fixpoint'Amount of strongly connected componentsliquid-fixpoint)F.SubcIds that transitively "reach" belowliquid-fixpointF.SubcIds with Concrete RHSliquid-fixpointDependencies between slKVarCsliquid-fixpoint7(Constraint id, vertex key, edges to other constraints)The vertex key is always equal to the constraint id. The redundancy is imposed by how containers:Data.Graph requires graphs to be created.liquid-fixpointDramatis Personaeliquid-fixpointreal kvar vertexliquid-fixpoint)dummy to ensure each kvar has a successorliquid-fixpoint1existentially bound "ghost paramter" to solve forliquid-fixpoint(constraint-id which creates a dependencyliquid-fixpointCMap API -------------------------------------------------------------/ / , Safe-Inferred=Zliquid-fixpoint? is representation of the KVGraph with a fast succ, pred lookupliquid-fixpointout-edges of a liquid-fixpointin-edges of a   - Safe-Inferred"%&/Fliquid-fixpoint0number of kvars whose removal makes deps acyclicliquid-fixpoint,number of kvars that appear >= 2 in some LHSliquid-fixpointnumber of kvarsliquid-fixpointis dep-graph reducibleliquid-fixpointset of non-linear kvarsliquid-fixpointGeneric Dependencies ------------------------------------------------------liquid-fixpointCompute constraints that transitively affect target constraints, and delete everything else from F.SInfo aliquid-fixpointDO NOT DELETE! sliceCSucc :: Slice -> CSucc sliceCSucc sl = i -> M.lookupDefault [] i im where im = M.fromList [(i, is) | (i,_,is) <- slEdges sl]liquid-fixpointConstraint Graph ----------------------------------------------------------liquid-fixpointRanks from Graph ----------------------------------------------------------Yields the strongly conected components and a map of constraint ids to an index identifying the strongly connected component to which it belongs. The scc indices correspond with a topological ordering of the sccs.liquid-fixpointDependencies --------------------------------------------------------------liquid-fixpointEliminated Dependenciesliquid-fixpoint0 "eliminates" a kvar k by replacing every "path"ki -> ci -> k -> c with an edgeki ------------> cliquid-fixpointCompute Dependencies and Cuts ---------------------------------------------liquid-fixpoint returns an  that renders the dependency graph acyclic by picking _at least one_ kvar from each non-trivial SCC in the graphliquid-fixpoint extends the input  by adding kuts that ensure that the *maximum distance* between an eliminated KVar and a cut KVar is *upper bounded* by a given threshold.liquid-fixpointConverts dependencies between constraints and kvars, to dependencies between constraints.'TODO merge these with cGraph and kvSuccliquid-fixpointConverts dependencies between constraints and kvars to dependencies between constraints.The returned map tells for each coonstraint writing a kvar which constraints are reading the kvar.liquid-fixpointRemoves the kut vars from the graph, and recomputes the SCC indices.  . Safe-Inferred"/Lliquid-fixpointType alias for a function to construct a partition. mkPartition and mkPartition' are the two primary functions that conform to this interfaceliquid-fixpointMulticore info ------------------------------------------------------------liquid-fixpointConstraint Partition Container --------------------------------------------liquid-fixpointPartition an FInfo into multiple disjoint FInfos. Info is Nothing to produce the maximum possible number of partitions. Or a MultiCore Info to control the partitioningliquid-fixpointPartition an FInfo into a specific number of partitions of roughly equal amounts of work.liquid-fixpointReturn the "size" of a CPart. Used to determine if it's substantial enough to be worth parallelizing.liquid-fixpointConvert a CPart to an FInfoliquid-fixpointConvert an FInfo to a CPartliquid-fixpoint"typically a F.FInfo a or F.CPart aliquid-fixpoint*Describes thresholds and partition amountsliquid-fixpointThe originial FInfoliquid-fixpoint&A list of the smallest possible CPartsliquid-fixpoint,At most N partitions of at least thresh workliquid-fixpointmkPartition or mkPartition'liquid-fixpoint  F.FInfo aor [F.CPart a]G Safe-InferredLv / Safe-Inferred";M10 Safe-InferredO liquid-fixpoint Constraint Idliquid-fixpointTime at which insertedliquid-fixpointRank of constraintliquid-fixpointWorkItems ------------------------------------------------------------liquid-fixpointWorklist ------------------------------------------------------------------liquid-fixpointInitialize worklist and slice out irrelevant constraints ------------------liquid-fixpointCandidate Constraints to be checked AFTER computing Fixpoint ---------liquid-fixpoint Pending APIliquid-fixpointSet API --------------------------------------------------------------1 Safe-Inferred"Zliquid-fixpoint computes the "real" domain of each kvar, which is a SUBSET of the input domain, in which we KILL the parameters x which appear in substitutions of the form `K[x := y]` where y is not in the env.liquid-fixpointdropAdtMeasures removes all the measure definitions that correspond to constructor, selector or test names for declared datatypes, as these are now "natively" handled by the SMT solver.liquid-fixpoint traverses the constraints to find (string) literals that are then added to the dLits field.liquid-fixpoint4 converts equations of the form f x = g x into f = gliquid-fixpointSee issue liquid-fixpoint issue #230. This checks that whenever we have, G1 |- K.su1 G2, K.su2 |- rhs then G1 cap G2 subseteq wenv(k)liquid-fixpoint removes dead `K[x := e]` where x NOT in the domain of K.liquid-fixpoint updates the kvar-domains in the wf constraints to a subset of the original binders, where we DELETE the parameters x= which appear in substitutions of the form `K[x := y]` where y is not in the env.liquid-fixpoint*`restrictWf kve k w` restricts the env of w to the parameters in `kve k`.liquid-fixpoint;check that no constraint has free variables (ignores kvars)liquid-fixpoint$check that every DataDecl is regularliquid-fixpoint*check that no qualifier has free variablesliquid-fixpoint=check that each constraint has RHS of form [k1,...,kn] or [p]liquid-fixpoint1symbol |-> sort for EVERY variable in the SInfo;  can ONLY be called with **sanitized** environments (post the uniqification etc.) or else you get duplicate sorts and other such errors. We do this peculiar dance with env0 to extract the apply-sorts from the function definitions inside the AxiomEnv which cannot be elaborated as it makes it hard to actually find the fundefs within (breaking PLE.)liquid-fixpointDrop func-sorted bind that are shadowed by constant (if same type, else error)liquid-fixpoint-Drop irrelevant binders from WfC Environmentsliquid-fixpoint nonDerivedLH* keeps a bind x if it does not start with  which is used typically for names that are automatically "derived" by GHC (and which can) blow up the environments thereby clogging instantiation, etc. NOTE: This is an LH specific hack and should be moved there.liquid-fixpoint+Generic API for Deleting Binders from FInfoliquid-fixpoint0Replace KVars that do not have a WfC with PFalse9 2 Safe-Inferred ")*\rliquid-fixpointSubstitute Gradual Solution ---------------------------------------------liquid-fixpointThe Unique Monad ---------------------------------------------------------liquid-fixpointMake each gradual appearence unique -------------------------------------liquid-fixpointexpandWF -----------------------------------------------------------------3 Safe-Inferred;_liquid-fixpointA  maps an old name and sort to new name, represented by a hashmap containing association lists. 3 as new name means the name is the same as the old.liquid-fixpointAn  stores for each constraint and BindId the set of other BindIds that it references, i.e. those where it needs to know when their names gets changedliquid-fixpointBind identifierliquid-fixpointConstraint identifier?liquid-fixpoint replaces the refinements of "unused" binders with "true". see testspos5unused.fq for an example of why this phase is needed.liquid-fixpoint seems to do the actual work of renaming all the binders to use their sort-specific names.4 Safe-Inferredl liquid-fixpointInformation about size of formula corresponding to an "eliminated" KVar.liquid-fixpointThese are the bindings that the smt solver knows about and can be referred as EVar (bindSymbol  bindId)$ instead of serializing them again.liquid-fixpoint NOTE:qual-clusterIt is wasteful to perform instantiation *individually* on each qualifier, as many qualifiers have "equivalent" parameters, and so have the "same" instances in an environment. To exploit this structure, %Group the [Qualifier] into a QClusterRefactor instK to use QClusterliquid-fixpointInitial Solution (from Qualifiers and WF constraints) ---------------------liquid-fixpointPredicate corresponding to LHS of constraint in current solutionliquid-fixpoint7Produces a predicate from a constraint defining a kvar. This is written in imitation of ;. However, there are some differences since the result of * is fed to the verification pipeline and  bareCubePred is meant for human inspection.1) Only one existential quantifier is introduced at the top of the expression. 2)  bareCubePred< doesn't elaborate the expression, so it avoids calling .  is invoked to eliminate other kvars though, and apply will invoke , so HI might need to be called on the output to remove the elaboration. 3) The expression is created from its defining constraints only, while cubePred does expect the caller to supply the substitution at a particular use of the KVar. Thus cubePred produces a different expression for every use site of the kvar, while here we produce one expression for all the uses.liquid-fixpoint/`cubePred g s k su c` returns the predicate for(k . su)defined by using cubec := [b1,...,bn] |- (k . su')in the binder environment g.bs' := the subset of "extra" binders in [b1...bn] that are *not* in g p' := the predicate corresponding to the "extra" bindersliquid-fixpoint cubePredExc computes the predicate for the subset of binders bs'. The output is a tuple, `(xts, psu, p, kI)` such that the actual predicate we want is `Exists xts. (psu / p)`.liquid-fixpoint substElim returns the binders that must be existentially quantified, and the equality predicate relating the kvar-"parameters" and their actual values. i.e. givenK[x1 := e1]...[xn := en]where e1 ... en have types t1 ... tn we want to quantify outx1:t1 ... xn:tnand generate the equality predicate && [x1 ~~ e1, ... , xn ~~ en] we use ~~ because the param and value may have different sorts, see:testsposkvar-param-poly-00.hs*Finally, we filter out binders if they are "free" in e1...en i.e. in the outer environment. (Hmm, that shouldn't happen...?)are binders corresponding to sorts (e.g. `a : num`, currently used to hack typeclasses current.)liquid-fixpoint: constructs the information about the "ebind-definitions".5 Safe-Inferred"oliquid-fixpointSMT Solver Contextliquid-fixpointAll variables and typesliquid-fixpointSolver Statisticsliquid-fixpointSolver Monadic API --------------------------------------------------------liquid-fixpointSMT Interface -------------------------------------------------------------Takes the environment of bindings already known to the SMT, and the environment of all bindings that need to be known.+Yields the ids of bindings known to the SMTliquid-fixpoint`filterRequired [(x1, p1),...,(xn, pn)] q` returns a minimal list [xi] s.t. / [pi] => qliquid-fixpoint`filterValid p [(q1, x1),...,(qn, xn)]` returns the list `[ xi | p => qi]`liquid-fixpoint`filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]` | for some p in the list ps6 Safe-InferredpZliquid-fixpointInitial Gradual Solution (from Qualifiers and WF constraints) -------------7 Safe-Inferredp8 Safe-Inferred"sliquid-fixpoint'allow higher order thus defunctionalizeliquid-fixpoint/lambda expressions appearing in the expressionsliquid-fixpoint$redexes appearing in the expressionsliquid-fixpointsorts of new lambda-bindersliquid-fixpointContainers defunctionalization --------------------------------------------liquid-fixpointExpressions defunctionalization --------------------------------------------------------liquid-fixpoint*normalize lambda arguments [TODO: example]Renames lambda bindings to lamb_arg##i. Each use of a lambda binding is surrounded with a cast.liquid-fixpointLow level monad manipulation ----------------------------------------------9 Safe-Inferred "%&|fliquid-fixpointNormalization of Equation: make their arguments unique -------------------liquid-fixpointKnowledge (SMT Interaction)liquid-fixpoint7Rewrite rules came from match and data type definitionsliquid-fixpoint+All function definitions -- restore ! here?liquid-fixpointsummary of functions to be evaluates (knSims and knAsms) with their arityliquid-fixpoint$data constructors drawn from Rewriteliquid-fixpointUnfold is the result of running PLE at a single equality; (e, [(e1, e1')...]) is the source e@ and the (possible empty) list of PLE-generated equalities (e1, e1') ...liquid-fixpointInstRes( is the final result of PLE; a map from BindId( to the equations "known" at that BindIdliquid-fixpointICtx is the local information -- at each trie node -- obtained by incremental PLEliquid-fixpoint Candidates for unfoldingliquid-fixpointAccumulated equalitiesliquid-fixpoint#Terms that we have already expandedliquid-fixpointMap of expressions to constantsliquid-fixpointCurrent subconstraint IDliquid-fixpointInstEnv, has the global information needed to do PLEliquid-fixpoint*Strengthen Constraint Environments via PLEliquid-fixpoint Step 1a: instEnv( sets up the incremental-PLE environmentliquid-fixpoint Step 1b: mkCTrie builds the Trie- of constraints indexed by their environmentsliquid-fixpointStep 2: pleTrie walks over the CTrie# to actually do the incremental-PLEliquid-fixpointple10 performs the PLE at a single "node" in the Trieliquid-fixpointStep 3: resSInfo uses incremental PLE result InstRes" to produce the strengthened SInfoliquid-fixpointupdCtx env ctx delta cidMb* adds the assumptions and candidates from delta and cidMb to the context.liquid-fixpoint unfolds or instantiates an equation at a particular list of argument values. We must also substitute the sort-variables that appear as coercions. See testsproofple1.fqliquid-fixpointin "reverse" order: Safe-Inferred"|; Safe-Inferred "%&`,liquid-fixpointNormalization of Equation: make their arguments unique -------------------liquid-fixpointA type to express whether SMeasures originate from data definitions. That is whether they are constructor tests, selectors, or something else.liquid-fixpointKnowledge (SMT Interaction)liquid-fixpoint*Rewrites rules came from match definitionsThey are grouped by the data constructor that they unfold, and are augmented with an attribute that say whether they originate from a user data declaration.liquid-fixpointAll function definitionsliquid-fixpointsummary of functions to be evaluates (knSims and knAsms) with their arityliquid-fixpoint$data constructors drawn from Rewriteliquid-fixpointdata constructors by nameliquid-fixpoint0Equalities where we couldn't evaluate the guardsliquid-fixpoint:Equalities discovered during a traversal of an expressionliquid-fixpoint.Whether an expression is valid or its negationliquid-fixpointUnfold is the result of running PLE at a single equality; (e, [(e1, e1')...]) is the source e@ and the (possible empty) list of PLE-generated equalities (e1, e1') ...liquid-fixpointInstRes( is the final result of PLE; a map from BindId( to the equations "known" at that BindIdliquid-fixpointICtx is the local information -- at each trie node -- obtained by incremental PLEliquid-fixpoint"Equalities converted to SMT formatliquid-fixpoint Candidates for unfoldingliquid-fixpointAccumulated equalitiesliquid-fixpointMap of expressions to constantsliquid-fixpointCurrent subconstraint IDliquid-fixpointInstEnv, has the global information needed to do PLEliquid-fixpoint*Strengthen Constraint Environments via PLEliquid-fixpoint Step 1a: instEnv( sets up the incremental-PLE environmentliquid-fixpoint Step 1b: mkCTrie builds the Trie- of constraints indexed by their environmentsThe trie is a way to unfold the equalities a minimum number of times. Say you have 11: [1, 2, 3, 4, 5] => p1 2: [1, 2, 3, 6, 7] => p2Then you build the tree  1 -> 2 -> 3 -> 4 -> 5 @ [Constraint 1] | -> 6 -> 7 @ [Constraint 2]which you use to unfold everything in 1, 2, and 3 once (instead of twice) and with the proper existing environmentliquid-fixpointStep 2: pleTrie walks over the CTrie# to actually do the incremental-PLEliquid-fixpointAdds to ctx6 candidate expressions to unfold from the bindings in delta and the rhs of cidMb.Adds to ctx assumptions from env and delta."Sets the current constraint id in ctx to cidMb.Pushes assumptions from the modified context to the SMT solver, runs act!, and then pops the assumptions.liquid-fixpointple10 performs the PLE at a single "node" in the TrieIt will generate equalities for all function invocations in the candidates in ctx for which definitions are known. The function definitions are in ieKnowl.liquid-fixpointGenerate equalities for all function invocations in the candidates in ctx for which definitions are known. The function definitions are in ieKnowl.In pseudocode: do for every candidate discover equalities, unfold function invocations, update candidates with the unfolded expressions send newly discovered equalities to the SMT solver until no new equalities are discovered or the environment becomes inconsistentliquid-fixpointStep 3: resSInfo uses incremental PLE result InstRes" to produce the strengthened SInfoliquid-fixpointupdCtx env ctx delta cidMb* adds the assumptions and candidates from delta and cidMb to the context.liquid-fixpoint)Discover the equalities in an expression.The discovered equalities are in the environment of the monad, and the list of produced expressions contains the result of unfolding definitions. When REST is in effect, more than one expression might be returned because expressions can then be rewritten in more than one way.liquid-fixpoint,Unfolds function invocations in expressions.Also reduces if-then-else when the boolean condition or the negation can be proved valid. This is the actual implementation of guard-validation-before-unfolding that is described in publications.Also adds to the monad state all the unfolding equalities that have been discovered as necessary.liquid-fixpoint evalELamb produces equations that preserve the context of a rewrite so equations include any necessary lambda bindings.liquid-fixpointAdds to the monad state all the subexpressions that have been rewritten as pairs 1(original_subexpression, rewritten_subexpression).Also folds constants.The main difference with  is that " takes into account autorewrites.liquid-fixpointevalApp kn ctx e es unfolds expressions in  eApps e es using rewrites and equationsliquid-fixpointEvaluates if-then-else statements until they can't be evaluated anymore or some other expression is found.liquid-fixpointCreates equations that explain how to rewrite a given constructor application with all measures that aren't user data measuresliquid-fixpoint unfolds or instantiates an equation at a particular list of argument values. We must also substitute the sort-variables that appear as coercions. See testsproofple1.fqliquid-fixpointmkCoSub senv eTs xTs = su creates a substitution su such that subst su xTs == eTs.The variables in the domain of the substitution are those that appear as  FObj symbol in xTs.liquid-fixpointPartitions the input rewrites into constructor tests and others.We don't need to deal in PLE with data constructor tests. That is, functions of the form isCons :: List a -> Bool or isNil :: List a -> Bool when List a is defined by the user.The SMT solver knows about these functions when datatypes are declared to it, so PLE doesn't need to unfold them. Non-user defined datatypes like [a] still need to have tests unfolded because they are not declared as datatypes to the SMT solver.Also, REST could need this functions unfolded since otherwise it may not discover possible rewrites.liquid-fixpointLike  but for selectors.liquid-fixpoint8Normalize the given named expression if it is recursive.liquid-fixpointIncrement the fuel count of the given symbol in the current evaluation environment.liquid-fixpointIncrement the fuel count.liquid-fixpointReturns False if there is a fuel count in the evaluation environment and the fuel count exceeds the maximum. Returns True otherwise.liquid-fixpointin "reverse" orderliquid-fixpoint6The longest path suffix without forks in reverse orderliquid-fixpoint6bind id of the branch ancestor of the trie if any. ! when this is the top-level trie.liquid-fixpoint6The longest path suffix without forks in reverse orderliquid-fixpoint8bind id of the branch ancestor of the branch if any. - when this is a branch of the top-level trie.9 < Safe-Inferred "%&(liquid-fixpointKnowledge (SMT Interaction)liquid-fixpoint*Measure info, asserted for each new Ctor ()liquid-fixpoint.(Recursive) function definitions, used for PLEliquid-fixpoint NOTE: Eval-IteWe should not be doing any PLE/eval under if-then-else where the guard condition does not provably hold. For example, see issue #387. However, its ok and desirable to  in this case, as long as one is not unfolding recursive functions. To permit this, we track the "call-stack" and whether or not,  is occurring under an unresolved guard: if so, we do not expand under any function that is already on the call-stack.liquid-fixpointUnfold is the result of running PLE at a single equality; (e, [(e1, e1')...]) is the source e@ and the (possible empty) list of PLE-generated equalities (e1, e1') ... type Unfold = (Maybe Expr, [(Expr, Expr)])liquid-fixpointInstRes( is the final result of PLE; a map from BindId( to the equations "known" at that BindIdliquid-fixpointICtx is the local information -- at each trie node -- obtained by incremental PLEliquid-fixpoint+Hypotheses, already converted to SMT formatliquid-fixpoint Candidates for unfoldingliquid-fixpointKnown equalitiesliquid-fixpoint#Terms that we have already expandedliquid-fixpointInstEnv, has the global information needed to do PLEliquid-fixpoint*Strengthen Constraint Environments via PLEliquid-fixpointNew  Incremental PLE -- see [NOTE:TREE-LIKE] NOTE:TREE-LIKEincremental PLE relies crucially on the SInfo satisfying a "tree like" invariant: forall constraints c, c'. if i in c and i in c' then forall 0 <= j < i, j in c and j in c'liquid-fixpoint Step 1a: instEnv( sets up the incremental-PLE environmentliquid-fixpoint Step 1b: mkCTrie builds the Trie- of constraints indexed by their environmentsliquid-fixpointStep 2: pleTrie walks over the CTrie# to actually do the incremental-PLEliquid-fixpointple10 performs the PLE at a single "node" in the Trieliquid-fixpointStep 3: resSInfo uses incremental PLE result InstRes" to produce the strengthened SInfoliquid-fixpointupdCtx env ctx delta cidMb* adds the assumptions and candidates from delta and cidMb to the context.liquid-fixpointOld GLOBAL PLEliquid-fixpointSymbolic Evaluation with SMTliquid-fixpoint also evaluates all the partial applications for hacky reasons, suppose `foo g = id` then we want `foo g 10 = 10` and for that we need to  the term `foo g` into  to tickle the  on `id 10`. This seems a bit of a hack. At any rate, this can lead to divergence. TODO: distill a .fq test from the MOSSAKA-hw3 example.liquid-fixpoint$Minimal test case illustrating this  hack is LH#testsplepos/MossakaBug.hs too tired & baffled to generate simple .fq version. TODO:nuke and rewrite PLE!liquid-fixpoint unfolds or instantiates an equation at a particular list of argument values. We must also substitute the sort-variables that appear as coercions. See testsproofple1.fqliquid-fixpointThis creates the rewrite rule e1 -> e2, applied when: 1. when e2 is a DataCon and can lead to further reductions 2. when size e2 < size e1liquid-fixpointCreating Measure Infoliquid-fixpointin "reverse" orderliquid-fixpoint Definitionsliquid-fixpointEnvironment of "true" factsliquid-fixpointCandidates for unfoldingliquid-fixpoint Constraint Idliquid-fixpointNewly unfolded equalities9 = Safe-Inferred%liquid-fixpoint Map each 6 to the list of constraints on which it appears on RHSliquid-fixpoint constructs a  comprising the Solution and various indices needed by the worklist-based refinement loop> Safe-Inferred"liquid-fixpoint Progress Barliquid-fixpointtidyResult ensures we replace the temporary kVarArg names introduced to ensure uniqueness with the original names in the given WF constraints.liquid-fixpointSingle Step Refinement -----------------------------------------------liquid-fixpointConvert Solution into Result ----------------------------------------------liquid-fixpoint transforms each KVar's result by removing conjuncts that are implied by others. That is, {qs:[Pred] | subset qs ps}such that `minimizeConjuncts ps` is a minimal subset of ps where no is implied by /_{q' in qs qs} see: testsposmin00.fq for an example.liquid-fixpointPredicate corresponding to RHS of constraint in current solutionliquid-fixpointInteraction with the user when Solving -----------------------------------? Safe-Inferred#@ Safe-Inferred", liquid-fixpointUnpleasant hack to save meta-data that can be recovered from SrcSpanliquid-fixpointSolve an .fq file ----------------------------------------------------liquid-fixpointSolve FInfo system of horn-clause constraints -----------------------------liquid-fixpointSolve in parallel after partitioning an FInfo to indepdendant partsliquid-fixpointSolve in parallel after partitioning an FInfo to indepdendant partsliquid-fixpointSolve a list of FInfos using the provided solver function in parallelliquid-fixpointNative Haskell Solver -----------------------------------------------------liquid-fixpointNative Haskell Solver -----------------------------------------------------liquid-fixpointParse External Qualifiers -------------------------------------------------   A Safe-Inferred"2liquid-fixpointflatten removes redundant s and empty conjuncts.For example: >>> :{ flatten $ doParse' hCstrP "" "(forall ((VV##15 int) (VV##15 == anf##3)) ((and (and ($k13 VV##15 anf##3 moo##5) (true)))))":} (forall ((VV##15 int) (VV##15 == anf##3)) ((k13 VV##15 anf##3 moo##5)))liquid-fixpoint-uniq makes sure each binder has a unique nameliquid-fixpointsolveEbs takes a query and returns a query with the ebinds solved outit has some preconditions - pi -> k -> pi structure. That is, there are no cycles, and while ks can depend on other ks, pis cannot directly depend on other pis - predicate for exists binder is true. (TODO: is this pre stale?)liquid-fixpointCollects the defining constraint for  that is, given `D .D n. => c`, returns `((, n:), c)`liquid-fixpointSolve out the given pivarsliquid-fixpointpokec skolemizes the EHC into an HC + side condition >>> (q, opts) <- parseFromFile hornP "testshornpos/ebind01.smt2" >>> F.pprint $ pokec (qCstr q) (and (forall ((m int) (true)) (and (forall ((x1 int) (x1 x1)) (and (forall ((v int) (v == m + 1)) (((v == x1)))) (forall ((v int) (v == x1 + 1)) (((v == 2 + m)))))) (exists ((x1 int) (true)) ((x1 x1))))))>(q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"F.pprint $ pokec (qCstr q)(and (forall ((m int) (true)) (forall ((z int) (z == m - 1)) (and$ (forall ((v1 int) (v1 == z + 2)) ((k v1))) (and (forall ((x1 int) (x1 x1)) (and (forall ((v2 int) (k v2)) (((v2 == x1))))( (forall ((v3 int) (v3 == x1 + 1)) (((v3 == m + 2)))))) (exists ((x1 int) (true)) ((x1 x1))))))))let c = doParse' hCstrP "" "(forall ((a Int) (p a)) (exists ((b Int) (q b)) (and (($k a)) (($k b)))))"F.pprint $ pokec c(forall ((a int) (p a)) (and (forall ((b int) (b b)) (and ((k a)) ((k b)))) (exists ((b int) (q b)) ((b b)))))liquid-fixpointNow we split the poked constraint into the side conditions and the meat of the constraint>(q, opts) <- parseFromFile hornP "tests/horn/pos/ebind01.smt2"F.pprint $ qCstr q(and (forall ((m int) (true)) (exists ((x1 int) (true)) (and" (forall ((v int) (v == m + 1)) (((v == x1))))# (forall ((v int) (v == x1 + 1)) (((v == 2 + m))))))))6let (Just noside, Just side) = split $ pokec $ qCstr q F.pprint side(forall ((m int) (true)) (exists ((x1 int) (true)) ((x1 x1))))F.pprint noside(forall ((m int) (true)) (forall ((x1 int) (x1 x1)) (and! (forall ((v int) (v == m + 1)) (((v == x1))))" (forall ((v int) (v == x1 + 1)) (((v == 2 + m)))))))>(q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"F.pprint $ qCstr q (and (forall ((m int) (true)) (forall ((z int) (z == m - 1)) (and$ (forall ((v1 int) (v1 == z + 2)) ((k v1))) (exists ((x1 int) (true)) (and (forall ((v2 int) (k v2)) (((v2 == x1))))' (forall ((v3 int) (v3 == x1 + 1)) (((v3 == m + 2))))))))))6let (Just noside, Just side) = split $ pokec $ qCstr q F.pprint side(forall ((m int) (true)) (forall ((z int) (z == m - 1)) (exists ((x1 int) (true)) ((x1 x1)))))F.pprint noside (forall ((m int) (true)) (forall ((z int) (z == m - 1)) (and# (forall ((v1 int) (v1 == z + 2)) ((k v1))) (forall ((x1 int) (x1 x1)) (and (forall ((v2 int) (k v2)) (((v2 == x1))))& (forall ((v3 int) (v3 == x1 + 1)) (((v3 == m + 2)))))))))liquid-fixpoint>(q, opts) <- parseFromFile hornP "tests/horn/pos/ebind01.smt2"6let (Just noside, Just side) = split $ pokec $ qCstr q)F.pprint $ elimPis ["x1"] (noside, side )(forall ((m int) (true))$ (forall ((x1 int) (forall [v : int] . v == m + 1 => v == x1&& forall [v : int]" . v == x1 + 1 => v == 2 + m)) (and! (forall ((v int) (v == m + 1)) (((v == x1))))" (forall ((v int) (v == x1 + 1))3 (((v == 2 + m))))))) : (forall ((m int) (true))5 (exists ((x1 int) (true))/ ((forall [v : int]8 . v == m + 1 => v == x12 && forall [v : int] . v == x1 + 1 => v == 2 + m))))>(q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"6let (Just noside, Just side) = split $ pokec $ qCstr q)F.pprint $ elimPis ["x1"] (noside, side )(forall ((m int) (true)) (forall ((z int) (z == m - 1)) (and# (forall ((v1 int) (v1 == z + 2)) ((k v1)))' (forall ((x1 int) (forall [v2 : int]1 . $k[fix$36$$954$arg$36$k$35$1:=v2] => v2 == x1&& forall [v3 : int]$ . v3 == x1 + 1 => v3 == m + 2)) (and (forall ((v2 int) (k v2)) (((v2 == x1))))& (forall ((v3 int) (v3 == x1 + 1))8 (((v3 == m + 2))))))))) : (forall ((m int) (true))? (forall ((z int) (z == m - 1)); (exists ((x1 int) (true))6 ((forall [v2 : int] . $k[fix$36$$954$arg$36$k$35$1:=v2] => v2 == x19 && forall [v3 : int] . v3 == x1 + 1 => v3 == m + 2)))))liquid-fixpoint$The defining constraints for a pivarThe defining constraints are those that bound the value of pi_x.We're looking to lower-bound the greatest solution to pi_x. If we eliminate pivars before we eliminate kvars (and then apply the kvar solutions to the side conditions to solve out the pis), then we know that the only constraints that mention pi in the noside case are those under the corresponding pivar binder. A greatest solution for this pivar can be obtained as the _weakest precondition_ of the constraints under the binderThe greatest Pi that implies the constraint under it is simply that constraint itself. We can leave off constraints that don't mention n, see +https://photos.app.goo.gl/6TorPprC3GpzV8PL7Actually, we can really just throw away any constraints we can't QE, can't we?:{let c = doParse' hCstrP "" "\(forall ((m int) (true)) \ (forall ((x1 int) (and (true) (x1 x1))) \ (and \ (forall ((v int) (v == m + 1)) \ (((v == x1)))) \ (forall ((v int) (v == x1 + 1)) \ (((v == 2 + m)))))))":}F.pprint $ defs "x1" c Just (and$ (forall ((v int) (v == m + 1)) ((v == x1)))% (forall ((v int) (v == x1 + 1)) ((v == 2 + m))))>(q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2".let (Just noside, _) = split $ pokec $ qCstr qF.pprint $ defs "x1" noside Just (and (forall ((v2 int) (k v2)) ((v2 == x1)))' (forall ((v3 int) (v3 == x1 + 1)) ((v3 == m + 2))))liquid-fixpoint(q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"6let (Just noside, Just side) = split $ pokec $ qCstr q7F.pprint $ elimKs ["k"] $ elimPis ["x1"] (noside, side)(forall ((m int) (true)) (forall ((z int) (z == m - 1)) (and# (forall ((v1 int) (v1 == z + 2)) ((true)))' (forall ((x1 int) (forall [v2 : int] . exists [v1 : int] . (v2 == v1)" && v1 == z + 2 => v2 == x1&& forall [v3 : int]$ . v3 == x1 + 1 => v3 == m + 2)) (and% (forall ((v1 int) (v1 == z + 2))# (forall ((v2 int) (v2 == v1)) (((v2 == x1)))))& (forall ((v3 int) (v3 == x1 + 1))8 (((v3 == m + 2))))))))) : (forall ((m int) (true))? (forall ((z int) (z == m - 1)); (exists ((x1 int) (true))6 ((forall [v2 : int]: . exists [v1 : int]7 . (v2 == v1) && v1 == z + 2 => v2 == x19 && forall [v3 : int] . v3 == x1 + 1 => v3 == m + 2)))))liquid-fixpointQuantifier elimination for use with implicit solver qe :: Cstr a -> Cstr aliquid-fixpointelim solves all of the KVars in a Cstr (assuming no cycles...) >>> elim . qCstr . fst  $ parseFromFile hornP "testshornpos/test00.smt2" (and (forall ((x int) (x > 0)) (forall ((y int) (y > x)) (forall ((v int) (v == x + y)) ((v > 0)))))) >>> elim . qCstr . fst  $ parseFromFile hornP "testshornpos/test01.smt2" (and (forall ((x int) (x > 0)) (and (forall ((y int) (y > x)) (forall ((v int) (v == x + y)) ((v > 0)))) (forall ((z int) (z > 100)) (forall ((v int) (v == x + z)) ((v > 100))))))) >>> elim . qCstr . fst  $ parseFromFile hornP "testshornpos/test02.smt2" (and (forall ((x int) (x > 0)) (and (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) ((true)))) (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) (forall ((z int) (z == v)) (forall ((v int) (v == x + z)) ((v > 100)))))))))liquid-fixpointsc <- scope "k0" . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2"sc(forall ((x ... (and (forall ((y ... (forall ((v ... ((k0 v)))) (forall ((z ...liquid-fixpointA solution is a Hyp of binders (including one anonymous binder that I've singled out here). (What does Hyp stand for? Hypercube? but the dims don't line up...)c <- qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2"sol1 ("k0") (scope "k0" c)[[((y int) (y > x + 100)),((v int) (v == x + y)),((_ bool) (arg$k0#1 == v))]]c <- qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2"sol1 ("k0") (scope "k0" c)[[((x int) (x > 0)),((v int) (v == x)),((_ bool) (arg$k0#1 == v))],[((y int) (k0 y)),((v int) (v == y + 1)),((_ bool) (arg$k0#1 == v))]]let c = doParse' hCstrP "" "(forall ((a Int) (p a)) (forall ((b Int) (q b)) (and (($k a)) (($k b)))))" sol1 "k" c[[((a int) (p a)),((b int) (q b)),((_ bool) (arg$k#1 == a))],[((a int) (p a)),((b int) (q b)),((_ bool) (arg$k#1 == b))]]liquid-fixpointLET c = doParse' hCstrP "" "(forall ((z Int) ($k0 z)) ((z = x)))"doelim "k0" [[Bind "v" F.boolSort (Reft $ F.EVar "v"), Bind "_" F.boolSort (Reft $ F.EVar "donkey")]] c>(forall ((v bool) (v)) (forall ((z int) (donkey)) ((z == x))))liquid-fixpointReturns a list of KVars with their arguments that are present asboundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/ebind01.smt2"... []boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/ebind02.smt2" ... ["k"]boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test00.smt2"... []boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test01.smt2"... []boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2" ... ["k0"]boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2" ... ["k0"]liquid-fixpointReturns true if the constraint does not contain any existential bindersliquid-fixpointCleanup Horn Constraint We want to simplify the Query a little bit, and make sure it is Horn, that is, only a kvar-free (ie concrete) predicate or a single kvar in each headliquid-fixpointSplit heads into one for each kvar so that queries are always horn constraintsB Safe-InferredpJKLMNOMNPMNQMNRMNSMNTMNUMNUVWXVWYVWZVW[VW\VW]VW^VW_VW`VWaVWbVWcVWdVWeVWfVWgVWhVWiVWjVWkVWlVWmVWnVWoVWpVWqVWrVWsVWtVWuVWvVWwVWxVWyVWzVW{VW|VW}VW~VWVWVWVWVWVWVWVWVWVWVWVWVVVVVVVVVVVVVVVj                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       I                                                                                                                     !!!!!!""""""""""#$$$$$$$$$$$$%%%%%%%%%%%%%%%%%%%%%%%&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&_&&&&&&&&&&j&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&'( (( ((((((((((((((((((((((((((((((((( (((((((((((((((((((((((((((((((((((((((((())))))***+++++++++++++++++++++++++++++++++++++++++++++++++++++++++,,,,,,,,,,,--------------- -................./// / / 0 0000000 0000000 0 11122222222222222222222223333344444444455555555555555556777777788888888888888888899999999999999999999999999::;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;<<<<=>>???@@@@@AAAAAAAAAAAAAABBCCCCCCCCJ  J   !""""""""""""#####$$%%&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&))* ***--------------.....000000111111111111111111223J33333444444444488888 889999999999999;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;<<<<<<<<<<<<<<<<<<<<<<<<J<<<<<=>>>>>>>@@@@@@AJAAAAAAAAAAAAAAA.liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOWLanguage.Fixpoint.Utils.BuilderLanguage.Fixpoint.Types.Spans Text.PrettyPrint.HughesPJ.Compat Data.ShareMap Language.Fixpoint.Conditional.Z3 Language.Fixpoint.Utils.ProgressLanguage.Fixpoint.MiscLanguage.Fixpoint.Utils.FilesLanguage.Fixpoint.Types.Config#Language.Fixpoint.Types.PrettyPrintLanguage.Fixpoint.Utils.TrieLanguage.Fixpoint.Types.NamesLanguage.Fixpoint.Types.Sorts#Language.Fixpoint.Types.Refinements Language.Fixpoint.Types.Triggers!Language.Fixpoint.Types.Templates%Language.Fixpoint.Types.SubstitutionsLanguage.Fixpoint.Solver.StatsLanguage.Fixpoint.Types.Errors$Language.Fixpoint.Types.Environments Language.Fixpoint.Types.Theories#Language.Fixpoint.Types.ConstraintsLanguage.Fixpoint.Types.UtilsLanguage.Fixpoint.Types.Visitor%Language.Fixpoint.Solver.UniqifyKVars Language.Fixpoint.Solver.Rewrite%Language.Fixpoint.Solver.GradualSolveLanguage.Fixpoint.Smt.TypesLanguage.Fixpoint.Smt.Theories!Language.Fixpoint.Solver.SimplifyLanguage.Fixpoint.SortCheck!Language.Fixpoint.Types.Solutions$Language.Fixpoint.Solver.TrivialSort-Language.Fixpoint.Solver.EnvironmentReduction!Language.Fixpoint.Solver.PrettifyLanguage.Fixpoint.Smt.SerializeLanguage.Fixpoint.Smt.InterfaceLanguage.Fixpoint.Parse!Language.Fixpoint.Graph.ReducibleLanguage.Fixpoint.Horn.TypesLanguage.Fixpoint.Horn.ParseLanguage.Fixpoint.Horn.InfoLanguage.Fixpoint.Graph.TypesLanguage.Fixpoint.Graph.IndexedLanguage.Fixpoint.Graph.Deps!Language.Fixpoint.Graph.Partition"Language.Fixpoint.Utils.Statistics!Language.Fixpoint.Solver.Worklist!Language.Fixpoint.Solver.Sanitize Language.Fixpoint.Types.Graduals%Language.Fixpoint.Solver.UniqifyBinds!Language.Fixpoint.Solver.SolutionLanguage.Fixpoint.Solver.Monad(Language.Fixpoint.Solver.GradualSolution'Language.Fixpoint.Solver.Extensionality!Language.Fixpoint.Defunctionalize$Language.Fixpoint.Solver.InterpreterLanguage.Fixpoint.Solver.CommonLanguage.Fixpoint.Solver.PLE$Language.Fixpoint.Solver.Instantiate"Language.Fixpoint.Solver.EliminateLanguage.Fixpoint.Solver.SolveLanguage.Fixpoint.MinimizeLanguage.Fixpoint.Solver&Language.Fixpoint.Horn.TransformationsLanguage.Fixpoint.Horn.SolvePaths_liquid_fixpoint Data.Generics everywhereLanguage.Fixpoint.TypesLanguage.Fixpoint.GraphLiquid.Fixpoint.SortCheckunElabbase Data.String fromString&megaparsec-9.5.0-nV6NFlDOdsDHucVPlnquIText.Megaparsec.PosunPosmkPosPos sourceColumn sourceLine sourceName SourcePospretty-1.1.3.6Text.PrettyPrint.HughesPJDoc zeroWidthTextvcattextspace sizedTextsepsemirparen renderStylerender reduceDocrbrackrbracerationalquotes punctuateptextparensnest maybeQuotes maybeParensmaybeDoubleQuotes maybeBrackets maybeBraceslparenlbracklbraceisEmptyintegerinthsephcathang fullRenderfsepfloatfcatequalsempty doubleQuotesdoublecommacoloncharcatbracketsbraces<+>$+$$$#Text.PrettyPrint.Annotated.HughesPJStrPStrChr TextDetailsribbonsPerLinemode lineLengthStyle ZigZagModePageMode OneLineModeLeftModeModestyleShareMap toHashMap insertWith mergeKeysWithmap$fShowInternalKey$fShowShareMap$fShowReversibleMap$fEqInternalKey$fHashableInternalKeymakeZ3builtWithZ3AsALibraryfromText parenSeqskeykey2key3seqsbShowbFloat withProgress progressInit progressTick progressClose<->EqHashListNEMoodsOkLoudSadHappyAngryWary|-> firstMaybe asyncMapM traceShowhashMapToAscList findNearestargMinheadMb getUniqueInt editDistance moodColor wrapStars withColor colorStrLn colorPhaseLn startPhasedoneLine donePhase putBlankLnwraprepeatserrorP errorstarfst3snd3thd3secondMmlookup safeLookup mfromJustinsertsremovescountgroup groupBase groupListgroupMapallMapsetNubsortNub sortNubBynubOrd hashNubWith mFromList duplicatessafeZip safeZipWith safeFromListsafeHeadsafeLastsafeInit safeUncons safeUnsnocexecuteShellCommand applyNonNullarrowdcolon interspersetshow writeLoud ensurePathfMwhenMifM mapEitherisRightcomponentsWith topoSortWithsccsWithexTopocoalesce coalesceEdgesmapFstmapSndallCombinationspowerset=>><<=nubDifffold1MExtCgiFqOutHtmlAnnotVimHsHsBootLHsJsTsSpecBinSpecHqualsResultCstMkdnJsonSavedCacheDotPartAutoPredPAssDatBinFqSmt2HSmt2MinMinQualsMinKVarsgetFixpointPath getZ3LibPathwithExt extFileName tempDirectory extFileNameR isExtFile extModuleName copyFiles getFileInDirsisBinary$fEqExt$fOrdExt $fShowExt EliminateNoneSomeAllHorn ExistentialsScrapeNoHeadBoth SMTSolverZ3Z3memCvc4Mathsat RESTOrderingRESTKBORESTLPORESTRPORESTFuelConfigsrcFilecores minPartSize maxPartSizesolverlinear stringTheory defunctionallowHO allowHOqs eliminatescrape elimBound smtTimeout elimStats solverStatsmetadatastatspartssaveminimize minimizeQs minimizeKs minimalSoletaElimgradual ginteractiveautoKuts nonLinCutsnoslice rewriteAxiomspleWithUndecidedGuards interpreteroldPLE noIncrPlenoEnvironmentReductioninlineANFBindings checkCstrextensionalityrwTerminationCheckstdinjson noLazyPLEfuel restOrdering withPragmasdefaultMinPartSizedefaultMaxPartSizeuseElim defConfiggetOptsrestOC multicore queryFile$fReadRESTOrdering$fShowRESTOrdering$fDefaultRESTOrdering$fNFDataSMTSolver$fStoreSMTSolver$fShowSMTSolver$fDefaultSMTSolver $fShowScrape$fDefaultScrape$fNFDataScrape $fStoreScrape$fSerializeScrape$fShowEliminate$fDefaultEliminate$fNFDataEliminate$fStoreEliminate$fSerializeEliminate$fDefaultConfig $fEqConfig $fDataConfig $fShowConfig$fGenericConfig $fEqEliminate$fDataEliminate$fGenericEliminate $fEqScrape $fDataScrape$fGenericScrape $fEqSMTSolver$fDataSMTSolver$fGenericSMTSolver$fEqRESTOrdering$fDataRESTOrdering$fGenericRESTOrderingPTableptableDocTablePPrint pprintTidy pprintPrecTidyLossyFullFixpointtoFixsimplifytraceFixshowFixpprintshowpp showTabletracepp notracepp pprintKVsboxHSepboxDocdocBox$fFixpointDouble$fFixpointInteger $fFixpointInt$fFixpointBool$fFixpoint(,,) $fFixpoint(,) $fFixpoint[]$fFixpointMaybe $fFixpoint()$fFixpointHashSet $fPPrintText$fPPrintInteger $fPPrintInt $fPPrint() $fPPrintFloat $fPPrintBool $fPPrint(,)$fPPrint(,,,,) $fPPrint(,,,) $fPPrint(,,) $fPPrintChar$fPPrintHashMap$fPPrintHashSet $fPPrint[] $fPPrintMaybe$fPPrintEither $fPPrintDoc$fPPrintDocTable$fMonoidDocTable$fSemigroupDocTable$fEqTidy $fOrdTidyBranchBindValTrieNodeinsertfromListfoldfoldM $fPPrintTrie $fEqBranch $fShowBranch$fEqTrie $fShowTrieSrcSpanSSsp_startsp_stopLocatedLocloclocEval SourceNamesrcSpanpredPossuccPossafePos safeSourcePos ofSourcePos toSourcePos sourcePosEltssrcLine dummySpan panicSpanatLoclocAtdummyLocdummyPos$fBinarySourcePos $fBinaryPos$fFixpointSourcePos$fHashableSourcePos$fPPrintSourcePos$fSerializeSourcePos$fStoreSourcePos$fPrintfArgPos $fHashablePos$fSerializePos $fStorePos$fBinaryLocated$fIsStringLocated$fHashableLocated$fStoreLocated $fOrdLocated $fEqLocated$fPPrintLocated$fTraversableLocated$fFoldableLocated$fFunctorLocated$fFixpointLocated$fNFDataLocated$fHashableSrcSpan$fPPrintSrcSpan$fBinarySrcSpan$fSerializeSrcSpan$fStoreSrcSpan$fNFDataSrcSpan $fShowLocated$fLocSourcePos$fLoc() $fLocSrcSpan $fLocLocated $fEqSrcSpan $fOrdSrcSpan $fShowSrcSpan $fDataSrcSpan$fGenericSrcSpan $fDataLocated$fGenericLocatedSymbolicsymbolLocText LocSymbolSymbol mappendSymisDummy symbolText symbolStringsymbolSafeTextsymbolSafeStringisFixKeysymChars isPrefixOfSym isSuffixOfSymheadSymconsSym unconsSym lengthSymdropSymdropPrefixOfSym prefixOfSym suffixOfSym stripPrefix stripSuffix suffixSymbolvvisNontrivialVVvvCon dummySymbol testSymbol isTestSymbol litSymbol isLitSymbol unLitSymbol intSymbolappendSymbolText tempSymbol renameSymbol kArgSymbol existSymbol gradIntSymbol bindSymbol tempPrefix anfPrefix tidySymbol nonSymbol isNonSymbolsymbolicString symbolBuilder buildMany lambdaName lamArgSymbolisLamArgSymbol setToIntNamebitVecToIntName mapToIntName realToIntName toIntName tyCastName boolToIntName setApplyNamebitVecApplyName mapApplyName boolApplyName realApplyName intApplyName applyName coerceName preludeName dummyName boolConName funConName listConName listLConName tupConName setConName mapConNamevvName propConName strConName charConName intbv32Name intbv64Name bv32intName bv64intNamenilNameconsNamesizeName bitVecName mulFuncName divFuncNameisPrimprims$fFixpointText$fFixpointSymbol$fPPrintSymbol $fShowSymbol$fIsStringSymbol$fBinarySymbol $fStoreSymbol$fNFDataSymbol$fHashableSymbol$fHashableDescription$fUninternableSymbol$fInternedSymbol $fOrdSymbol $fEqSymbol$fSymbolicSymbol $fSymbolic[]$fSymbolicText$fSymbolicLocated$fEqDescription $fDataSymbol$fGenericSymbol$fGenericInternedText$fDataInternedTextTCArgsWithArgsNoArgsTCEmbSubDataDeclDDeclddTyConddVarsddCtorsDataCtorDCtordcNamedcFields DataFieldDFielddfNamedfSortSortFIntFRealFNumFFracFObjFVarFFuncFAbsFTCFAppFTycon mappendFTC intFTyCon boolFTyCon realFTyCon numFTyCon strFTyCon listFTyCon setFTyCon mapFTyConisListTCsizeBv fTyconSymbolsymbolNumInfoFTyCon symbolFTyconfAppfAppTCfTyconSelfSortunFAppunAbsfObj sortFTycon functionSortsortAbsmapFVar sortSymbols substSortmuSort isFirstOrder isNumericisRealisStringmkFFuncbkFFuncbkAbs isPolyInstmkPolyboolSortcharSortstrSortintSortrealSortfuncSortsetSort bitVecSortsizedBitVecSortmapSort fTyconSort basicSorts mkSortSubst sortSubst tceInsertWith tceInsert tceLookuptceMap tceFromList tceToList tceMember$fNFDataTCInfo$fBinaryTCInfo $fStoreTCInfo$fMonoidTCInfo$fSemigroupTCInfo$fNFDataFTycon$fBinaryFTycon $fStoreFTycon$fPPrintFTycon$fFixpointFTycon $fLocFTycon$fHashableFTycon $fEqFTycon$fSymbolicFTycon $fMonoidSort$fSemigroupSort $fNFDataSort $fBinarySort $fStoreSort$fFixpointSort$fHashableSort $fPPrintSort$fNFDataDataField$fStoreDataField$fPPrintDataField$fFixpointDataField$fSymbolicDataField$fNFDataDataCtor$fStoreDataCtor$fPPrintDataCtor$fFixpointDataCtor$fSymbolicDataCtor$fNFDataDataDecl$fStoreDataDecl$fPPrintDataDecl$fFixpointDataDecl$fSymbolicDataDecl $fLocDataDecl $fNFDataSub $fStoreSub$fPPrintTCArgs$fMonoidTCArgs$fSemigroupTCArgs$fBinaryTCArgs$fHashableTCArgs$fNFDataTCArgs $fStoreTCArgs $fMonoidTCEmb$fSemigroupTCEmb $fPPrintTCEmb$fHashableTCEmb $fNFDataTCEmb $fBinaryTCEmb $fEqTCEmb $fShowTCEmb $fDataTCEmb$fGenericTCEmb $fEqTCArgs $fOrdTCArgs $fShowTCArgs $fDataTCArgs$fGenericTCArgs $fGenericSub $fEqDataDecl $fOrdDataDecl$fShowDataDecl$fDataDataDecl$fGenericDataDecl $fEqDataCtor $fOrdDataCtor$fShowDataCtor$fDataDataCtor$fGenericDataCtor $fEqDataField$fOrdDataField$fShowDataField$fDataDataField$fGenericDataField$fEqSort $fOrdSort $fShowSort $fDataSort $fGenericSort $fOrdFTycon $fShowFTycon $fDataFTycon$fGenericFTycon $fEqTCInfo $fOrdTCInfo $fShowTCInfo $fDataTCInfo$fGenericTCInfoReftableisTautoppTytopbotmeettoReftofReftparamsSubablesymssubstasubstfsubstsubst1isFalse Predicateprop Expressionexpr SortedReftRRsr_sortsr_reftReftGradInfogsrcgusedExprESymEConEVarEAppENegEBinEIteECstELamETAppETAbsPAndPOrPNotPImpPIffPAtomPKVarPAllPExistPGradECoercBopPlusMinusTimesDivModRTimesRDivBrelEqNeGtGeLtLeUeqUneConstantIRLSymConstSLKVSubKVSksuVVksuSortksuKVarksuSubstSubstSuKVarKVkv HasGradual isGradualgVarsungradERDivEDivERTimesETimesEEqEBotPFalsePTopPTrue reftConjuncts concConjunctsintKvaronEverySubexprexprSymbolsSetsubstSortInExpr exprKVars srcGradInfomkEAppeApps splitEAppsplitEAppThroughECstdropECst splitPAndeAppCeCst debruijnIndexsortedReftSymbolselit isContraPred isTautoPred pprintRefteVarePropisSingletonExprconjpAnd pAndNoDeduppOr&.&|.|pItepExistmkPropisSingletonReftexprReft notExprReft uexprReftpropReftpredReftreft mapPredReftisFunctionSortedReft isNonTrivialreftPredreftBindpGAndspGAnd symbolReft usymbolReftvv_trueSortedRefttrueReft falseReft flattenRefas conjuncts $fFixpointDoc$fBinaryHashMap$fBinaryHashSet $fPPrintKVar$fFixpointKVar$fHashableKVar $fShowKVar $fBinaryKVar $fStoreKVar $fNFDataKVar$fPPrintSymConst$fFixpointSymConst$fSymbolicSymConst$fHashableSymConst$fBinarySymConst$fStoreSymConst$fNFDataSymConst$fPPrintConstant$fFixpointConstant$fHashableConstant$fBinaryConstant$fStoreConstant$fNFDataConstant $fPPrintBrel$fFixpointBrel$fHashableBrel $fBinaryBrel $fStoreBrel $fNFDataBrel $fPPrintBop $fFixpointBop $fHashableBop $fBinaryBop $fStoreBop $fNFDataBop$fHashableGradInfo$fBinaryGradInfo$fStoreGradInfo$fNFDataGradInfo $fPPrintExpr$fFixpointExpr $fPPrintSubst$fFixpointSubst $fShowSubst$fHashableExpr$fHashableSubst$fHasGradualExpr $fBinaryExpr $fBinarySubst $fStoreExpr $fStoreSubst $fNFDataExpr $fNFDataSubst $fPPrintKVSub$fHashableReft$fHasGradualReft $fBinaryReft $fStoreReft $fNFDataReft$fHashableSortedReft$fHasGradualSortedReft$fStoreSortedReft$fNFDataSortedReft$fExpressionLocated$fExpressionInt$fExpressionInteger$fExpressionText$fExpressionSymbol$fExpressionExpr$fExpressionReft$fExpressionSortedReft$fPredicateBool$fPredicateExpr$fPredicateSymbol$fFalseableReft$fFalseableExpr$fSubableLocated$fEqSortedReft$fOrdSortedReft$fDataSortedReft$fGenericSortedReft$fEqReft $fOrdReft $fDataReft $fGenericReft $fEqKVSub $fDataKVSub$fGenericKVSub $fShowKVSub$fEqExpr $fShowExpr $fOrdExpr $fDataExpr $fGenericExpr $fEqSubst $fDataSubst $fOrdSubst$fGenericSubst $fEqGradInfo $fOrdGradInfo$fShowGradInfo$fDataGradInfo$fGenericGradInfo$fEqBop$fOrdBop $fShowBop $fDataBop $fGenericBop$fEqBrel $fOrdBrel $fShowBrel $fDataBrel $fGenericBrel $fEqConstant $fOrdConstant$fShowConstant$fDataConstant$fGenericConstant $fEqSymConst $fOrdSymConst$fShowSymConst$fDataSymConst$fGenericSymConst$fEqKVar $fOrdKVar $fDataKVar $fGenericKVar$fIsStringKVarTrigger NoTrigger LeftHandSide TriggeredTR noTriggerdefaultTrigger makeTriggers$fNFDataTrigger$fStoreTrigger$fPPrintTrigger$fNFDataTriggered$fStoreTriggered$fPPrintTriggered $fEqTriggered$fShowTriggered$fFunctorTriggered$fGenericTriggered $fEqTrigger $fShowTrigger$fGenericTriggerfilterUnMatched TemplatesmatchesTemplates makeTemplatesisEmptyTemplatesisAnyTemplatesanything$fPPrintTemplates$fMonoidTemplates$fSemigroupTemplates$fHasTemplatesReft$fHasTemplatesExpr$fShowTemplates filterSubstcatSubstmkSubst isEmptySubsttargetSubstSyms subst1Except substfExcept substExcept$fExpression(,)$fShowSortedReft $fShowReft$fFixpointSortedReft$fFixpointReft$fPPrintSortedReft $fPPrintReft$fReftableSortedReft$fReftableReft $fReftable()$fSubableSortedReft $fSubableReft$fMonoidSortedReft$fSemigroupSortedReft $fMonoidReft$fSemigroupReft $fMonoidExpr$fSemigroupExpr $fSubableExpr$fSubableSymbol$fSubableHashMap$fSubableMaybe $fSubable[] $fSubable(,) $fSubable() $fMonoidSubst$fSemigroupSubstStatsnumCstrnumIternumBrktnumChcknumValdchecked totalWork $fMonoidStats$fFromJSONStats $fToJSONStats$fSemigroupStats $fPTableStats$fSerializeStats $fStoreStats $fNFDataStats $fDataStats $fShowStats$fGenericStats $fEqStats FixResultCrashUnsafeSafeError1errLocerrMsgErrorerrscatError catErrorserrpanicdiedieAtexit resultDoc colorResult resultExiterrBadDataDeclerrFreeVarInQualerrFreeVarInConstrainterrIllScopedKVar$fSerializeDoc$fSerializeTextDetails$fSerializeDoc0$fSerializeAnnotDetails$fFixpointError1$fPPrintError1 $fOrdError1$fSerializeError1$fExceptionError $fPPrintError$fSerializeError$fPPrintFixResult$fToJSONFixResult$fMonoidFixResult$fSemigroupFixResult $fEqFixResult$fNFDataFixResult$fStoreFixResult$fSerializeFixResult$fDataFixResult$fFoldableFixResult$fFunctorFixResult$fTraversableFixResult$fShowFixResult$fGenericFixResult $fEqError $fOrdError $fShowError$fGenericError $fEqError1 $fShowError1$fGenericError1$fGenericAnnotDetailsPackspackmSESearchFoundAltsEBindEnvBindEnvbeBindsSEnvSEseBindsIBindEnvBindMapBindIdsplitByQuantifiers toListSEnv fromListSEnv fromMapSEnvmapSEnvmapMSEnvmapSEnvWithKey deleteSEnv insertSEnv lookupSEnv emptySEnv memberSEnvintersectWithSEnvdifferenceSEnv filterSEnv unionSEnv unionSEnv'lookupSEnvWithDistance emptyIBindEnvdeleteIBindEnvmemberIBindEnvinsertsIBindEnv elemsIBindEnvfromListIBindEnv insertBindEnvfromListBindEnv emptyBindEnv filterBindEnvbindEnvFromList elemsBindEnv bindEnvToList mapBindEnvmapWithKeyMBindEnv lookupBindEnvfilterIBindEnv unionIBindEnvunionsIBindEnvintersectionIBindEnv nullIBindEnv diffIBindEnv adjustBindEnv deleteBindEnvenvCsgetPackmakePack$fStoreIBindEnv$fNFDataIBindEnv$fFixpointIBindEnv$fMonoidIBindEnv$fSemigroupIBindEnv$fPPrintIBindEnv $fStoreSEnv $fNFDataSEnv $fMonoidSEnv$fSemigroupSEnv $fShowSEnv$fFixpointSEnv $fFunctorSEnv $fPPrintSEnv$fPPrintSizedEnv$fStoreSizedEnv$fNFDataSizedEnv$fMonoidSizedEnv$fSemigroupSizedEnv$fFixpointSizedEnv$fFixpointEBindEnv $fMonoidPacks$fSemigroupPacks $fPPrintPacks$fFixpointPacks $fStorePacks $fNFDataPacks $fEqPacks $fShowPacks$fGenericPacks $fEqSizedEnv$fShowSizedEnv$fFunctorSizedEnv$fFoldableSizedEnv$fGenericSizedEnv$fTraversableSizedEnv$fEqSEnv $fDataSEnv $fGenericSEnv$fFoldableSEnv$fTraversableSEnv $fEqIBindEnv$fDataIBindEnv$fShowIBindEnv$fGenericIBindEnvSmtSortSIntSBoolSRealSStringSSetSMapSBitVecSVarSDataSemUninterpCtorTestFieldTheory TheorySymbolThytsSymtsRawtsSorttsInterpSymEnvseSortseTheoryseDataseLitsseApplsRawsymEnv symEnvTheory symEnvSort insertSymEnv insertsSymEnv symbolAtNamesymbolAtSmtName isIntSmtSort sortSmtSort $fStoreSem $fPPrintSem $fNFDataSem$fPPrintTheorySymbol$fFixpointTheorySymbol$fStoreTheorySymbol$fNFDataTheorySymbol$fPPrintSmtSort$fStoreSmtSort$fNFDataSmtSort$fHashableSmtSort$fMonoidSymEnv$fSemigroupSymEnv $fStoreSymEnv$fNFDataSymEnv $fEqSymEnv $fShowSymEnv $fDataSymEnv$fGenericSymEnv $fEqSmtSort $fOrdSmtSort $fShowSmtSort $fDataSmtSort$fGenericSmtSort$fEqTheorySymbol$fOrdTheorySymbol$fShowTheorySymbol$fDataTheorySymbol$fGenericTheorySymbol$fEqSem$fOrdSem $fShowSem $fDataSem $fGenericSemRewriteSMeasuresmNamesmDCsmArgssmBody AutoRewritearArgsarLHSarRHSEquationEqueqNameeqArgseqBodyeqSorteqRecAxiomEnvAEnvaenvEqs aenvSimpl aenvExpand aenvAutoRWSolverGInfoFIcmwsbsebindsgLitsdLitskutsqualsbindInfoddeclshoInfoassertsaeHOInfoHOIhoBindshoQualsSInfoFInfo FInfoWithOptsFIOfioFIfioOptsKutsKSksVars QualPatternPatNone PatPrefix PatSuffixPatExact QualParamQPqpSymqpPatqpSort QualifierQqNameqParamsqBodyqPos resStatus resSolutionresNonCutsSolution gresSolution FixSolution GFixSolutionTaggedCsenv updateSEnvsidstagsinfoclhscrhsSimpC_cenv_crhs_cidcbind_ctag_cinfoSubCslhssrhsSubcIdGWInfogsymgsortgexprginfoWfCGWfCwenvwrftwinfowexprwlocTaggwInfo updateWfCExprisGWfc strengthenHypstrengthenBindssubcId toGFixSolunsafesafeisSafeisUnsafewfCmkSubCsubCshiftVVaddIdstrueQual qualifiermkQ qualBinds remakeQualmkQualgSorts substVarssortVarsksMemberfi allowHOquals toFixpoint writeFInfo convertFormat sinfoToFInfo saveQuerydedupAutoRewrites mkEquation $fNFDataWfC $fStoreWfC $fFixpointWfC $fPPrintWfC $fShowWfC$fHasGradualWfC$fNFDataGWInfo $fStoreGWInfo $fNFDataSubC $fStoreSubC $fPPrintSubC $fShowSubC$fFixpointFixResult $fNFDataSimpC $fStoreSimpC $fPPrintSimpC $fShowSimpC $fLocSimpC$fFixpointSimpC$fFixpointSubC$fTaggedCSubCa$fTaggedCSimpCa$fNFDataGFixSol$fStoreGFixSol $fShowGFixSol$fPPrintGFixSol$fNFDataResult$fMonoidResult$fSemigroupResult$fToJSONResult$fPPrintQualPattern$fBinaryQualPattern$fHashableQualPattern$fNFDataQualPattern$fStoreQualPattern$fPPrintQualParam$fFixpointQualParam$fBinaryQualParam$fHashableQualParam$fNFDataQualParam$fStoreQualParam$fPPrintQualifier$fFixpointQualifier$fSubableQualifier$fLocQualifier$fBinaryQualifier$fHashableQualifier$fNFDataQualifier$fStoreQualifier $fMonoidKuts$fSemigroupKuts$fFixpointKuts $fNFDataKuts $fStoreKuts$fMonoidHOInfo$fSemigroupHOInfo$fNFDataHOInfo $fStoreHOInfo$fFixpointEquation$fPPrintEquation$fSubableEquation$fNFDataEquation$fStoreEquation$fHashableEquation$fFixpointHashMap$fHashableAutoRewrite$fNFDataAutoRewrite$fStoreAutoRewrite$fPPrintRewrite$fFixpointRewrite$fNFDataRewrite$fStoreRewrite$fFixpointAxiomEnv$fPPrintAxiomEnv$fMonoidAxiomEnv$fSemigroupAxiomEnv$fNFDataAxiomEnv$fStoreAxiomEnv $fMonoidGInfo$fSemigroupGInfo$fHasGradualGInfo $fNFDataGInfo $fStoreGInfo $fPTableGInfo $fEqGInfo $fShowGInfo$fFunctorGInfo$fGenericGInfo $fEqAxiomEnv$fShowAxiomEnv$fGenericAxiomEnv $fDataRewrite $fEqRewrite $fOrdRewrite $fShowRewrite$fGenericRewrite$fEqAutoRewrite$fOrdAutoRewrite$fShowAutoRewrite$fGenericAutoRewrite$fDataEquation $fEqEquation $fOrdEquation$fShowEquation$fGenericEquation $fEqHOInfo $fShowHOInfo$fGenericHOInfo$fEqKuts $fShowKuts $fGenericKuts $fEqQualifier$fOrdQualifier$fShowQualifier$fDataQualifier$fGenericQualifier $fEqQualParam$fOrdQualParam$fShowQualParam$fDataQualParam$fGenericQualParam$fEqQualPattern$fOrdQualPattern$fShowQualPattern$fDataQualPattern$fGenericQualPattern$fGenericResult $fShowResult$fFunctorResult$fGenericGFixSol$fSemigroupGFixSol$fMonoidGFixSol$fFunctorGFixSol$fGenericSimpC$fFunctorSimpC$fEqSubC $fGenericSubC $fFunctorSubC $fEqGWInfo$fGenericGWInfo$fEqWfC $fGenericWfC $fFunctorWfC kvarDomain reftFreeVarssortedReftConcKVars checkRegularorderDeclarations SymConsts symConstsCoSub VisitablevisitVisitorctxExprtxExpraccExprdefaultVisitortransmapKVars mapKVars' mapGVars'mapExpr mapExprOnExprmapMExpr mapKVarSubstssizelamSizeeapps kvarsExprenvKVars envKVarsNrhsKVarsisKvarCisConcCisConc stripCasts applyCoSubfoldSort foldDataDecl$fVisitableRewrite$fVisitableEquation$fVisitableAxiomEnv$fVisitableGInfo$fVisitableSubC$fVisitableSimpC$fVisitableSizedEnv$fVisitable(,,)$fVisitableSortedReft$fVisitableReft$fVisitableExpr $fMonoidMInt$fSemigroupMInt$fSymConstsExpr$fSymConstsReft$fSymConstsSortedReft$fSymConstsSimpC$fSymConstsSubC$fSymConstsSizedEnv$fSymConstsGInfo$fSymConstsRewrite$fSymConstsEquation$fSymConstsAxiomEnv $fSymConsts[] wfcUniqifyOCType RewriteArgsRWArgs isRWValidrwTerminationOptsRWTerminationOptsRWTerminationCheckEnabledRWTerminationCheckDisabled TermOriginPLERWSubExprordConstraintsconvertpassesTerminationCheck getRewritesubExprsunify$fPPrintTermOrigin $fEqOCType $fShowOCType$fGenericOCType$fHashableOCType$fShowTermOrigin$fEqTermOrigin solveGradualSMTLIB2smt2ContextCtx ctxSolverctxClosectxLog ctxVerbose ctxSymEnvResponseSatUnsatUnknownValuesCommandPushPopExitSetMbqiCheckSatDeclDataDeclareDefine DefineFuncAssertAssertAxDistinctGetValueCManyrunSmt2$fPPrintCommand $fEqResponse$fShowResponse $fEqCommand $fShowCommandsetEmptysetEmpsetCapsetSubsetAddsetMemsetComsetCupsetDifsetSngmapSelmapStomapCupmapDef smt2Symbolsmt2App isSmt2Apppreamble theorySymbols maxLamArg axiomLiteralsdataDeclSymbols$fSMTLIB2SmtSortapplyBooleanFoldingapplyConstantFolding isSetPredapplySetFoldingTVSubstEnv Elaborate elaborateisMono elabNumericelabExpr elabApplysortExpr checkSortExpr mkSearchEnvrunCM0checkSortedReftcheckSortedReftFull checkSortFull checkSortedpruneUnsortedReft defuncEApptoIntunElabSortedReftunApplySortedReftunApply unApplyAt applySortsexprSort exprSortMaybeunifyTo1 unifySorts unifyFastunifysapply$fElaborateSimpC$fElaborateSizedEnv$fElaborateSortedReft $fElaborate[]$fElaborate(,)$fElaborateExpr$fElaborateEquation$fElaborateRewrite$fElaborateAxiomEnv$fElaborateSort$fElaborateMaybe$fElaborateTriggered$fElaborateGInfo$fExceptionChError $fShowChError$fCheckableSortedReft$fCheckableExpr$fMonoidTVSubst$fSemigroupTVSubst $fShowTVSubstCMapIndexFastIdxbindExprkvUsekvDefenvBindsenvTxenvSortsBindPredBPbpConcbpKVarBIndexRootCstrKIndexkiBIndexkiPoskiKVarEQualEQLeqQualeqPred_eqArgsCandCubecuBindscuSubstcuIdcuTagHypSolsEnvgMapsHypsScpsEbdsxEnvEbindSolEbDefEbSolEbIncrGBindQBind GSolutionSolutionupdate emptyGMapupdateGMapWithKeyqbqbExprsqbToGbgbToQbsgbEqualsequalsGb gbFilterMqbFilter updateEbind updateGMapresult resultGradualqbPreds lookupQBindglookuplookup trueEqualeQual$fPPrintEbindSol $fShowCube $fPPrintCube $fPPrintSol $fFunctorSol $fMonoidSol$fSemigroupSol $fNFDataEQual $fPPrintEQual $fLocEQual $fNFDataGBind $fPPrintQBind $fNFDataQBind$fPPrintKIndex$fHashableKIndex$fPPrintBIndex$fHashableBIndex$fPPrintBindPred$fShowBindPred $fEqBIndex $fOrdBIndex $fShowBIndex$fGenericBIndex $fEqKIndex $fOrdKIndex $fShowKIndex$fGenericKIndex $fShowQBind $fDataQBind$fGenericQBind $fEqQBind $fShowGBind $fDataGBind$fGenericGBind $fEqEQual $fShowEQual $fDataEQual$fGenericEQual $fGenericSol $fGenericCube $fNFDataCube$fShowEbindSol$fGenericEbindSol$fNFDataEbindSol $fNFDataSol nontrivsorts $fHashableNTV$fEqNTV$fOrdNTV $fShowNTV $fGenericNTVreduceEnvironmentssimplifyBindingsmergeDuplicatedBindingsundoANFSimplifyingWithundoANF undoANFAndVVinlineInSortedReft inlineInExprsimplifyBooleanReftsdropLikelyIrrelevantBindingssavePrettifiedQuery smt2SortMono$fSMTLIB2Triggered$fSMTLIB2Command $fSMTLIB2Expr $fSMTLIB2Brel $fSMTLIB2Bop$fSMTLIB2Constant$fSMTLIB2SymConst$fSMTLIB2Located $fSMTLIB2Int$fSMTLIB2Symbol $fSMTLIB2(,)checkValidWithContext checkValid checkValid' checkValidscommand smtSetMbqi makeContextmakeContextWithSEnvmakeContextNoLogcleanupContextsmtPushsmtPopsmtDeclssmtDecl smtFuncDecl smtCheckSat smtAssert smtDefineFuncsmtAssertAxiom smtDistinct smtCheckUnsat smtBracketAt smtBracket Inputablerrrr'FixityFInfixFPrefixFPostfixfpredfnamefop2fassocfop1Assoc AssocNone AssocLeft AssocRight LayoutStackEmptyResetAtAfterPState fixityTable fixityOpsempListsingListsupply layoutStack numTyConsParser setLayout popLayoutspaceslexeme locLexemelocated indentedBlock indentedLineindentedOrExplicitBlock explicitBlockdotblockexplicitCommaBlockreserved locReserved reservedOpangles stringLiterallocStringLiteralnatural locNaturalcondIdR isNotReservedisSmallupperIdPlowerIdPsymbolP locLowerIdP locUpperIdP locSymbolP constantPexpr0PexprP addOperatorP addNumTyCon infixSymbolPlocInfixSymbolPfunAppPsortPpredPrefaPrefBindPbindPrefPrefDefP dataFieldP dataCtorP dataDeclP qualifierPpairPdefinePmatchP remainderP initPStatedoParse' parseTest' parseFromFileparseFromStdIn freshIntP $fInputable[]$fInputableCommand$fInputableFInfoWithOpts$fInputableGInfo$fInputable(,)$fInputableFixResult$fInputableExpr$fInputableConstant$fInputableSymbol $fShowDef $fGenericDef$fShowLayoutStack isReducibleNoTagTagQueryTagVarQueryqQualsqVarsqCstrqConqDisqEqnsqMatsqDataCAndAnybSymbSortbPredbMetaVarHVarhvNamehvArgshvMetacLabelokCstr $fPPrintVar $fShowVar $fPPrintPred $fShowPred $fSubablePred $fMonoidPred$fSemigroupPred $fPPrintBind $fShowBind $fSubableBind $fPPrintCstr $fShowCstr $fPPrintQuery $fToJSONTag $fPPrintTag $fFixpointTag$fLocTag $fNFDataTag $fDataTag $fGenericTag $fShowTag $fDataQuery$fGenericQuery$fFunctorQuery $fDataCstr $fGenericCstr $fFunctorCstr$fEqCstr $fDataBind $fGenericBind $fFunctorBind$fEqBind $fDataPred $fGenericPred$fEqPred$fEqVar$fOrdVar $fDataVar $fGenericVar $fFunctorVarhornPhCstrPhPredP hQualifierPhVarP$fFunctorHThing hornFInfo$fGenericKVInfo$fFunctorKVInfo SolverInfoSIsiSolsiQuerysiDepssiVarsRankrSccrIccrTagCDepsCDscSucccPrevcRankcNumSccCGraphgEdgesgRanksgSuccgSccsSliceslKVarCsslConcCsslEdgesDepEdgeKVReadKVCompsCompsCEdgeKVGraphkvgEdgesCVertexDKVarEBind writeGraph writeEdges isRealEdge lookupCMap$fHashableCVertex$fPPrintCVertex$fPPrintKVGraph $fPPrintRank$fEqRank $fShowRank $fEqSlice $fShowSlice $fEqCVertex $fOrdCVertex $fShowCVertex$fGenericCVertexIKVGraphigSuccigPredaddLinksdelNodes edgesIkvg ikvgEdgesgetSuccsgetPreds$fShowIKVGraphElimsDepsdepCuts depNonCutssliceisTarget decomposekvEdgeselimDepselimVarsgraphStatistics $fMonoidElims$fSemigroupElims $fPPrintElims $fShowElimsMCInfomcCores mcMinPartSize mcMaxPartSizeCPartpwspcmmcInfo partition partition' partitionNdumpPartitions $fMonoidCPart$fSemigroupCPart $fShowMCInfo statistics $fPPrintStatsWorklistwRanksinitunsatCandidatespoppush $fOrdWorkItem$fPPrintWorkItem$fPTableWorklist$fPPrintWorklist $fEqWorkItem$fShowWorkItemsanitizedropDeadSubsts symbolEnvGradualgsubstGSol makeSolutionsuniquify $fShowGSol $fMonoidGSol$fSemigroupGSol$fUniqueannExpr$fUniqueannReft$fUniqueannSortedReft$fUniqueannInt$fUniqueannIBindEnv$fUniqueaSimpC$fUniqueannHashMap$fGradualGInfo$fGradualHashMap$fGradualSizedEnv$fGradualSimpC$fGradualSortedReft $fGradualReft $fGradualExpr renameAll $fHashableRef $fNFDataRef$fEqRef $fGenericReflhsPred nonCutsResult$fLocCombinedEnv $fMonoidKInfo$fSemigroupKInfo $fEqKInfo $fOrdKInfo $fShowKInfo SolverStatessCtxssBindsssStatsSolveM runSolverMgetBindssendConcreteBindingsToSMTfilterRequired filterValidfilterValidGradual smtEnablembqicheckSattickIterexpand$fExtendaSimpC$fExtendannInteger$fExtendann(,)$fExtendannHashMap$fExtendaGInfo$fEqPosDefuncdefuncdefunctionalize defuncAny$fDefuncHashMap $fDefunc[] $fDefuncSort$fDefuncSizedEnv $fDefuncSEnv $fDefuncExpr $fDefuncReft $fDefunc(,) $fDefunc(,)0$fDefuncSortedReft $fDefuncWfC $fDefuncSimpC$fDefuncTriggered $fDefuncGInfo Simplifiable KnowledgeKNknSimsknAmsknLams knSummaryknDCsknAllDCsknSelsknConstsICtxicCandsicEqualsicSolvedicSimplicSubcIdinstInterpreter interpret$fSimplifiableExpr$fNormalizableEquation$fNormalizableRewrite$fNormalizableAxiomEnv$fNormalizableGInfoaskSMTtoSMT knContextknPreds knDataCtors knAutoRWsknRWTerminationOpts FuelCountFCfcMapfcMaxicAssmsicANFs instantiate$fEqIsUserDataSMeasure$fShowIsUserDataSMeasure$fShowFinalExpand $fEqEvalType$fShowFuelCount $fPPrintRecur $fEqRecur $fShowRecur solverInfosolveminQueryminQualsminKvarssolveFQresultExitCode simplifyFInfo parseFInfoflattensolveEbselimPis cstrToExpruniqelim$fVisitableCstr$fVisitablePred $fFlatten[] $fFlattenExpr $fFlatten[]0 $fFlattenPred $fFlatten[]1 $fFlattenCstr solveHorn ReversibleMap reverseLookup reversedMap InternalKey unsharedMapshareMapversiongetDataFileName getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirGHC.Base<> _example0ColumnLineSafeText$ textSymbol alphaChars Falseable everywhereOnAparensIf exprSymbols wiredInEnv funcSortsghc-prim GHC.TypesInt$++$ isRegularmapSortOnlyOnce newTopBindsubseltsetselfSortfldSorttheorifyCheckM checkExprelabeCstAtomBoolcheckSymcheckItecheckCst checkApp'checkNeg checkPredcheckRel unifyExpr checkFunSort errElabExprsMap NonTrivSorts reducedEnvoriginalConstraint constraintIddropIrrelevantBindingsreduceWFConstraintEnvironmentsrelatedKVarBindsaxiomEnvSymbolsreachableSymbolssubstBindingsSimplifyingWith substBindingsundoANFOnlyModifiedrelatedSymbolseraseUnusedBindingsshortenVarNamesproposeRenamingstoPrefixSuffixMaptoSymMap padDataDeclsmt2CastsymKinddistinctLiteralsDefOpTablepopLayoutStackmodifyLayoutStack resetLayoutguardIndentLevel guardLayoutstrictGuardLayoutsymlocSym lhLineCommentlhBlockComment identLetteropLetterupperIdRlowerIdRsymbolR symconstP exprCastPexpr1PflattenOpTable/parser-combinators-1.3.0-88KGhmkz8neAczPN45sOphControl.Monad.Combinators.ExprmakeExprParsermkInfixOperator addOperatormakePrecinsertOperator initOpTablebopstuplePlitPlamP funcSortPsortP'pred0PtruePfalsePpredsPpredrPbrelP autoRewriteP fixResultPHThingsymSortPKVEnvgoS scrapeCstr stNumKVCuts stNumKVNonLin stNumKVTotal stIsReducible stSetKVNonLincGraph graphRankskvSucc graphElimsccElims boundElimscGraphCEcSuccMinRanks PartitionCtor cpartSize cpartToFinfo finfoToCpartpartitionByConstraintswiCIdwiTimewiRankWorkSetaddPendssAddsKvDom safeKvarEnv_dropAdtMeasures addLiterals eliminateEta_banIllScopedKvarsrestrictKVarDomain restrictWfbanConstraintFreeVarsbanIrregularDatabanQualifFreeVars banMixedRhsdropFuncSortedShadowedBinders sanitizeWfC _nonDerivedLH dropBindersreplaceDeadKvars==>UniqueMexpandWF RenameMap GHC.MaybeNothingIdMapRBRIdropUnusedBinds renameVarsKInfoceBindingsInSmtQCluster bareCubePredcubePred elabExist cubePredExc substElim ebindInfodfHOdfLamsdfRedexdfBinds normalizeLamsfreshSym NormalizableCTrieInstResInstEnvinstEnvmkCTriepleTrieple1resSInfoupdCtx unfoldExprsubstEqDiffIsUserDataSMeasureevPendingUnfoldingsevNewEqualities evSMTCache withAssms evalCandsLoopevalOneevalevalELamevalRESTevalAppevalItenoUserDataMeasureEqsmkCoSub!partitionUserDataConstructorTests%partitionUserDataConstructorSelectors normalizeBodyuseFuel useFuelCount checkFuelloopTloopB<|>assertSelectorsRecurUnfoldincrInstantiate' instantiate'evaluateevalArgsidevalOkinitEqualities~>withProgressFI tidyResultrefineCminimizeResultrhsPred_iMergePartitionsErrorMap solveSeqWith solveParWithinParallelUsing solveNative solveNative'Flatten Data.Foldableand piDefConstrsolPispokecsplitdefselimKs'rewriteWithEqualitiesscopesol1doelim boundKvarsisNNFhornify