Goal class
A set of formulas, Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.
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
-
assertExpr(
AST a) → void -
Add a new formula
ato the given goal. -
convert(
Model? m) → Model - Converts a model of the formulas of a goal to a model of an original goal.
-
getDepth(
) → int - Returns the depth of the goal, i.e. how many transformations were applied to it.
-
getNumExprs(
) → int - Returns the number of formulas, subformulas and terms in the goal.
-
getPrecision(
) → GoalPrecision - Return the "precision" of the given goal.
-
getSize(
) → int - Returns the number of formulas in the goal.
-
isDecidedSat(
) → bool - Returns whether the goal is empty and precise.
-
isDecidedUnsat(
) → bool - Returns whether the goal is inconsistent and precise.
-
isInconsistent(
) → bool - Returns whether or not the goal contains false.
-
noSuchMethod(
Invocation invocation) → dynamic -
Invoked when a nonexistent method or property is accessed.
inherited
-
reset(
) → void - Removes all formulas from the goal.
-
toContext(
Context c) → Goal - Transfers this goal to another Z3 context.
-
toDimacs(
{bool includeNames = true}) → String - Convert a goal into a DIMACS formatted string.
-
toString(
) → String -
A string representation of this object.
override
Operators
-
operator ==(
Object other) → bool -
The equality operator.
inherited