de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2

Class SMTInterpol

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NoopScript

de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol

All Implemented Interfaces:

Script

public class SMTInterpol
extends NoopScript

Implementation of the Script interface to interact with SMTInterpol. Users should however stick to the Script interface which provides most of the methods provided in this class.

Author:

Juergen Christ

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	SMTInterpol.CheckType

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

Script.LBool

Field Summary

Fields inherited from class de.uni_freiburg.informatik.ultimate.logic.NoopScript

mSolverSetup, mStackLevel

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
SMTInterpol() Default constructor using a default logger and no user termination request.
SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger) Construct SMTInterpol with a user-owned logger but without user termination request.
SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger, boolean ignored) Deprecated. Use a constructor version without the boolean parameter!
SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger, boolean ignored, TerminationRequest cancel) Deprecated. Use a constructor version without the boolean parameter.
SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger, TerminationRequest cancel) Construct SMTInterpol with a logger and a user termination request.
SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap options) Construct SMTInterpol with an option map.
SMTInterpol(SMTInterpol other, java.util.Map<java.lang.String,java.lang.Object> options, de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap.CopyMode mode) Copy the current context and modify some pre-theory options.
SMTInterpol(TerminationRequest cancel) Default constructor using a default logger and a given user termination request.
SMTInterpol(TerminationRequest cancel, de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap options) Construct SMTInterpol with a user termination request and a user created option map.

Method Summary

Modifier and Type	Method and Description
Script.LBool	assertTerm(Term term) Assert a Boolean term into the solver.
java.lang.Iterable<Term[]>	checkAllsat(Term[] input) 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	declareFun(java.lang.String fun, Sort[] paramSorts, Sort resultSort) Declare a function symbol.
Term[]	findImpliedEquality(Term[] x, Term[] y) Try to find an equality between x and y that is implied in the current satisfiable context.
void	flipDecisions() Perform a restart and switch the decisions of all undecided literals.
void	flipNamedLiteral(java.lang.String name) Flip the truth value decision for a name literal.
Term[]	getAssertions() Get all assertions contained in the assertion stack.
Assignments	getAssignment() Get values for all named boolean terms in the model.
de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier	getClausifier() Access to the internal CNF transformer.
de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine	getEngine() Access to the internal DPLL engine.
java.lang.Object	getInfo(java.lang.String info) Get information from the solver.
Term[]	getInterpolants(Term[] partition, int[] startOfSubtree) Compute a sequence of interpolants.
de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy	getLogger() Access to the logger used by SMTInterpol.
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[]	getSatisfiedLiterals() Get all literals currently set to true.
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.
boolean	isTerminationRequested()
void	pop(int n) Pop some levels from the assertion stack.
void	push(int n) Push some levels onto the assertion stack.
void	reset() Unset the logic and clear the assertion stack.
void	resetAssertions() Resets the assertion stack.
de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.Clause	retrieveProof() Retrieve the proof in its internal format.
protected void	setClausifier(de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier clausifier)
protected void	setEngine(de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine engine)
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.

Methods inherited from class de.uni_freiburg.informatik.ultimate.logic.NoopScript

annotate, binary, decimal, decimal, declareSort, defineFun, defineSort, echo, exit, getInterpolants, getTheory, hexadecimal, let, numeral, numeral, quantifier, sort, sort, sortVariables, string, term, term, variable

Methods inherited from class java.lang.Object

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

Constructor Detail

SMTInterpol

public SMTInterpol()

Default constructor using a default logger and no user termination request. If this constructor is used, SMTInterpol assumes ownership of the logger.

SMTInterpol

public SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger)

Construct SMTInterpol with a user-owned logger but without user termination request.

Parameters:

logger - The logger owned by the caller.

SMTInterpol

@Deprecated
public SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger,
                               boolean ignored)

Deprecated. Use a constructor version without the boolean parameter!

Construct SMTInterpol with a logger but without user termination request. The logger is assumed to be configured by the user.

Parameters:

logger - The logger owned by the caller.

ignored - This parameter is ignored!

SMTInterpol

public SMTInterpol(TerminationRequest cancel)

Default constructor using a default logger and a given user termination request.

Parameters:

cancel - User termination request to poll during checks.

SMTInterpol

public SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger,
                   TerminationRequest cancel)

Construct SMTInterpol with a logger and a user termination request. This is the main constructor of SMTInterpol.

Parameters:

logger - The logger owned by the caller.

cancel - User termination request to poll during checks.

SMTInterpol

public SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap options)

Construct SMTInterpol with an option map. SMTInterpol will use the logger used to initialize the option map.

Parameters:

options - The option map used to handle all options.

SMTInterpol

public SMTInterpol(TerminationRequest cancel,
                   de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap options)

Construct SMTInterpol with a user termination request and a user created option map. This constructor is mainly used by the front ends to set an option map including front end options.

Parameters:

cancel - User termination request to poll during checks.

options - Option map to handle options.

SMTInterpol

@Deprecated
public SMTInterpol(de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy logger,
                               boolean ignored,
                               TerminationRequest cancel)

Deprecated. Use a constructor version without the boolean parameter.

Construct SMTInterpol with a user-owned logger but without user termination request. Note that the logger is assumed to be correctly set up.

Parameters:

logger - The logger owned by the caller.

ignored - This option is ignored!

cancel - User termination request to poll during checks.

SMTInterpol

public SMTInterpol(SMTInterpol other,
                   java.util.Map<java.lang.String,java.lang.Object> options,
                   de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap.CopyMode mode)

