Class/Object

ap.api

SimpleAPI

Related Docs: object SimpleAPI | package api

Permalink

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. All

Value Members

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

    Permalink

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

  2. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  3. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any

  4. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  5. def ??(conc: IFormula): Unit

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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])

    Permalink

    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

    Permalink

    Add an abbreviation introduced in a different SimpleAPI instance.

    Add an abbreviation introduced in a different SimpleAPI instance.

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

    Permalink

    Add an abbreviation introduced in a different SimpleAPI instance.

    Add an abbreviation introduced in a different SimpleAPI instance.

  20. def addAssertion(assertion: Formula): Unit

    Permalink

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

  21. def addAssertion(assertion: IFormula): Unit

    Permalink

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

  22. def addAssertionPreproc(assertion: Formula): Unit

    Permalink

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

  23. def addBooleanVariable(f: IFormula): Unit

    Permalink

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

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

    Permalink

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

  25. def addConclusion(conc: Formula): Unit

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

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

  29. def addConstantRaw(c: ConstantTerm): Unit

    Permalink

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

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

    Permalink

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

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

    Permalink

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

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

    Permalink

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

  33. def addFunction(f: BooleanFunApplier): Unit

    Permalink

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

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

    Permalink

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

  35. def addFunction(f: IFunction): Unit

    Permalink

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

  36. def addRelation(p: Predicate): Unit

    Permalink

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

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

    Permalink

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

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

    Permalink

    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

    Permalink

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

  40. def addTheory(newTheory: Theory): Unit

    Permalink

    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

    Permalink

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

  42. def asIFormula(c: Conjunction): IFormula

    Permalink

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

  43. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any

  44. def backtrackToL0: Unit

    Permalink

    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

    Permalink

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

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

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

    Permalink

    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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )

  48. def completeModel: Evaluator

    Permalink

    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

    Permalink

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

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

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

  55. def createBooleanVariable(rawName: String): IFormula

    Permalink

    Create a new Boolean variable (nullary predicate).

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

    Permalink

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

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

  57. def createConstant(sort: Sort): ITerm

    Permalink

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

  58. def createConstant: ITerm

    Permalink

    Create a new symbolic constant with predefined name.

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

    Permalink

    Create a new symbolic constant with given sort.

  60. def createConstant(rawName: String): ITerm

    Permalink

    Create a new symbolic constant.

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

    Permalink

    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

    Permalink

    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]

    Permalink

    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]

    Permalink

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

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

    Permalink

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

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

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

    Permalink

    Create num new symbolic constants with predefined name.

    Create num new symbolic constants with predefined name.

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

    Permalink

    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]

    Permalink

    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

    Permalink

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

  70. def createExistentialConstant: ITerm

    Permalink

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

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

    Permalink

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

  72. def createExistentialConstant(rawName: String): ITerm

    Permalink

    Create a new symbolic constant that is implicitly existentially quantified.

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

    Permalink

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

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

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

    Permalink

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

    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

    Permalink

    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

    Permalink

    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

    Permalink

    Create a new uninterpreted function with fixed arity.

  78. def createInfUninterpretedSort(name: String): InfUninterpretedSort

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef

  84. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  85. def eval(f: IFormula): Boolean

    Permalink

    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

    Permalink

    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

    Permalink

    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]

    Permalink

    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]

    Permalink

    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]

    Permalink

    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]

    Permalink

    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]

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink
    Attributes
    protected[ap.api]

  96. def evaluatorStopped: Unit

    Permalink
    Attributes
    protected[ap.api]

  97. def execSMTLIB(input: Reader): Unit

    Permalink

    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]

    Permalink

    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])

    Permalink

    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

    Permalink

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

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

  101. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  102. def getConstraint: IFormula

    Permalink

    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.

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

    Permalink

    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.

  104. def getConstraintRaw: Conjunction

    Permalink

    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.

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

    Permalink

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

  106. def getMinimisedConstraint: IFormula

    Permalink

    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

    Permalink

    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.

    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

    Permalink

    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

    Permalink

    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]

    Permalink

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

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

    Permalink

    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]

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  114. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  115. def makeExistential(constants: Iterator[ITerm]): Unit

    Permalink

    Make given constants implicitly existentially quantified.

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

    Permalink

    Make given constants implicitly existentially quantified.

  117. def makeExistential(constant: ITerm): Unit

    Permalink

    Make a given constant implicitly existentially quantified.

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

    Permalink

    Make given constants implicitly existentially quantified.

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

    Permalink

    Make given constants implicitly existentially quantified.

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

    Permalink

    Make given constants implicitly universally quantified.

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

    Permalink

    Make given constants implicitly universally quantified.

  122. def makeUniversal(constant: ITerm): Unit

    Permalink

    Make a given constant implicitly universally quantified.

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

    Permalink

    Make given constants implicitly universally quantified.

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

    Permalink

    Make given constants implicitly universally quantified.

  125. def mulTheory: MulTheory

    Permalink

    The current theory used for non-linear problems.

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

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef

  128. def needsExhaustiveProver: Boolean

    Permalink
    Attributes
    protected[ap.api]

  129. def nextModel(block: Boolean): SimpleAPI.ProverStatus.Value

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  131. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  132. def order: TermOrder

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    Pop the top-most frame from the assertion stack.

  136. def pp(f: IExpression): String

    Permalink

    Pretty-print a formula or term.

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

    Permalink

    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

    Permalink

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

  139. def push(): Unit

    Permalink

    Add a new frame to the assertion stack.

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

    Permalink

    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

    Permalink

    Create a reducer with the current settings.

  142. def reduceWithFormula(c: Conjunction): ReduceWithConjunction

    Permalink

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

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

  143. def reset: Unit

    Permalink

  144. def scope[A](resetFormulas: Boolean = false, resetOptions: Boolean = false)(comp: ⇒ A): A

    Permalink

    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

    Permalink

    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

    Permalink

    Construct proofs in subsequent checkSat calls.

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

  147. def setMostGeneralConstraints(b: Boolean): Unit

    Permalink

    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

    Permalink

    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

    Permalink

    Install a theory plugin in the prover.

  150. def shutDown: Unit

    Permalink

  151. def simplify(f: IFormula): IFormula

    Permalink

    Simplify a formula by eliminating quantifiers.

  152. def smtPP(f: IExpression): String

    Permalink

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

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

    Permalink

    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

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef

  156. def theories: Seq[Theory]

    Permalink

    The theories currectly loaded in this prover.

  157. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any

  158. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  159. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  160. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  161. def withCompleteModel[A](comp: (Evaluator) ⇒ A): A

    Permalink

    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

    Permalink

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

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

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

    Permalink

    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]

    Permalink

    Return the value of an array as a map

    Return the value of an array as a map

    Deprecated

  2. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

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

    Permalink

    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

    Permalink

    select function of the theory of arrays.

    select function of the theory of arrays.

    Deprecated

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

    Permalink

    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

    Permalink

    store function of the theory of arrays.

    store function of the theory of arrays.

    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped