úÎa›Z¡}      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|Safe"#V†m;Log messages with minimal formatting. Mostly for debugging.Log a message.Increase indentation.Decrease indentation.An interactive solver process. Send a command to the solver. Terminate the solver. 7S-expressions. These are the basic format for SmtLib-2.&Common values returned by SMT solvers. Boolean valueIntegral valueRational valueBit vector: width, valueSome other value'Results of checking for satisfiability.The assertions are satisfiable The assertions are unsatisfiableThe result is inconclusiveShow an s-expression.Parse an s-expression.Start a new solver process.Load the contents of a file.}Load a raw SMT string.%A command with no interesting result.AA command entirely made out of atoms, with no interesting result.¡Run a command and return True if successful, and False if unsupported. This is useful for setting options that unsupported by some solvers, but used by others.Set a solver option. BSet a solver option, returning False if the option is unsupported.!<Set the solver's logic. Usually, this should be done first."DSet the solver's logic, returning False if the logic is unsupported.#%Checkpoint state. A special case of %.$0Restore to last check-point. A special case of &.%Push multiple scopes.&Pop multiple scopes.'DExecute the IO action in a new solver scope (push before, pop after)(/Declare a constant. A common abbreviation for )J. For convenience, returns an the declared name as a constant expression.)jDeclare a function or a constant. For convenience, returns an the declared name as a constant expression.*9Declare an ADT using the format introduced in SmtLib 2.6.+/Declare a constant. A common abbreviation for )F. For convenience, returns the defined name as a constant expression.,hDefine a function or a constant. For convenience, returns an the defined name as a constant expression.-Assume a fact..4Check if the current set of assertion is consistent.~#Convert an s-expression to a value./:Get the values of some s-expressions. Only valid after a  result.0JGet the values of some constants in the current model. A special case of /. Only valid after a  result.1%Get the value of a single expression.2#Get the value of a single constant.3?A constant, corresponding to a family indexed by some integers.4An SMT function.5$An SMT constant. A special case of 4.6The type of integers.7The type of booleans.8The type of reals.9The type of arrays.:The type of bit vectors.;Boolean literals.<Integer literals.=Real (well, rational) literals.>#A bit vector represented in binary.GIf the value does not fit in the bits, then the bits will be increased.&The width should be strictly positive.? A bit vector represented in hex.zIf the value does not fit in the bits, the bits will be increased to the next multiple of 4 that will fit the value.OIf the width is not a multiple of 4, it will be rounded up so that it is.&The width should be strictly positive.@Render a value as an expression. Bit-vectors are rendered in hex, if their width is a multiple of 4, and in binary otherwise.ALogical negation.B Conjunction.D Disjunction.F Exclusive-or.G Implication.HIIf-then-else. This is polymorphic and can be used to construct any term.I Equality.K Greater-thenL Less-then.MGreater-than-or-equal-to.NLess-than-or-equal-to.O"Unsigned less-than on bit-vectors.P+Unsigned less-than-or-equal on bit-vectors.Q Signed less-than on bit-vectors.R)Signed less-than-or-equal on bit-vectors.SAddition. See also fU Subtraction.V6Arithmetic negation for integers and reals. See also e.WMultiplication.XAbsolute value.YInteger division.ZModulus.[.Is the number divisible by the given constant.\Division of real numbers.]Bit vector concatenation.^-Extend to the signed equivalent bitvector by i bits_;Extend with zeros to the unsigned equivalent bitvector by i bits`'Extract a sub-sequence of a bit vector.aBitwise negation.bBitwise conjuction.cBitwise disjunction.dBitwise exclusive or.eBit vector arithmetic negation.fAddition of bit vectors.gSubtraction of bit vectors.hMultiplication of bit vectors.iBit vector unsigned division.jBit vector unsigned reminder.kBit vector signed division.lBit vector signed reminder.m Shift left.nLogical shift right.o4Arithemti shift right (copies most significant bit).pGet an elemeent of an array.qUpdate an arrayrRRun an IO action with the logger set to a specific level, restoring it when done.t&Log a message at a specific log level.urA simple stdout logger. Shows only messages logged at a level that is greater than or equal to the passed level.  Executable  Arguments Optional logging here *datatype name sort parameters  constructors + New symbol  Symbol type Symbol definition , New symbol Parameters, with types Type of result  Definition 9Type of indexes Type of elements :Number of bits >Width, in bits Value ?Width, in bits Value mvalue  shift amount nvalue  shift amount ovalue  shift amount parray index qarray index  new value v  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuv  urts!" #%$&'()*+,-./1023456789:<=;>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]`aebdcfghijklmno^_pq        !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~%simple-smt-0.8-JvCYGcBzHRP4Nbrdtc7Y3A SimpleSMTLogger logMessagelogLevel logSetLevellogTablogUntabSolvercommandstopSExprAtomListValueBoolIntRealBitsOtherResultSatUnsatUnknown showsSExpr readSExpr newSolverloadFile ackCommand simpleCommandsimpleCommandMaybe setOptionsetOptionMaybesetLogic setLogicMaybepushpoppushManypopMany inNewScopedeclare declareFundeclareDatatypedefine defineFunassertcheckgetExprs getConstsgetExprgetConstfamfunconsttInttBooltRealtArraytBitsboolintrealbvBinbvHexvaluenotandandManyororManyxorimpliesiteeqdistinctgtltgeqleqbvULtbvULeqbvSLtbvSLeqaddaddManysubnegmulabsdivmod divisiblerealDivconcat signExtend zeroExtendextractbvNotbvAndbvOrbvXOrbvNegbvAddbvSubbvMulbvUDivbvURembvSDivbvSRembvShlbvLShrbvAShrselectstore withLogLevel logIndented logMessageAt newLogger $fEqResult $fShowResult $fEqSExpr $fOrdSExpr $fShowSExpr $fEqValue $fShowValue loadString sexprToVal