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 | |
goal & | operator= (goal const &s) |
void | add (expr const &f) |
unsigned | size () const |
expr | operator[] (int 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 |
expr | as_expr () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, goal const &g) |
Definition at line 1326 of file z3++.h.
:object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
~goal | ( | ) | [inline] |
Definition at line 1329 of file z3++.h.
{ Z3_goal_dec_ref(ctx(), m_goal); }
Definition at line 1338 of file z3++.h.
{ check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
unsigned depth | ( | ) | const [inline] |
Definition at line 1343 of file z3++.h.
{ return Z3_goal_depth(ctx(), m_goal); }
bool inconsistent | ( | ) | const [inline] |
Definition at line 1342 of file z3++.h.
{ return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
bool is_decided_sat | ( | ) | const [inline] |
Definition at line 1346 of file z3++.h.
{ return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
bool is_decided_unsat | ( | ) | const [inline] |
Definition at line 1347 of file z3++.h.
{ return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
unsigned num_exprs | ( | ) | const [inline] |
Definition at line 1345 of file z3++.h.
{ return Z3_goal_num_exprs(ctx(), m_goal); }
Definition at line 1331 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[] | ( | int | i | ) | const [inline] |
Definition at line 1340 of file z3++.h.
Referenced by goal::as_expr().
{ assert(0 <= i); 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 1341 of file z3++.h.
{ return Z3_goal_precision(ctx(), m_goal); }
void reset | ( | ) | [inline] |
Definition at line 1344 of file z3++.h.
{ Z3_goal_reset(ctx(), m_goal); }
unsigned size | ( | ) | const [inline] |
Definition at line 1339 of file z3++.h.
Referenced by goal::as_expr().
{ return Z3_goal_size(ctx(), m_goal); }
std::ostream& operator<< | ( | std::ostream & | out, |
goal const & | g | ||
) | [friend] |
Definition at line 1361 of file z3++.h.
{ out << Z3_goal_to_string(g.ctx(), g); return out; }