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	closed
protected boolean	enableSL
protected boolean	generateUnsatCores

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

NO_MODEL_HELP

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	Description
@Nullable T	addConstraint(BooleanFormula constraint)	Add a constraint to the latest backtracking point.
protected abstract @Nullable T	addConstraintImpl(BooleanFormula constraint)
protected void	checkEnableSeparationLogic()
protected void	checkGenerateAllSat()
protected void	checkGenerateModels()
protected void	checkGenerateUnsatCores()
protected void	checkGenerateUnsatCoresOverAssumptions()
void	close()	Closes the prover environment.
protected void	closeAllEvaluators()
protected ImmutableSet<T>	getAssertedConstraintIds()
protected ImmutableSet<BooleanFormula>	getAssertedFormulas()
void	pop()	Remove one backtracking point/level from the current stack.
protected abstract void	popImpl()
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, isUnsat, isUnsatWithAssumptions, push, registerUserPropagator, unsatCoreOverAssumptions

Field Detail

generateUnsatCores

protected final boolean generateUnsatCores

enableSL

protected final boolean enableSL

closed

protected boolean closed

Constructor Detail

AbstractProver

protected AbstractProver(Set<SolverContext.ProverOptions> pOptions)

Method Detail

checkGenerateModels

protected final void checkGenerateModels()

checkGenerateAllSat

protected final void checkGenerateAllSat()

checkGenerateUnsatCores

protected final void checkGenerateUnsatCores()

checkGenerateUnsatCoresOverAssumptions

protected final void checkGenerateUnsatCoresOverAssumptions()

checkEnableSeparationLogic

protected final void checkEnableSeparationLogic()

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

getAssertedFormulas

protected ImmutableSet<BooleanFormula> getAssertedFormulas()

getAssertedConstraintIds

protected ImmutableSet<T> getAssertedConstraintIds()

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>