Model class
A model containing the solution to a satisfiability query.
- Available extensions
Properties
- hashCode → int
-
The hash code for this object.
no setterinherited
- runtimeType → Type
-
A representation of the runtime type of the object.
no setterinherited
Methods
-
addConstInterp(
ConstVar v, Expr value) → void - Assigns a value to the given constant.
-
addFuncInterp(
FuncDecl decl, Expr defaultValue) → FuncInterp - Adds an interpretation for the given function declaration.
-
eval<
A extends Expr?> (Expr query, {bool completion = true}) → A -
Evaluates the expression
queryin this model. -
evalConst<
A extends Expr> (ConstVar query) → A? -
Evaluates the constant
queryin this model. -
getConsts(
) → List< ConstVar> - Gets all of the constants in this model.
-
getFuncInterp(
FuncDecl decl) → FuncInterp? - Finds the interpretation of the given function declaration, returns null if it was never assigned by the solver.
-
getFuncs(
) → List< FuncDecl> - Gets all of the functions in this model.
-
getSorts(
) → List< Sort> - Gets all of the sorts in this model.
-
getSortUniverse(
Sort s) → List< Expr> - Gets all of the expressions that satisfy the given sort.
-
noSuchMethod(
Invocation invocation) → dynamic -
Invoked when a nonexistent method or property is accessed.
inherited
-
toContext(
Context c) → Model - Transfers this model to another Z3 context.
-
toString(
) → String -
A string representation of this object.
override
Operators
-
operator ==(
Object other) → bool -
The equality operator.
inherited
-
operator [](
Expr expr) → Expr -
Available on Model, provided by the ModelExtension extension
Evaluate an expression in this model.