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

Nested Class Summary

Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.Model

Model.ValueAssignment

Constructor Summary

Constructors

Constructor	Description
CachingModel(Model pDelegate)

Method Summary

Modifier and Type	Method	Description
ImmutableList<Model.ValueAssignment>	asList()	Returns a list of model assignments that remains valid after the model is closed (via Model.close()).
void	close()	Free resources associated with this model (existing Model.ValueAssignment instances stay valid, but Evaluator.evaluate(Formula) etc.
<T extends Formula> @Nullable T	eval(T formula)	Evaluate a given formula substituting the values from the model and return it as formula.
@Nullable BigInteger	evaluate(BitvectorFormula formula)	Type-safe evaluation for bitvector formulas.
@Nullable Boolean	evaluate(BooleanFormula formula)	Type-safe evaluation for boolean formulas.
@Nullable String	evaluate(EnumerationFormula formula)	Type-safe evaluation for enumeration formulas.
@Nullable FloatingPointNumber	evaluate(FloatingPointFormula formula)	Type-safe evaluation for floating-point formulas.
@Nullable Object	evaluate(Formula formula)	Evaluate a given formula substituting the values from the model.
@Nullable BigInteger	evaluate(NumeralFormula.IntegerFormula formula)	Type-safe evaluation for integer formulas.
@Nullable Rational	evaluate(NumeralFormula.RationalFormula formula)	Type-safe evaluation for rational formulas.
@Nullable String	evaluate(StringFormula formula)	Type-safe evaluation for string formulas.
String	toString()	Pretty-printing of the model values.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Methods inherited from interface org.sosy_lab.java_smt.api.Model

iterator

Constructor Detail

CachingModel

public CachingModel(Model pDelegate)

Method Detail

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