Package org.sosy_lab.java_smt.api

Interface Model

All Superinterfaces:

AutoCloseable, Evaluator, Iterable<Model.ValueAssignment>

All Known Implementing Classes:

AbstractModel, CachingModel, DebuggingModel

public interface Model
extends Evaluator, Iterable<Model.ValueAssignment>, AutoCloseable

This class provides a model with concrete evaluations for symbols and formulas from the satisfiable solver environment.

This class is an extensions of Evaluator and provides more features:

• a listing of model assignments, i.e., the user can iterate over all available symbols and their assignments,
• a guaranteed availability even after applying any operation on the original prover stack, i .e., the model instance stays constant and remains valid for one given satisfiable prover environment.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static class	Model.ValueAssignment

Method Summary

Modifier and Type	Method	Description
ImmutableList<Model.ValueAssignment>	asList()	Build a list of assignments that stays valid after closing the model.
void	close()	Free resources associated with this model (existing Model.ValueAssignment instances stay valid, but Evaluator.evaluate(Formula) etc.
default Iterator<Model.ValueAssignment>	iterator()	Iterate over all values present in the model.
String	toString()	Pretty-printing of the model values.

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

eval, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Method Detail

iterator

default Iterator<Model.ValueAssignment> iterator()

Iterate over all values present in the model. Note that iterating multiple times may be inefficient for some solvers, it is recommended to use BasicProverEnvironment.getModelAssignments() instead in this case.

The iteration includes value assignments for...

• all relevant free variables of simple type. If a variable is irrelevant for satisfiability, it can be null or missing in the iteration.
• (nested) arrays with all accesses. If an array access is applied within a quantified context, some value assignments can be missing in the iteration. Please use a direct evaluation query to get the evaluation in such a case.
• uninterpreted functions with all applications. If an uninterpreted function is applied within a quantified context, some value assignments can be missing in the iteration. Please use a direct evaluation query to get the evaluation in such a case.

Specified by:

iterator in interface Iterable<Model.ValueAssignment>

asList

ImmutableList<Model.ValueAssignment> asList()

Build a list of assignments that stays valid after closing the model.

toString

String toString()

Pretty-printing of the model values.

Please only use this method 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.

Overrides:

toString in class Object

close

void close()

Free resources associated with this model (existing Model.ValueAssignment instances stay valid, but Evaluator.evaluate(Formula) etc. and iterator() must not be called again).

Specified by:

close in interface AutoCloseable

Specified by:

close in interface Evaluator