Z3 |

Public Member Functions | Friends
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 ()
| operator Z3_goal () const
goal & | operator= (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)
context & | ctx () 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
context * | m_ctx

## Detailed Description

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

2775:object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_mk_goal
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 | ( | context & | c,
|  | Z3_goal | s
| ) |  |
| inline

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

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

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() [3/3]

goal | ( | goal const & | s | ) |
| inline

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

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

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

~goal | ( |  | ) |
| inline

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

2778{ Z3_goal_dec_ref(ctx(), m_goal); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_goal_dec_ref
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 2787 of file z3++.h.

2787{ check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426
Z3_goal_assert
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__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

## ◆ add() [2/2]

void add | ( | expr_vector const & | v | ) |
| inline

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

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

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

## ◆ as_expr()

expr as_expr | ( |  | ) | const
| inline

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

2809 {
2810 unsigned n = size();
2811 if (n == 0)
2812 return ctx().bool_val(true);
2813 else if (n == 1)
2814 return operator[](0);
2815 else {
2816 array<Z3_ast> args(n);
2817 for (unsigned i = 0; i < n; i++)
2818 args[i] = operator[](i);
2819 return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2820 }
2821 }
z3::context::bool_val
expr bool_val(bool b)
Definition: z3++.h:3388
z3::goal::size
unsigned size() const
Definition: z3++.h:2789
z3::goal::operator[]
expr operator[](int i) const
Definition: z3++.h:2790
Z3_mk_and
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 2798 of file z3++.h.

2798 {
2799 check_context(*this, m);
2800 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2801 check_error();
2802 return model(ctx(), new_m);
2803 }
Z3_goal_convert_model
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 2793 of file z3++.h.

2793{ return Z3_goal_depth(ctx(), m_goal); }
Z3_goal_depth
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 2822 of file z3++.h.

2822{ return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
Z3_goal_to_dimacs_string
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 2804 of file z3++.h.

2804 {
2805 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2806 check_error();
2807 return model(ctx(), new_m);
2808 }

## ◆ inconsistent()

bool inconsistent | ( |  | ) | const
| inline

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

2792{ return Z3_goal_inconsistent(ctx(), m_goal); }
Z3_goal_inconsistent
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 2796 of file z3++.h.

2796{ return Z3_goal_is_decided_sat(ctx(), m_goal); }
Z3_goal_is_decided_sat
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 2797 of file z3++.h.

2797{ return Z3_goal_is_decided_unsat(ctx(), m_goal); }
Z3_goal_is_decided_unsat
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 2795 of file z3++.h.

2795{ return Z3_goal_num_exprs(ctx(), m_goal); }
Z3_goal_num_exprs
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 2779 of file z3++.h.

2779{ return m_goal; }

## ◆ operator=()

goal & operator= | ( | goal const & | s | ) |
| inline

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

2780 {
2781 Z3_goal_inc_ref(s.ctx(), s.m_goal);
2782 Z3_goal_dec_ref(ctx(), m_goal);
2783 object::operator=(s);
2784 m_goal = s.m_goal;
2785 return *this;
2786 }
Z3_goal_inc_ref
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 2790 of file z3++.h.

2790{ assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
Z3_goal_formula
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 2791 of file z3++.h.

2791{ return Z3_goal_precision(ctx(), m_goal); }
Z3_goal_precision
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 2794 of file z3++.h.

2794{ Z3_goal_reset(ctx(), m_goal); }
Z3_goal_reset
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 2789 of file z3++.h.

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

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

## Friends And Related Function Documentation

## ◆ operator<<

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

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

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