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_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)

---

Detailed Description

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

---

Constructor & Destructor Documentation

apply_result	(	context &	c,
		Z3_apply_result	s
	)		[inline]

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

:object(c) { init(s); }

apply_result

(

apply_result const &

s

)

[inline]

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

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

~apply_result

(

)

[inline]

Definition at line 1373 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 [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]

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

{ return m_apply_result; }

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); }

---

Friends And Related Function Documentation

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; }