Package org.sosy_lab.java_smt.basicimpl

Class CachingModel

java.lang.Object
org.sosy_lab.java_smt.basicimpl.CachingModel
All Implemented Interfaces:
AutoCloseable, Iterable<Model.ValueAssignment>, Evaluator, Model
public class CachingModel extends Object implements Model

  • Constructor Details

    • CachingModel

      public CachingModel(Model pDelegate)

  • Method Details

    • asList

      public ImmutableList<Model.ValueAssignment> asList()
      Description copied from interface: Model
      Returns a list of model assignments that remains valid after the model is closed (via Model.close()).

      The returned ImmutableList contains the same Model.ValueAssignment elements that Model.iterator() would provide, but it is a materialized copy such that the list and its elements can still be accessed safely after the model has been closed. Methods that rely on live solver state such as Model.iterator() or Evaluator.evaluate(Formula) should not be used after Model.close(), whereas the returned list can always be used, until the underlying solver context is closed (SolverContext.close()).

      This representation is primarily intended for model inspection and debugging. For precise evaluation of individual formulas prefer targeted calls to Evaluator.evaluate(Formula).

      Specified by:
      asList in interface Model

    • close

      public void close()
      Description copied from interface: Model
      Free resources associated with this model (existing Model.ValueAssignment instances stay valid, but Evaluator.evaluate(Formula) etc. and Model.iterator() must not be called again).

      For several solvers (such as MATHSAT5, SMTInterpol, Z3) the model remains valid even after changes to the prover environment from which it was obtained. For other solvers (CVC4, CVC5, Princess, Boolector, Bitwuzla) the model becomes invalid after any change to the prover environment.

      Specified by:
      close in interface AutoCloseable
      Specified by:
      close in interface Evaluator
      Specified by:
      close in interface Model

    • eval

      public <T extends Formula> @Nullable T eval(T formula)
      Description copied from interface: Evaluator
      Evaluate a given formula substituting the values from the model and return it as formula.

      If a value is not relevant to the satisfiability result, the solver can choose either to insert an arbitrary value (e.g., the value 0 for the matching type) or just return null.

      The formula does not need to be a variable, we also allow complex expression. The solver will replace all symbols from the formula with their model values and then simplify the formula into a simple formula, e.g., consisting only of a numeral expression.

      Specified by:
      eval in interface Evaluator
      Parameters:
      formula - Input formula to be evaluated.
      Returns:
      evaluation of the given formula or null if the solver does not provide a better evaluation.

    • evaluate

      public @Nullable Object evaluate(Formula formula)
      Description copied from interface: Evaluator
      Evaluate a given formula substituting the values from the model.

      If a value is not relevant to the satisfiability result, the model can choose either an arbitrary value (e.g., the value 0 for the matching type) or just return null.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator
      Parameters:
      formula - Input formula
      Returns:
      Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean

    • evaluate

      public @Nullable BigInteger evaluate(NumeralFormula.IntegerFormula formula)
      Description copied from interface: Evaluator
      Type-safe evaluation for integer formulas.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator

    • evaluate

      public @Nullable Rational evaluate(NumeralFormula.RationalFormula formula)
      Description copied from interface: Evaluator
      Type-safe evaluation for rational formulas.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator

    • evaluate

      public @Nullable Boolean evaluate(BooleanFormula formula)
      Description copied from interface: Evaluator
      Type-safe evaluation for boolean formulas.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator

    • evaluate

      public @Nullable BigInteger evaluate(BitvectorFormula formula)
      Description copied from interface: Evaluator
      Type-safe evaluation for bitvector formulas.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator

    • evaluate

      public @Nullable String evaluate(StringFormula formula)
      Description copied from interface: Evaluator
      Type-safe evaluation for string formulas.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator

    • evaluate

      public @Nullable String evaluate(EnumerationFormula formula)
      Description copied from interface: Evaluator
      Type-safe evaluation for enumeration formulas.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator

    • evaluate

      public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
      Description copied from interface: Evaluator
      Type-safe evaluation for floating-point formulas.

      The formula does not need to be a variable, we also allow complex expression.

      Specified by:
      evaluate in interface Evaluator

    • toString

      public String toString()
      Description copied from interface: Model
      Pretty-printing of the model values.

      Please use this method only for debugging and not for retrieving relevant information about the model. The returned model representation is not intended for further usage like parsing, because we do not guarantee any specific format, e.g., for arrays and uninterpreted functions, and we allow the SMT solver to include arbitrary additional information about the current solver state, e.g., any available symbol in the solver, even from other provers, and temporary internal symbols.

      Specified by:
      toString in interface Model
      Overrides:
      toString in class Object