Package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper

Class InterpolatingProverWithAssumptionsWrapper<T>

java.lang.Object

org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper<T>

All Implemented Interfaces:

AutoCloseable, BasicProverEnvironment<T>, InterpolatingProverEnvironment<T>

public class InterpolatingProverWithAssumptionsWrapper<T>
extends Object
implements InterpolatingProverEnvironment<T>

Nested Class Summary

Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment

BasicProverEnvironment.AllSatCallback<R>

Field Summary

Fields

Modifier and Type	Field	Description
protected final InterpolatingProverEnvironment<T>	delegate
protected final List<BooleanFormula>	solverAssumptionsAsFormula

Fields inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment

ASSUMPTION_SOLVING_NOT_SUPPORTED, NO_MODEL_HELP, UNSAT_CORE_NOT_SUPPORTED, UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED

Constructor Summary

Constructors

Constructor	Description
InterpolatingProverWithAssumptionsWrapper(InterpolatingProverEnvironment<T> pDelegate, FormulaManager pFmgr)

Method Summary

Modifier and Type	Method	Description
T	addConstraint(BooleanFormula constraint)	Add a constraint to the latest backtracking point.
<R> R	allSat(BasicProverEnvironment.AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)	Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.
protected void	clearAssumptions()
void	close()	Closes the prover environment.
BooleanFormula	getInterpolant(Collection<T> pFormulasOfA)	Get an interpolant for two groups of formulas.
Model	getModel()	Get a satisfying assignment.
ImmutableList<Model.ValueAssignment>	getModelAssignments()	Get a list of satisfying assignments.
List<BooleanFormula>	getSeqInterpolants(List<? extends Collection<T>> pPartitionedFormulas)	This method returns interpolants of an 'inductive sequence'.
ImmutableMap<String,String>	getStatistics()	Get statistics for a concrete ProverEnvironment in a solver.
List<BooleanFormula>	getTreeInterpolants(List<? extends Collection<T>> pPartitionedFormulas, int[] pStartOfSubTree)	Compute a sequence of interpolants.
List<BooleanFormula>	getUnsatCore()	Get an unsat core.
boolean	isUnsat()	Check whether the conjunction of all formulas on the stack is unsatisfiable.
boolean	isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)	Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.
void	pop()	Remove one backtracking point/level from the current stack.
void	push()	Create a new backtracking point, i.e., a new level on the assertion stack.
protected void	registerPushedFormula(T pPushResult)	overridden in subclass.
int	size()	Get the number of backtracking points/levels on the current stack.
String	toString()
Optional<List<BooleanFormula>>	unsatCoreOverAssumptions(Collection<BooleanFormula> pAssumptions)	Returns an UNSAT core (if it exists, otherwise Optional.empty()), over the chosen assumptions.

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment

addConstraint, allSat, close, getEvaluator, getModel, getModelAssignments, getStatistics, getUnsatCore, isUnsat, isUnsatWithAssumptions, pop, push, push, registerUserPropagator, size, unsatCoreOverAssumptions

Methods inherited from interface org.sosy_lab.java_smt.api.InterpolatingProverEnvironment

getSeqInterpolants0, getTreeInterpolants0

Field Details

delegate

protected final InterpolatingProverEnvironment<T> delegate

solverAssumptionsAsFormula

protected final List<BooleanFormula> solverAssumptionsAsFormula

Constructor Details

InterpolatingProverWithAssumptionsWrapper

public InterpolatingProverWithAssumptionsWrapper(InterpolatingProverEnvironment<T> pDelegate,
 FormulaManager pFmgr)

Method Details

getInterpolant

public BooleanFormula getInterpolant(Collection<T> pFormulasOfA)
                              throws SolverException,
InterruptedException

Description copied from interface: InterpolatingProverEnvironment

Get an interpolant for two groups of formulas. This should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned true.

There is no direct guarantee that the interpolants returned are part of an inductive sequence', however this seems to work for most solvers as long as the same proof is used, i.e. all interpolants are computed after the same SAT-check. If a solver does not use the same internal proof for several interpolation queries (such as CVC5), then the returned interpolants might not satisfy the sequence-criteria. We suggest the proper method InterpolatingProverEnvironment.getSeqInterpolants(java.util.List<? extends java.util.Collection<T>>) for that case.

Specified by:

getInterpolant in interface InterpolatingProverEnvironment<T>

Parameters:

pFormulasOfA - A collection of values returned by BasicProverEnvironment.push(BooleanFormula). All the corresponding formulas from group A, the remaining formulas form group B.

