h*J@      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                1.3.0 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= hasmtlib<-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 .hasmtlib5Unsigned and length-indexed bitvector with MSB first..0/123456789:;<=>?@A.0/123456789:;<=>?@A Safe-Inferred ")19LhasmtlibA map-like array with a default constant value and partially overwritten values. PhasmtlibClass 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)Uhasmtlib Wrapper for Q which hides the  LONMPTSRQU\] PTSRQULONM]\ Safe-Inferred  ")11_hasmtlib? y assert $ x === min' 42 100 hasmtlib!Minimum of two as SMT-Expression.hasmtlib!Maximum of two as SMT-Expression.  4444 Safe-Inferred")1`  Safe-Inferred")1hasmtlibOut of many bool-expressions build a formula which encodes that at most k of them are truehasmtlibOut of many bool-expressions build a formula which encodes that at least k of them are truehasmtlibOut of many bool-expressions build a formula which encodes that exactly k of them are true Safe-Inferred"()1 hasmtlib4Test multiple expressions on equality within in the SMT -Problem.hasmtlib8Test multiple expressions on distinctness within in the SMT -Problem.hasmtlib,A universal quantification for any specific b. 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 b 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.hasmtlibBitvector shift lefthasmtlibBitvector logical shift righthasmtlibConcat two bitvectorshasmtlibRotate bitvector lefthasmtlibRotate bitvector right,bdcefg_`a|{uvwxyz}~opqrstmnjkilh,bdcefg_`a|{uvwxyz}~opqrstmnjkilh  Safe-Inferred")1 ]hasmtlibOptions for SMT-Solvers.hasmtlib$Print "success" after each operationhasmtlib>Produce a satisfying assignment after each successful checkSathasmtlibIncremental solving  Safe-Inferred ")1#8 hasmtlib!A solution for a single variable.hasmtlibA variable in the SMT-Problemhasmtlib-An assignment for this variable in a solutionhasmtlib Newtype for  u( so we can use it as right-hand-side of .hasmtlibA Solution is a dependent map  from os 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 b with an  { hasmtlibAlias class for constraint  ({ t)hasmtlib Create a  from some s.  Safe-Inferred ")1=$hasmtlib)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-hasmtlibA ! 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/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-Optionshasmtlib Render a -Problem to SMTLib2-Syntax. Each element of the returned Sequence is a line. Safe-Inferred")10=## Safe-Inferred ")12hasmtlibA 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")15hasmtlib0A 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")161 Safe-Inferred")16b Safe-Inferred")16 Safe-Inferred")16 Safe-Inferred")1=hasmtlibData 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 $ Incremental True 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 hasmtlibConstruct a variable datum of a data-type by creating variables for all its fields. 8 data V3 a = V3 a a a instance Variable a => V3 a /varV3 <- variable @(V3 (Expr RealType)) ; varV33 V3 (Var RealType) (Var RealType) (Var RealType)hasmtlib Wrapper for  which takes a  Safe-Inferred")1>hbdcefg_`a{uvwxyzopqrstmnjkil|}~PQRSTLMNOU\]   !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKKLMNOPQRSTUVWXYZ[\]^_`abcdefghhijklmnopqrstuvwxyzz{|}~                                         Z[QXY                                                       hasmtlib-1.3.0-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.CountingLanguage.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 renderNary$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$fOrderableExpr1atMostatLeastexactlyequaldistinctfor_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-e48e6cfc5b05a63d77db592c35689ed45354f1c624d15434e8672fe9374cbdedData.Dependent.Map.InternalDMap GHC.ClassesOrd mtl-2.3.1Control.Monad.State.Class MonadStatesmtlib-backends-0.4-e22f6c2dcc3539aa92c2f01afc2f30e6be9843764844b4a0de19b127cfd8f50eSMTLIB.BackendsQueuingsmtlib-backends-process-0.3-190155361ed45443722304f1143df316732c4674a60f75737e3e87f29125e4e4SMTLIB.Backends.ProcessConfigHandle GHC.MaybeJust