Package org.sosy_lab.java_smt.basicimpl

Class AbstractEvaluator<TFormulaInfo,TType,TEnv>

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

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