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

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_resultoperator= (apply_result const &s)
unsigned size () const
goal operator[] (unsigned i) const
goal operator[] (int i) const
model convert_model (model const &m, unsigned i=0) const
- Public Member Functions inherited from object
 object (context &c)
 object (object const &s)
contextctx () const
void check_error () const


std::ostream & operator<< (std::ostream &out, apply_result const &r)

Additional Inherited Members

- Protected Attributes inherited from object

Detailed Description

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

Constructor & Destructor Documentation

apply_result ( context c,
Z3_apply_result  s 

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

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

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

:object(s) { init(s.m_apply_result); }
~apply_result ( )

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

{ Z3_apply_result_dec_ref(ctx(), m_apply_result); }

Member Function Documentation

model convert_model ( model const &  m,
unsigned  i = 0 
) const

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

check_context(*this, m);
Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
return model(ctx(), new_m);
operator Z3_apply_result ( ) const

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

{ return m_apply_result; }
apply_result& operator= ( apply_result const &  s)

Definition at line 1258 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[] ( unsigned  i) const

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

{ Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
goal operator[] ( int  i) const

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

Referenced by apply_result::operator[]().

{ assert(i >= 0); return this->operator[](static_cast<unsigned>(i)); }
unsigned size ( ) const

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

{ return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }

Friends And Related Function Documentation

std::ostream& operator<< ( std::ostream &  out,
apply_result const &  r 

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

{ out << Z3_apply_result_to_string(r.ctx(), r); return out; }