Interface InterpolatingProverEnvironment<T>
-
- Type Parameters:
T
- The type of the objects which can be used to select formulas for interpolant creation.
- All Superinterfaces:
AutoCloseable
,BasicProverEnvironment<T>
- All Known Implementing Classes:
DebuggingInterpolatingProverEnvironment
,InterpolatingProverWithAssumptionsWrapper
public interface InterpolatingProverEnvironment<T> extends BasicProverEnvironment<T>
This class provides an interface to an incremental SMT solver with methods for pushing and popping formulas as well as SAT checks. Furthermore, interpolants can be generated for an unsatisfiable list of formulas.
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment
BasicProverEnvironment.AllSatCallback<R>
-
-
Field Summary
-
Fields inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment
NO_MODEL_HELP
-
-
Method Summary
All Methods Static Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description static boolean
checkTreeStructure(int numOfPartitions, int[] startOfSubTree)
Checks for a valid subtree-structure.BooleanFormula
getInterpolant(Collection<T> formulasOfA)
Get an interpolant for two groups of formulas.default List<BooleanFormula>
getSeqInterpolants(List<? extends Collection<T>> partitionedFormulas)
This method returns interpolants of an 'inductive sequence'.default List<BooleanFormula>
getSeqInterpolants0(List<T> formulas)
This utility method wraps each formula in a collection and then forwards togetSeqInterpolants(java.util.List<? extends java.util.Collection<T>>)
.List<BooleanFormula>
getTreeInterpolants(List<? extends Collection<T>> partitionedFormulas, int[] startOfSubTree)
Compute a sequence of interpolants.default List<BooleanFormula>
getTreeInterpolants0(List<T> formulas, int[] startOfSubTree)
This utility method wraps each formula in a collection and then forwards togetTreeInterpolants(java.util.List<? extends java.util.Collection<T>>, int[])
.-
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
-
-
-
-
Method Detail
-
getInterpolant
BooleanFormula getInterpolant(Collection<T> formulasOfA) throws SolverException, InterruptedException
Get an interpolant for two groups of formulas. This should be called only immediately after anBasicProverEnvironment.isUnsat()
call that returnedtrue
.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
getSeqInterpolants(java.util.List<? extends java.util.Collection<T>>)
for that case.- Parameters:
formulasOfA
- A collection of values returned byBasicProverEnvironment.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 incompleteInterruptedException
-
getSeqInterpolants
default List<BooleanFormula> getSeqInterpolants(List<? extends Collection<T>> partitionedFormulas) throws SolverException, InterruptedException
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.
- Returns:
- a '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 incompleteInterruptedException
-
getSeqInterpolants0
default List<BooleanFormula> getSeqInterpolants0(List<T> formulas) throws SolverException, InterruptedException
This utility method wraps each formula in a collection and then forwards togetSeqInterpolants(java.util.List<? extends java.util.Collection<T>>)
.
-
getTreeInterpolants
List<BooleanFormula> getTreeInterpolants(List<? extends Collection<T>> partitionedFormulas, int[] startOfSubTree) throws SolverException, InterruptedException
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.
- Parameters:
partitionedFormulas
- of formulasstartOfSubTree
- 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 incompleteInterruptedException
-
getTreeInterpolants0
default List<BooleanFormula> getTreeInterpolants0(List<T> formulas, int[] startOfSubTree) throws SolverException, InterruptedException
This utility method wraps each formula in a collection and then forwards togetTreeInterpolants(java.util.List<? extends java.util.Collection<T>>, int[])
.
-
checkTreeStructure
static boolean checkTreeStructure(int numOfPartitions, int[] startOfSubTree)
Checks for a valid subtree-structure. This code is taken from SMTinterpol.
-
-