Package org.sosy_lab.java_smt.basicimpl

Class AbstractProverWithAllSat<T>

java.lang.Object

org.sosy_lab.java_smt.basicimpl.AbstractProver<T>

org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat<T>

All Implemented Interfaces:

AutoCloseable, BasicProverEnvironment<T>

public abstract class AbstractProverWithAllSat<T>
extends AbstractProver<T>

This class is a utility-class to avoid repeated implementation of the AllSAT computation.

If a solver does not support direct AllSAT computation, please inherit from this class.

Nested Class Summary

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

BasicProverEnvironment.AllSatCallback<R>

Field Summary

Fields inherited from class org.sosy_lab.java_smt.basicimpl.AbstractProver

contextShutdownNotifier, NO_MODEL_HELP, proverShutdownNotifier

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractProverWithAllSat(Set<SolverContext.ProverOptions> pOptions, BooleanFormulaManager pBmgr, ShutdownNotifier pContextShutdownNotifier, @Nullable ShutdownNotifier pProverShutdownNotifier)

Method Summary

Modifier and Type	Method	Description
<R> R	allSat(BasicProverEnvironment.AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)	Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.
protected abstract Evaluator	getEvaluatorWithoutChecks()	Get an evaluator instance for model evaluation without executing checks for prover options.

Methods inherited from class org.sosy_lab.java_smt.basicimpl.AbstractProver

addConstraint, addConstraintImpl, checkEnableSeparationLogic, checkGenerateAllSat, checkGenerateModels, checkInterpolationArguments, checkShutdownState, close, closeAllEvaluators, getAssertedConstraintIds, getAssertedFormulas, getEvaluator, getEvaluatorImpl, getModel, getModelAssignments, getModelImpl, getShutdownReason, getUnsatCore, getUnsatCoreImpl, isClosed, isGenerateUnsatCores, isSeparationLogicEnabled, isUnsat, isUnsatImpl, isUnsatWithAssumptions, isUnsatWithAssumptionsImpl, pop, popImpl, push, pushImpl, registerEvaluator, setLastSatCheckSat, setLastSatCheckUnsat, setStackNotChangedSinceLastQuery, shouldShutdown, shutdownIfNecessary, size, stackChangedSinceLastQuery, unregisterEvaluator, unsatCoreOverAssumptions, unsatCoreOverAssumptionsImpl, wasLastSatCheckSat

Methods inherited from class java.lang.Object

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

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

getStatistics, push, registerUserPropagator

Constructor Detail

AbstractProverWithAllSat

protected AbstractProverWithAllSat(Set<SolverContext.ProverOptions> pOptions,
                                   BooleanFormulaManager pBmgr,
                                   ShutdownNotifier pContextShutdownNotifier,
                                   @Nullable ShutdownNotifier pProverShutdownNotifier)

Method Detail

allSat

public <R> R allSat(BasicProverEnvironment.AllSatCallback<R> callback,
                    List<BooleanFormula> importantPredicates)
             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.

importantPredicates - 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

getEvaluatorWithoutChecks

protected abstract Evaluator getEvaluatorWithoutChecks()
                                                throws SolverException,
                                                       InterruptedException

Get an evaluator instance for model evaluation without executing checks for prover options.

This method allows model evaluation without explicitly enabling the prover-option SolverContext.ProverOptions.GENERATE_MODELS. We only use this method internally, when we know about a valid solver state. The returned evaluator does not have caching or any direct optimization for user interaction.

Throws:

SolverException - if model can not be constructed.

InterruptedException