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>

  • 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

  • Method Details

    • checkGenerateModels

      protected final void checkGenerateModels()

    • checkGenerateAllSat

      protected final void checkGenerateAllSat()

    • checkGenerateUnsatCores

      protected final void checkGenerateUnsatCores()

    • checkGenerateUnsatCoresOverAssumptions

      protected final void checkGenerateUnsatCoresOverAssumptions()

    • checkClosed

      protected void checkClosed()
      Checks whether the prover has been closed already. Only to be used if this is the only check performed in a call.

    • 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.

    • 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.

      Some solvers (such as MathSAT or Z3) guarantee that a model stays constant and valid as long as the solver context is available, even if constraints are added to, pushed or popped from the prover stack. If the solver does not provide this guarantee, the model will be invalidated by the next such operation, and using it will lead to an exception.

      A model might not provide values for all symbols known to the solver, but it should at least provide values for all free symbols occurring in the asserted formulas. For other symbols, the behavior is solver-dependent, e.g., the model might provide default values or leave them undefined. For uninterpreted functions, the model should provide values for all instantiations. For arrays, the model should provide values for all accessed indices. For both, uninterpreted functions and arrays, some solvers do not provide all instantiations, but only most of them. A model might contain additional symbols with their evaluation, if a solver uses its own temporary symbols.

      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

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