Returns:

An interpolant for A and B

Throws:

SolverException - if interpolant cannot be computed, for example because interpolation procedure is incomplete

InterruptedException

getSeqInterpolants

public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<T>> pPartitionedFormulas)
                                        throws SolverException,
InterruptedException

Description copied from interface: InterpolatingProverEnvironment

This method returns interpolants of an 'inductive sequence'. This property must be supported by the interpolation-strategy of the underlying SMT-solver! Depending on the underlying SMT-solver this method might be faster than N direct calls to getInterpolant().

The prover stack should contain the partitioned formulas, but any order is allowed. For an input of N partitions we return N-1 interpolants. Any asserted formula that is on the prover stack and not part of the partitioned list, will be used for background theory and its symbols can appear in any interpolant.

Specified by:

getSeqInterpolants in interface InterpolatingProverEnvironment<T>

Returns:

an 'inductive sequence' of interpolants, such that the implication AND(I_i, P_i) => I_(i+1) is satisfied for all i, where P_i is the conjunction of all formulas in partition i.

Throws:

SolverException - if interpolant cannot be computed, for example because interpolation procedure is incomplete

InterruptedException

getTreeInterpolants

public List<BooleanFormula> getTreeInterpolants(List<? extends Collection<T>> pPartitionedFormulas,
 int[] pStartOfSubTree)
                                         throws SolverException,
InterruptedException

Description copied from interface: InterpolatingProverEnvironment

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.

Example:

 A  D
 |  |
 B  E
 | /
 C
 |
 F  H
 | /
 G

 arrayIndex     = [0,1,2,3,4,5,6,7]  // only for demonstration, not needed
 partition      = [A,B,D,E,C,F,H,G]  // post-order of tree
 startOfSubTree = [0,0,2,2,0,0,6,0]  // index of left-most leaf of the current element
 

The prover stack should contain the partitioned formulas. For an input of N partitions (nodes in the tree) we return N-1 interpolants (one interpolant for/below each node except the root). Any asserted formula that is on the prover stack and not part of the partitioned list, will be used for background theory and its symbols can appear in any interpolant.

Specified by:

getTreeInterpolants in interface InterpolatingProverEnvironment<T>

Parameters:

pPartitionedFormulas - of formulas

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

Returns:

Tree interpolants respecting the nesting relation.

Throws:

SolverException - if interpolant cannot be computed, for example because interpolation procedure is incomplete

InterruptedException

registerPushedFormula

protected void registerPushedFormula(T pPushResult)

overridden in subclass.

clearAssumptions

protected void clearAssumptions()

pop

public void pop()

Description copied from interface: BasicProverEnvironment

Remove one backtracking point/level from the current stack. This removes the latest level including all of its formulas, i.e., all formulas that were added for this backtracking point.

Specified by:

pop in interface BasicProverEnvironment<T>

addConstraint

public T addConstraint(BooleanFormula constraint)
                throws InterruptedException

Description copied from interface: BasicProverEnvironment

Add a constraint to the latest backtracking point.

Specified by:

addConstraint in interface BasicProverEnvironment<T>

Throws:

InterruptedException

push

public void push()
          throws InterruptedException

Description copied from interface: BasicProverEnvironment

Create a new backtracking point, i.e., a new level on the assertion stack. Each level can hold several asserted formulas.

If formulas are added before creating the first backtracking point, they can not be removed via a POP-operation.

Specified by:

push in interface BasicProverEnvironment<T>

Throws:

InterruptedException

size

public int size()

Description copied from interface: BasicProverEnvironment

Get the number of backtracking points/levels on the current stack.

Caution: This is the number of PUSH-operations, and not necessarily equal to the number of asserted formulas. On any level there can be an arbitrary number of asserted formulas. Even with size of 0, formulas can already be asserted (at bottom level).

Specified by:

size in interface BasicProverEnvironment<T>

isUnsat

public boolean isUnsat()
                throws SolverException,
InterruptedException

Description copied from interface: BasicProverEnvironment

Check whether the conjunction of all formulas on the stack is unsatisfiable.

Specified by:

isUnsat in interface BasicProverEnvironment<T>

Throws:

SolverException

InterruptedException

isUnsatWithAssumptions

public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
                               throws SolverException,
InterruptedException

Description copied from interface: BasicProverEnvironment

Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.

Specified by:

isUnsatWithAssumptions in interface BasicProverEnvironment<T>

Parameters:

