h*H!=e      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                              1.1.2 Safe-Inferred")1 hasmtlibLift a hasmtlibThe true constant  =  hasmtlibThe false constant  =  hasmtlibLogical conjunction.hasmtlib#Logical disjunction (inclusive or).hasmtlibLogical implication.hasmtlibLogical negationhasmtlib 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  320 Safe-Inferred")1= chasmtlib<-like class for clean API. In context hide the Preludes .  Safe-Inferred")1 #hasmtlib9Render values to their SMTLib2-Lisp form, represented as Builder.#$%&'#$%&' Safe-Inferred"()1 s-hasmtlib5Unsigned and length-indexed bitvector with MSB first.-/.0123456789:;<=>?@-/.0123456789:;<=>?@ Safe-Inferred ")1KhasmtlibA map-like array with a default constant value and partially overwritten values. OhasmtlibClass that allows access to a map-like array where specific values are is the default value or 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 (store A i x) == xforall A i j x: i /= j ==> (arrSelect (arrStore A i x) j === arrSelect A j)Thasmtlib Wrapper for P which hides the  KNMLOSRQPT[\ OSRQPTKNML\[ Safe-Inferred  ")1^hasmtlib? y assert $ x === min' 42 100 hasmtlib!Minimum of two as SMT-Expression.hasmtlib!Maximum of two as SMT-Expression.  4444 Safe-Inferred")1hasmtlibBitvector shift lefthasmtlibBitvector logical shift righthasmtlibConcat two bitvectorshasmtlibRotate bitvector lefthasmtlibRotate bitvector right Safe-Inferred")1{hasmtlib,A universal quantification for any specific a. If the type cannot be inferred, apply a type-annotation. Nested quantifiers are also supported.Usage:  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/An existential quantification for any specific a If the type cannot be inferred, apply a type-annotation. Nested quantifiers are also supported.Usage:  assert $ for_all @(BvSort 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.*acbdef^_`{ztuvwxy|}nopqrslm~ijhkg*acbdef^_`{ztuvwxy|}nopqrslm~ijhkg  Safe-Inferred")1hasmtlibOptions for SMT-Solvers.hasmtlib$Print "success" after each operationhasmtlib>Produce a satisfying assignment after each successful checkSathasmtlibIncremental solving  Safe-Inferred ")1 hasmtlib!A solution for a single variable.hasmtlibA variable in the SMT-Problemhasmtlib-An assignment for this variable in a solutionhasmtlib Newtype for  t( so we can use it as right-hand-side of .hasmtlibA Solution is a dependent map  from ns t to  t.hasmtlibResults of check-sat commands.hasmtlib9Function that turns a state into a result and a solution.hasmtlib-An existential wrapper that hides some known a with an  z hasmtlibAlias class for constraint  (z t)hasmtlib Create a  from some s.  Safe-Inferred")1="shasmtlib)Lift values to SMT-Values or decode them.hasmtlib$Decode a value using given solution.hasmtlibEncode a value as constant.hasmtlibCompute the default   for every functor-wrapper. Useful for instances using default signatures.hasmtlibDecode and evaluate expressions  Safe-Inferred")1+UhasmtlibA ! that allows incremental solving.hasmtlib6Push a new context (one) to the solvers context-stack.hasmtlib%Pop the solvers context-stack by one.hasmtlib%Run 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. x <- var @RealSort y <- var assert $ x >? y && y print "Unsat. Cannot get model." r -> do model <- getModel liftIO $ print $ decode model x hasmtlibEvaluate any expressions value in the solvers model. Requires a  or  check-sat response beforehand. 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.hasmtlibConstruct a variable. This is mainly intended for internal use. In the API use  instead. 2x :: SMTVar RealType <- smtvar' (Proxy @RealType) hasmtlib#Construct a variable as expression. -x :: Expr RealType <- var' (Proxy @RealType) hasmtlibAssert a boolean expression. 8x :: Expr IntType <- var @IntType assert $ x + 5 === 42 hasmtlibSet an SMT-Solver-Option. setOption $ Incremental True hasmtlib(Set the logic for the SMT-Solver to use. setLogic "QF_LRA" hasmtlib Wrapper for  which hides the .hasmtlib Wrapper for  which hides the . This is mainly intended for internal use. In the API use  instead.hasmtlibCreate a constant. constant True Constant (BoolValue True)"let x :: Integer = 10 ; constant x Constant (IntValue 10)constant @IntType 5 Constant (IntValue 5)constant @(BvType 8) 5 Constant (BvValue 0000101)hasmtlibAssign quantified variables to all quantified subexpressions of an expression. This shall only be used internally. Usually before rendering an assert.hasmtlib First run  and then  on the current problem. Safe-Inferred ")1-DhasmtlibThe 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-Optionshasmtlib Render a -Problem to SMTLib2-Syntax. Each element of the returned Sequence is a line. Safe-Inferred")1-## Safe-Inferred ")10=hasmtlibA 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-SolverhasmtlibActive pipe to the backend Safe-Inferred")13Lhasmtlib0A type holding actions to execute for debugging  solving.hasmtlibA newtype-wrapper for 0 which configures a solver via external process.hasmtlib Creates a  from a hasmtlibCreates a debugging  from a hasmtlibCreates an interactive session with a solver by creating and returning an alive process-handle .hasmtlibA  which holds an external process with a SMT-Solver. This will:  Encode the  -problem,0Start a new external process for the SMT-Solver,#Send the problem to the SMT-Solver,#Wait for an answer and parse it and-close the process and clean up all resources.   Safe-Inferred")13 Safe-Inferred")13 Safe-Inferred")14 Safe-Inferred")14@ Safe-Inferred")1:yhasmtlibData that can have 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 .&Here is a small example of how to use : import Language.Hasmtlib main :: IO () main = do res <- solveWith (solver cvc5) $ do setLogic "QF_LIA" x <- var @IntSort assert $ x >? 0 return x print res hasmtlibPipes an SMT-problem interactively to the solver. Enables incremental solving by default. Here is a small example of how to use it for solving a problem utilizing the solvers incremental stack: import Language.Hasmtlib import Control.Monad.IO.Class main :: IO () main = do cvc5Living <- interactiveSolver cvc5 interactiveWith cvc5Living $ do setOption $ ProduceModels True setLogic "QF_LIA" x <- var IntSort assert $ x >? 0 (res, sol) <- solve liftIO $ print res liftIO $ print $ decode sol x push y <- var IntSort assert $ y V3 a /varV3 <- variable @(V3 (Expr RealType)) ; varV33 V3 (Var RealType) (Var RealType) (Var RealType)hasmtlib Wrapper for  which takes a  Safe-Inferred")1<0gacbdef^_`ztuvwxynopqrslmijhk{|}~OPQRSKLMNT[\   !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIIJKLMNOPQRSTUVWXYZ[\]^_`abcdeffghijklmnopqrstuvwxxyz{|}~                                      XYOVW                                                                        hasmtlib-1.1.2-inplaceLanguage.Hasmtlib.BooleanLanguage.Hasmtlib.Integraled!Language.Hasmtlib.Internal.Render!Language.Hasmtlib.Internal.BitvecLanguage.Hasmtlib.Type.ArrayMapLanguage.Hasmtlib.Type.ExprLanguage.Hasmtlib.IteableLanguage.Hasmtlib.EquatableLanguage.Hasmtlib.OrderableLanguage.Hasmtlib.Type.OptionLanguage.Hasmtlib.Type.SolutionLanguage.Hasmtlib.CodecLanguage.Hasmtlib.Type.MonadSMTLanguage.Hasmtlib.Type.SMT!Language.Hasmtlib.Internal.ParserLanguage.Hasmtlib.Type.PipeLanguage.Hasmtlib.Solver.CommonLanguage.Hasmtlib.Solver.Z3Language.Hasmtlib.Solver.Yices Language.Hasmtlib.Solver.MathSATLanguage.Hasmtlib.Solver.CVC5Language.Hasmtlib.Type.SolverLanguage.Hasmtlib.VariablehasmtlibLanguage.Hasmtlib.Internal.Expr#Language.Hasmtlib.Internal.Expr.NumLanguage.HasmtlibBooleanbooltruefalse&&||==>notxorandornandnorallany$fBooleanVector $fBooleanBit $fBooleanBool IntegraledquotremdivmodquotRemdivMod$fIntegraledConst$fIntegraledIdentity$fIntegraledWord64$fIntegraledWord32$fIntegraledWord16$fIntegraledWord8$fIntegraledNatural$fIntegraledWord$fIntegraledInteger$fIntegraledIntRenderrender renderUnary renderBinary renderTernary$fRenderBuilder$fRenderDouble$fRenderInteger$fRenderNatural $fRenderBoolBitvecunBitvec bvReverse bvReplicate bvReplicate' bvGeneratebvConcatbvTake'bvDrop' bvSplitAt'bvToList bvFromListN bvFromListN'bvRotLbvRotRbvShLbvLShR bvZeroExtend bvExtract$fIntegralBitvec $fRealBitvec $fEnumBitvec$fBoundedBitvec $fNumBitvec$fRenderBitvec $fShowBitvec $fEqBitvec $fOrdBitvec$fBooleanBitvec ConstArray _arrConst_storedArrayMapasConst' viewConst arrSelectarrStoreasConst$fShowConstArray$fEqConstArray$fOrdConstArray$fFunctorConstArray$fFoldableConstArray$fTraversableConstArrayarrConststored$fArrayMapConstArraykvSMTVar_varIdSMTSortBoolSortIntSortRealSortBvSort ArraySortExprSomeKnownSMTSort SomeSMTSortAllC KnownSMTSortsortSingSSMTSortSIntSort SRealSort SBoolSortSBvSort SArraySortValueIntValue RealValue BoolValueBvValue ArrayValue HaskellTypevarId unwrapValue wrapValue sortSing'Iteableite$fIteableExpr(,,,,,,,)$fIteableExpr(,,,,,,)$fIteableExpr(,,,,,)$fIteableExpr(,,,,)$fIteableExpr(,,,)$fIteableExpr(,,)$fIteableExpr(,)$fIteableExpr()$fIteableExprTree$fIteableExprSeq$fIteableExprMaybe$fIteableExprList$fIteableBoola$fIteableExprExpr GEquatable===# Equatable===/==$fGEquatablekM1$fGEquatablek:+:$fGEquatablek:*:$fGEquatablekV1$fGEquatablekU1$fEquatableBool$fEquatableOrdering$fEquatableDouble$fEquatableFloat$fEquatableChar$fEquatableInt64$fEquatableInt32$fEquatableInt16$fEquatableInt8$fEquatableWord64$fEquatableWord32$fEquatableWord16$fEquatableWord8$fEquatableWord$fEquatableNatural$fEquatableInteger$fEquatableInt$fEquatableVoid $fEquatable()$fGEquatablekK1$fEquatableExpr GOrderable=??min'max'$fGOrderablekM1$fGOrderablek:+:$fGOrderablek:*:$fGOrderablekV1$fGOrderablekU1$fOrderableBool$fOrderableOrdering$fOrderableDouble$fOrderableFloat$fOrderableChar$fOrderableInt64$fOrderableInt32$fOrderableInt16$fOrderableInt8$fOrderableWord64$fOrderableWord32$fOrderableWord16$fOrderableWord8$fOrderableWord$fOrderableNatural$fOrderableInteger$fOrderableInt$fOrderableVoid $fOrderable()$fGOrderablekK1$fOrderableExpr$fOrderableExpr0$fOrderableExpr1for_allexistsselectstore SMTOption PrintSuccess ProduceModels Incremental$fRenderSMTOption$fShowSMTOption $fEqSMTOption$fOrdSMTOption$fDataSMTOption SMTVarSol_solVar_solVal IntValueMapSolutionResultUnsatUnknownSatSolver$fShowSMTVarSol$fShowIntValueMap$fSemigroupIntValueMap$fMonoidIntValueMap $fShowResult $fEqResult $fOrdResultSomeKnownOrdSMTSortOrdHaskellTypesolValsolVarfromSomeVarSols$fOrdHaskellTypetCodecDecodeddecodeencodeDefaultDecoded $fCodecEither $fCodecTree $fCodecSeq $fCodecMaybe $fCodecMap $fCodecIntMap $fCodecList$fCodec(,,,,,,,)$fCodec(,,,,,,)$fCodec(,,,,,) $fCodec(,,,,) $fCodec(,,,) $fCodec(,,) $fCodec(,) $fCodec() $fCodecExpr MonadIncrSMTpushpopcheckSatgetModelgetValueMonadSMTsmtvar'var'assert setOptionsetLogicvarsmtvarconstantquantifysolveSMT _lastVarId_vars _formulas_mlogic_optionsformulas lastVarIdmlogicoptionsvars renderSMTrenderSetLogicrenderDeclareVar renderAssert renderVars$fMonadSMTSMTm $fDefaultSMT answerParser resultParseranyModelParserdefaultModelParsersmt2ModelParser parseSomeSol parseSomeSortparseSomeBitVecSortparseSomeArraySort parseExpr' parseExpr constantExpr anyBitvector binBitvector hexBitvectorliteralBitvector constArray parseSelect parseStoreunarybinarynarysmtPi toRealFuntoIntFunisIntFunsmtIteanyValue negativeValueparseRatioDoubleparseToRealDouble parseBoolgetValueParserPipe_lastPipeVarId _mPipeLogic_pipe lastPipeVarId mPipeLogicpipe$fMonadIncrSMTPipem$fMonadSMTPipemDebuggerdebugSMT debugProblemdebugResultResponsedebugModelResponse ProcessSolverconfsolverdebuginteractiveSolver processSolver$fDefaultDebuggerz3yicesmathsatcvc5 WithSolver withSolver solveWithinteractiveWith$fWithSolverPipeVariablevariable variable'$fVariableEither$fVariableMaybe$fVariable(,,,,,,,)$fVariable(,,,,,,)$fVariable(,,,,,)$fVariable(,,,,)$fVariable(,,,)$fVariable(,,) $fVariable(,) $fVariable()$fVariableExprghc-prim GHC.TypesBoolTrueFalsebaseGHC.RealIntegral Data.ProxyProxyInt ConstraintTypeExistsForAllArrStore ArrSelectBvuGTBvuGTHEBvuLTHEBvuLTBvRotRBvRotLBvConcatBvLShRBvShLBvuRemBvuDivBvMulBvSubBvAddBvNegBvNorBvNandBvXorBvOrBvAndBvNotIteIsIntToIntToRealAtanAcosAsinTanCosSinSqrtPiImplOrGTHGTHEEQULTHELTHIDivAbsMulNegVarDistinctConstantPlusExpAndXorNotModDivrenderQuantifiercontainers-0.6.7Data.IntMap.InternalIntMapdependent-map-0.4.0.0-a235545eda2a655cdf4cca7553296c6e52185aba051d72a70533c94f0bc4bc64Data.Dependent.Map.InternalDMap GHC.ClassesOrd mtl-2.3.1Control.Monad.State.Class MonadStatesmtlib-backends-0.4-a9c505a407ca53fe5ef7bbf9365df419d6877a7eb53d306b16f5e1090373c050SMTLIB.BackendsQueuingsmtlib-backends-process-0.3-b353a0edeac87a3e0972eb107fa8d536f76668e82c2c042ffbac6a54a1744dafSMTLIB.Backends.ProcessConfigHandle GHC.MaybeJust