Z3
 
Loading...
Searching...
No Matches
goal Class Reference

#include <z3++.h>

+ 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 () override
 
 operator Z3_goal () const
 
goaloperator= (goal const &s)
 
void add (expr const &f)
 
void add (expr_vector const &v)
 
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
 
model convert_model (model const &m) const
 
model get_model () const
 
expr as_expr () const
 
std::string dimacs (bool include_names=true) const
 
- Public Member Functions inherited from object
 object (context &c)
 
virtual ~object ()=default
 
contextctx () const
 
Z3_error_code 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 3000 of file z3++.h.

Constructor & Destructor Documentation

◆ goal() [1/3]

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

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

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

Referenced by Goal::__del__(), Goal::assert_exprs(), Goal::convert_model(), Goal::depth(), Goal::dimacs(), Goal::get(), Goal::inconsistent(), Goal::prec(), Goal::sexpr(), Goal::size(), and Goal::translate().

◆ goal() [2/3]

◆ goal() [3/3]

◆ ~goal()

~goal ( )
inlineoverride

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

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

Member Function Documentation

◆ add() [1/2]

void add ( expr const & f)
inline

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

3019{ check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
Z3_error_code check_error() const
Definition z3++.h:475
friend void check_context(object const &a, object const &b)
Definition z3++.h:478
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal. The formula is split according to the following procedure that...

Referenced by Solver::__iadd__().

◆ add() [2/2]

void add ( expr_vector const & v)
inline

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

3020{ check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
void add(expr const &f)
Definition z3++.h:3019

Referenced by Solver::__iadd__(), and goal::add().

◆ as_expr()

expr as_expr ( ) const
inline

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

3041 {
3042 unsigned n = size();
3043 if (n == 0)
3044 return ctx().bool_val(true);
3045 else if (n == 1)
3046 return operator[](0u);
3047 else {
3048 array<Z3_ast> args(n);
3049 for (unsigned i = 0; i < n; i++)
3050 args[i] = operator[](i);
3051 return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
3052 }
3053 }
expr bool_val(bool b)
Definition z3++.h:3791
unsigned size() const
Definition z3++.h:3021
expr operator[](int i) const
Definition z3++.h:3022
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].

◆ convert_model()

model convert_model ( model const & m) const
inline

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

3030 {
3031 check_context(*this, m);
3032 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
3033 check_error();
3034 return model(ctx(), new_m);
3035 }
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)
Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...

◆ depth()

unsigned depth ( ) const
inline

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

3025{ return Z3_goal_depth(ctx(), m_goal); }
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it.

◆ dimacs()

std::string dimacs ( bool include_names = true) const
inline

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

3054{ return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names)
Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...

◆ get_model()

model get_model ( ) const
inline

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

3036 {
3037 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
3038 check_error();
3039 return model(ctx(), new_m);
3040 }

◆ inconsistent()

bool inconsistent ( ) const
inline

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

3024{ return Z3_goal_inconsistent(ctx(), m_goal); }
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.

◆ is_decided_sat()

bool is_decided_sat ( ) const
inline

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

3028{ return Z3_goal_is_decided_sat(ctx(), m_goal); }
bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.

◆ is_decided_unsat()

bool is_decided_unsat ( ) const
inline

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

3029{ return Z3_goal_is_decided_unsat(ctx(), m_goal); }
bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation.

◆ num_exprs()

unsigned num_exprs ( ) const
inline

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

3027{ return Z3_goal_num_exprs(ctx(), m_goal); }
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.

◆ operator Z3_goal()

operator Z3_goal ( ) const
inline

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

3011{ return m_goal; }

◆ operator=()

goal & operator= ( goal const & s)
inline

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

3012 {
3013 Z3_goal_inc_ref(s.ctx(), s.m_goal);
3014 Z3_goal_dec_ref(ctx(), m_goal);
3015 object::operator=(s);
3016 m_goal = s.m_goal;
3017 return *this;
3018 }
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.

◆ operator[]()

expr operator[] ( int i) const
inline

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

3022{ 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(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.

Referenced by goal::as_expr().

◆ precision()

Z3_goal_prec precision ( ) const
inline

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

3023{ return Z3_goal_precision(ctx(), m_goal); }
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...

◆ reset()

void reset ( )
inline

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

3026{ Z3_goal_reset(ctx(), m_goal); }
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.

◆ size()

unsigned size ( ) const
inline

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

3021{ return Z3_goal_size(ctx(), m_goal); }
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.

Referenced by Goal::__len__(), ParamDescrsRef::__len__(), goal::as_expr(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().

Friends And Related Symbol Documentation

◆ operator<<

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

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

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