#include <z3++.h>
Definition at line 3000 of file z3++.h.
◆ 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)); }
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(), operator<<, and operator=().
◆ goal() [2/3]
Definition at line 3008 of file z3++.h.
3008:object(c) { init(s); }
◆ goal() [3/3]
Definition at line 3009 of file z3++.h.
3009:object(s) { init(s.m_goal); }
◆ ~goal()
Definition at line 3010 of file z3++.h.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
◆ add() [1/2]
void add |
( |
expr const & | f | ) |
|
|
inline |
Definition at line 3019 of file z3++.h.
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...
void check_context(object const &a, object const &b)
◆ add() [2/2]
Definition at line 3020 of file z3++.h.
3020{
check_context(*
this, v);
for (
unsigned i = 0; i < v.size(); ++i) add(v[i]); }
Referenced by add().
◆ as_expr()
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 }
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()
Definition at line 3030 of file z3++.h.
3030 {
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()
Definition at line 3025 of file z3++.h.
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.
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 {
3038 check_error();
3039 return model(ctx(), new_m);
3040 }
◆ inconsistent()
bool inconsistent |
( |
| ) |
const |
|
inline |
Definition at line 3024 of file z3++.h.
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.
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.
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.
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 |
◆ operator=()
Definition at line 3012 of file z3++.h.
3012 {
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 as_expr().
◆ precision()
Definition at line 3023 of file z3++.h.
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()
Definition at line 3026 of file z3++.h.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
◆ size()
Definition at line 3021 of file z3++.h.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
Referenced by as_expr().
◆ operator<<
std::ostream & operator<< |
( |
std::ostream & | out, |
|
|
goal const & | g ) |
|
friend |
Definition at line 3057 of file z3++.h.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.