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 ShutdownNotifier`	`contextShutdownNotifier`
`protected static String`	`NO_MODEL_HELP`
`protected @Nullable ShutdownNotifier`	`proverShutdownNotifier`

Constructor Summary

Constructors
Modifier	Constructor	Description
`protected`	`AbstractProver(ShutdownNotifier pContextShutdownNotifier, @Nullable ShutdownNotifier pProverShutdownNotifier, Set<SolverContext.ProverOptions> pOptions)`

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
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`	`checkInterpolationArguments(Collection<T> formulasOfA)`
`void`	`checkShutdownState()`
`void`	`close()`	Closes the prover environment.
`protected void`	`closeAllEvaluators()`
`protected ImmutableSet<T>`	`getAssertedConstraintIds()`
`protected ImmutableSet<BooleanFormula>`	`getAssertedFormulas()`
`Evaluator`	`getEvaluator()`	Get a temporary view on the current satisfying assignment.
`protected Evaluator`	`getEvaluatorImpl()`
`Model`	`getModel()`	Get a satisfying assignment.
`ImmutableList<Model.ValueAssignment>`	`getModelAssignments()`	Get a list of satisfying assignments.
`protected abstract Model`	`getModelImpl()`
`protected String`	`getShutdownReason()`	Only to be called when at least one of the shutdown notifiers is supposed to be shutting down! Throws an Exception if no shutdown is requested!
`List<BooleanFormula>`	`getUnsatCore()`	Get an unsat core.
`protected abstract List<BooleanFormula>`	`getUnsatCoreImpl()`
`protected boolean`	`isClosed()`
`protected boolean`	`isGenerateUnsatCores()`
`protected boolean`	`isSeparationLogicEnabled()`
`boolean`	`isUnsat()`	Check whether the conjunction of all formulas on the stack is unsatisfiable.
`protected abstract boolean`	`isUnsatImpl()`
`boolean`	`isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)`	Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.
`protected abstract boolean`	`isUnsatWithAssumptionsImpl(Collection<BooleanFormula> assumptions)`
`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.
`protected void`	`setLastSatCheckSat()`
`protected void`	`setLastSatCheckUnsat()`
`protected void`	`setStackNotChangedSinceLastQuery()`
`protected boolean`	`shouldShutdown()`
`protected void`	`shutdownIfNecessary()`
`int`	`size()`	Get the number of backtracking points/levels on the current stack.
`protected boolean`	`stackChangedSinceLastQuery()`
`protected void`	`unregisterEvaluator(Evaluator pEvaluator)`
`Optional<List<BooleanFormula>>`	`unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions)`	Returns an UNSAT core (if it exists, otherwise `Optional.empty()`), over the chosen assumptions.
`protected abstract Optional<List<BooleanFormula>>`	`unsatCoreOverAssumptionsImpl(Collection<BooleanFormula> assumptions)`
`protected boolean`	`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
allSat, getStatistics, push, registerUserPropagator

- Field Detail
  - NO_MODEL_HELP
```
protected static final String NO_MODEL_HELP
```
    See Also:
    
    Constant Field Values
  - proverShutdownNotifier
```
protected final @Nullable ShutdownNotifier proverShutdownNotifier
```
  - contextShutdownNotifier
```
protected final ShutdownNotifier contextShutdownNotifier
```
- Constructor Detail
  - AbstractProver
```
protected AbstractProver(ShutdownNotifier pContextShutdownNotifier,
                         @Nullable ShutdownNotifier pProverShutdownNotifier,
                         Set<SolverContext.ProverOptions> pOptions)
```
- Method Detail
  - shutdownIfNecessary
```
protected final void shutdownIfNecessary()
                                  throws InterruptedException
```
    Throws:
    
    InterruptedException
  - shouldShutdown
```
protected final boolean shouldShutdown()
```
  - checkShutdownState
```
public void checkShutdownState()
```
  - isGenerateUnsatCores
```
protected boolean isGenerateUnsatCores()
```
  - isClosed
```
protected boolean isClosed()
```
  - isSeparationLogicEnabled
```
protected boolean isSeparationLogicEnabled()
```
  - stackChangedSinceLastQuery
```
protected boolean stackChangedSinceLastQuery()
```
  - setStackNotChangedSinceLastQuery
```
protected void setStackNotChangedSinceLastQuery()
```
  - wasLastSatCheckSat
```
protected boolean wasLastSatCheckSat()
```
  - setLastSatCheckSat
```
protected void setLastSatCheckSat()
```
  - setLastSatCheckUnsat
```
protected void setLastSatCheckUnsat()
```
  - getShutdownReason
```
protected final String getShutdownReason()
```
    Only to be called when at least one of the shutdown notifiers is supposed to be shutting down! Throws an Exception if no shutdown is requested!
  - checkGenerateModels
```
protected final void checkGenerateModels()
```
  - checkGenerateAllSat
```
protected final void checkGenerateAllSat()
```
  - 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>
  - isUnsat
