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

---

Detailed Description

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

---

Constructor & Destructor Documentation

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

Definition at line 1326 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 1327 of file z3++.h.

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

goal

(

goal const &

s

)

[inline]

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

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

~goal

(

)

[inline]

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

{ Z3_goal_dec_ref(ctx(), m_goal); }

---

Member Function Documentation

void add

(

expr const &

f

)

[inline]

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

{ check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }

expr as_expr

(

)

const [inline]

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

                             {
            unsigned n = size();
            if (n == 0) 
                return ctx().bool_val(true);
            else if (n == 1)
                return operator[](0);
            else {
                array<Z3_ast> args(n);
                for (unsigned i = 0; i < n; i++)
                    args[i] = operator[](i);
                return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
            }
        }

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

operator Z3_goal

(

)

const [inline]

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

{ return m_goal; }

goal& operator=

(

goal const &

s

)

[inline]

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

---

Friends And Related Function Documentation

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