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 SMTLIB command language.
 Alphabetic
 By Inheritance
 SimpleAPI
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Value Members

def
!!(assertion: IFormula): Unit
Add an assertion to the prover: assume that the given formula is true

final
def
!=(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

final
def
##(): Int
 Definition Classes
 AnyRef → Any

final
def
==(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

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 ofUnsat/Sat
. 
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.

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 daglike 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. 
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 daglike 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. 
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 daglike 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. 
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 daglike 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. 
def
abbrevSharedExpressions(t: IFormula, sizeThreshold: Int): IFormula
Abbreviate (large) shared subexpressions.
Abbreviate (large) shared subexpressions. This method avoids the worstcase exponential blowup resulting from expressions with nested shared subexpressions.

def
abbrevSharedExpressions(t: ITerm, sizeThreshold: Int): ITerm
Abbreviate (large) shared subexpressions.
Abbreviate (large) shared subexpressions. This method avoids the worstcase exponential blowup resulting from expressions with nested shared subexpressions.

def
abbrevSharedExpressions(t: IFormula): IFormula
Abbreviate (large) shared subexpressions.
Abbreviate (large) shared subexpressions. This method avoids the worstcase exponential blowup resulting from expressions with nested shared subexpressions.

def
abbrevSharedExpressions(t: ITerm): ITerm
Abbreviate (large) shared subexpressions.
Abbreviate (large) shared subexpressions. This method avoids the worstcase exponential blowup resulting from expressions with nested shared subexpressions.

def
abbrevSharedExpressions(t: IExpression, sizeThreshold: Int): IExpression
Abbreviate (large) shared subexpressions.
Abbreviate (large) shared subexpressions. This method avoids the worstcase exponential blowup resulting from expressions with nested shared subexpressions.

def
abbrevSharedExpressions(t: IExpression): IExpression
Abbreviate (large) shared subexpressions.
Abbreviate (large) shared subexpressions. This method avoids the worstcase exponential blowup resulting from expressions with nested shared subexpressions.

def
abbrevSharedExpressionsWithMap(t: IExpression, sizeThreshold: Int): (IExpression, Map[IExpression, IExpression])
Abbreviate (large) shared subexpressions.
Abbreviate (large) shared subexpressions. This method avoids the worstcase exponential blowup resulting from expressions with nested shared subexpressions. This method also returns a map with the created abbreviations.

def
addAbbrev(abbrevFor: IFormula, fullFor: IFormula): IFormula
Add an abbreviation introduced in a different
SimpleAPI
instance. 
def
addAbbrev(abbrevTerm: ITerm, fullTerm: ITerm): ITerm
Add an abbreviation introduced in a different
SimpleAPI
instance. 
def
addAssertion(assertion: Formula): Unit
Add an assertion to the prover: assume that the given formula is true

def
addAssertion(assertion: IFormula): Unit
Add an assertion to the prover: assume that the given formula is true

def
addBooleanVariable(f: IFormula): Unit
Add an externally defined boolean variable to the environment of this prover.

def
addBooleanVariables(fs: Iterable[IFormula]): Unit
Add a sequence of externally defined boolean variables to the environment of this prover.

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 ofUnsat/Sat
. 
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 ofUnsat/Sat
. 
def
addConstant(t: ITerm): Unit
Add an externally defined constant to the environment of this prover.

def
addConstantRaw(c: ConstantTerm): Unit
Add an externally defined constant to the environment of this prover.

def
addConstants(ts: Iterable[ITerm]): Unit
Add a sequence of externally defined constants to the environment of this prover.

def
addConstantsRaw(cs: Iterable[ConstantTerm]): Unit
Add a sequence of externally defined constant to the environment of this prover.

def
addFunction(f: BooleanFunApplier, functionalityMode: SimpleAPI.FunctionalityMode.Value): Unit
Add an externally defined function to the environment of this prover.

def
addFunction(f: BooleanFunApplier): Unit
Add an externally defined function to the environment of this prover.

def
addFunction(f: IFunction, functionalityMode: SimpleAPI.FunctionalityMode.Value): Unit
Add an externally defined function to the environment of this prover.

def
addFunction(f: IFunction): Unit
Add an externally defined function to the environment of this prover.

def
addRelation(p: Predicate): Unit
Add an externally defined relation to the environment of this prover.

def
addRelations(ps: Iterable[Predicate]): Unit
Add a sequence of externally defined relations to the environment of this prover.

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.

def
addTheoriesFor(order: TermOrder): Unit
Add all theories to the prover that occur in the given order.

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.

def
arrayAsMap(t: IdealInt, arity: Int): Map[Seq[IdealInt], IdealInt]
Return the value of an array as a map

def
asConjunction(f: IFormula): Conjunction
Convert a formula in input syntax to the internal prover format.

def
asIFormula(c: Conjunction): IFormula
Convert a formula from the internal prover format to input syntax.

final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

def
certificateAsString(partNames: Map[Int, PartName], format: parameters.Param.InputFormat.Value): String
After receiving the result
ProverStatus.Unsat
orProverStates.Valid
, produce a certificate in textual/readable format. 
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. 
def
clone(): AnyRef
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @native() @throws( ... )

implicit
def
convert2RichMulTerm(term: ITerm): RichMulTerm
Convert a term to a rich term, offering operations
mul, div, mod
, etc., for nonlinear arithmetic. 
def
createADT(sortNames: Seq[String], ctorSignatures: Seq[(String, CtorSignature)], measure: theories.ADT.TermMeasure.Value = ADT.TermMeasure.RelDepth): ADT
Create an algebraic datatype.
Create an algebraic datatype.
TODO: logging

def
createBooleanFunction(rawName: String, argSorts: Seq[Sort], partial: Boolean = false, functionalityMode: SimpleAPI.FunctionalityMode.Value = FunctionalityMode.Full): BooleanFunApplier
Create a new uninterpreted Booleanvalued function with given arguments.
Create a new uninterpreted Booleanvalued function with given arguments. Booleans values are encoded into integers, mapping
true
to0
andfalse
to1
.
In contrast to predicates (generated usingcreateRelation
), Boolean functions can be used within triggers. 
def
createBooleanFunction(rawName: String, arity: Int, functionalityMode: SimpleAPI.FunctionalityMode.Value): BooleanFunApplier
Create a new uninterpreted Booleanvalued function with fixed arity.
Create a new uninterpreted Booleanvalued function with fixed arity. Booleans values are encoded into integers, mapping
true
to0
andfalse
to1
.
In contrast to predicates (generated usingcreateRelation
), Boolean functions can be used within triggers. 
def
createBooleanFunction(rawName: String, arity: Int): BooleanFunApplier
Create a new uninterpreted Booleanvalued function with fixed arity.
Create a new uninterpreted Booleanvalued function with fixed arity. Booleans values are encoded into integers, mapping
true
to0
andfalse
to1
.
In contrast to predicates (generated usingcreateRelation
), Boolean functions can be used within triggers. 
def
createBooleanVariable: IFormula
Create a new Boolean variable (nullary predicate) with predefined name.

def
createBooleanVariable(rawName: String): IFormula
Create a new Boolean variable (nullary predicate).

def
createBooleanVariables(num: Int): IndexedSeq[IFormula]
Create
num
new Boolean variable (nullary predicate) with predefined name. 
def
createConstant(sort: Sort): ITerm
Create a new symbolic constant with predefined name and given sort.

def
createConstant: ITerm
Create a new symbolic constant with predefined name.

def
createConstant(rawName: String, sort: Sort): ITerm
Create a new symbolic constant with given sort.

def
createConstant(rawName: String): ITerm
Create a new symbolic constant.

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

def
createConstants(prefix: String, nums: Range): IndexedSeq[ITerm]
Create a sequence of new symbolic constants, with name starting with the given prefix.

def
createConstants(num: Int, sort: Sort): IndexedSeq[ITerm]
Create
num
new symbolic constants with predefined name and given sort. 
def
createConstants(num: Int): IndexedSeq[ITerm]
Create
num
new symbolic constants with predefined name. 
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. 
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. 
def
createExistentialConstant(sort: Sort): ITerm
Create a new symbolic constant with predefined name and given sort that is implicitly existentially quantified.

def
createExistentialConstant: ITerm
Create a new symbolic constant with predefined name that is implicitly existentially quantified.

def
createExistentialConstant(rawName: String, sort: Sort): ITerm
Create a new symbolic constant with given sort that is implicitly existentially quantified.

def
createExistentialConstant(rawName: String): ITerm
Create a new symbolic constant that is implicitly existentially quantified.

def
createExistentialConstants(num: Int, sort: Sort): IndexedSeq[ITerm]
Create
num
new symbolic constant with predefined name that is implicitly existentially quantified. 
def
createExistentialConstants(num: Int): IndexedSeq[ITerm]
Create
num
new symbolic constant with predefined name that is implicitly existentially quantified. 
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.

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.

def
createFunction(rawName: String, arity: Int): IFunction
Create a new uninterpreted function with fixed arity.

def
createInfUninterpretedSort(name: String): InfUninterpretedSort
Create a new uninterpreted sort of infinite cardinality.
Create a new uninterpreted sort of infinite cardinality.
TODO: logging

def
createRelation(rawName: String, argSorts: Seq[Sort]): Predicate
Create a new uninterpreted predicate with the given arguments.
Predicates are more lowlevel than Boolean functions, and cannot be used within triggers. 
def
createRelation(rawName: String, arity: Int): Predicate
Create a new uninterpreted predicate with fixed arity.
Predicates are more lowlevel than Boolean functions, and cannot be used within triggers. 
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

val
decoderContext: DecoderContext
Decoding data needed (and implicitly read) by theories.

final
def
eq(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

def
equals(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

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
orProverStates.Invalid
orProverStatus.Inconclusive
. 
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
orProverStates.Invalid
orProverStatus.Inconclusive
, or which case the term is evaluated in the computed model, or  after receiving
the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants. In this case the queried termt
may only consist of existential constants.
 after receiving the result

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
orProverStates.Invalid
orProverStatus.Inconclusive
, which case the term is evaluated in the computed model, or  after receiving
the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants. In this case the queried termt
may only consist of existential constants.
 after receiving the result

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 resultProverStatus.Sat
orProverStates.Invalid
orProverStatus.Inconclusive
. 
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
orProverStates.Invalid
orProverStatus.Inconclusive
, or which case the term is evaluated in the computed model, or  after receiving
the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants. In this case the queried termt
may only consist of existential constants.
 after receiving the result

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
orProverStates.Invalid
orProverStatus.Inconclusive
, or which case the term is evaluated in the computed model, or  after receiving
the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants. In this case the queried termt
may only consist of existential constants.
 after receiving the result

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 resultProverStatus.Sat
orProverStates.Invalid
orProverStatus.Inconclusive
. 
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 resultProverStatus.Sat
orProverStates.Invalid
orProverStatus.Inconclusive
. 
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
orProverStates.Invalid
orProverStatus.Inconclusive
. 
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
orProverStates.Invalid
orProverStatus.Inconclusive
. 
def
execSMTLIB(input: Reader): Unit
Execute an SMTLIB script.
Execute an SMTLIB 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.

def
extractSMTLIBAssertions(input: Reader): Seq[IFormula]
Extract the assertions in an SMTLIB script.
Extract the assertions in an SMTLIB 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.

def
extractSMTLIBAssertionsSymbols(input: Reader): (Seq[IFormula], Map[IFunction, SMTFunctionType], Map[ConstantTerm, SMTType])
Extract assertions and declared symbols in an SMTLIB script.
Extract assertions and declared symbols in an SMTLIB 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.

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

def
getCertificate: Certificate
After receiving the result
ProverStatus.Unsat
orProverStates.Valid
, produce an (unsimplified) certificate. 
final
def
getClass(): Class[_]
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

def
getConstraint: IFormula
After receiving the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants, return a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants. 
def
getConstraintRaw: Conjunction
After receiving the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants, return a (satisfiable) constraint over the existential constants that describes satisfying assignments of the existential constants. 
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.

def
getMinimisedConstraint: IFormula
After receiving the result
ProverStatus.Unsat
orProverStates.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
orProverStates.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. 
def
getStatus(timeout: Long): SimpleAPI.ProverStatus.Value
Query result of the last
checkSat
ornextModel
call.Query result of the last
checkSat
ornextModel
call. Will block until a result is available, or untiltimeout
milliseconds elapse. 
def
getStatus(block: Boolean): SimpleAPI.ProverStatus.Value
Query result of the last
checkSat
ornextModel
call.Query result of the last
checkSat
ornextModel
call. Will block until a result is available ifblock
argument is true, otherwise return immediately. 
def
getSymbolMap: Map[String, AnyRef]
Create a map with all declared symbols known to this prover.

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.

def
getUnsatCore: Set[Int]
After receiving the result
ProverStatus.Unsat
orProverStates.Valid
, produce a core of assertions/conclusions that are already unsatisfiable or valid.After receiving the result
ProverStatus.Unsat
orProverStates.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. 
def
hashCode(): Int
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

final
def
isInstanceOf[T0]: Boolean
 Definition Classes
 Any

def
makeExistential(constants: Iterator[ITerm]): Unit
Make given constants implicitly existentially quantified.

def
makeExistential(constants: Iterable[ITerm]): Unit
Make given constants implicitly existentially quantified.

def
makeExistential(constant: ITerm): Unit
Make a given constant implicitly existentially quantified.

def
makeExistentialRaw(constants: Iterator[ConstantTerm]): Unit
Make given constants implicitly existentially quantified.

def
makeExistentialRaw(constants: Iterable[ConstantTerm]): Unit
Make given constants implicitly existentially quantified.

def
makeUniversal(constants: Iterator[ITerm]): Unit
Make given constants implicitly universally quantified.

def
makeUniversal(constants: Iterable[ITerm]): Unit
Make given constants implicitly universally quantified.

def
makeUniversal(constant: ITerm): Unit
Make a given constant implicitly universally quantified.

def
makeUniversalRaw(constants: Iterator[ConstantTerm]): Unit
Make given constants implicitly universally quantified.

def
makeUniversalRaw(constants: Iterable[ConstantTerm]): Unit
Make given constants implicitly universally quantified.

def
mulTheory: MulTheory
The current theory used for nonlinear problems.

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 nonlinear operator
mulTheory.mul
will be chosen. 
final
def
ne(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

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 likecheckSat
. 
final
def
notify(): Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

final
def
notifyAll(): Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

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. 
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
orProverStates.Invalid
orProverStatus.Inconclusive
, or  after receiving
the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants. In this case the model only assigns existential constants.
 after receiving the result

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
orProverStates.Invalid
orProverStatus.Inconclusive
, or  after receiving
the result
ProverStatus.Unsat
orProverStates.Valid
for a problem that contains existential constants. In this case the model only assigns existential constants.
 after receiving the result

def
pop: Unit
Pop the topmost frame from the assertion stack.

def
pp(f: IExpression): String
Prettyprint a formula or term.

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.

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.

def
push: Unit
Add a new frame to the assertion stack.

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
.  def reset: Unit

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

def
select(args: ITerm*): ITerm
Generate a
select
expression in the theory of arrays. 
def
selectFun(arity: Int): IFunction
select
function of the theory of arrays. 
def
setConstructProofs(b: Boolean): Unit
Construct proofs in subsequent
checkSat
calls.Construct proofs in subsequent
checkSat
calls. Proofs are needed for extract interpolants. 
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 nontermination of the prover. 
def
setPartitionNumber(num: Int): Unit
Add subsequent formulae to partition
num
.Add subsequent formulae to partition
num
. Index1
represents formulae belonging to all partitions (e.g., theory axioms). 
def
setupTheoryPlugin(plugin: Plugin): Unit
Install a theory plugin in the prover.
 def shutDown: Unit

def
simplify(f: IFormula): IFormula
Simplify a formula by eliminating quantifiers.

def
smtPP(f: IExpression): String
Prettyprint a formula or term in SMTLIB format.

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
, otherwiseUnknown
. Will block until completion ifblock
argument is true, otherwise return immediately. 
def
stop: SimpleAPI.ProverStatus.Value
Stop a running prover.
Stop a running prover. If the prover had already terminated, give same result as
getResult
, otherwiseUnknown
. 
def
store(args: ITerm*): ITerm
Generate a
store
expression in the theory of arrays. 
def
storeFun(arity: Int): IFunction
store
function of the theory of arrays. 
final
def
synchronized[T0](arg0: ⇒ T0): T0
 Definition Classes
 AnyRef

def
theories: Seq[Theory]
The theories currectly loaded in this prover.

def
toString(): String
 Definition Classes
 AnyRef → Any

final
def
wait(): Unit
 Definition Classes
 AnyRef
 Annotations
 @throws( ... )

final
def
wait(arg0: Long, arg1: Int): Unit
 Definition Classes
 AnyRef
 Annotations
 @throws( ... )

final
def
wait(arg0: Long): Unit
 Definition Classes
 AnyRef
 Annotations
 @native() @throws( ... )

def
withPartitionNumber[A](num: Int)(comp: ⇒ A): A
Execute the given code block with partition number set to
num
. 
def
withTimeout[A](millis: Long)(comp: ⇒ A): A
Run a block of commands for at most
millis
milliseconds.Run a block of commands for at most
millis
milliseconds. After this, calls to???
,checkSat(true)
,nextModel(true)
,getStatus(true)
,eval
,evalPartial
,partialModel
will throw aTimeoutException
.