A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. More...
Data Structures | |
class | DecRefQueue |
Public Member Functions | |
void | Assert (params BoolExpr[] constraints) |
Adds the constraints to the given goal. More... | |
void | Add (params BoolExpr[] constraints) |
Alias for Assert. More... | |
void | Reset () |
Erases all formulas from the given goal. More... | |
Goal | Translate (Context ctx) |
Translates (copies) the Goal to the target Context ctx . More... | |
Goal | Simplify (Params p=null) |
Simplifies the goal. More... | |
override string | ToString () |
Goal to string conversion. More... | |
BoolExpr | AsBoolExpr () |
Goal to BoolExpr conversion. More... | |
![]() | |
void | Dispose () |
Disposes of the underlying native Z3 object. More... | |
Properties | |
Z3_goal_prec | Precision [get] |
The precision of the goal. More... | |
bool | IsPrecise [get] |
Indicates whether the goal is precise. More... | |
bool | IsUnderApproximation [get] |
Indicates whether the goal is an under-approximation. More... | |
bool | IsOverApproximation [get] |
Indicates whether the goal is an over-approximation. More... | |
bool | IsGarbage [get] |
Indicates whether the goal is garbage (i.e., the product of over- and under-approximations). More... | |
bool | Inconsistent [get] |
Indicates whether the goal contains `false'. More... | |
uint | Depth [get] |
The depth of the goal. More... | |
uint | Size [get] |
The number of formulas in the goal. More... | |
BoolExpr [] | Formulas [get] |
The formulas in the goal. More... | |
uint | NumExprs [get] |
The number of formulas, subformulas and terms in the goal. More... | |
bool | IsDecidedSat [get] |
Indicates whether the goal is empty, and it is precise or the product of an under approximation. More... | |
bool | IsDecidedUnsat [get] |
Indicates whether the goal contains `false', and it is precise or the product of an over approximation. More... | |
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
|
inline |
Alias for Assert.
Definition at line 96 of file Goal.cs.
|
inline |
Definition at line 215 of file Goal.cs.
|
inline |
|
inline |
Simplifies the goal.
Essentially invokes the `simplify' tactic on the goal.
Definition at line 191 of file Goal.cs.
|
inline |
|
get |
|
get |
|
get |
|
get |
|
get |
|
get |
|
get |
|
get |
|
get |
The precision of the goal.
Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.