Package org.sosy_lab.java_smt.api

Interface Evaluator

  • All Superinterfaces:
    AutoCloseable
    All Known Subinterfaces:
    Model
    All Known Implementing Classes:
    AbstractEvaluator, AbstractModel, CachingModel, DebuggingModel
    public interface Evaluator
extends AutoCloseable
    This class provides methods to get concrete evaluations for formulas from the satisfiable solver environment.

    This class can be (but does not need to be!) a cheaper and more light-weight version of a Model and it misses several features compared to a full Model:

    • no listing of model assignments, i.e., the user needs to query each formula on its own,
    • no guaranteed availability after applying any operation on the original prover stack, i.e., the evaluation is only available directly after querying the solver with a satisfiable environment.

    If any of these features is required, please use the complete Model.

    • Method Detail

      • eval

        <T extends Formula> @Nullable T eval​(T formula)
        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.

        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

        @Nullable Object evaluate​(Formula formula)
        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.

        Parameters:
        formula - Input formula
        Returns:
        Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
        Throws:
        IllegalArgumentException - if a formula has unexpected type, e.g. Array.

      • evaluate

        @Nullable BigInteger evaluate​(NumeralFormula.IntegerFormula formula)
        Type-safe evaluation for integer formulas.

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

      • evaluate

        @Nullable Rational evaluate​(NumeralFormula.RationalFormula formula)
        Type-safe evaluation for rational formulas.

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

      • evaluate

        @Nullable Boolean evaluate​(BooleanFormula formula)
        Type-safe evaluation for boolean formulas.

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

      • evaluate

        @Nullable BigInteger evaluate​(BitvectorFormula formula)
        Type-safe evaluation for bitvector formulas.

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

      • evaluate

        @Nullable String evaluate​(StringFormula formula)
        Type-safe evaluation for string formulas.

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

      • evaluate

        @Nullable String evaluate​(EnumerationFormula formula)
        Type-safe evaluation for enumeration formulas.

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

      • evaluate

        @Nullable FloatingPointNumber evaluate​(FloatingPointFormula formula)
        Type-safe evaluation for floating-point formulas.

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

      • close

        void close()
        Free resources associated with this evaluator (existing Formula instances stay valid, but evaluate(Formula) etc. must not be called again).
        Specified by:
        close in interface AutoCloseable