de.uni_freiburg.informatik.ultimate.logic

Interface Script

All Known Implementing Classes:

LoggingScript, NoopScript, SMTInterpol

public interface Script

Basic interface for the interaction with an SMTLIB version 2 compliant solver. The interface provides all commands of the SMTLIB version 2 standard and some additional commands to create sorts and terms. Following table summarizes the standard options that should be understood by every implementation and gives their types.

Option	Type
:print-success	Boolean
:produce-proofs	Boolean
:produce-assignments	Boolean
:produce-models	Boolean
:regular-output-channel	String
:diagnostic-output-channel	String
:verbosity	Integer
:interactive-mode	Boolean
:random-seed	BigInteger
:timeout	BigInteger

Author:

Jochen Hoenicke, Juergen Christ

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	Script.LBool A lifted three valued Boolean datatype.

Field Summary

Fields

Modifier and Type	Field and Description
static Sort[]	EMPTY_SORT_ARRAY
static Term[]	EMPTY_TERM_ARRAY
static int	EXISTS Constant representing existential quantification.
static int	FORALL Constant representing universal quantification.

Method Summary

Modifier and Type	Method and Description
Term	annotate(Term t, Annotation... annotations) Annotate a term.
Script.LBool	assertTerm(Term term) Assert a Boolean term into the solver.
Term	binary(java.lang.String bin) Create a binary term.
java.lang.Iterable<Term[]>	checkAllsat(Term[] predicates) Perform an AllSAT computation over some important predicates.
Script.LBool	checkSat() Check for satisfiability of the current context.
Script.LBool	checkSatAssuming(Term... assumptions) Check for satisfiability of the current context under additional assumptions.
Term	decimal(java.math.BigDecimal decimal) Create a decimal term.
Term	decimal(java.lang.String decimal) Create a decimal term.
void	declareFun(java.lang.String fun, Sort[] paramSorts, Sort resultSort) Declare a function symbol.
void	declareSort(java.lang.String sort, int arity) Declare a user-defined sort.
void	defineFun(java.lang.String fun, TermVariable[] params, Sort resultSort, Term definition) Define an alias of a function symbol.
void	defineSort(java.lang.String sort, Sort[] sortParams, Sort definition) Define an alias of a sort.
QuotedObject	echo(QuotedObject msg) Echo a message on the regular output channel of the solver.
void	exit() Exit the solver.
Term[]	findImpliedEquality(Term[] x, Term[] y) Try to find an equality between x and y that is implied in the current satisfiable context.
Term[]	getAssertions() Get all assertions contained in the assertion stack.
Assignments	getAssignment() Get values for all named boolean terms in the model.
java.lang.Object	getInfo(java.lang.String info) Get information from the solver.
Term[]	getInterpolants(Term[] partition) Get interpolants for the partitions.
Term[]	getInterpolants(Term[] partition, int[] startOfSubtree) Compute a sequence of interpolants.
Model	getModel() Retrieve a complete model from the solver.
java.lang.Object	getOption(java.lang.String opt) Get the value of an option.
Term	getProof() Trigger a call to a proof processor.
Term[]	getUnsatAssumptions() Get the unsatisfiable assumptions.
Term[]	getUnsatCore() Get the unsat core.
java.util.Map<Term,Term>	getValue(Term[] terms) Get values for some terms in the model.
Term	hexadecimal(java.lang.String hex) Create a hexadecimal term.
Term	let(TermVariable[] vars, Term[] values, Term body) Create a let term.
Term	numeral(java.math.BigInteger num) Create a numeral term.
Term	numeral(java.lang.String num) Create a numeral term.
void	pop(int levels) Pop some levels from the assertion stack.
void	push(int levels) Push some levels onto the assertion stack.
Term	quantifier(int quantor, TermVariable[] vars, Term body, Term[]... patterns) Create a quantified formula.
void	reset() Reset the solver completely.
void	resetAssertions() Resets the assertion stack.
void	setInfo(java.lang.String info, java.lang.Object value) Set some information for the solver.
void	setLogic(Logics logic) Set the logic for the solver.
void	setLogic(java.lang.String logic) Set the logic for the solver.
void	setOption(java.lang.String opt, java.lang.Object value) Set an option for the solver.
Term	simplify(Term term) Simplify a term.
Sort	sort(java.lang.String sortname, java.math.BigInteger[] indices, Sort... params) Instantiate an indexed n-ary sort with parameters.
Sort	sort(java.lang.String sortname, Sort... params) Instantiate an n-ary sort with parameters.
Sort[]	sortVariables(java.lang.String... names) Create an array of sort parameters.
Term	string(java.lang.String str) Create a string term.
Term	term(java.lang.String funcname, java.math.BigInteger[] indices, Sort returnSort, Term... params) Create an n-ary term by name, indices and return sort.
Term	term(java.lang.String funcname, Term... params) Create an n-ary term by name.
TermVariable	variable(java.lang.String varname, Sort sort) Create a term variable.

