Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Friends
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
goaloperator= (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; }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines