mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

C++ API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-28 09:39:14 -07:00
parent 13e454ad63
commit cc577a431a
1 changed files with 2 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/c++/z3++.h
View file

@ -1491,7 +1491,6 @@ namespace z3 {
optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); } optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); } ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
operator Z3_optimize() const { return m_opt; } operator Z3_optimize() const { return m_opt; }
void add(expr const& e) { void add(expr const& e) {
assert(e.is_bool()); assert(e.is_bool());
Z3_optimize_assert(ctx(), m_opt, e); Z3_optimize_assert(ctx(), m_opt, e);
@ -1512,31 +1511,22 @@ namespace z3 {
handle minimize(expr const& e) { handle minimize(expr const& e) {
return handle(Z3_optimize_minimize(ctx(), m_opt, e)); return handle(Z3_optimize_minimize(ctx(), m_opt, e));
} }
check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); } check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); } model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); } void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
expr lower(handle const& h) { expr lower(handle const& h) {
Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h()); Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
check_error(); check_error();
return expr(ctx(), r); return expr(ctx(), r);
} }
expr upper(handle const& h) { expr upper(handle const& h) {
Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h()); Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
check_error(); check_error();
return expr(ctx(), r); return expr(ctx(), r);
} }
stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
friend std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; } friend std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
}; };
inline tactic fail_if(probe const & p) { inline tactic fail_if(probe const & p) {