Interface BasicProverEnvironment<T>
-
- All Superinterfaces:
AutoCloseable
- All Known Subinterfaces:
InterpolatingProverEnvironment<T>
,OptimizationProverEnvironment
,ProverEnvironment
- All Known Implementing Classes:
AbstractProver
,AbstractProverWithAllSat
,BasicProverWithAssumptionsWrapper
,DebuggingInterpolatingProverEnvironment
,DebuggingOptimizationProverEnvironment
,DebuggingProverEnvironment
,InterpolatingProverWithAssumptionsWrapper
,ProverWithAssumptionsWrapper
public interface BasicProverEnvironment<T> extends AutoCloseable
Super interface forProverEnvironment
andInterpolatingProverEnvironment
that provides only the common operations. In most cases, just use one of the two sub-interfaces
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static interface
BasicProverEnvironment.AllSatCallback<R>
-
Field Summary
Fields Modifier and Type Field Description static String
NO_MODEL_HELP
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description @Nullable T
addConstraint(BooleanFormula constraint)
Add a constraint to the latest backtracking point.<R> R
allSat(BasicProverEnvironment.AllSatCallback<R> callback, List<BooleanFormula> important)
Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.void
close()
Closes the prover environment.default Evaluator
getEvaluator()
Get a temporary view on the current satisfying assignment.Model
getModel()
Get a satisfying assignment.default ImmutableList<Model.ValueAssignment>
getModelAssignments()
Get a list of satisfying assignments.default ImmutableMap<String,String>
getStatistics()
Get statistics for a concrete ProverEnvironment in a solver.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.default @Nullable T
push(BooleanFormula f)
Push a backtracking point and add a formula to the current stack, asserting it.default boolean
registerUserPropagator(UserPropagator propagator)
Registers aUserPropagator
for this prover environment.int
size()
Get the number of backtracking points/levels on the current stack.Optional<List<BooleanFormula>>
unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions)
Returns an UNSAT core (if it exists, otherwiseOptional.empty()
), over the chosen assumptions.
-
-
-
Field Detail
-
NO_MODEL_HELP
static final String NO_MODEL_HELP
- See Also:
- Constant Field Values
-
-
Method Detail
-
push
@CanIgnoreReturnValue default @Nullable T push(BooleanFormula f) throws InterruptedException
Push a backtracking point and add a formula to the current stack, asserting it. The return value may be used to identify this formula later on in a query (this depends on the sub-type of the environment).- Throws:
InterruptedException
-
pop
void pop()
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.
-
addConstraint
@CanIgnoreReturnValue @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException
Add a constraint to the latest backtracking point.- Throws:
InterruptedException
-
push
void push() throws InterruptedException
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.
- Throws:
InterruptedException
-
size
int size()
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).
-
isUnsat
boolean isUnsat() throws SolverException, InterruptedException
Check whether the conjunction of all formulas on the stack is unsatisfiable.- Throws:
SolverException
InterruptedException
-
isUnsatWithAssumptions
boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException
Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.- Parameters:
assumptions
- A list of literals.- Throws:
SolverException
InterruptedException
-
getModel
Model getModel() throws SolverException
Get a satisfying assignment. This method should be called only immediately after anisUnsat()
call that returnedfalse
. The returned model is guaranteed to stay constant and valid as long as the solver context is available, even if constraints are added to, pushed or popped from the prover stack.A model might contain additional symbols with their evaluation, if a solver uses its own temporary symbols. There should be at least a value-assignment for each free symbol.
- Throws:
SolverException
-
getEvaluator
default Evaluator getEvaluator() throws SolverException
Get a temporary view on the current satisfying assignment. This should be called only immediately after anisUnsat()
call that returnedfalse
. The evaluator should no longer be used as soon as any constraints are added to, pushed, or popped from the prover stack.- Throws:
SolverException
-
getModelAssignments
default ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException
Get a list of satisfying assignments. This is equivalent toImmutableList.copyOf(getModel())
, but removes the need for callingModel.close()
.Note that if you need to iterate multiple times over the model it may be more efficient to use this method instead of
getModel()
(depending on the solver).- Throws:
SolverException
-
getUnsatCore
List<BooleanFormula> getUnsatCore()
Get an unsat core. This should be called only immediately after anisUnsat()
call that returnedfalse
.
-
unsatCoreOverAssumptions
Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException
Returns an UNSAT core (if it exists, otherwiseOptional.empty()
), over the chosen assumptions. Does NOT require theSolverContext.ProverOptions.GENERATE_UNSAT_CORE
option to work.- Parameters:
assumptions
- 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
default ImmutableMap<String,String> getStatistics()
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
ProverEnvironment
s returns accumulated number, i.e., we currently do not provide any possibility to reset the statistics. Calling the statistics for differentProverEnvironment
s 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.
- See Also:
SolverContext.getStatistics()
-
close
void close()
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 interfaceAutoCloseable
-
allSat
<R> R allSat(BasicProverEnvironment.AllSatCallback<R> callback, List<BooleanFormula> important) throws InterruptedException, SolverException
Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.- Parameters:
important
- 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
-
registerUserPropagator
default boolean registerUserPropagator(UserPropagator propagator)
Registers aUserPropagator
for this prover environment. Only a single user propagator can be registered at a time, and each user propagator shall only be registered once in its lifetime (see alsoUserPropagator.initializeWithBackend(org.sosy_lab.java_smt.api.PropagatorBackend)
).- Parameters:
propagator
- The (fresh) user propagator to register.- Returns:
true
, if the user propagator was successfully registered. Most SMT solvers do not support user propagators and hence returnfalse
.
-
-