Packages

class SimpleAPI extends AnyRef

API that simplifies the use of the prover; this tries to collect various functionality in one place, and provides an imperative API similar to the SMT-LIB command language.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SimpleAPI
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. def !!(assertion: IFormula): Unit

    Add an assertion to the prover: assume that the given formula is true

  2. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  3. final def ##: Int
    Definition Classes
    AnyRef → Any
  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def ??(conc: IFormula): Unit

    Add a conclusion to the prover: assume that the given formula is false.

    Add a conclusion to the prover: assume that the given formula is false. Adding conclusions will switch the prover to "validity" mode; from this point on, the prover answers with the status Valid/Invalid instead of Unsat/Sat.

  6. def ???: SimpleAPI.ProverStatus.Value

    Determine the status of the formulae asserted up to this point.

    Determine the status of the formulae asserted up to this point. This call is blocking, but will not run the prover repeatedly if nothing has changed since the last check.

  7. def abbrev(f: IFormula, rawName: String): IFormula

    Introduce and return a function representing the given formula f.

    Introduce and return a function representing the given formula f. This method can be used to represent dag-like formulas (which might grow exponentially when expanded to a tree) concisely. Abbreviations can also speed up handling of large numbers of queries with big expressions, since the abbreviated formulas are only translated once to internal datastructures.

  8. def abbrev(f: IFormula): IFormula

    Introduce and return a function representing the given formula f.

    Introduce and return a function representing the given formula f. This method can be used to represent dag-like formulas (which might grow exponentially when expanded to a tree) concisely. Abbreviations can also speed up handling of large numbers of queries with big expressions, since the abbreviated formulas are only translated once to internal datastructures.

  9. def abbrev(t: ITerm, rawName: String): ITerm

    Introduce and return a function representing the given term t.

    Introduce and return a function representing the given term t. This method can be used to represent dag-like terms (which might grow exponentially when expanded to a tree) concisely. Abbreviations can also speed up handling of large numbers of queries with big terms, since the abbreviated terms are only translated once to internal datastructures.

  10. def abbrev(t: ITerm): ITerm

    Introduce and return a function representing the given term t.

    Introduce and return a function representing the given term t. This method can be used to represent dag-like terms (which might grow exponentially when expanded to a tree) concisely. Abbreviations can also speed up handling of large numbers of queries with big terms, since the abbreviated terms are only translated once to internal datastructures.

  11. def abbrevSharedExpressions(t: IFormula, sizeThreshold: Int): IFormula

    Abbreviate (large) shared sub-expressions.

    Abbreviate (large) shared sub-expressions. This method avoids the worst-case exponential blow-up resulting from expressions with nested shared sub-expressions.

  12. def abbrevSharedExpressions(t: ITerm, sizeThreshold: Int): ITerm

    Abbreviate (large) shared sub-expressions.

    Abbreviate (large) shared sub-expressions. This method avoids the worst-case exponential blow-up resulting from expressions with nested shared sub-expressions.

  13. def abbrevSharedExpressions(t: IFormula): IFormula

    Abbreviate (large) shared sub-expressions.

    Abbreviate (large) shared sub-expressions. This method avoids the worst-case exponential blow-up resulting from expressions with nested shared sub-expressions.

  14. def abbrevSharedExpressions(t: ITerm): ITerm

    Abbreviate (large) shared sub-expressions.

    Abbreviate (large) shared sub-expressions. This method avoids the worst-case exponential blow-up resulting from expressions with nested shared sub-expressions.

  15. def abbrevSharedExpressions(t: IExpression, sizeThreshold: Int): IExpression

    Abbreviate (large) shared sub-expressions.

    Abbreviate (large) shared sub-expressions. This method avoids the worst-case exponential blow-up resulting from expressions with nested shared sub-expressions.

  16. def abbrevSharedExpressions(t: IExpression): IExpression

    Abbreviate (large) shared sub-expressions.

    Abbreviate (large) shared sub-expressions. This method avoids the worst-case exponential blow-up resulting from expressions with nested shared sub-expressions.

  17. def abbrevSharedExpressionsWithMap(t: IExpression, sizeThreshold: Int): (IExpression, Map[IExpression, IExpression])

    Abbreviate (large) shared sub-expressions.

    Abbreviate (large) shared sub-expressions. This method avoids the worst-case exponential blow-up resulting from expressions with nested shared sub-expressions. This method also returns a map with the created abbreviations.

  18. def addAbbrev(abbrevFor: IFormula, fullFor: IFormula): IFormula

    Add an abbreviation introduced in a different SimpleAPI instance.

  19. def addAbbrev(abbrevTerm: ITerm, fullTerm: ITerm): ITerm

    Add an abbreviation introduced in a different SimpleAPI instance.

  20. def addAssertion(assertion: Formula): Unit

    Add an assertion to the prover: assume that the given formula is true

  21. def addAssertion(assertion: IFormula): Unit

    Add an assertion to the prover: assume that the given formula is true

  22. def addAssertionPreproc(assertion: Formula): Unit

    Add an assertion that is already fully preprocessed to the prover: assume that the given formula is true

  23. def addBooleanVariable(f: IFormula): Unit

    Add an externally defined boolean variable to the environment of this prover.

  24. def addBooleanVariables(fs: Iterable[IFormula]): Unit

    Add a sequence of externally defined boolean variables to the environment of this prover.

  25. def addConclusion(conc: Formula): Unit

    Add a conclusion to the prover: assume that the given formula is false.

    Add a conclusion to the prover: assume that the given formula is false. Adding conclusions will switch the prover to "validity" mode; from this point on, the prover answers with the status Valid/Invalid instead of Unsat/Sat.

  26. def addConclusion(conc: IFormula): Unit

    Add a conclusion to the prover: assume that the given formula is false.

    Add a conclusion to the prover: assume that the given formula is false. Adding conclusions will switch the prover to "validity" mode; from this point on, the prover answers with the status Valid/Invalid instead of Unsat/Sat.

  27. def addConclusionPreproc(conc: Formula): Unit

    Add a conclusion that has already been fully preprocessed to the prover: assume that the given formula is false.

    Add a conclusion that has already been fully preprocessed to the prover: assume that the given formula is false. Adding conclusions will switch the prover to "validity" mode; from this point on, the prover answers with the status Valid/Invalid instead of Unsat/Sat.

  28. def addConstant(t: ITerm): Unit

    Add an externally defined constant to the environment of this prover.

  29. def addConstantRaw(c: ConstantTerm): Unit

    Add an externally defined constant to the environment of this prover.

  30. def addConstants(ts: Iterable[ITerm]): Unit

    Add a sequence of externally defined constants to the environment of this prover.

  31. def addConstantsRaw(cs: Iterable[ConstantTerm]): Unit

    Add a sequence of externally defined constant to the environment of this prover.

  32. def addFunction(f: BooleanFunApplier, functionalityMode: SimpleAPI.FunctionalityMode.Value): Unit

    Add an externally defined function to the environment of this prover.

  33. def addFunction(f: BooleanFunApplier): Unit

    Add an externally defined function to the environment of this prover.

  34. def addFunction(f: IFunction, functionalityMode: SimpleAPI.FunctionalityMode.Value): Unit

    Add an externally defined function to the environment of this prover.

  35. def addFunction(f: IFunction): Unit

    Add an externally defined function to the environment of this prover.

  36. def addRelation(p: Predicate): Unit

    Add an externally defined relation to the environment of this prover.

  37. def addRelations(ps: Iterable[Predicate]): Unit

    Add a sequence of externally defined relations to the environment of this prover.

  38. def addTheories(newTheories: Seq[Theory]): Unit

    Add new theories to the prover.

    Add new theories to the prover. Normally, calling this function is not necessary, since theories in asserted formulae will be detected automatically.

  39. def addTheoriesFor(order: TermOrder): Unit

    Add all theories to the prover that occur in the given order.

  40. def addTheory(newTheory: Theory): Unit

    Add a new theory to the prover.

    Add a new theory to the prover. Normally, calling this function is not necessary, since theories in asserted formulae will be detected automatically.

  41. def asConjunction(f: IFormula): Conjunction

    Convert a formula in input syntax to the internal prover format.

  42. def asIFormula(c: Conjunction): IFormula

    Convert a formula from the internal prover format to input syntax.

  43. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  44. def backtrackToL0: Unit

    For a stopped prover, make sure that all assumptions of the depth-first search are undone.

  45. def certificateAsString(partNames: Map[Int, PartName], format: parameters.Param.InputFormat.Value): String

    After receiving the result ProverStatus.Unsat or ProverStates.Valid, produce a certificate in textual/readable format.

  46. def checkSat(block: Boolean): SimpleAPI.ProverStatus.Value

    Check satisfiability of the currently asserted formulae.

    Check satisfiability of the currently asserted formulae. Will block until completion if block argument is true, otherwise return immediately.

  47. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  48. def completeModel: Evaluator

    Produce a model, i.e., an interpretation of constants, functions, and predicates.

    Produce a model, i.e., an interpretation of constants, functions, and predicates. This method can be called in two situations after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive. The evaluator representing the model has to be shut down explicitly after use, by calling its method Evaluator.shutDown.

  49. implicit def convert2RichMulTerm(term: ITerm): RichMulTerm

    Convert a term to a rich term, offering operations mul, div, mod, etc., for non-linear arithmetic.

  50. def createADT(sortNames: Seq[String], ctorSignatures: Seq[(String, CtorSignature)], measure: theories.ADT.TermMeasure.Value = ADT.TermMeasure.RelDepth): ADT

    Create an algebraic data-type.

    Create an algebraic data-type.

    TODO: logging

  51. def createBooleanFunction(rawName: String, argSorts: Seq[Sort], partial: Boolean = false, functionalityMode: SimpleAPI.FunctionalityMode.Value = FunctionalityMode.Full): BooleanFunApplier

    Create a new uninterpreted Boolean-valued function with given arguments.

    Create a new uninterpreted Boolean-valued function with given arguments. Booleans values are encoded into integers, mapping true to 0 and false to 1.
    In contrast to predicates (generated using createRelation), Boolean functions can be used within triggers.

  52. def createBooleanFunction(rawName: String, arity: Int, functionalityMode: SimpleAPI.FunctionalityMode.Value): BooleanFunApplier

    Create a new uninterpreted Boolean-valued function with fixed arity.

    Create a new uninterpreted Boolean-valued function with fixed arity. Booleans values are encoded into integers, mapping true to 0 and false to 1.
    In contrast to predicates (generated using createRelation), Boolean functions can be used within triggers.

  53. def createBooleanFunction(rawName: String, arity: Int): BooleanFunApplier

    Create a new uninterpreted Boolean-valued function with fixed arity.

    Create a new uninterpreted Boolean-valued function with fixed arity. Booleans values are encoded into integers, mapping true to 0 and false to 1.
    In contrast to predicates (generated using createRelation), Boolean functions can be used within triggers.

  54. def createBooleanVariable: IFormula

    Create a new Boolean variable (nullary predicate) with predefined name.

  55. def createBooleanVariable(rawName: String): IFormula

    Create a new Boolean variable (nullary predicate).

  56. def createBooleanVariables(num: Int): IndexedSeq[IFormula]

    Create num new Boolean variable (nullary predicate) with predefined name.

  57. def createConstant(sort: Sort): ITerm

    Create a new symbolic constant with predefined name and given sort.

  58. def createConstant: ITerm

    Create a new symbolic constant with predefined name.

  59. def createConstant(rawName: String, sort: Sort): ITerm

    Create a new symbolic constant with given sort.

  60. def createConstant(rawName: String): ITerm

    Create a new symbolic constant.

  61. def createConstantRaw(rawName: String, sort: Sort): ConstantTerm

    Create a new symbolic constant, without directly turning it into an ITerm.

    Create a new symbolic constant, without directly turning it into an ITerm. This method is only useful when working with formulae in the internal prover format.

  62. def createConstantRaw(rawName: String): ConstantTerm

    Create a new symbolic constant, without directly turning it into an ITerm.

    Create a new symbolic constant, without directly turning it into an ITerm. This method is only useful when working with formulae in the internal prover format.

  63. def createConstants(prefix: String, nums: Range, sort: Sort): IndexedSeq[ITerm]

    Create a sequence of new symbolic constants, with name starting with the given prefix and the given sort.

  64. def createConstants(prefix: String, nums: Range): IndexedSeq[ITerm]

    Create a sequence of new symbolic constants, with name starting with the given prefix.

  65. def createConstants(num: Int, sort: Sort): IndexedSeq[ITerm]

    Create num new symbolic constants with predefined name and given sort.

  66. def createConstants(num: Int): IndexedSeq[ITerm]

    Create num new symbolic constants with predefined name.

  67. def createConstantsRaw(prefix: String, nums: Range, sort: Sort): IndexedSeq[ConstantTerm]

    Create a sequence of new symbolic constants, without directly turning them into an ITerm.

    Create a sequence of new symbolic constants, without directly turning them into an ITerm. This method is only useful when working with formulae in the internal prover format.

  68. def createConstantsRaw(prefix: String, nums: Range): IndexedSeq[ConstantTerm]

    Create a sequence of new symbolic constants, without directly turning them into an ITerm.

    Create a sequence of new symbolic constants, without directly turning them into an ITerm. This method is only useful when working with formulae in the internal prover format.

  69. def createExistentialConstant(sort: Sort): ITerm

    Create a new symbolic constant with predefined name and given sort that is implicitly existentially quantified.

  70. def createExistentialConstant: ITerm

    Create a new symbolic constant with predefined name that is implicitly existentially quantified.

  71. def createExistentialConstant(rawName: String, sort: Sort): ITerm

    Create a new symbolic constant with given sort that is implicitly existentially quantified.

  72. def createExistentialConstant(rawName: String): ITerm

    Create a new symbolic constant that is implicitly existentially quantified.

  73. def createExistentialConstants(num: Int, sort: Sort): IndexedSeq[ITerm]

    Create num new symbolic constant with predefined name that is implicitly existentially quantified.

  74. def createExistentialConstants(num: Int): IndexedSeq[ITerm]

    Create num new symbolic constant with predefined name that is implicitly existentially quantified.

  75. def createFunction(rawName: String, argSorts: Seq[Sort], resSort: Sort, partial: Boolean = false, functionalityMode: SimpleAPI.FunctionalityMode.Value = FunctionalityMode.Full): IFunction

    Create a new uninterpreted function with given sorts, and chose whether the function is partial, and to which degree functionality axioms should be generated.

  76. def createFunction(rawName: String, arity: Int, functionalityMode: SimpleAPI.FunctionalityMode.Value): IFunction

    Create a new uninterpreted function with fixed arity, and chose to which degree functionality axioms should be generated.

  77. def createFunction(rawName: String, arity: Int): IFunction

    Create a new uninterpreted function with fixed arity.

  78. def createInfUninterpretedSort(name: String): InfUninterpretedSort

    Create a new uninterpreted sort of infinite cardinality.

    Create a new uninterpreted sort of infinite cardinality.

    TODO: logging

  79. def createRelation(rawName: String, argSorts: Seq[Sort]): Predicate

    Create a new uninterpreted predicate with the given arguments.
    Predicates are more low-level than Boolean functions, and cannot be used within triggers.

  80. def createRelation(rawName: String, arity: Int): Predicate

    Create a new uninterpreted predicate with fixed arity.
    Predicates are more low-level than Boolean functions, and cannot be used within triggers.

  81. def createUninterpretedSort(name: String): UninterpretedSort

    Create a new uninterpreted sort of finite or infinite cardinality.

    Create a new uninterpreted sort of finite or infinite cardinality.

    TODO: logging

  82. val decoderContext: DecoderContext

    Decoding data needed (and implicitly read) by theories; this will access the current model to extract the relevant decoding data.

  83. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  84. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  85. def eval(f: IFormula): Boolean

    Evaluate the given formula in the current model.

    Evaluate the given formula in the current model. This method can only be called after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive.

  86. def eval(c: ConstantTerm): IdealInt

    Evaluate the given symbol in the current model, returning None in case the model does not completely determine the value of the symbol.

    Evaluate the given symbol in the current model, returning None in case the model does not completely determine the value of the symbol. This method can be called in two situations:

    • after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive, or which case the term is evaluated in the computed model, or
    • after receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants. In this case the queried term t may only consist of existential constants.
  87. def eval(t: ITerm): IdealInt

    Evaluate the given term in the current model.

    Evaluate the given term in the current model. This method can be called in two situations:

    • after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive, which case the term is evaluated in the computed model, or
    • after receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants. In this case the queried term t may only consist of existential constants.
  88. def evalPartial(f: IFormula): Option[Boolean]

    Evaluate the given formula in the current model, returning None in case the model does not completely determine the value of the formula.

    Evaluate the given formula in the current model, returning None in case the model does not completely determine the value of the formula. This method can only be called after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive.

  89. def evalPartial(c: ConstantTerm): Option[IdealInt]

    Evaluate the given symbol in the current model, returning None in case the model does not completely determine the value of the symbol.

    Evaluate the given symbol in the current model, returning None in case the model does not completely determine the value of the symbol. This method can be called in two situations:

    • after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive, or which case the term is evaluated in the computed model, or
    • after receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants. In this case the queried term t may only consist of existential constants.
  90. def evalPartial(t: ITerm): Option[IdealInt]

    Evaluate the given term in the current model, returning None in case the model does not completely determine the value of the term.

    Evaluate the given term in the current model, returning None in case the model does not completely determine the value of the term. This method can be called in two situations:

    • after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive, or which case the term is evaluated in the computed model, or
    • after receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants. In this case the queried term t may only consist of existential constants.
  91. def evalPartialAsTerm(c: ConstantTerm): Option[ITerm]

    Evaluate the given symbol in the current model to a constructor term, returning None in case the model does not completely determine the value of the term.

    Evaluate the given symbol in the current model to a constructor term, returning None in case the model does not completely determine the value of the term. This method can be called after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive.

  92. def evalPartialAsTerm(t: ITerm): Option[ITerm]

    Evaluate the given term in the current model to a constructor term, returning None in case the model does not completely determine the value of the term.

    Evaluate the given term in the current model to a constructor term, returning None in case the model does not completely determine the value of the term. This method can be called after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive.

  93. def evalToTerm(c: ConstantTerm): ITerm

    Evaluate the given symbol in the current model to a constructor term.

    Evaluate the given symbol in the current model to a constructor term. This method can be called after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive.

  94. def evalToTerm(t: ITerm): ITerm

    Evaluate the given term in the current model to a constructor term.

    Evaluate the given term in the current model to a constructor term. This method can be called after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive.

  95. def evaluatorStarted: Unit
    Attributes
    protected[api]
  96. def evaluatorStopped: Unit
    Attributes
    protected[api]
  97. def execSMTLIB(input: Reader): Unit

    Execute an SMT-LIB script.

    Execute an SMT-LIB script. Symbols declared in the script will be added to the prover; however, if the prover already knows about symbols with the same name, they will be reused.

  98. def extractSMTLIBAssertions(input: Reader): Seq[IFormula]

    Extract the assertions in an SMT-LIB script.

    Extract the assertions in an SMT-LIB script. Symbols declared in the script will be added to the prover; however, if the prover already knows about symbols with the same name, they will be reused.

  99. def extractSMTLIBAssertionsSymbols(input: Reader, fullyInline: Boolean = false): (Seq[IFormula], Map[IFunction, SMTFunctionType], Map[ConstantTerm, SMTType], Map[Predicate, SMTFunctionType])

    Extract assertions and declared symbols in an SMT-LIB script.

    Extract assertions and declared symbols in an SMT-LIB script. Symbols declared in the script will be added to the prover; however, if the prover already knows about symbols with the same name, they will be reused. If option fullyInline is set, let-definitions and defined functions will be inlined in the extracted formulas.

  100. def getCertificate: Certificate

    After receiving the result ProverStatus.Unsat or ProverStates.Valid, produce an (unsimplified) certificate.

  101. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  102. def getConstraint: IFormula

    After receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants, return a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants.

  103. def getConstraintFull(negate: Boolean = false, minimise: Boolean = false): IFormula

    After receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants, return a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants.

  104. def getConstraintRaw: Conjunction

    After receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants, return a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants.

  105. def getInterpolants(partitions: Seq[Set[Int]], maxQETime: Long = Long.MaxValue): Seq[IFormula]

    Compute an inductive sequence of interpolants, for the given partitioning of the input problem.

  106. def getMinimisedConstraint: IFormula

    After receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants, return a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants.

    After receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants, return a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants. The produced constraint is simplified and minimised.

  107. def getNegatedConstraint: IFormula

    After receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants, return the negation of a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants.

  108. def getStatus(timeout: Long): SimpleAPI.ProverStatus.Value

    Query result of the last checkSat or nextModel call.

    Query result of the last checkSat or nextModel call. Will block until a result is available, or until timeout milli-seconds elapse.

  109. def getStatus(block: Boolean): SimpleAPI.ProverStatus.Value

    Query result of the last checkSat or nextModel call.

    Query result of the last checkSat or nextModel call. Will block until a result is available if block argument is true, otherwise return immediately.

  110. def getSymbolMap: Map[String, AnyRef]

    Create a map with all declared symbols known to this prover.

  111. def getTreeInterpolant(partitions: Tree[Set[Int]], maxQETime: Long = Long.MaxValue): Tree[IFormula]

    compute a tree interpolant for the given specification.

    compute a tree interpolant for the given specification. Interpolants might contain quantifiers, which cannot always be eliminated efficiently; the provided timeout (milliseconds) specifies how long it is attempted to eliminated quantifiers in each interpolant. If QE fails, interpolants with quantifiers are returned instead.

  112. def getUnsatCore: Set[Int]

    After receiving the result ProverStatus.Unsat or ProverStates.Valid, produce a core of assertions/conclusions that are already unsatisfiable or valid.

    After receiving the result ProverStatus.Unsat or ProverStates.Valid, produce a core of assertions/conclusions that are already unsatisfiable or valid. This requires proof construction to be enabled (setConstructProofs(true)), otherwise the set of all assertions/conclusions is returned.

  113. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  114. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  115. def makeExistential(constants: Iterator[ITerm]): Unit

    Make given constants implicitly existentially quantified.

  116. def makeExistential(constants: Iterable[ITerm]): Unit

    Make given constants implicitly existentially quantified.

  117. def makeExistential(constant: ITerm): Unit

    Make a given constant implicitly existentially quantified.

  118. def makeExistentialRaw(constants: Iterator[ConstantTerm]): Unit

    Make given constants implicitly existentially quantified.

  119. def makeExistentialRaw(constants: Iterable[ConstantTerm]): Unit

    Make given constants implicitly existentially quantified.

  120. def makeUniversal(constants: Iterator[ITerm]): Unit

    Make given constants implicitly universally quantified.

  121. def makeUniversal(constants: Iterable[ITerm]): Unit

    Make given constants implicitly universally quantified.

  122. def makeUniversal(constant: ITerm): Unit

    Make a given constant implicitly universally quantified.

  123. def makeUniversalRaw(constants: Iterator[ConstantTerm]): Unit

    Make given constants implicitly universally quantified.

  124. def makeUniversalRaw(constants: Iterable[ConstantTerm]): Unit

    Make given constants implicitly universally quantified.

  125. def mulTheory: MulTheory

    The current theory used for non-linear problems.

  126. def mult(t1: ITerm, t2: ITerm): ITerm

    Generate the product of the given terms.

    Generate the product of the given terms. Depending on the arguments, either Presburger multiplication with a constant, or the non-linear operator mulTheory.mul will be chosen.

  127. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  128. def needsExhaustiveProver: Boolean
    Attributes
    protected[api]
  129. def nextModel(block: Boolean): SimpleAPI.ProverStatus.Value

    After a Sat result, continue searching for the next model.

    After a Sat result, continue searching for the next model. In most ways, this method behaves exactly like checkSat.

  130. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  131. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  132. def order: TermOrder

    Export the current TermOrder of the prover.

    Export the current TermOrder of the prover. This method is only useful when working with formulae in the internal prover format.

  133. def partialModel: PartialModel

    Produce a partial model, i.e., a (usually) partial interpretation of constants, functions, and predicates.

    Produce a partial model, i.e., a (usually) partial interpretation of constants, functions, and predicates. This method can be called in two situations:

    • after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive, or
    • after receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants. In this case the model only assigns existential constants.
  134. def partialModelAsFormula: IFormula

    Produce a partial model, i.e., a (usually) partial interpretation of constants, functions, and predicates.

    Produce a partial model, i.e., a (usually) partial interpretation of constants, functions, and predicates. This method can be called in two situations:

    • after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive, or
    • after receiving the result ProverStatus.Unsat or ProverStates.Valid for a problem that contains existential constants. In this case the model only assigns existential constants.
  135. def pop(): Unit

    Pop the top-most frame from the assertion stack.

  136. def pp(f: IExpression): String

    Pretty-print a formula or term.

  137. def projectAll(f: IFormula, toConsts: Iterable[ITerm]): IFormula

    Project a formula to a given set of constants; all other constants are removed by quantifying them universally.

  138. def projectEx(f: IFormula, toConsts: Iterable[ITerm]): IFormula

    Project a formula to a given set of constants; all other constants are removed by quantifying them existentially.

  139. def push(): Unit

    Add a new frame to the assertion stack.

  140. def pushEmptyFrame(resetFormulas: Boolean = false, resetOptions: Boolean = false): Unit

    Add a new frame to the assertion stack.

    Add a new frame to the assertion stack. This method has the option to temporarily forget all asserted formulas, or temporarily reset the options setConstructProofs, setMostGeneralConstraints, makeExistential, makeUniversal.

  141. def reduce: ReduceWithConjunction

    Create a reducer with the current settings.

  142. def reduceWithFormula(c: Conjunction): ReduceWithConjunction

    Create a reducer with the current settings, reducing with c as assumptions.

  143. def reset: Unit
  144. def scope[A](resetFormulas: Boolean = false, resetOptions: Boolean = false)(comp: => A): A

    Execute a computation within a local scope.

    Execute a computation within a local scope. After leaving the scope, assertions and declarations done in the meantime will disappear. This method has the option to temporarily forget all asserted formulas, or temporarily reset the options setConstructProofs, setMostGeneralConstraints, makeExistential, makeUniversal.

  145. def scope[A](comp: => A): A

    Execute a computation within a local scope.

    Execute a computation within a local scope. After leaving the scope, assertions and declarations done in the meantime will disappear.

  146. def setConstructProofs(b: Boolean): Unit

    Construct proofs in subsequent checkSat calls.

    Construct proofs in subsequent checkSat calls. Proofs are needed for extract interpolants.

  147. def setMostGeneralConstraints(b: Boolean): Unit

    In subsequent checkSat calls for problems with existential constants, infer the most general constraint on existential constants satisfying the problem.

    In subsequent checkSat calls for problems with existential constants, infer the most general constraint on existential constants satisfying the problem. NB: If this option is used wrongly, it might lead to non-termination of the prover.

  148. def setPartitionNumber(num: Int): Unit

    Add subsequent formulae to partition num.

    Add subsequent formulae to partition num. Index -1 represents formulae belonging to all partitions (e.g., theory axioms).

  149. def setupTheoryPlugin(plugin: Plugin): Unit

    Install a theory plugin in the prover.

  150. def shutDown: Unit
  151. def simplify(f: IFormula): IFormula

    Simplify a formula by eliminating quantifiers.

  152. def smtPP(f: IExpression): String

    Pretty-print a formula or term in SMT-LIB format.

  153. def stop(block: Boolean): SimpleAPI.ProverStatus.Value

    Stop a running prover.

    Stop a running prover. If the prover had already terminated, give same result as getResult, otherwise Unknown. Will block until completion if block argument is true, otherwise return immediately.

  154. def stop: SimpleAPI.ProverStatus.Value

    Stop a running prover.

    Stop a running prover. If the prover had already terminated, give same result as getResult, otherwise Unknown.

  155. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  156. def theories: Seq[Theory]

    The theories currectly loaded in this prover.

  157. def toString(): String
    Definition Classes
    AnyRef → Any
  158. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  159. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  160. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  161. def withCompleteModel[A](comp: (Evaluator) => A): A

    Produce a model, i.e., an interpretation of constants, functions, and predicates.

    Produce a model, i.e., an interpretation of constants, functions, and predicates. This method can be called after receiving the result ProverStatus.Sat or ProverStates.Invalid or ProverStatus.Inconclusive. This method will automatically shut down the evaluator after executing the comp function.

  162. def withPartitionNumber[A](num: Int)(comp: => A): A

    Execute the given code block with partition number set to num.

  163. def withTimeout[A](millis: Long)(comp: => A): A

    Run a block of commands for at most millis milli-seconds.

    Run a block of commands for at most millis milli-seconds. After this, calls to ???, checkSat(true), nextModel(true), getStatus(true), eval, evalPartial, partialModel will throw a TimeoutException.

Deprecated Value Members

  1. def arrayAsMap(t: IdealInt, arity: Int): Map[Seq[IdealInt], IdealInt]

    Return the value of an array as a map

    Return the value of an array as a map

    Deprecated
  2. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

  3. def select(args: ITerm*): ITerm

    Generate a select expression in the theory of arrays.

    Generate a select expression in the theory of arrays.

    Deprecated
  4. def selectFun(arity: Int): IFunction

    select function of the theory of arrays.

    select function of the theory of arrays.

    Deprecated
  5. def store(args: ITerm*): ITerm

    Generate a store expression in the theory of arrays.

    Generate a store expression in the theory of arrays.

    Deprecated
  6. def storeFun(arity: Int): IFunction

    store function of the theory of arrays.

    store function of the theory of arrays.

    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped