Package org.sosy_lab.java_smt.api
Interface ProverEnvironment
-
- All Superinterfaces:
AutoCloseable
,BasicProverEnvironment<Void>
- All Known Implementing Classes:
DebuggingProverEnvironment
,ProverWithAssumptionsWrapper
public interface ProverEnvironment extends BasicProverEnvironment<Void>
An interface to an incremental SMT solver with methods for pushing and popping formulas as well as SAT checks. Instances of this class can be used once for a series of related queries. After that, theBasicProverEnvironment.close()
method should be called (preferably using the try-with-resources syntax). All methods are expected to throwIllegalStateException
s after close was called.All solving methods are expected to throw
SolverException
if the solver fails to solve the given query, andInterruptedException
if a thread interrupt was requested or a shutdown request via theShutdownNotifier
. It is not guaranteed, though, that solvers respond in a timely manner (or at all) to shut down or interrupt requests.
-
-
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
-
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
-
-