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.
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]Definition at line 3008 of file z3++.h.
3008:
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]Definition at line 3009 of file z3++.h.
3009:
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()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 ) inlineDefinition at line 3019 of file z3++.h.
Z3_error_code check_error() const
friend void check_context(object const &a, object const &b)
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] ◆ as_expr()Definition at line 3041 of file z3++.h.
3042 unsignedn =
size();
3048array<Z3_ast> args(n);
3049 for(
unsignedi = 0; i < n; i++)
3050args[i] =
operator[](i);
expr operator[](int i) const
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.
3034 returnmodel(
ctx(), new_m);
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 inlineDefinition at line 3036 of file z3++.h.
3039 returnmodel(
ctx(), new_m);
◆ inconsistent() bool inconsistent ( ) const inlineDefinition 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 inlineDefinition 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 inlineDefinition 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 inlineDefinition 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.
3015object::operator=(s);
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 inlineDefinition at line 3022 of file z3++.h.
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()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() ◆ operator<< std::ostream& operator<< ( std::ostream & out, goal const & g ) friendDefinition 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.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4