```
public final boolean isUnsat()
                      throws SolverException,
                             InterruptedException
```
    Description copied from interface: BasicProverEnvironment
    
    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
  - getUnsatCore
```
public List<BooleanFormula> getUnsatCore()
```
    Description copied from interface: BasicProverEnvironment
    
    Get an unsat core. This should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned false.
    
    Specified by:
    
    getUnsatCore in interface BasicProverEnvironment<T>
  - getUnsatCoreImpl
```
protected abstract List<BooleanFormula> getUnsatCoreImpl()
```
  - unsatCoreOverAssumptions
```
public final Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions)
                                                              throws SolverException,
                                                                     InterruptedException
```
    Description copied from interface: BasicProverEnvironment
    
    Returns an UNSAT core (if it exists, otherwise Optional.empty()), over the chosen assumptions. Does NOT require the SolverContext.ProverOptions.GENERATE_UNSAT_CORE option to work, but SolverContext.ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS.
    
    Specified by:
    
    unsatCoreOverAssumptions in interface BasicProverEnvironment<T>
    
    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
  - unsatCoreOverAssumptionsImpl
```
protected abstract Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(Collection<BooleanFormula> assumptions)
                                                                        throws SolverException,
                                                                               InterruptedException
```
    Throws:
    
    SolverException
    
    InterruptedException
  - isUnsatWithAssumptions
```
public final boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
                                     throws SolverException,
                                            InterruptedException
```
    Description copied from interface: BasicProverEnvironment
    
    Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.
    
    Specified by:
    
    isUnsatWithAssumptions in interface BasicProverEnvironment<T>
    
    Parameters:
    
    assumptions - A list of literals.
    
    Throws:
    
    SolverException
    
    InterruptedException
  - isUnsatWithAssumptionsImpl
```
protected abstract boolean isUnsatWithAssumptionsImpl(Collection<BooleanFormula> assumptions)
                                               throws SolverException,
                                                      InterruptedException
```
    Throws:
    
    SolverException
    
    InterruptedException
  - getModel
```
public final Model getModel()
                     throws SolverException
```
    Description copied from interface: BasicProverEnvironment
    
    Get a satisfying assignment. This method should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned false. 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.
    
    Specified by:
    
    getModel in interface BasicProverEnvironment<T>
    
    Throws:
    
    SolverException
  - getModelImpl
```
protected abstract Model getModelImpl()
                               throws SolverException
```
    Throws:
    
    SolverException
  - getEvaluator
```
public final Evaluator getEvaluator()
                             throws SolverException
```
    Description copied from interface: BasicProverEnvironment
    
    Get a temporary view on the current satisfying assignment. This should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned false. The evaluator should no longer be used as soon as any constraints are added to, pushed, or popped from the prover stack.
    
    Specified by:
    
    getEvaluator in interface BasicProverEnvironment<T>
    
    Throws:
    
    SolverException
  - getEvaluatorImpl
```
protected Evaluator getEvaluatorImpl()
                              throws SolverException
```
    Throws:
    
    SolverException
  - 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()
```
  - checkInterpolationArguments
```
protected void checkInterpolationArguments(Collection<T> formulasOfA)
```
  - 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()
```
  - getModelAssignments
```
public ImmutableList<Model.ValueAssignment> getModelAssignments()
                                                         throws SolverException
```
    Description copied from interface: BasicProverEnvironment
    
    Get a list of satisfying assignments. This is equivalent to ImmutableList.copyOf(getModel()), but removes the need for calling Model.close().
    Note that if you need to iterate multiple times over the model it may be more efficient to use this method instead of BasicProverEnvironment.getModel() (depending on the solver).
    
    Specified by:
    
    getModelAssignments in interface BasicProverEnvironment<T>
    
    Throws:
    
    SolverException
  - 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>

Class AbstractProver<T>

Nested Class Summary

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

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

NO_MODEL_HELP

proverShutdownNotifier

contextShutdownNotifier

Constructor Detail

AbstractProver

Method Detail

shutdownIfNecessary

shouldShutdown

checkShutdownState

isGenerateUnsatCores

isClosed

isSeparationLogicEnabled

stackChangedSinceLastQuery

setStackNotChangedSinceLastQuery

wasLastSatCheckSat

setLastSatCheckSat

setLastSatCheckUnsat

getShutdownReason

checkGenerateModels

checkGenerateAllSat

checkEnableSeparationLogic

size

isUnsat

isUnsatImpl

getUnsatCore

getUnsatCoreImpl

unsatCoreOverAssumptions

unsatCoreOverAssumptionsImpl

isUnsatWithAssumptions

isUnsatWithAssumptionsImpl

getModel

getModelImpl

getEvaluator

getEvaluatorImpl

push

pushImpl

pop

popImpl

addConstraint

addConstraintImpl

getAssertedFormulas

getAssertedConstraintIds

checkInterpolationArguments

registerEvaluator

unregisterEvaluator

closeAllEvaluators

getModelAssignments

close