assumptions - A list of literals.

Throws:

SolverException

InterruptedException

getModel

public Model getModel()
               throws SolverException

Description copied from interface: BasicProverEnvironment

Get a satisfying assignment. This method should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned false.

Some solvers (such as MathSAT or Z3) guarantee that a model stays constant and valid as long as the solver context is available, even if constraints are added to, pushed or popped from the prover stack. If the solver does not provide this guarantee, the model will be invalidated by the next such operation, and using it will lead to an exception.

A model might not provide values for all symbols known to the solver, but it should at least provide values for all free symbols occurring in the asserted formulas. For other symbols, the behavior is solver-dependent, e.g., the model might provide default values or leave them undefined. For uninterpreted functions, the model should provide values for all instantiations. For arrays, the model should provide values for all accessed indices. For both, uninterpreted functions and arrays, some solvers do not provide all instantiations, but only most of them. A model might contain additional symbols with their evaluation, if a solver uses its own temporary symbols.

Specified by:

getModel in interface BasicProverEnvironment<T>

Throws:

SolverException

getModelAssignments

public ImmutableList<Model.ValueAssignment> getModelAssignments()
                                                         throws SolverException

Description copied from interface: BasicProverEnvironment

Get a list of satisfying assignments. This is equivalent to ImmutableList.copyOf(getModel()), but removes the need for calling Model.close().

Note that if you need to iterate multiple times over the model it may be more efficient to use this method instead of BasicProverEnvironment.getModel() (depending on the solver).

Specified by:

getModelAssignments in interface BasicProverEnvironment<T>

Throws:

SolverException

getUnsatCore

public List<BooleanFormula> getUnsatCore()

Description copied from interface: BasicProverEnvironment

Get an unsat core.

This should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned false. Requires the SolverContext.ProverOptions.GENERATE_UNSAT_CORE option to work.

Specified by:

getUnsatCore in interface BasicProverEnvironment<T>

unsatCoreOverAssumptions

public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> pAssumptions)
                                                        throws SolverException,
InterruptedException

Description copied from interface: BasicProverEnvironment

Returns an UNSAT core (if it exists, otherwise Optional.empty()), over the chosen assumptions. Neither BasicProverEnvironment.isUnsat(), nor BasicProverEnvironment.isUnsatWithAssumptions(Collection) needs to be called before using this method, as BasicProverEnvironment.isUnsatWithAssumptions(Collection) is automatically called with the given assumptions.

Requires the SolverContext.ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS option to work. SolverContext.ProverOptions.GENERATE_UNSAT_CORE is not needed, but both options can be safely combined.

Specified by:

unsatCoreOverAssumptions in interface BasicProverEnvironment<T>

Parameters:

pAssumptions - Selected assumptions.

Returns:

Empty optional if the constraints with assumptions are satisfiable, subset of assumptions which is unsatisfiable with the original constraints otherwise.

Throws:

SolverException

InterruptedException

getStatistics

public ImmutableMap<String,String> getStatistics()

Description copied from interface: BasicProverEnvironment

Get statistics for a concrete ProverEnvironment in a solver. The returned mapping is intended to provide solver-internal statistics for only this instance. The keys can differ between individual solvers.

Calling the statistics several times for the same ProverEnvironments returns accumulated number, i.e., we currently do not provide any possibility to reset the statistics. Calling the statistics for different ProverEnvironments returns independent statistics.

We do not guarantee any specific key to be present, as this depends on the used solver. We might even return an empty mapping if the solver does not support calling this method or is in an invalid state.

Specified by:

getStatistics in interface BasicProverEnvironment<T>

See Also:

• SolverContext.getStatistics()

close

public void close()

Description copied from interface: BasicProverEnvironment

Closes the prover environment. The object should be discarded, and should not be used after closing. The first call of this method will close the prover instance, further calls are ignored.

Specified by:

close in interface AutoCloseable

Specified by:

close in interface BasicProverEnvironment<T>

toString

public String toString()

Overrides:

toString in class Object

allSat

public <R> R allSat(BasicProverEnvironment.AllSatCallback<R> pCallback,
 List<BooleanFormula> pImportant)
             throws InterruptedException,
SolverException

Description copied from interface: BasicProverEnvironment

Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.

Specified by:

allSat in interface BasicProverEnvironment<T>

pImportant - A set of (positive) variables appearing in the asserted queries. Only these variables will appear in the region.

Returns:

A region representing all satisfying models of the formula.

Throws:

InterruptedException

SolverException