java.lang.Object
- org.sosy_lab.java_smt.basicimpl.AbstractEvaluator<TFormulaInfo,TType,TEnv>

All Implemented Interfaces:: AutoCloseable, Evaluator

Direct Known Subclasses:: AbstractModel

public abstract class AbstractEvaluator<TFormulaInfo,TType,TEnv>
extends Object
implements Evaluator

Field Summary

Fields
Modifier and Type Field Description

protected FormulaCreator<TFormulaInfo,TType,TEnv,?> creator

Constructor Summary

Constructors
Modifier Constructor Description

protected AbstractEvaluator(AbstractProver<?> pProver, FormulaCreator<TFormulaInfo,TType,TEnv,?> creator)

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`void`	`close()`	Free resources associated with this evaluator (existing `Formula` instances stay valid, but `Evaluator.evaluate(Formula)` etc.
`<T extends Formula> @Nullable T`	`eval(T f)`	Evaluate a given formula substituting the values from the model and return it as formula.
`protected abstract @Nullable TFormulaInfo`	`evalImpl(TFormulaInfo formula)`	Simplify the given formula and replace all symbols with their model values.
`@Nullable BigInteger`	`evaluate(BitvectorFormula f)`	Type-safe evaluation for bitvector formulas.
`@Nullable Boolean`	`evaluate(BooleanFormula f)`	Type-safe evaluation for boolean formulas.
`@Nullable String`	`evaluate(EnumerationFormula f)`	Type-safe evaluation for enumeration formulas.
`@Nullable FloatingPointNumber`	`evaluate(FloatingPointFormula f)`	Type-safe evaluation for floating-point formulas.
`@Nullable Object`	`evaluate(Formula f)`	Evaluate a given formula substituting the values from the model.
`@Nullable BigInteger`	`evaluate(NumeralFormula.IntegerFormula f)`	Type-safe evaluation for integer formulas.
`@Nullable Rational`	`evaluate(NumeralFormula.RationalFormula f)`	Type-safe evaluation for rational formulas.
`@Nullable String`	`evaluate(StringFormula f)`	Type-safe evaluation for string formulas.
`protected @Nullable Object`	`evaluateImpl(TFormulaInfo f)`	Simplify the given formula and replace all symbols with their model values.
`protected boolean`	`isClosed()`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - creator
```
protected final FormulaCreator<TFormulaInfo,TType,TEnv,?> creator
```
- Constructor Detail
  - AbstractEvaluator
```
protected AbstractEvaluator(AbstractProver<?> pProver,
                            FormulaCreator<TFormulaInfo,TType,TEnv,?> creator)
```
- Method Detail
  - eval
```
public final <T extends Formula> @Nullable T eval(T f)
```
    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:
    
    f - Input formula to be evaluated.
    
    Returns:
    
    evaluation of the given formula or null if the solver does not provide a better evaluation.
  - evaluate
```
public final @Nullable BigInteger evaluate(NumeralFormula.IntegerFormula f)
```
    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 f)
```
    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 final @Nullable Boolean evaluate(BooleanFormula f)
```
    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 final @Nullable String evaluate(StringFormula f)
```
    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 final @Nullable String evaluate(EnumerationFormula f)
```
    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 final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f)
```
    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
  - evaluate
```
public final @Nullable BigInteger evaluate(BitvectorFormula f)
```
    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 final @Nullable Object evaluate(Formula f)
```
    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:
    
    f - Input formula
    
    Returns:
    
    Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
  - evalImpl
```
protected abstract @Nullable TFormulaInfo evalImpl(TFormulaInfo formula)
```
    Simplify the given formula and replace all symbols with their model values. If a symbol is not set in the model and evaluation aborts, return null.
  - evaluateImpl
```
protected final @Nullable Object evaluateImpl(TFormulaInfo f)
```
    Simplify the given formula and replace all symbols with their model values. If a symbol is not set in the model and evaluation aborts, return null. Afterward convert the formula into a Java object as far as possible, i.e., try to match a primitive or simple type.
  - isClosed
```
protected boolean isClosed()
```
  - close
```
public void close()
```
    Description copied from interface: Evaluator
    
    Free resources associated with this evaluator (existing Formula instances stay valid, but Evaluator.evaluate(Formula) etc. must not be called again).
    
    Specified by:
    
    close in interface AutoCloseable
    
    Specified by:
    
    close in interface Evaluator

Class AbstractEvaluator<TFormulaInfo,​TType,​TEnv>

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

creator

Constructor Detail

AbstractEvaluator

Method Detail

eval

evaluate

evaluate

evaluate

evaluate

evaluate

evaluate

evaluate

evaluate

evalImpl

evaluateImpl

isClosed

close

Class AbstractEvaluator<TFormulaInfo,TType,TEnv>