Field Detail

EMPTY_SORT_ARRAY

static final Sort[] EMPTY_SORT_ARRAY

EMPTY_TERM_ARRAY

static final Term[] EMPTY_TERM_ARRAY

FORALL

static final int FORALL

Constant representing universal quantification.

See Also:

Constant Field Values

EXISTS

static final int EXISTS

Constant representing existential quantification.

See Also:

Constant Field Values

Method Detail

setLogic

void setLogic(java.lang.String logic)
       throws java.lang.UnsupportedOperationException,
              SMTLIBException

Set the logic for the solver. The logic should be the name of one of the elements in the Logics enumeration.

Parameters:

logic - Name of the logic to set.

Throws:

java.lang.UnsupportedOperationException - If the logic is not supported by the solver.

SMTLIBException - If a logic is already set.

setLogic

void setLogic(Logics logic)
       throws java.lang.UnsupportedOperationException,
              SMTLIBException

Set the logic for the solver.

Parameters:

logic - Name of the logic to set.

Throws:

java.lang.UnsupportedOperationException - If the logic is not supported by the solver.

SMTLIBException - If a logic is already set.

setOption

void setOption(java.lang.String opt,
               java.lang.Object value)
        throws java.lang.UnsupportedOperationException,
               SMTLIBException

Set an option for the solver. At least the options described in the standard should be valid options.

Parameters:

opt - Name of the option. Note that it has to start with

:

.

value - Value for this option.

Throws:

java.lang.UnsupportedOperationException - If the option is unsupported.

SMTLIBException - In case of type errors.

setInfo

void setInfo(java.lang.String info,
             java.lang.Object value)

Set some information for the solver. Note that according to the standard a solver has to return success, but ignore the info.

Parameters:

info - Name of the info. Note that it has to start with

:

.

value - Value for this info.

declareSort

void declareSort(java.lang.String sort,
                 int arity)
          throws SMTLIBException

Declare a user-defined sort.

Parameters:

sort - The name of the new sort.

arity - The arity of the new sort.

Throws:

SMTLIBException - If no logic is set, the logic does not allow user-defined sorts, or a sort with this name already exists.

defineSort

void defineSort(java.lang.String sort,
                Sort[] sortParams,
                Sort definition)
         throws SMTLIBException

Define an alias of a sort.

Parameters:

sort - Name of the alias.

sortParams - Sort parameters.

definition - Original sort.

Throws:

SMTLIBException - If no logic is set, the logic does not allow user-defined sorts, or a sort with this name already exists.

declareFun

void declareFun(java.lang.String fun,
                Sort[] paramSorts,
                Sort resultSort)
         throws SMTLIBException

Declare a function symbol.

Parameters:

fun - Name of the function symbol.

paramSorts - Sorts of the parameters.

resultSort - Sort of the result of an application of this function.

Throws:

SMTLIBException - If the logic is not set, the logic is not an UF logic but the function takes parameters, or a function with this name already exists.

defineFun

void defineFun(java.lang.String fun,
               TermVariable[] params,
               Sort resultSort,
               Term definition)
        throws SMTLIBException

Define an alias of a function symbol.

Parameters:

fun - Name of the alias.

params - Parameters of the alias.

resultSort - Return sort of the alias.

definition - Definition of the function alias.

Throws:

SMTLIBException - If the logic is not set, the logic is not an UF logic but the function takes parameters, or a function with this name already exists.

push

void push(int levels)
   throws SMTLIBException

Push some levels onto the assertion stack.

Parameters:

levels - The number of levels to push.

Throws:

SMTLIBException - If logic is not set.

pop

void pop(int levels)
  throws SMTLIBException

Pop some levels from the assertion stack.

Parameters:

levels - The number of levels to pop.

Throws:

SMTLIBException - If not enough stack levels are available.

assertTerm

Script.LBool assertTerm(Term term)
                 throws SMTLIBException

Assert a Boolean term into the solver. The solver might return a change in the state of the logical context. Compliant solvers do not have to do a full check here but return Script.LBool.UNKNOWN.

Parameters:

