h*      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                   2.7.2 Safe-Inferred")1hasmtlibLift a .hasmtlibThe true constant.  =  hasmtlibThe false constant.  =  hasmtlibLogical conjunction.hasmtlib#Logical disjunction (inclusive or).hasmtlibLogical implication.hasmtlib(Logical implication with arrow reversed. $forall x y. (x ==> y) === (y <== x) hasmtlibLogical equivalence. hasmtlibLogical negation. hasmtlib Exclusive-or. hasmtlib*The logical conjunction of several values. hasmtlib*The logical disjunction of several values. hasmtlib2The negated logical conjunction of several values.   =   .  hasmtlib2The negated logical disjunction of several values.  =   .  hasmtlibThe logical conjunction of the mapping of a function over several values.hasmtlibThe logical disjunction of the mapping of a function over several values.hasmtlibDefined bitwise    32004 4 Safe-Inferred")1 Safe-Inferred ")1QhasmtlibA map-like array with a default constant value and partially overwritten values.hasmtlibClass that allows access to a map-like array where any value is either the default value or an overwritten values. Every index has a value by default. Values at indices can be overwritten manually.'Based on McCarthy`s basic array theory.)Therefore the following axioms must hold: +forall A i x: arrSelect (arrStore i x) == xforall A i j x: i /= j ==> (arrSelect (arrStore i x) j === arrSelect A j)hasmtlib Construct an  via it's const value.hasmtlibView the const value of the . hasmtlibSelect a value from the .Returns the specific value for given key if there is one. Returns the const value otherwise.!hasmtlib,Store a specific value at a given key in an ."hasmtlib Wrapper for  which hides the .  !")*  !")* Safe-Inferred "()1 ,hasmtlibLength-indexed bitvector ( ) carrying a phantom type-level 4.Most significant bit is first (index 0) for unsigned bitvectors. Signed bitvectors have their sign bit first (index 0) and their most significant bit second (index 1)./hasmtlibCompute singleton 1 from it's promoted type 4.1hasmtlibSingleton for 4.4hasmtlib?Type of Bitvector encoding - used as promoted type (data-kind).7hasmtlib Wrapper for 0 which takes a .8hasmtlib Wrapper for 0 which takes a  and some ballast. This is helpful for singing on values of type , where the ballst is a .9hasmtlibConvert , with any encoding 4 to 5.:hasmtlibConvert , with any encoding 4 to 6.;hasmtlib-A Lens on the sign-bit of a signed bitvector.<hasmtlib Concatenation of two bitvectors.=hasmtlib%Constructing a bitvector from a list.>hasmtlib:Constructing a bitvector from a list with length given as .456123/078,-.<9:=>;456123/078,-.<9:=>; Safe-Inferred")1ShasmtlibOptions for SMT-Solvers.Thasmtlib$Print "success" after each operationUhasmtlib>Produce a satisfying assignment after each successful checkSatVhasmtlibIncremental solvingWhasmtlib=Custom options. First String is the option, second its value.SWVUTSWVUT Safe-Inferred  ")1 \hasmtlib-An existential wrapper that hides some known g.]hasmtlibCompute singleton _ from it's promoted type g._hasmtlibSingleton for g.fhasmtlib0Injective type-family that computes the Haskell  of an g.ghasmtlib5Sorts in SMTLib2 - used as promoted type (data-kind).hhasmtlib Sort of Boolihasmtlib Sort of Intjhasmtlib Sort of Realkhasmtlib5Sort of BitVec with type of encoding enc and length nlhasmtlib)Sort of Array with indices k and values vmhasmtlibSort of Stringnhasmtlib Wrapper for ^ which takes a .ghijklmf_`abcde]^n\ghijklmf_`abcde]^n\ Safe-Inferred")1 zhasmtlibA wrapper for values of g6s. This wraps a Haskell-value into the SMT-Context.hasmtlib-Unwraps a Haskell-value from the SMT-Context-z.hasmtlib+Wraps a Haskell-value into the SMT-Context-z. z{|}~ z{|}~ Safe-Inferred "()1=7T(hasmtlib? y assert $ x === min' 42 100 hasmtlib)Symbolically test two values on equality.&A generic default implementation with  is possible.Example x <- var @RealType y <- var assert $ y === x && not (y /== x) && x === 42 hasmtlib5Test whether two values are equal in the SMT-Problem.hasmtlib9Test whether two values are not equal in the SMT-Problem.hasmtlib2Class that allows branching on predicates of type b on branches of type a.2If predicate (p :: b) then (t :: a) else (f :: a).5There is a default implementation if your type is an .Examplesite True "1" "2" "1"ite False 100 42 42hasmtlibAn SMT-Expression. For building expressions use the corresponding instances.With a lot of criminal energy you may build invalid expressions regarding the SMTLib Version 2.6 - specification. Therefore it is highly recommended to rely on the instances.hasmtlibJust v if quantified var has been created already, Nothing otherwisehasmtlibJust v if quantified var has been created already, Nothing otherwisehasmtlibIndicates whether an expression is a leaf. All non-recursive contructors are leafs.hasmtlibSize of the expression. Counts the amount of operations.ExamplesnodeSize $ x + y === x + y 3nodeSize $ false 0hasmtlib:Symbolic evaluation of the minimum of two symbolic values.hasmtlib:Symbolic evaluation of the maximum of two symbolic values.hasmtlib3Symbolically test multiple expressions on equality.Returns " if given less than two arguments.hasmtlib7Symbolically test multiple expressions on distinctness.Returns " if given less than two arguments.hasmtlib*Universal quantification for any specific g.Example  assert $ for_all @IntSort $ x -> x + 0 === x && 0 + x === x  The lambdas x is all-quantified here. It will only be scoped for the lambdas body.hasmtlib,Existential quantification for any specific gExample  assert $ for_all @(BvSort Unsigned 8) $ x -> exists $ y -> x - y === 0  The lambdas y is existentially quantified here. It will only be scoped for the lambdas body.hasmtlibSelect a value from an array.hasmtlibStore a value in an array.hasmtlibConcats two bitvectors.hasmtlibConverts an expression of type i to type j.hasmtlibConverts an expression of type j to type i.hasmtlib%Checks whether an expression of type j! may be safely converted to type i.hasmtlibLength of a string.hasmtlibSingleton string containing a character at given position or empty string when position is out of range. The leftmost position is 0.hasmtlib(strSubstring s i n)8 evaluates to the longest (unscattered) substring of s of length at most n starting at position i). It evaluates to the empty string if n is negative or i is not in the interval [0,l-1] where l is the length of s.hasmtlib+First string is a prefix of second one. (strPrefixof s t) is true iff s is a prefix of t.hasmtlib+First string is a suffix of second one. (strSuffixof s t) is true iff s is a suffix of t.hasmtlib$First string contains second one (strContains s t) iff s contains t.hasmtlibIndex of first occurrence of second string in first one starting at the position specified by the third argument. (strIndexof s t i), with  0 <= i <= |s|/ is the position of the first occurrence of t in s at or after position i, if any. Otherwise, it is -1. Note that the result is i whenever i is within the range [0, |s|] and t is empty.hasmtlib(strReplace s t t') is the string obtained by replacing the first occurrence of t in s , if any, by t'. Note that if t' is empty, the result is to prepend t' to s ; also, if t does not occur in s then the result is s.hasmtlib(strReplaceAll s t t@) is s if t is the empty string. Otherwise, it is the string obtained from s! by replacing all occurrences of t in s by t@, starting with the first occurrence and proceeding in left-to-right order.hasmtlib#Caution for quantified expressions:  will only be applied if quantification has taken place already.hasmtlib#Caution for quantified expressions:  will only be applied if quantification has taken place already.hasmtlibThis instance is partial for testBit and popCount-, it's only intended for use with constants ().hasmtlibThis instance is partial for testBit and popCount-, it's only intended for use with constants ().hasmtlibThis instance is partial for 6, this method is only intended for use with constants.hasmtlibThis instance is partial for 6, this method is only intended for use with constants.hasmtlibThis instance is partial for 6, this method is only intended for use with constants.hasmtlibNot part of the SMTLib standard Version 2.6. Some solvers support it. At least valid for CVC5 and MathSAT.444444  Safe-Inferred ")1;9hasmtlib!A solution for a single variable.hasmtlibA variable in the SMT-Problemhasmtlib-An assignment for this variable in a solutionhasmtlib Newtype for  z( so we can use it as right-hand-side of .hasmtlibResults of check-sat commands.hasmtlib-An existential wrapper that hides some known g with an  fhasmtlibAlias class for constraint  (f t)hasmtlib Create a  from some s.  Safe-Inferred")1Chasmtlib Wrapper for  which takes a .hasmtlibOut of many bool-expressions build a formula which encodes how many of them are .hasmtlibOut of many bool-expressions build a formula which encodes that at most k of them are . is defined as follows:  0 =    1 =   k = ( k) .  hasmtlibOut of many bool-expressions build a formula which encodes that at least k of them are . is defined as follows:  0 =    1 =    k = ( k) .  hasmtlibOut of many bool-expressions build a formula which encodes that exactly k of them are . is defined as follows:  0 xs =   xs  1 xs =  @t 1 xs   @t 1 xs  k xs =  xs  k hasmtlibThe squareroot-encoding, also called product-encoding, is a special encoding for atMost 1.*The original product-encoding provided by  Jingchao Chen in 7A New SAT Encoding of the At-Most-One Constraint (2010) used auxiliary variables and would therefore be monadic. It requires ' 2 \sqrt{n} + \mathcal{O}(\sqrt[4]{n})  auxiliary variables and + 2n + 4\sqrt{n} + \mathcal{O}(\sqrt[4]{n})  clauses.To make this encoding pure, all auxiliary variables are replaced with a disjunction of size  \mathcal{O}(\sqrt{n}) . Therefore zero auxiliary variables are required and technically clause-count remains the same, although the clauses get bigger.hasmtlibThe quadratic-encoding, also called pairwise-encoding, is a special encoding for atMost 1.It's the naive encoding for the at-most-one-constraint and produces  \binom{n}{2} % clauses and no auxiliary variables..  Safe-Inferred "()1=Dhasmtlib)Lift values to SMT-Values or decode them.9You can derive an instance of this class if your type is .hasmtlibResult of decoding a.hasmtlib$Decode a value using given solution.hasmtlibEncode a value as constant.hasmtlibComputes a default   by distributing  over it's type arguments.hasmtlibDecode and evaluate expressions    Safe-Inferred")1UhasmtlibA . that addtionally allows optimization targets.Example problem :: MonadOMT s m => StateT s m (Expr (BvSort Unsigned 8)) problem = do setLogic "QF_BV" x <- var @(BvSort Unsigned 8) assertSoftWeighted (x ? -2 minimize x  will give x := -1 as solution.hasmtlib8Maximizes a numerical expression within the OMT-Problem.Example 7x <- var @(BvSort Signed 4) assert $ x StateT s m () problem = do setOption $ Incremental True setLogic "QF_LIA" x <- var @IntSort push assert $ x + 2 === x * 2 res <- checkSat case res of Sat -> do x' <- getValue x ... _ -> pop ... return () hasmtlib6Push a new context (one) to the solvers context-stack.hasmtlib%Pop the solvers context-stack by one.hasmtlibRun  check-sat on the current problem.hasmtlibRun get-model on the current problem. This can be used to decode temporary models within the SMT-Problem.Example x <- var @RealSort y <- var assert $ x >? y && y do model <- getModel liftIO $ print $ decode model x r -> print $ show r <> ": Cannot get model." hasmtlibEvaluate any expressions value in the solvers model. Requires a  or  check-sat response beforehand.Example x <- var @RealSort assert $ x >? 10 res <- checkSat case res of Unsat -> print "Unsat. Cannot get value for x." r -> do x' <- getValue x liftIO $ print $ show r ++ ": x = " ++ show x' hasmtlibA  that holds an SMT-Problem.Example problem :: MonadSMT s m => StateT s m (Expr IntSort) problem = do setLogic "QF_LIA" x <- var @IntSort assert $ x + 2 === x * 2 return x hasmtlibConstruct a variable. This is mainly intended for internal use. In the API use  instead.hasmtlib#Construct a variable as expression.Example x <- var' (Proxy @RealType) hasmtlibAssert a boolean expression.Example )x <- var @IntType assert $ x - 27 === 42 hasmtlibSet an SMT-Solver-Option.Example setOption $ Incremental True hasmtlib(Set the logic for the SMT-Solver to use.Example setLogic "QF_LRA" hasmtlib Wrapper for  which hides the .Example x <- var @BoolSort hasmtlib Wrapper for  which hides the . This is mainly intended for internal use. In the API use  instead.hasmtlibCreate a constant.Examples constant True Constant (BoolValue True)constant (10 :: Integer) Constant (IntValue 10)constant @RealSort 5 Constant (RealValue 5.0) constant @(BvSort Unsigned 8) 14 Constant (BvValue 00001110)hasmtlib"Maybe assert a boolean expression.Asserts given expression if  is a . Does nothing otherwise.hasmtlibAssign quantified variables to all quantified subexpressions of an expression.Quantifies bottom-up.This is intended for internal use. Usually before rendering an assert.hasmtlib First run  and then  on the current problem.Example x <- var @BoolSort assert $ x xor false (res, sol) <- solve case res of Sat -> do liftIO $ print $ decode sol x r -> print r hasmtlibLike , but forces a weight and omits the group-id.  Safe-Inferred")1d2hasmtlib Relation a b represents a binary relation R \subseteq A \times B , where the domain A is a finite subset of the type a, and the codomain B is a finite subset of the type b.#A relation is stored internally as Array (a,b) Expr BoolSort, so a and b have to be instances of  , and both A and B are intervals.hasmtlib"relation ((amin,bmin),(amax,mbax))& constructs an indeterminate relation R \subseteq A \times B  where A is {amin .. amax} and B is {bmin .. bmax}.hasmtlib%Constructs an indeterminate relation R \subseteq B \times B  that is symmetric, i.e., <\forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) .hasmtlibConstructs a relation R \subseteq A \times B  from a list.hasmtlibConstructs a relation R \subseteq A \times B  from a function.hasmtlib%Constructs an indeterminate relation R \subseteq A \times B from a function.hasmtlib!Constructs the identity relation 0I = \{ (x,x) ~|~ x \in A \} \subseteq A \times A.hasmtlibThe bounds of the array that correspond to the matrix representation of the given relation.hasmtlib; corresponds to the matrix representation of this relation.hasmtlibSince a symmetric relation must be homogeneous, the domain must equal the codomain. Therefore, given bounds  ((p,q),(r,s)), it must hold that p=q and r=s.hasmtlibA list of tuples, where the first element represents an element (x,y) \in A \times B & and the second element is a positive  h if  (x,y) \in R , or a negative  h if (x,y) \notin R .hasmtlibA function that assigns a  h-value to each element (x,y) \in A \times B .hasmtlibSince the identity relation is homogeneous, the domain must equal the codomain. Therefore, given bounds  ((p,q),(r,s)), it must hold that p=q and r=s. Trustworthy")1ie hasmtlib5States that can share expressions by comparing their s.hasmtlibA constraint on the monad used when asserting the shared node in .hasmtlibA  on a mapping between a  and it's  we may share.hasmtlibAsserts that a node-expression is represented by it's auxiliary node-variable: nodeExpr :: Expr t === nodeVar. Also gives access to the  of the original expression.hasmtlib?Sets the mode used for sharing common expressions. Defaults to .hasmtlibMode used for sharing.hasmtlib(Common expressions are not shared at allhasmtlib%Expressions that resolve to the same  are sharedhasmtlibShares all possible sub-expressions in given expression. Replaces each node in the expression-tree with an auxiliary variable. All nodes x y where $makeStableName x == makeStableName y are replaced with the same auxiliary variable. Therefore this creates a DAG.hasmtlibReturns an auxiliary variable representing this expression node. If such a shared auxiliary variable exists already, returns that. Otherwise creates one and returns it.   Safe-Inferred ")1k?hasmtlibThe state of the SMT-problem.hasmtlibLast Id assigned to a new varhasmtlibAll constructed variableshasmtlibAll asserted formulashasmtlibLogic for the SMT-Solverhasmtlib*All manually configured SMT-Solver-OptionshasmtlibHow to share common expressionshasmtlibMapping between a  and it's  we may share Safe-Inferred ")1n hasmtlibAn assertion of a booolean expression in OMT that may be weighted.hasmtlibThe underlying soft formulahasmtlibWeight of the soft formulahasmtlibGroup-Id of the soft formulahasmtlibThe state of the OMT-problem.hasmtlibThe underlying -ProblemhasmtlibAll expressions to minimizehasmtlibAll expressions to maximizehasmtlib*All soft assertions of boolean expressionshasmtlibA newtype for numerical expressions that are target of a maximization.hasmtlibA newtype for numerical expressions that are target of a minimization. Safe-Inferred")1shasmtlib%A class that allows debugging states.hasmtlibDebugs information about the problem like the amount of variables and assertions.hasmtlibA type holding actions for debugging states holding SMT-Problems.hasmtlibDebug the entire statehasmtlib#Debug the solvers raw response for  (check-sat)hasmtlib#Debug the solvers raw response for  (get-model)hasmtlib The silent . Does not debug at all.hasmtlib The noisy .%Debugs the entire problem definition.hasmtlib The verbose .Debugs all communication between Haskell and the external solver.hasmtlibA 7 for debugging all rendered options that have been set.hasmtlibA + for debugging the logic that has been set.hasmtlibA ) for debugging all variable declarations.hasmtlibA  for debugging all assertions.hasmtlibA  for debugging every push/pop-interaction with the solvers incremental stack.hasmtlibA  for debugging every  (get-value) call to the solver.hasmtlibA  for debugging the entire and raw responses of a solver for the commands  (check-sat) and  (get-model). Safe-Inferred")1thasmtlib9Render values to their SMTLib2-Lisp form, represented as . Safe-Inferred")1u Safe-Inferred ")1xhasmtlibA pipe to the solver. If  is  then all commands that do not expect an answer are sent to the queue. All commands that expect an answer have the queue to be sent to the solver before sending the command itself. If  is not 2, all commands are sent to the solver immediately.hasmtlibLast Id assigned to a new varhasmtlibLogic for the SMT-SolverhasmtlibHow to share common expressionshasmtlibMapping between a  and it's  we may sharehasmtlibIndex of each  (' ()) is incremental stack height where 0 representing auxiliary var that has been sharedhasmtlibActive pipe to the backendhasmtlib3Debugger for communication with the external solver Safe-Inferred")1 hasmtlib#Configuration for solver processes.hasmtlib$The underlying config of the processhasmtlibTimeout in microsecondshasmtlib/Debugger for communication with external solverhasmtlib#Function that turns a state into a  and a .hasmtlib Creates a 3 which holds an external process with a SMT-Solver. This will: Encode the SMT-problem,0start a new external process for the SMT-Solver,#send the problem to the SMT-Solver, wait for an answer and parse it,0close the process and clean up all resources andreturn the decoded solution.hasmtlib Decorates a , with a timeout. The timeout is given as an # which specifies after how many  microseconds the entire problem including problem construction, solver interaction and solving time may time out.When timing out, the  will always be . This uses  internally.hasmtlib Decorates a  with a .hasmtlib solver prob solves a SMT problem prob with the given solver". It returns a pair consisting of: A  that indicates if prob is satisfiable (), unsatisfiable (9), or if the solver could not determine any results ().A / answer that was decoded using the solution to prob6. Note that this answer is only meaningful if the  is  or " and the answer value is in a .Example import Language.Hasmtlib main :: IO () main = do res <- solveWith @SMT (solver cvc5) $ do setLogic "QF_LIA" x <- var @IntSort assert $ x >? 0 return x print res %The solver will probably answer with x := 1.hasmtlib1Pipes an SMT-problem interactively to the solver.Example import Language.Hasmtlib import Control.Monad.IO.Class main :: IO () main = do interactiveWith z3 $ do setOption $ ProduceModels True setLogic "QF_LRA" x <- var @RealSort assert $ x >? 0 (res, sol) <- solve liftIO $ print res liftIO $ print $ decode sol x push y <- var @IntSort assert $ y ? 4 solveMinimized x Nothing Nothing The solver will return x := 5. The first  indicates that each intermediate result will be set as next upper bound. The second  shows that we do not care about intermediate, but only the final (minimal) result. x <- var @IntSort assert $ x >? 4 solveMinimized x (Just (\r -> r-1)) (Just print) The solver will still return x := 5.>However, here we want the next bound of each refinement to be lastResult - 1.. Also, every intermediate result is printed.hasmtlibSolves the current problem with respect to a maximal solution for a given numerical expression.This is done by incrementally refining the lower bound for a given target. Terminates, when setting the last intermediate result as new lower bound results in . Then removes that last assertion and returns the previous (now confirmed maximal) result.You can also provide a step-size. You do not have to worry about stepping over the optimal result. This implementation takes care of it.7Access to intermediate results is also possible via an -Action.Examples x <- var @IntSort assert $ x However, here we want the next bound of each refinement to be lastResult + 1.. Also, every intermediate result is printed.hasmtlibTarget to minimizehasmtlibStep-size: Lambda is given last result as argument, producing the next upper boundhasmtlib Accessor to intermediate resultshasmtlibTarget to maximizehasmtlibStep-size: Lambda is given last result as argument, producing the next lower boundhasmtlib Accessor to intermediate results Safe-Inferred")1hasmtlibA  for Z3. Requires binary z3 to be in path. Safe-Inferred")1]hasmtlibA  for Yices. Requires binary  yices-smt2 to be in path. Safe-Inferred")1hasmtlibA ! for OpenSMT. Requires binary opensmt to be in path. Safe-Inferred")1hasmtlibA ! for MathSAT. Requires binary mathsat to be in path.hasmtlibA % for OptiMathSAT. Requires binary  optimathsat to be in path. Safe-Inferred")1VhasmtlibA  for CVC5. Requires binary cvc5 to be in path. Safe-Inferred")1hasmtlibA " for Bitwuzla. Requires binary bitwuzla to be in path.As of v0.5 Bitwuzla uses Cadical as SAT-Solver by default. Make sure it's default SAT-Solver binary - probably cadical - is in path too.hasmtlibA 3 for Bitwuzla with Kissat as underlying sat-solver.Requires binary bitwuzla$ and to be in path. Will use the kissat shipped with bitwuzla.It is recommended to build bitwuzla* from source for this to work as expected. Safe-Inferred")1=hasmtlibConstruct a variable datum of a data-type by creating variables for all its fields.9You can derive an instance of this class if your type is ! and has exactly one constructor.hasmtlib Wrapper for  which takes a  Safe-Inferred")1ghijklmf_`abcde]^\nz{|}~,-.456/012378<9:=>; !")*STUVW    !"#$%&'()*+,-./01234567889:;<=>?@ABCDEFGHIJJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                   hasmtlib-2.7.2-inplaceLanguage.Hasmtlib.Boolean$Language.Hasmtlib.Internal.Uniplate1Language.Hasmtlib.Type.ArrayMapLanguage.Hasmtlib.Type.BitvecLanguage.Hasmtlib.Type.OptionLanguage.Hasmtlib.Type.SMTSortLanguage.Hasmtlib.Type.ValueLanguage.Hasmtlib.Type.ExprLanguage.Hasmtlib.Type.SolutionLanguage.Hasmtlib.CountingLanguage.Hasmtlib.CodecLanguage.Hasmtlib.Type.MonadSMTLanguage.Hasmtlib.Type.Relation"Language.Hasmtlib.Internal.SharingLanguage.Hasmtlib.Type.SMTLanguage.Hasmtlib.Type.OMTLanguage.Hasmtlib.Type.Debugger!Language.Hasmtlib.Internal.Render!Language.Hasmtlib.Internal.ParserLanguage.Hasmtlib.Type.PipeLanguage.Hasmtlib.Type.SolverLanguage.Hasmtlib.Solver.Z3Language.Hasmtlib.Solver.Yices Language.Hasmtlib.Solver.OpenSMT Language.Hasmtlib.Solver.MathSATLanguage.Hasmtlib.Solver.CVC5!Language.Hasmtlib.Solver.BitwuzlaLanguage.Hasmtlib.VariablehasmtlibLanguage.HasmtlibBooleanbooltruefalse&&||==><==<==>notxorandornandnorallany$fBooleanVector $fBooleanBit $fBooleanBool Uniplate1 uniplate1 transformM1 transform1 lazyParaM1 ConstArray _arrConst_storedArrayMapasConst' viewConst arrSelectarrStoreasConst$fShowConstArray$fEqConstArray$fOrdConstArray$fFunctorConstArray$fFoldableConstArray$fTraversableConstArrayarrConststored$fArrayMapConstArraykvBitvecunBitvec KnownBvEnc bvEncSingSBvEnc SUnsignedSSignedBvEncUnsignedSigned bvEncSing' bvEncSing'' asUnsignedasSigned_signBit bitvecConcatbitvecFromListNbitvecFromListN'$fGCompareBvEncSBvEnc$fGEqBvEncSBvEnc$fKnownBvEncSigned$fKnownBvEncUnsigned$fIntegralBitvec $fRealBitvec $fEnumBitvec$fBoundedBitvec $fNumBitvec $fBitsBitvec $fShowBitvec $fEqBitvec $fOrdBitvec$fBooleanBitvec $fShowBvEnc $fEqBvEnc $fOrdBvEnc $fOrdSBvEnc $fEqSBvEnc $fShowSBvEnc SMTOption PrintSuccess ProduceModels IncrementalCustom$fShowSMTOption $fEqSMTOption$fOrdSMTOption$fDataSMTOptionSomeKnownSMTSort KnownSMTSortsortSingSSMTSortSIntSort SRealSort SBoolSortSBvSort SArraySort SStringSort HaskellTypeSMTSortBoolSortIntSortRealSortBvSort ArraySort StringSort sortSing'$fKnownSMTSortStringSort$fKnownSMTSortArraySort$fKnownSMTSortBvSort$fKnownSMTSortBoolSort$fKnownSMTSortRealSort$fKnownSMTSortIntSort$fGCompareSMTSortSSMTSort$fGEqSMTSortSSMTSort $fOrdSSMTSort $fEqSSMTSort$fShowSSMTSortValueIntValue RealValue BoolValueBvValue ArrayValue StringValue unwrapValue wrapValue$fBooleanValue$fFractionalValue $fNumValue$fGCompareSMTSortValue$fGEqSMTSortValue $fOrdValue $fEqValueSMTVar_varId $fShowSMTVar$fGenericSMTVar $fEqSMTVar $fOrdSMTVar GOrderable=?? GEquatable===# Equatable===/==IteableiteExprVarConstantPlusMinusNegMulAbsModRemIDivDivLTHLTHEEQUDistinctGTHEGTHNotAndOrImplXorPiSqrtExpSinCosTanAsinAcosAtanToRealToIntIsIntIteBvNandBvNorBvShLBvLShRBvAShRBvConcatBvRotLBvRotR ArrSelectArrStore StrConcat StrLengthStrAt StrSubstring StrPrefixOf StrSuffixOf StrContains StrIndexOf StrReplace StrReplaceAllForAllExistsvarIdisLeafexprSizemin'max'equaldistinctfor_allexistsselectstorebvConcat toRealSort toIntSort isIntSort strLengthstrAt strSubstring strPrefixOf strSuffixOf strContains strIndexOf strReplace strReplaceAll$fGCompareSMTSortExpr$fGEqSMTSortExpr $fOrdExpr$fEqExpr$fGNFDataSMTSortExpr $fPlatedExpr$fUniplate1SMTSortExpr: $fIxedExpr $fIxedExpr0$fIsStringExpr $fMonoidExpr$fSemigroupExpr $fBitsExpr $fBitsExpr0 $fBoundedExpr$fBoundedExpr0 $fBooleanExpr$fIntegralExpr $fEnumExpr $fRealExpr$fFloatingExpr$fFractionalExpr$fSuffixedExpr$fPrefixedExpr$fIteableExpr(,,,,,,,)$fIteableExpr(,,,,,,)$fIteableExpr(,,,,,)$fIteableExpr(,,,,)$fIteableExpr(,,,)$fIteableExpr(,,)$fIteableExpr(,)$fIteableExpr()$fIteableExprIdentity$fIteableExprDual$fIteableExprLast$fIteableExprFirst$fIteableExprProduct$fIteableExprSum$fIteableExprTree$fIteableExprSeq$fIteableExprMaybe$fIteableExprList$fIteableBoola$fIteableExprExpr$fGEquatablekM1$fGEquatablek:+:$fGEquatablek:*:$fGEquatablekV1$fGEquatablekU1 $fAsEmptyExpr$fBooleanExpr0$fEquatableIdentity$fEquatableDual$fEquatableLast$fEquatableFirst$fEquatableProduct$fEquatableSum$fEquatableEither$fEquatableMaybe$fEquatableTree$fEquatableList$fEquatable(,,,,,,,)$fEquatable(,,,,,,)$fEquatable(,,,,,)$fEquatable(,,,,)$fEquatable(,,,)$fEquatable(,,)$fEquatable(,)$fEquatableBool$fEquatableOrdering$fEquatableDouble$fEquatableFloat$fEquatableChar$fEquatableInt64$fEquatableInt32$fEquatableInt16$fEquatableInt8$fEquatableWord64$fEquatableWord32$fEquatableWord16$fEquatableWord8$fEquatableWord$fEquatableNatural$fEquatableInteger$fEquatableInt$fEquatableVoid $fEquatable()$fGEquatablekK1$fEquatableExpr$fGOrderablekM1$fGOrderablek:+:$fGOrderablek:*:$fGOrderablekV1$fGOrderablekU1$fSnocExprExprExprExpr$fConsExprExprExprExpr $fNumExpr$fOrderableIdentity$fOrderableDual$fOrderableLast$fOrderableFirst$fOrderableProduct$fOrderableSum$fOrderableEither$fOrderableMaybe$fOrderableTree$fOrderableList$fOrderable(,,,,,,,)$fOrderable(,,,,,,)$fOrderable(,,,,,)$fOrderable(,,,,)$fOrderable(,,,)$fOrderable(,,)$fOrderable(,)$fOrderableBool$fOrderableOrdering$fOrderableDouble$fOrderableFloat$fOrderableChar$fOrderableInt64$fOrderableInt32$fOrderableInt16$fOrderableInt8$fOrderableWord64$fOrderableWord32$fOrderableWord16$fOrderableWord8$fOrderableWord$fOrderableNatural$fOrderableInteger$fOrderableInt$fOrderableVoid $fOrderable()$fGOrderablekK1$fOrderableExpr SMTVarSol_solVar_solVal IntValueMapSolutionResultUnsatUnknownSat$fSemigroupIntValueMap$fMonoidIntValueMap $fShowResult $fEqResult $fOrdResult$fShowIntValueMapSomeKnownOrdSMTSortOrdHaskellTypesolValsolVarfromSomeVarSols$fOrdHaskellTypet$fShowSMTVarSolcount'countatMostatLeastexactlyamoSqrtamoQuadGCodecGDecodedgdecodegencodeCodecDecodeddecodeencodeDefaultDecoded $fGCodecM1 $fGCodec:+: $fGCodec:*: $fGCodecV1 $fGCodecU1 $fGCodecK1 $fCodecBool$fCodecOrdering $fCodecDouble $fCodecFloat $fCodecChar $fCodecInt64 $fCodecInt32 $fCodecInt16 $fCodecInt8 $fCodecWord64 $fCodecWord32 $fCodecWord16 $fCodecWord8 $fCodecWord$fCodecNatural$fCodecInteger $fCodecInt $fCodecArray $fCodecMap $fCodecSeq $fCodecIntMap$fCodecIdentity $fCodecDual $fCodecLast $fCodecFirst$fCodecProduct $fCodecSum $fCodecEither $fCodecTree $fCodecMaybe $fCodecList$fCodec(,,,,,,,)$fCodec(,,,,,,)$fCodec(,,,,,) $fCodec(,,,,) $fCodec(,,,) $fCodec(,,) $fCodec(,) $fCodec() $fCodecExprMonadOMTminimizemaximize assertSoft MonadIncrSMTpushpopcheckSatgetModelgetValueMonadSMTsmtvar'var'assert setOptionsetLogicvarsmtvarconstant assertMaybequantifysolveassertSoftWeightedRelationrelationsymmetric_relationbuild buildFrom buildFromMidentityboundsindicesassocselems!?!domaincodomainimagepreimagetable$fIxedRelation$fEachRelationRelationExprExpr$fCodecRelationSharing SharingMonad stableMapassertSharedNodesetSharingMode SharingModeNone StableNames runSharingshare$fDefaultSharingMode$fShowSharingModeSMT _lastVarId_vars _formulas_mlogic_options _sharingMode _stableMapformulas lastVarIdmlogicoptions sharingModevars$fMonadSMTSMTm $fSharingSMT $fDefaultSMT SoftFormula_formula_mWeight _mGroupIdOMT_smt_targetMinimize_targetMaximize _softFormulasMaximize _targetMaxMinimize _targetMinformulamGroupIdmWeightsmt softFormulastargetMaximizetargetMinimize$fMonadOMTOMTm$fMonadSMTOMTm $fSharingOMT $fDefaultOMT StateDebugger statisticallyDebugger debugState debugOption debugLogicdebugVar debugAssert debugPushdebugPop debugCheckSat debugGetModel debugGetValue debugMinimize debugMaximizedebugAssertSoftdebugResultResponsedebugModelResponsesilentlynoisy verbosely optionishlogicishvarish assertionishincrementalStackish getValueish responseish$fDefaultDebugger$fStateDebuggerOMT$fStateDebuggerSMT RenderProblem renderOptions renderLogicrenderDeclareVarsrenderAssertionsrenderSoftAssertionsrenderMinimizationsrenderMaximizationsRenderrenderrender1render2render3renderNrenderQuantifierrenderSetLogicrenderDeclareVar renderAssertrenderGetValue renderPush renderPoprenderCheckSatrenderGetModel$fRenderMaximize$fRenderMinimize$fRenderSoftFormula$fRenderSMTOption$fRenderSSMTSort $fRenderExpr $fShowExpr $fRenderValue $fShowValue$fRenderSMTVar$fRenderBitvec $fRenderText$fRenderBuilder $fRenderList $fRenderChar$fRenderDouble$fRenderInteger$fRenderNatural $fRenderBool$fRenderProblemOMT$fRenderProblemSMT answerParser resultParseranyModelParserdefaultModelParsersmt2ModelParser parseSomeSol parseSomeSortparseSomeBitVecSortparseSomeArraySort parseExpr' parseExpr constantExpr anyBitvector binBitvector hexBitvectorliteralBitvector constArrayparseSmtStringunarybinaryternarynarysmtPianyValue negativeValueparseRatioDoubleparseToRealDouble parseBoolgetValueParserPipe_lastPipeVarId _mPipeLogic_pipeSharingMode_pipeStableMap_incrSharedAuxs _pipeSolver_mPipeDebuggerincrSharedAuxs lastPipeVarId mPipeLogicpipeSharingMode pipeSolver pipeStableMap$fMonadOMTPipem$fMonadIncrSMTPipem$fMonadSMTPipem $fSharingPipe SolverConfig_processConfig _mTimeout _mDebuggerSolver mDebuggermTimeout processConfigsolver timingout debugging solveWithinteractiveWithsolveMinimizedsolveMaximizedz3yicesopensmtmathsat optimathsatcvc5bitwuzlabitwuzlaKissat GVariable gvariableVariablevariable variable'$fGVariablekM1$fGVariablek:*:$fGVariablekU1$fGVariablekK1$fVariableEither$fVariableMaybe$fVariableCompose $fVariableAlt$fVariableConst$fVariableIdentity$fVariableDual$fVariableLast$fVariableFirst$fVariableProduct $fVariableSum$fVariable(,,,,,,,)$fVariable(,,,,,,)$fVariable(,,,,,)$fVariable(,,,,)$fVariable(,,,)$fVariable(,,) $fVariable(,) $fVariable()$fVariableExprghc-prim GHC.TypesBoolTrueFalsebase Data.ProxyProxyvector-sized-1.6.1-169aaf09d7cae55683a9b0938b983b1005e4815ca2813cf5dcb5b457b3289e87Data.Vector.Unboxed.SizedVector GHC.TypeNatsNatTypeIntGHC.Base Applicativelens-5.3.2-91ce879581d0c2e231e581ee2396e336e2934c42478138a3648c0a5f4ff59c77Control.Lens.PlatedplateGHC.Real toIntegerGHC.EnumfromEnum toRationalcontainers-0.6.7Data.IntMap.InternalIntMapdependent-map-0.4.0.0-389a18fa07b476120aa99de3e3d149d607e406cc7ff029188f9d0b95e3bfa2b2Data.Dependent.Map.InternalDMap GHC.ClassesOrdconst GHC.GenericsGeneric mtl-2.3.1Control.Monad.State.Class MonadState GHC.MaybeMaybeJustGHC.IxIxNothingGHC.StableName StableNameControl.Lens.TypeLens'bytestring-0.11.5.3 Data.ByteString.Builder.InternalBuildersmtlib-backends-0.4-36b7c32d9b849b5840ac2a4dea6977cb1b78c701dc4e32239363fba866136ee9SMTLIB.BackendsQueuingData.Sequence.InternalSeqlifted-base-0.2.3.12-e8767ab3a82019f843d2a852230df8d24a1f26e28977eacc4d84cc69de378142System.Timeout.LiftedtimeoutIO