Public Member Functions | |
apply_result (context &c, Z3_apply_result s) | |
apply_result (apply_result const &s) | |
~apply_result () | |
operator Z3_apply_result () const | |
apply_result & | operator= (apply_result const &s) |
unsigned | size () const |
goal | operator[] (int i) const |
model | convert_model (model const &m, unsigned i=0) const |
Friends | |
std::ostream & | operator<< (std::ostream &out, apply_result const &r) |
apply_result | ( | context & | c, |
Z3_apply_result | s | ||
) | [inline] |
apply_result | ( | apply_result const & | s | ) | [inline] |
~apply_result | ( | ) | [inline] |
Definition at line 1373 of file z3++.h.
{ Z3_apply_result_dec_ref(ctx(), m_apply_result); }
model convert_model | ( | model const & | m, |
unsigned | i = 0 |
||
) | const [inline] |
Definition at line 1384 of file z3++.h.
{ check_context(*this, m); Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m); check_error(); return model(ctx(), new_m); }
operator Z3_apply_result | ( | ) | const [inline] |
apply_result& operator= | ( | apply_result const & | s | ) | [inline] |
Definition at line 1375 of file z3++.h.
{ Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result); Z3_apply_result_dec_ref(ctx(), m_apply_result); m_ctx = s.m_ctx; m_apply_result = s.m_apply_result; return *this; }
goal operator[] | ( | int | i | ) | const [inline] |
Definition at line 1383 of file z3++.h.
{ assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
unsigned size | ( | ) | const [inline] |
Definition at line 1382 of file z3++.h.
{ return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
std::ostream& operator<< | ( | std::ostream & | out, |
apply_result const & | r | ||
) | [friend] |
Definition at line 1390 of file z3++.h.
{ out << Z3_apply_result_to_string(r.ctx(), r); return out; }