term - The Boolean term to assert.

Returns:

Possibly an unsatisfiability detected by the solver.

Throws:

SMTLIBException - If the term is not Boolean or a named term matches an already defined function.

checkSat

Script.LBool checkSat()
               throws SMTLIBException

Check for satisfiability of the current context. Note that this function should return Script.LBool.UNKNOWN in case of errors.

Returns:

The result of the check as a lifted Boolean.

Throws:

SMTLIBException - If the logic is not set.

checkSatAssuming

Script.LBool checkSatAssuming(Term... assumptions)
                       throws SMTLIBException

Check for satisfiability of the current context under additional assumptions. Note that this function should return Script.LBool.UNKNOWN in case of errors.

Parameters:

assumptions - Additional assumptions as Boolean constants (nullary ApplicationTerms of sort Bool or their negations).

Returns:

The result of the check as a lifted Boolean.

Throws:

SMTLIBException - If the logic is not set.

getAssertions

Term[] getAssertions()
              throws SMTLIBException

Get all assertions contained in the assertion stack. Note that this command is only available in interactive mode. To enable interactive mode, call setOption(":interactive-mode", true).

Returns:

An array of all asserted terms.

Throws:

SMTLIBException - If interactive mode is not enabled.

getProof

Term getProof()
       throws SMTLIBException,
              java.lang.UnsupportedOperationException

Trigger a call to a proof processor. Note that this command is only available if proof production is enabled and the last checkSat() returned Script.LBool.UNSAT. To enable proof production, call setOption(":produce-proofs", true).

Returns:

the proof. This is given as a big smtlib term of the internal type @proof.

Throws:

SMTLIBException - If proof production is not enabled or the solver did not detect unsatisfiability.

java.lang.UnsupportedOperationException - If proof generation is unsupported.

getUnsatCore

Term[] getUnsatCore()
             throws SMTLIBException,
                    java.lang.UnsupportedOperationException

Get the unsat core. Note that this command is only available if unsat core production is enabled and the last checkSat() returned Script.LBool.UNSAT. To enable unsat core production, call setOption(":produce-unsat-cores", true).

Returns:

An array of terms forming an unsat core.

Throws:

SMTLIBException - If proof production is not enabled or the solver did not detect unsatisfiability.

java.lang.UnsupportedOperationException - If unsat core computation is unsupported.

getUnsatAssumptions

Term[] getUnsatAssumptions()
                    throws SMTLIBException,
                           java.lang.UnsupportedOperationException

Get the unsatisfiable assumptions. Note that this command is only available if unsat assumption production is enabled and the last checkSatAssuming(Term...) returned Script.LBool.UNSAT. To enable unsat assumption production, call setOption (":produce-unsat-assumptions", true).

Returns:

An array of terms that correspond to an unsatisfiable subset of last assumptions.

Throws:

SMTLIBException - If unsat assumption production is not enabled or the solver did not detect unsatisfiability.

java.lang.UnsupportedOperationException - If unsat assumption computation is unsupported.

getValue

java.util.Map<Term,Term> getValue(Term[] terms)
                           throws SMTLIBException,
                                  java.lang.UnsupportedOperationException

Get values for some terms in the model. Note that this command is only available if model production is enabled and the last checkSat() did not return Script.LBool.UNSAT. To enable model production, call setOption(":produce-models", true).

Parameters:

terms - an array of terms whose value should be computed.

Returns:

