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.
|
void | Add (params BoolExpr[] constraints) |
| Alias for Assert.
|
void | Reset () |
| Erases all formulas from the given goal.
|
Goal | Translate (Context ctx) |
| Translates (copies) the Goal to the target Context ctx .
|
Goal | Simplify (Params p=null) |
| Simplifies the goal.
|
override string | ToString () |
| Goal to string conversion.
|
Properties |
Z3_goal_prec | Precision [get] |
| The precision of the goal.
|
bool | IsPrecise [get] |
| Indicates whether the goal is precise.
|
bool | IsUnderApproximation [get] |
| Indicates whether the goal is an under-approximation.
|
bool | IsOverApproximation [get] |
| Indicates whether the goal is an over-approximation.
|
bool | IsGarbage [get] |
| Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
|
bool | Inconsistent [get] |
| Indicates whether the goal contains `false'.
|
uint | Depth [get] |
| The depth of the goal.
|
uint | Size [get] |
| The number of formulas in the goal.
|
BoolExpr[] | Formulas [get] |
| The formulas in the goal.
|
uint | NumExprs [get] |
| The number of formulas, subformulas and terms in the goal.
|
bool | IsDecidedSat [get] |
| Indicates whether the goal is empty, and it is precise or the product of an under approximation.
|
bool | IsDecidedUnsat [get] |
| Indicates whether the goal contains `false', and it is precise or the product of an over approximation.
|
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
Definition at line 31 of file Goal.cs.