de.uni_freiburg.informatik.ultimate.logic

Class LoggingScript

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.LoggingScript

All Implemented Interfaces:

Script

public class LoggingScript
extends java.lang.Object
implements Script

A logging script variant. This is actually a wrapper around a concrete implementation of the Script interface that produces an interaction file in (almost) SMTLIB 2 compliant format. We still have some extra commands like "simplify", "reset", or "get-interpolants".

Author:

Juergen Christ

Nested Class Summary

Nested classes/interfaces inherited from interface de.uni_freiburg.informatik.ultimate.logic.Script

Script.LBool

Field Summary

Fields inherited from interface de.uni_freiburg.informatik.ultimate.logic.Script

EMPTY_SORT_ARRAY, EMPTY_TERM_ARRAY, EXISTS, FORALL

Constructor Summary

Constructors

Constructor and Description
LoggingScript(Script script, java.lang.String file, boolean autoFlush) Create a new script logging the interaction between the user and the wrapped script into a file.
LoggingScript(Script script, java.lang.String file, boolean autoFlush, boolean useCSE) Create a new script logging the interaction between the user and the wrapped script into a file.
LoggingScript(java.lang.String file, boolean autoFlush) Create a new script logging the commands by the user.

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.
void	comment(java.lang.String comment) Write a comment to the generated SMTLIB dump file.
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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

LoggingScript

public LoggingScript(java.lang.String file,
                     boolean autoFlush)
              throws java.io.FileNotFoundException

Create a new script logging the commands by the user. Most commands are not supported, e.g., checkSat always returns unknown. Furthermore, common subexpression elimination is not used in the output.

Parameters:

file - The name of the logging file (should end in .smt2).

autoFlush - Automatically flush the output stream after every command.

Throws:

java.io.FileNotFoundException - If the file cannot be opened.

LoggingScript

public LoggingScript(Script script,
                     java.lang.String file,
                     boolean autoFlush)
              throws java.io.FileNotFoundException

Create a new script logging the interaction between the user and the wrapped script into a file. This constructor sets up logging to not use common subexpression elimination.

Parameters:

script - The wrapped script.

file - The name of the logging file (should end in .smt2).

autoFlush - Automatically flush the output stream after every command.

Throws:

java.io.FileNotFoundException - If the file cannot be opened.

LoggingScript

public LoggingScript(Script script,
                     java.lang.String file,
                     boolean autoFlush,
                     boolean useCSE)
              throws java.io.FileNotFoundException

Create a new script logging the interaction between the user and the wrapped script into a file. This constructor can be used to set up logging using common subexpression elimination.

Parameters:

script - The wrapped script.

file - The name of the logging file (should end in .smt2).

autoFlush - Automatically flush the output stream after every command.

useCSE - Use common subexpression elimination in output (introduces let terms)

Throws:

java.io.FileNotFoundException - If the file cannot be opened.

Method Detail

setLogic

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

Description copied from interface: Script

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

Specified by:

setLogic in interface Script

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

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

Description copied from interface: Script

Set the logic for the solver.

Specified by:

setLogic in interface Script

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

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

Description copied from interface: Script

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

Specified by:

setOption in interface Script

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

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

Description copied from interface: Script

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

Specified by:

setInfo in interface Script

Parameters:

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

:

.

value - Value for this info.

declareSort

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

Description copied from interface: Script

Declare a user-defined sort.

Specified by:

declareSort in interface Script

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

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

Description copied from interface: Script

Define an alias of a sort.

Specified by:

defineSort in interface Script

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

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

Description copied from interface: Script

Declare a function symbol.

Specified by:

declareFun in interface Script

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

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

Description copied from interface: Script

Define an alias of a function symbol.

Specified by:

defineFun in interface Script

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

public void push(int levels)
          throws SMTLIBException

Description copied from interface: Script

Push some levels onto the assertion stack.

Specified by:

push in interface Script

Parameters:

levels - The number of levels to push.

Throws:

SMTLIBException - If logic is not set.

pop

public void pop(int levels)
         throws SMTLIBException

Description copied from interface: Script

Pop some levels from the assertion stack.

Specified by:

pop in interface Script

Parameters:

levels - The number of levels to pop.

Throws:

SMTLIBException - If not enough stack levels are available.

assertTerm

public Script.LBool assertTerm(Term term)
                        throws SMTLIBException

Description copied from interface: Script

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.

Specified by:

assertTerm in interface Script

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

public Script.LBool checkSat()
                      throws SMTLIBException

Description copied from interface: Script

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

Specified by:

checkSat in interface Script

Returns:

The result of the check as a lifted Boolean.

Throws:

SMTLIBException - If the logic is not set.

checkSatAssuming

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

Description copied from interface: Script

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

Specified by:

checkSatAssuming in interface Script

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

public Term[] getAssertions()
                     throws SMTLIBException

Description copied from interface: Script

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

Specified by:

getAssertions in interface Script

Returns:

An array of all asserted terms.

Throws:

SMTLIBException - If interactive mode is not enabled.

getProof

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

Description copied from interface: Script

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

Specified by:

getProof in interface Script

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

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

Description copied from interface: Script

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

Specified by:

getUnsatCore in interface Script

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.

getValue

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

Description copied from interface: Script

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

Specified by:

getValue in interface Script

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

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