A valuation (mapping from term to value (which is again represented by a term) where the keys are the given terms.

Throws:

SMTLIBException - If model production is not enabled or the solver detected unsatisfiability.

java.lang.UnsupportedOperationException - If model computation is unsupported

getAssignment

Assignments getAssignment()
                   throws SMTLIBException,
                          java.lang.UnsupportedOperationException

Get values for all named boolean terms in the model. Note that this command is only available if assignment production is enabled and the last checkSat() did not return Script.LBool.UNSAT. To enable assignment production, call setOption(":produce-assignments", true).

Returns:

An Assignments.

Throws:

SMTLIBException - If assignment production is not enabled, or the solver did not detect unsatisfiability.

java.lang.UnsupportedOperationException - If model computation is unsupported

getOption

java.lang.Object getOption(java.lang.String opt)
                    throws java.lang.UnsupportedOperationException

Get the value of an option.

Parameters:

opt - Name of an option.

Returns:

The value of this option.

Throws:

java.lang.UnsupportedOperationException - If option is unsupported.

getInfo

java.lang.Object getInfo(java.lang.String info)
                  throws java.lang.UnsupportedOperationException,
                         SMTLIBException

Get information from the solver. Note that the solver only has to implement the info values described in the standard.

Parameters:

info - Name of the info. Note that it has to start with

:

.

Returns:

Value of the option.

Throws:

java.lang.UnsupportedOperationException - If the info is unsupported.

SMTLIBException - If info is :reason-unknown but last check did not return unknown.

exit

void exit()

Exit the solver.

sort

Sort sort(java.lang.String sortname,
          Sort... params)
   throws SMTLIBException

Instantiate an n-ary sort with parameters.

Parameters:

sortname - Name of the sort.

params - Sort parameters.

Returns:

The corresponding sort.

Throws:

SMTLIBException - If and only if the sort does not exist.

sort

Sort sort(java.lang.String sortname,
          java.math.BigInteger[] indices,
          Sort... params)
   throws SMTLIBException

Instantiate an indexed n-ary sort with parameters.

Parameters:

sortname - Name of the sort.

indices - Sort indices.

params - Sort parameters.

Returns:

The corresponding sort.

Throws:

SMTLIBException - If and only if the sort does not exist.

sortVariables

Sort[] sortVariables(java.lang.String... names)
              throws SMTLIBException

Create an array of sort parameters. These parameters can be used when defining a sort. Note that these names cannot be used in the sort functions since the result does not contain any real sort. Users have to save the array and use its components. The result contains the variables in the order in which the names are specified in the input.

Parameters:

names - The names of the variables

Returns:

An array corresponding to sort variables with the given names.

Throws:

SMTLIBException - If an error occured.

term

Term term(java.lang.String funcname,
          Term... params)
   throws SMTLIBException

Create an n-ary term by name. This function should also be used to construct Boolean terms. I.e., the function names "and", "or", "=>", "ite", "=", "distinct", or "not" might be used to create formulas.

Parameters:

funcname - Name of the function.

params - The parameters of the function application.

Returns:

The constructed term.

Throws:

SMTLIBException - If an error occurred.

term

Term term(java.lang.String funcname,
          java.math.BigInteger[] indices,
          Sort returnSort,
          Term... params)
   throws SMTLIBException

Create an n-ary term by name, indices and return sort. This term constructor can be used to resolve overloaded function symbols, or create applications of the "as" function.

Parameters:

funcname - Name of the function.

indices - Indices for the function.

returnSort - Return sort of the function.

params - The parameters of the function application.

Returns:

The constructed term.

Throws:

SMTLIBException - If an error occurred.

variable

TermVariable variable(java.lang.String varname,
                      Sort sort)
               throws SMTLIBException

Create a term variable.

Parameters:

varname - Name of the variable.

sort - Sort of the variable.

Returns:

The term variable.

Throws:

SMTLIBException - If no name or an invalid sort is given.

quantifier

Term quantifier(int quantor,
                TermVariable[] vars,
                Term body,
                Term[]... patterns)
         throws SMTLIBException

Create a quantified formula.

Parameters:

quantor - The quantor flag (one of EXISTS, or FORALL)

vars - The quantified variables.

body - The body of the quantified formula.

patterns - Possible patterns for e-matching (may be null).

Returns:

The quantified formula.

Throws:

SMTLIBException - If an error occurred.

let

Term let(TermVariable[] vars,
         Term[] values,
         Term body)
  throws SMTLIBException

Create a let term. Note that you have to provide exactly as many variables as you provide values.

Parameters:

vars - Variables bound by a let.

values - Values for these variables.

body - Body of the let term.

Returns:

The let term.

Throws:

SMTLIBException - If an error occurred.

annotate

Term annotate(Term t,
              Annotation... annotations)
       throws SMTLIBException

Annotate a term. This can be used to create named terms.

Parameters:

t - Term to annotate.

annotations - Annotations for this term.

Returns:

The annotated term.

Throws:

SMTLIBException - If the annotation is invalid, or the evaluation of :named produces an error.

numeral

Term numeral(java.lang.String num)
      throws SMTLIBException

Create a numeral term.

Parameters:

num - String representation of the numeral.

Returns:

A numeral term.

Throws:

SMTLIBException - If an error occurred.

numeral

Term numeral(java.math.BigInteger num)
      throws SMTLIBException

Create a numeral term.

Parameters:

num - the numeral as a big integer.

Returns:

A numeral term.

Throws:

SMTLIBException - If an error occurred.

decimal

Term decimal(java.lang.String decimal)
      throws SMTLIBException

Create a decimal term.

Parameters:

decimal - String representation of the decimal.

Returns:

A decimal term.

Throws:

SMTLIBException

decimal

Term decimal(java.math.BigDecimal decimal)
      throws SMTLIBException

Create a decimal term.

Parameters:

decimal - the decimal as a big decimal.

Returns:

A decimal term.

Throws:

SMTLIBException

hexadecimal

Term hexadecimal(java.lang.String hex)
          throws SMTLIBException

Create a hexadecimal term.

Parameters:

hex - String representation of the hexadecimal.

Returns:

A hexadecimal term.

Throws:

SMTLIBException - If an error occurred.

binary

Term binary(java.lang.String bin)
     throws SMTLIBException

Create a binary term.

Parameters:

bin - String representation of the binary.

Returns:

A binary term.

Throws:

SMTLIBException - If an error occurred.

string

Term string(java.lang.String str)
     throws SMTLIBException

Create a string term.

Parameters:

str - The parsed string with quotes removed.

Returns:

A string term.

Throws:

SMTLIBException - If an error occurred.

simplify

Term simplify(Term term)
       throws SMTLIBException

Simplify a term. This returns a term that is under the current assertions equivalent to the input term.

Parameters:

term - A (usually Boolean) term to simplify.

Returns:

The simplified term.

Throws:

SMTLIBException - If an error occurred or unsupported.

reset

void reset()

Reset the solver completely. Note that this invalidates all objects previously returned and unsets the logic.

resetAssertions

void resetAssertions()

Resets the assertion stack. This option will keep the logic and all globally defined symbols.

getInterpolants

Term[] getInterpolants(Term[] partition)
                throws SMTLIBException,
                       java.lang.UnsupportedOperationException

Get interpolants for the partitions. Note that the arguments to this call must either be the names of Boolean top-level assertions, or the conjunction of such names.

Parameters:

partition - Partitioning of the assertion stack.

Returns:

Interpolants.

Throws:

SMTLIBException - An error occurred.

java.lang.UnsupportedOperationException - If interpolant computation is unsupported.

getInterpolants

Term[] getInterpolants(Term[] partition,
                       int[] startOfSubtree)
                throws SMTLIBException,
                       java.lang.UnsupportedOperationException

Compute a sequence of interpolants. The nesting array describes the start of the subtree for tree interpolants. For inductive sequences of interpolants use a nesting array completely filled with 0.

Parameters:

partition - The array of formulas. This should contain either top-level names or conjunction of top-level names.

startOfSubtree - The start of the subtree containing the formula at this index as root.

Returns:

Tree interpolants respecting the nesting relation.

Throws:

SMTLIBException - An error occurred.

java.lang.UnsupportedOperationException - If interpolant computation is unsupported.

getModel

Model getModel()
        throws SMTLIBException,
               java.lang.UnsupportedOperationException

Retrieve a complete model from the solver. This is an optional (non- SMTLIB compliant) operation. This function can only be called when the previous checkSat() returned Script.LBool.SAT or (optionally) Script.LBool.UNKNOWN and no assertion stack command was issued after this check.

Returns:

A model for the current formula.

Throws:

SMTLIBException - Model production was not enabled.

java.lang.UnsupportedOperationException - The solver does not support this operation.

checkAllsat

java.lang.Iterable<Term[]> checkAllsat(Term[] predicates)
                                throws SMTLIBException,
                                       java.lang.UnsupportedOperationException

Perform an AllSAT computation over some important predicates.

Parameters:

predicates - The important predicates. Must be Boolean.

Returns:

Iterator over minterms found during iteration.

Throws:

SMTLIBException - If a predicate is non-Boolean.

java.lang.UnsupportedOperationException - If the operation is unsupported.

findImpliedEquality

Term[] findImpliedEquality(Term[] x,
                           Term[] y)

Try to find an equality between x and y that is implied in the current satisfiable context. If successful, this method returns an array of parameters a,b,c such that the equality a*x = b*y + c is implied by the current context. Note that the x array and the y array must be of equal length and of length at least 2.

Parameters:

x - The different incarnations of the lhs variable.

y - The different incarnations of the rhs variable.

Returns:

Array of length 3 or array of length 0 if no equality is implied.

echo

QuotedObject echo(QuotedObject msg)

Echo a message on the regular output channel of the solver. Although this function is not specified in the SMTLIB standard, we do not expect implementations to throw any exceptions. Instead, if the command is unsupported, it should simply be implemented as the identity function.

Parameters:

msg - The message to print.

Returns:

The message.