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...  
Public Member Functions inherited from Z3Object  
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 underapproximation. More...  
bool  IsOverApproximation [get] 
Indicates whether the goal is an overapproximation. More...  
bool  IsGarbage [get] 
Indicates whether the goal is garbage (i.e., the product of over and underapproximations). 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 

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.