Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Friends
goal Class Reference
+ Inheritance diagram for goal:

Public Member Functions

 goal (context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
 
 goal (context &c, Z3_goal s)
 
 goal (goal const &s)
 
 ~goal ()
 
 operator Z3_goal () const
 
goaloperator= (goal const &s)
 
void add (expr const &f)
 
unsigned size () const
 
expr operator[] (unsigned i) const
 
Z3_goal_prec precision () const
 
bool inconsistent () const
 
unsigned depth () const
 
void reset ()
 
unsigned num_exprs () const
 
bool is_decided_sat () const
 
bool is_decided_unsat () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

std::ostream & operator<< (std::ostream &out, goal const &g)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

Definition at line 1215 of file z3++.h.

Constructor & Destructor Documentation

goal ( context c,
bool  models = true,
bool  unsat_cores = false,
bool  proofs = false 
)
inline

Definition at line 1222 of file z3++.h.

:object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
goal ( context c,
Z3_goal  s 
)
inline

Definition at line 1223 of file z3++.h.

:object(c) { init(s); }
goal ( goal const &  s)
inline

Definition at line 1224 of file z3++.h.

:object(s) { init(s.m_goal); }
~goal ( )
inline

Definition at line 1225 of file z3++.h.

{ Z3_goal_dec_ref(ctx(), m_goal); }

Member Function Documentation

void add ( expr const &  f)
inline

Definition at line 1234 of file z3++.h.

{ check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
unsigned depth ( ) const
inline

Definition at line 1239 of file z3++.h.

{ return Z3_goal_depth(ctx(), m_goal); }
bool inconsistent ( ) const
inline

Definition at line 1238 of file z3++.h.

{ return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
bool is_decided_sat ( ) const
inline

Definition at line 1242 of file z3++.h.

{ return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
bool is_decided_unsat ( ) const
inline

Definition at line 1243 of file z3++.h.

{ return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
unsigned num_exprs ( ) const
inline

Definition at line 1241 of file z3++.h.

{ return Z3_goal_num_exprs(ctx(), m_goal); }
operator Z3_goal ( ) const
inline

Definition at line 1226 of file z3++.h.

{ return m_goal; }
goal& operator= ( goal const &  s)
inline

Definition at line 1227 of file z3++.h.

{
Z3_goal_inc_ref(s.ctx(), s.m_goal);
Z3_goal_dec_ref(ctx(), m_goal);
m_ctx = s.m_ctx;
m_goal = s.m_goal;
return *this;
}
expr operator[] ( unsigned  i) const
inline

Definition at line 1236 of file z3++.h.

{ Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
Z3_goal_prec precision ( ) const
inline

Definition at line 1237 of file z3++.h.

{ return Z3_goal_precision(ctx(), m_goal); }
void reset ( )
inline

Definition at line 1240 of file z3++.h.

{ Z3_goal_reset(ctx(), m_goal); }
unsigned size ( ) const
inline

Definition at line 1235 of file z3++.h.

{ return Z3_goal_size(ctx(), m_goal); }

Friends And Related Function Documentation

std::ostream& operator<< ( std::ostream &  out,
goal const &  g 
)
friend

Definition at line 1244 of file z3++.h.

{ out << Z3_goal_to_string(g.ctx(), g); return out; }