Add an assertion to the prover: assume that the given formula is true
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
.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Add an abbreviation introduced in a different SimpleAPI
instance.
Add an abbreviation introduced in a different SimpleAPI
instance.
Add an abbreviation introduced in a different SimpleAPI
instance.
Add an abbreviation introduced in a different SimpleAPI
instance.
Add an assertion to the prover: assume that the given formula is true
Add an assertion to the prover: assume that the given formula is true
Add an externally defined boolean variable to the environment of this prover.
Add a sequence of externally defined boolean variables to the environment of this prover.
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
.
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
.
Add an externally defined constant to the environment of this prover.
Add an externally defined constant to the environment of this prover.
Add a sequence of externally defined constants to the environment of this prover.
Add a sequence of externally defined constant to the environment of this prover.
Add an externally defined function to the environment of this prover.
Add an externally defined function to the environment of this prover.
Add an externally defined function to the environment of this prover.
Add an externally defined function to the environment of this prover.
Add an externally defined relation to the environment of this prover.
Add a sequence of externally defined relations to the environment of this prover.
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.
Add all theories to the prover that occur in the given order.
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.
Return the value of an array as a map
Convert a formula in input syntax to the internal prover format.
Convert a formula from the internal prover format to input syntax.
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.
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.
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.
Create an algebraic data-type.
Create an algebraic data-type.
TODO: logging
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.
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.
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.
Create a new Boolean variable (nullary predicate) with predefined name.
Create a new Boolean variable (nullary predicate).
Create num
new Boolean variable (nullary predicate) with
predefined name.
Create num
new Boolean variable (nullary predicate) with
predefined name.
Create a new symbolic constant with predefined name and given sort.
Create a new symbolic constant with predefined name.
Create a new symbolic constant with given sort.
Create a new symbolic constant.
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.
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.
Create a sequence of new symbolic constants, with name starting with the given prefix and the given sort.
Create a sequence of new symbolic constants, with name starting with the given prefix.
Create num
new symbolic constants with predefined name and
given sort.
Create num
new symbolic constants with predefined name and
given sort.
Create num
new symbolic constants with predefined name.
Create num
new symbolic constants with predefined name.
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.
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.
Create a new symbolic constant with predefined name and given sort that is implicitly existentially quantified.
Create a new symbolic constant with predefined name that is implicitly existentially quantified.
Create a new symbolic constant with given sort that is implicitly existentially quantified.
Create a new symbolic constant that is implicitly existentially quantified.
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.
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.
Create a new uninterpreted function with given sorts, and chose whether the function is partial, and to which degree functionality axioms should be generated.
Create a new uninterpreted function with fixed arity, and chose to which degree functionality axioms should be generated.
Create a new uninterpreted function with fixed arity.
Create a new uninterpreted sort of infinite cardinality.
Create a new uninterpreted sort of infinite cardinality.
TODO: logging
Create a new uninterpreted predicate with the given arguments.
Predicates are more low-level than Boolean functions, and
cannot be used within triggers.
Create a new uninterpreted predicate with fixed arity.
Predicates are more low-level than Boolean functions, and
cannot be used within triggers.
Create a new uninterpreted sort of finite or infinite cardinality.
Create a new uninterpreted sort of finite or infinite cardinality.
TODO: logging
Decoding data needed (and implicitly read) by theories; this will access the current model to extract the relevant decoding data.
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
.
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:
ProverStatus.Sat
or ProverStates.Invalid
or ProverStatus.Inconclusive
, or
which case the term is evaluated in the computed model, orProverStatus.Unsat
or ProverStates.Valid
for a problem that contains existential constants. In this case the
queried term t
may only consist of existential constants.Evaluate the given term in the current model.
Evaluate the given term in the current model. This method can be called in two situations:
ProverStatus.Sat
or ProverStates.Invalid
or ProverStatus.Inconclusive
,
which case the term is evaluated in the computed model, orProverStatus.Unsat
or ProverStates.Valid
for a problem that contains existential constants. In this case the
queried term t
may only consist of existential constants.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
.
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:
ProverStatus.Sat
or ProverStates.Invalid
or ProverStatus.Inconclusive
, or
which case the term is evaluated in the computed model, orProverStatus.Unsat
or ProverStates.Valid
for a problem that contains existential constants. In this case the
queried term t
may only consist of existential constants.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:
ProverStatus.Sat
or ProverStates.Invalid
or ProverStatus.Inconclusive
, or
which case the term is evaluated in the computed model, orProverStatus.Unsat
or ProverStates.Valid
for a problem that contains existential constants. In this case the
queried term t
may only consist of existential constants.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
.
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
.
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
.
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
.
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.
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.
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.
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.
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.
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.
Compute an inductive sequence of interpolants, for the given partitioning of the input problem.
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.
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.
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.
Create a map with all declared symbols known to this prover.
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.
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.
Make given constants implicitly existentially quantified.
Make given constants implicitly existentially quantified.
Make a given constant implicitly existentially quantified.
Make given constants implicitly existentially quantified.
Make given constants implicitly existentially quantified.
Make given constants implicitly universally quantified.
Make given constants implicitly universally quantified.
Make a given constant implicitly universally quantified.
Make given constants implicitly universally quantified.
Make given constants implicitly universally quantified.
The current theory used for non-linear problems.
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.
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
.
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.
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:
ProverStatus.Sat
or ProverStates.Invalid
or ProverStatus.Inconclusive
, orProverStatus.Unsat
or ProverStates.Valid
for a problem that contains existential constants. In this case the
model only assigns existential constants.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:
ProverStatus.Sat
or ProverStates.Invalid
or ProverStatus.Inconclusive
, orProverStatus.Unsat
or ProverStates.Valid
for a problem that contains existential constants. In this case the
model only assigns existential constants.Pop the top-most frame from the assertion stack.
Pretty-print a formula or term.
Project a formula to a given set of constants; all other constants are removed by quantifying them universally.
Project a formula to a given set of constants; all other constants are removed by quantifying them existentially.
Add a new frame to the assertion stack.
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
.
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
.
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.
Generate a select
expression in the theory of arrays.
Generate a select
expression in the theory of arrays.
select
function of the theory of arrays.
select
function of the theory of arrays.
Construct proofs in subsequent checkSat
calls.
Construct proofs in subsequent checkSat
calls. Proofs are
needed for extract interpolants.
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.
Add subsequent formulae to partition num
.
Add subsequent formulae to partition num
.
Index -1
represents formulae belonging to all partitions
(e.g., theory axioms).
Install a theory plugin in the prover.
Simplify a formula by eliminating quantifiers.
Pretty-print a formula or term in SMT-LIB format.
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.
Stop a running prover.
Stop a running prover. If the prover had already terminated, give same
result as getResult
, otherwise Unknown
.
Generate a store
expression in the theory of arrays.
Generate a store
expression in the theory of arrays.
store
function of the theory of arrays.
store
function of the theory of arrays.
The theories currectly loaded in this prover.
Execute the given code block with partition number set to
num
.
Execute the given code block with partition number set to
num
.
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
.
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.