Copy the current context and modify some pre-theory options. The copy shares the push/pop stack on the symbols but not on the assertions. Users should be careful not to mess up the push/pop stack, i.e., not to push on one context and pop on another one. Note that this cloning does not clone the assertion stack and should not be used in multi-threaded contexts since users cannot guarantee correct push/pop-stack treatment.

Parameters:

other - The context to clone.

options - The options to set before setting the logic.

mode - What to do when copying existing options.

Method Detail

reset

public final void reset()

Unset the logic and clear the assertion stack. This does not reset online modifiable options.

Specified by:

reset in interface Script

Overrides:

reset in class NoopScript

resetAssertions

public final 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

Overrides:

resetAssertions in class NoopScript

push

public void push(int n)
          throws SMTLIBException

Description copied from interface: Script

Push some levels onto the assertion stack.

Specified by:

push in interface Script

Overrides:

push in class NoopScript

Parameters:

n - The number of levels to push.

Throws:

SMTLIBException - If logic is not set.

pop

public void pop(int n)
         throws SMTLIBException

Description copied from interface: Script

Pop some levels from the assertion stack.

Specified by:

pop in interface Script

Overrides:

pop in class NoopScript

Parameters:

n - The number of levels to pop.

Throws:

SMTLIBException - If not enough stack levels are available.

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

Overrides:

checkSat in class NoopScript

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

Overrides:

checkSatAssuming in class NoopScript

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.

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

Overrides:

setLogic in class NoopScript

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

Overrides:

setLogic in class NoopScript

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.

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

Overrides:

assertTerm in class NoopScript

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.

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

Overrides:

getAssertions in class NoopScript

Returns:

An array of all asserted terms.

Throws:

SMTLIBException - If interactive mode is not enabled.

getAssignment

public Assignments getAssignment()
                          throws SMTLIBException

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

Overrides:

getAssignment in class NoopScript

Returns:

An Assignments.

Throws:

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

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

Overrides:

getInfo in class NoopScript

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.

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

Overrides:

getOption in class NoopScript

Parameters:

opt - Name of an option.

Returns:

The value of this option.

Throws:

java.lang.UnsupportedOperationException - If option is unsupported.

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

Overrides:

getProof in class NoopScript

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.

getInterpolants

public Term[] getInterpolants(Term[] partition,
                              int[] startOfSubtree)

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

Overrides:

getInterpolants in class NoopScript

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.

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

Overrides:

getUnsatCore in class NoopScript

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

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

Overrides:

getUnsatAssumptions in class NoopScript

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

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

Overrides:

getValue in class NoopScript

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

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

Overrides:

getModel in class NoopScript

Returns:

A model for the current formula.

Throws:

SMTLIBException - Model production was not enabled.

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

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

Overrides:

setInfo in class NoopScript

Parameters:

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

:

.

value - Value for this info.

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

Overrides:

setOption in class NoopScript

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.

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

Overrides:

simplify in class NoopScript

Parameters:

term - A (usually Boolean) term to simplify.

Returns:

The simplified term.

Throws:

SMTLIBException - If an error occurred or unsupported.

flipDecisions

public void flipDecisions()

Perform a restart and switch the decisions of all undecided literals. This method should efficiently lead the solver to explore another path in the search tree.

flipNamedLiteral

public void flipNamedLiteral(java.lang.String name)
                      throws SMTLIBException

Flip the truth value decision for a name literal.

Parameters:

name - The name used in the annotation for this literal.

Throws:

SMTLIBException - If name not known.

getClausifier

public de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier getClausifier()

Access to the internal CNF transformer. Should not be used by users.

Returns:

Internal CNF transformer.

getEngine

public de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine getEngine()

Access to the internal DPLL engine. Should not be used by users.

Returns:

Internal DPLL engine.

getLogger

public de.uni_freiburg.informatik.ultimate.smtinterpol.LogProxy getLogger()

Access to the logger used by SMTInterpol.

Returns:

The logger used by SMTInterpol.

setEngine

protected void setEngine(de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine engine)

setClausifier

protected void setClausifier(de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier clausifier)

retrieveProof

public de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.Clause retrieveProof()
                                                                          throws SMTLIBException

Retrieve the proof in its internal format. Users should use getProof() to retrieve the proof as a proof term.

Returns:

Internal proof.

Throws:

SMTLIBException - If no proof is present or the proof is found to to be incorrect.

getSatisfiedLiterals

public Term[] getSatisfiedLiterals()
                            throws SMTLIBException

Get all literals currently set to true. Note that this function might also be called if SMTInterpol is currently in an unsat state. Then, it will simply return an empty array.

Returns:

All literals currently set to true.

Throws:

SMTLIBException - If the assertion stack is modified since the last clean state.

checkAllsat

public java.lang.Iterable<Term[]> checkAllsat(Term[] input)

Description copied from interface: Script

Perform an AllSAT computation over some important predicates.

Specified by:

checkAllsat in interface Script

Overrides:

checkAllsat in class NoopScript

Parameters:

input - The important predicates. Must be Boolean.

Returns:

Iterator over minterms found during iteration.

findImpliedEquality

public Term[] findImpliedEquality(Term[] x,
                                  Term[] y)
                           throws SMTLIBException,
                                  java.lang.UnsupportedOperationException

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

Overrides:

findImpliedEquality in class NoopScript

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.

Throws:

SMTLIBException

java.lang.UnsupportedOperationException

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

Overrides:

declareFun in class NoopScript

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.

isTerminationRequested

public boolean isTerminationRequested()