Package org.sosy_lab.java_smt.basicimpl

Class AbstractProver<T>

java.lang.Object

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

All Implemented Interfaces:

AutoCloseable, BasicProverEnvironment<T>

Direct Known Subclasses:

AbstractProverWithAllSat

public abstract class AbstractProver<T>
extends Object
implements BasicProverEnvironment<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 boolean	changedSinceLastSatQuery
protected boolean	closed
protected final boolean	enableSL
protected final boolean	generateAllSat
protected final boolean	generateModels
protected final boolean	generateUnsatCores
protected final boolean	generateUnsatCoresOverAssumptions
protected boolean	wasLastSatCheckSatisfiable

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

Modifier	Constructor	Description
protected	AbstractProver(Set<SolverContext.ProverOptions> pOptions)

Method Summary

Modifier and Type	Method	Description
final @Nullable T	addConstraint(BooleanFormula constraint)	Add a constraint to the latest backtracking point.
protected abstract @Nullable T	addConstraintImpl(BooleanFormula constraint)
final OptimizationProverEnvironment.OptStatus	check()	Performs an optimization-aware check and returns the optimization status.
protected final void	checkEnableSeparationLogic()
protected final void	checkGenerateAllSat()
protected final void	checkGenerateInterpolants(Collection<T> formulasOfA)
protected final void	checkGenerateModels()
protected final void	checkGenerateSeqInterpolants(List<? extends Collection<T>> partitionedFormulas)
protected final void	checkGenerateTreeInterpolants(List<? extends Collection<T>> partitionedFormulas, int[] startOfSubTree)
protected final void	checkGenerateUnsatCores()
protected final void	checkGenerateUnsatCoresOverAssumptions()
protected OptimizationProverEnvironment.OptStatus	checkImpl()	Implementation of optimization-aware satisfiability-check.
void	close()	Closes the prover environment.
protected void	closeAllEvaluators()
protected ImmutableSet<T>	getAssertedConstraintIds()
protected ImmutableSet<BooleanFormula>	getAssertedFormulas()
protected ImmutableMap<T,BooleanFormula>	getAssertedFormulasById()	Flatten and inverse the prover-stack and return all asserted constraints.
protected abstract boolean	hasPersistentModel()
final boolean	isUnsat()	Check whether the conjunction of all formulas on the stack is unsatisfiable.
protected abstract boolean	isUnsatImpl()
final void	pop()	Remove one backtracking point/level from the current stack.
protected abstract void	popImpl()
final void	push()	Create a new backtracking point, i.e., a new level on the assertion stack.
protected abstract void	pushImpl()
protected <E extends Evaluator> E	registerEvaluator(E pEvaluator)	This method registers the Evaluator to be cleaned up before the next change on the prover stack.
int	size()	Get the number of backtracking points/levels on the current stack.
protected void	unregisterEvaluator(Evaluator pEvaluator)

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

allSat, getEvaluator, getModel, getModelAssignments, getStatistics, getUnsatCore, isUnsatWithAssumptions, push, registerUserPropagator, unsatCoreOverAssumptions

Field Details

generateModels

protected final boolean generateModels

generateAllSat

protected final boolean generateAllSat

generateUnsatCores

protected final boolean generateUnsatCores

generateUnsatCoresOverAssumptions

protected final boolean generateUnsatCoresOverAssumptions

enableSL

protected final boolean enableSL

closed

protected boolean closed

wasLastSatCheckSatisfiable

protected boolean wasLastSatCheckSatisfiable

changedSinceLastSatQuery

protected boolean changedSinceLastSatQuery

Constructor Details

AbstractProver

protected AbstractProver(Set<SolverContext.ProverOptions> pOptions)

Method Details

checkGenerateModels

protected final void checkGenerateModels()

checkGenerateAllSat

protected final void checkGenerateAllSat()

checkGenerateUnsatCores

protected final void checkGenerateUnsatCores()

checkGenerateUnsatCoresOverAssumptions

protected final void checkGenerateUnsatCoresOverAssumptions()

checkGenerateInterpolants

protected final void checkGenerateInterpolants(Collection<T> formulasOfA)

checkGenerateSeqInterpolants

protected final void checkGenerateSeqInterpolants(List<? extends Collection<T>> partitionedFormulas)

checkGenerateTreeInterpolants

protected final void checkGenerateTreeInterpolants(List<? extends Collection<T>> partitionedFormulas,
 int[] startOfSubTree)

checkEnableSeparationLogic

protected final void checkEnableSeparationLogic()

hasPersistentModel

protected abstract boolean hasPersistentModel()

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>

push

public final 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

pushImpl

protected abstract void pushImpl()
                          throws InterruptedException

Throws:

InterruptedException

pop

public final 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>

popImpl

protected abstract void popImpl()

addConstraint

@CanIgnoreReturnValue
public final @Nullable 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

addConstraintImpl

protected abstract @Nullable T addConstraintImpl(BooleanFormula constraint)
                                          throws InterruptedException

Throws:

InterruptedException

isUnsat

public final boolean isUnsat()
                      throws SolverException,
InterruptedException

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

Specified by:

isUnsat in interface BasicProverEnvironment<T>

Throws:

SolverException

InterruptedException

isUnsatImpl

protected abstract boolean isUnsatImpl()
                                throws SolverException,
InterruptedException

Throws:

SolverException

InterruptedException

check

public final OptimizationProverEnvironment.OptStatus check()
                                                    throws InterruptedException,
SolverException

Performs an optimization-aware check and returns the optimization status.

This method is the public entry point for optimization checks. It validates that the prover is open, resets internal change-tracking state, and delegates solver-specific work to checkImpl(). Subclasses that implement optimization support must provide the actual checking logic in checkImpl().

The signature of this method matches that of OptimizationProverEnvironment.check(), to allow overrides in subclasses that implement both BasicProverEnvironment and OptimizationProverEnvironment.

Returns:

the optimization status; OptimizationProverEnvironment.OptStatus.OPT indicates a satisfiable/optimal result

Throws:

InterruptedException

SolverException

checkImpl

protected OptimizationProverEnvironment.OptStatus checkImpl()
                                                     throws InterruptedException,
SolverException

Implementation of optimization-aware satisfiability-check.

Throws:

InterruptedException - if the thread is interrupted during the check

SolverException - if the underlying solver reports an error

UnsupportedOperationException - if optimization is not supported by this prover

getAssertedFormulas

protected ImmutableSet<BooleanFormula> getAssertedFormulas()

getAssertedConstraintIds

protected ImmutableSet<T> getAssertedConstraintIds()

getAssertedFormulasById

protected ImmutableMap<T,BooleanFormula> getAssertedFormulasById()

Flatten and inverse the prover-stack and return all asserted constraints.

Each formula can be asserted several times. However, each assertion has a unique id. This implies that the inverted mapping is a plain Map, not a Multimap.

registerEvaluator

protected <E extends Evaluator> E registerEvaluator(E pEvaluator)

This method registers the Evaluator to be cleaned up before the next change on the prover stack.

unregisterEvaluator

protected void unregisterEvaluator(Evaluator pEvaluator)

closeAllEvaluators

protected void closeAllEvaluators()

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>