Description copied from interface: Script

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 Script.checkSat() did not return Script.LBool.UNSAT. To enable assignment production, call setOption(":produce-assignments", true).

Specified by:

getAssignment in interface Script

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

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

Description copied from interface: Script

Get the value of an option.

Specified by:

getOption in interface Script

Parameters:

opt - Name of an option.

Returns:

The value of this option.

Throws:

java.lang.UnsupportedOperationException - If option is unsupported.

getInfo

public java.lang.Object getInfo(java.lang.String info)
                         throws java.lang.UnsupportedOperationException

Description copied from interface: Script

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

Specified by:

getInfo in interface Script

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.

simplify

public Term simplify(Term term)
              throws SMTLIBException

Description copied from interface: Script

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

Specified by:

simplify in interface Script

Parameters:

term - A (usually Boolean) term to simplify.

Returns:

The simplified term.

Throws:

SMTLIBException - If an error occurred or unsupported.

reset

public void reset()

Description copied from interface: Script

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

Specified by:

reset in interface Script

getInterpolants

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

Description copied from interface: Script

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.

Specified by:

getInterpolants in interface Script

Parameters:

partition - Partitioning of the assertion stack.

Returns:

Interpolants.

Throws:

SMTLIBException - An error occurred.

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

getInterpolants

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

Description copied from interface: Script

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.

Specified by:

getInterpolants in interface Script

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.

exit

public void exit()

Description copied from interface: Script

Exit the solver.

Specified by:

exit in interface Script

sort

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

Description copied from interface: Script

Instantiate an n-ary sort with parameters.

Specified by:

sort in interface Script

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

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

Description copied from interface: Script

Instantiate an indexed n-ary sort with parameters.

Specified by:

sort in interface Script

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.

term

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

Description copied from interface: Script

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.

Specified by:

term in interface Script

Parameters:

funcname - Name of the function.

params - The parameters of the function application.

Returns:

The constructed term.

Throws:

SMTLIBException - If an error occurred.

term

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

Description copied from interface: Script

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.

Specified by:

term in interface Script

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

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

Description copied from interface: Script

Create a term variable.

Specified by:

variable in interface Script

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

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

Description copied from interface: Script

Create a quantified formula.

Specified by:

quantifier in interface Script

Parameters:

quantor - The quantor flag (one of Script.EXISTS, or Script.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

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

Description copied from interface: Script

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

Specified by:

let in interface Script

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

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

Description copied from interface: Script

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

Specified by:

annotate in interface Script

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

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

Description copied from interface: Script

Create a numeral term.

Specified by:

numeral in interface Script

Parameters:

num - String representation of the numeral.

Returns:

A numeral term.

Throws:

SMTLIBException - If an error occurred.

numeral

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

Description copied from interface: Script

Create a numeral term.

Specified by:

numeral in interface Script

Parameters:

num - the numeral as a big integer.

Returns:

A numeral term.

Throws:

SMTLIBException - If an error occurred.

decimal

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

Description copied from interface: Script

Create a decimal term.

Specified by:

decimal in interface Script

Parameters:

decimal - String representation of the decimal.

Returns:

A decimal term.

Throws:

SMTLIBException

decimal

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

Description copied from interface: Script

Create a decimal term.

Specified by:

decimal in interface Script

Parameters:

decimal - the decimal as a big decimal.

Returns:

A decimal term.

Throws:

SMTLIBException

string

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

Description copied from interface: Script

Create a string term.

Specified by:

string in interface Script

Parameters:

str - The parsed string with quotes removed.

Returns:

A string term.

Throws:

SMTLIBException - If an error occurred.

hexadecimal

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

Description copied from interface: Script

Create a hexadecimal term.

Specified by:

hexadecimal in interface Script

Parameters:

hex - String representation of the hexadecimal.

Returns:

A hexadecimal term.

Throws:

SMTLIBException - If an error occurred.

binary

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

Description copied from interface: Script

Create a binary term.

Specified by:

binary in interface Script

Parameters:

bin - String representation of the binary.

Returns:

A binary term.

Throws:

SMTLIBException - If an error occurred.

sortVariables

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

Description copied from interface: Script

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.

Specified by:

sortVariables in interface Script

Parameters:

names - The names of the variables

Returns:

An array corresponding to sort variables with the given names.

Throws:

SMTLIBException - If an error occured.

getModel

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

Description copied from interface: Script

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

Specified by:

getModel in interface Script

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

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

Description copied from interface: Script

Perform an AllSAT computation over some important predicates.

Specified by:

checkAllsat in interface Script

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

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

Description copied from interface: Script

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.

Specified by:

findImpliedEquality in interface Script

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

public QuotedObject echo(QuotedObject msg)

Description copied from interface: Script

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.

Specified by:

echo in interface Script

Parameters:

msg - The message to print.

Returns:

The message.

comment

public void comment(java.lang.String comment)

Write a comment to the generated SMTLIB dump file. Note that this function is only available in the LoggingScript and not in the interface Script since it only makes sense for logging and not for solving.

Parameters:

comment - The comment to write to the dump file.

resetAssertions

public void resetAssertions()

Description copied from interface: Script

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

Specified by:

resetAssertions in interface Script

getUnsatAssumptions

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

Description copied from interface: Script

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

Specified by:

getUnsatAssumptions in interface Script

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.