Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

std::ostream & operator<< (std::ostream &out, goal const &g)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

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.

1326 :object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
object(context &c)
Definition: z3++.h:270
Z3_goal Z3_API Z3_mk_goal(__in Z3_context c, __in Z3_bool models, __in Z3_bool unsat_cores, __in Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
goal ( context c,
Z3_goal  s 
)
inline

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

1327 :object(c) { init(s); }
object(context &c)
Definition: z3++.h:270
goal ( goal const &  s)
inline

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

1328 :object(s) { init(s.m_goal); }
object(context &c)
Definition: z3++.h:270
~goal ( )
inline

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

1329 { Z3_goal_dec_ref(ctx(), m_goal); }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_goal_dec_ref(__in Z3_context c, __in Z3_goal g)
Decrement the reference counter of the given goal.

Member Function Documentation

void add ( expr const &  f)
inline

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

1338 { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
void Z3_API Z3_goal_assert(__in Z3_context c, __in Z3_goal g, __in Z3_ast a)
Add a new formula a to the given goal.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr as_expr ( ) const
inline

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

1348  {
1349  unsigned n = size();
1350  if (n == 0)
1351  return ctx().bool_val(true);
1352  else if (n == 1)
1353  return operator[](0);
1354  else {
1355  array<Z3_ast> args(n);
1356  for (unsigned i = 0; i < n; i++)
1357  args[i] = operator[](i);
1358  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
1359  }
1360  }
expr operator[](int i) const
Definition: z3++.h:1340
context & ctx() const
Definition: z3++.h:272
Z3_ast Z3_API Z3_mk_and(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].The array args must have num_arg...
unsigned size() const
Definition: z3++.h:1339
expr bool_val(bool b)
Definition: z3++.h:1636
unsigned depth ( ) const
inline

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

1343 { return Z3_goal_depth(ctx(), m_goal); }
context & ctx() const
Definition: z3++.h:272
unsigned Z3_API Z3_goal_depth(__in Z3_context c, __in Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
bool inconsistent ( ) const
inline

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

1342 { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
Z3_bool Z3_API Z3_goal_inconsistent(__in Z3_context c, __in Z3_goal g)
Return true if the given goal contains the formula false.
context & ctx() const
Definition: z3++.h:272
bool is_decided_sat ( ) const
inline

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

1346 { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
context & ctx() const
Definition: z3++.h:272
Z3_bool Z3_API Z3_goal_is_decided_sat(__in Z3_context c, __in Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
bool is_decided_unsat ( ) const
inline

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

1347 { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
context & ctx() const
Definition: z3++.h:272
Z3_bool Z3_API Z3_goal_is_decided_unsat(__in Z3_context c, __in Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation...
unsigned num_exprs ( ) const
inline

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

1345 { return Z3_goal_num_exprs(ctx(), m_goal); }
context & ctx() const
Definition: z3++.h:272
unsigned Z3_API Z3_goal_num_exprs(__in Z3_context c, __in Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
operator Z3_goal ( ) const
inline

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

1330 { return m_goal; }
goal& operator= ( goal const &  s)
inline

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

1331  {
1332  Z3_goal_inc_ref(s.ctx(), s.m_goal);
1333  Z3_goal_dec_ref(ctx(), m_goal);
1334  m_ctx = s.m_ctx;
1335  m_goal = s.m_goal;
1336  return *this;
1337  }
void Z3_API Z3_goal_inc_ref(__in Z3_context c, __in Z3_goal g)
Increment the reference counter of the given goal.
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_goal_dec_ref(__in Z3_context c, __in Z3_goal g)
Decrement the reference counter of the given goal.
context * m_ctx
Definition: z3++.h:268
expr operator[] ( int  i) const
inline

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

Referenced by goal::as_expr().

1340 { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_goal_formula(__in Z3_context c, __in Z3_goal g, __in unsigned idx)
Return a formula from the given goal.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_goal_prec precision ( ) const
inline

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

1341 { return Z3_goal_precision(ctx(), m_goal); }
Z3_goal_prec Z3_API Z3_goal_precision(__in Z3_context c, __in Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
context & ctx() const
Definition: z3++.h:272
void reset ( )
inline

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

1344 { Z3_goal_reset(ctx(), m_goal); }
void Z3_API Z3_goal_reset(__in Z3_context c, __in Z3_goal g)
Erase all formulas from the given goal.
context & ctx() const
Definition: z3++.h:272
unsigned size ( ) const
inline

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

Referenced by goal::as_expr().

1339 { return Z3_goal_size(ctx(), m_goal); }
context & ctx() const
Definition: z3++.h:272
unsigned Z3_API Z3_goal_size(__in Z3_context c, __in Z3_goal g)
Return the number of formulas in the given goal.

Friends And Related Function Documentation

std::ostream& operator<< ( std::ostream &  out,
goal const &  g 
)
friend

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

1361 { out << Z3_goal_to_string(g.ctx(), g); return out; }
Z3_string Z3_API Z3_goal_to_string(__in Z3_context c, __in Z3_goal g)
Convert a goal into a string.