mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

adding C++ API for optimization

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

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

@ -1479,6 +1479,66 @@ namespace z3 {
}
};
class optimize : public object {
Z3_optimize m_opt;
public:
class handle {
unsigned m_h;
public:
handle(unsigned h): m_h(h) {}
unsigned h() const { return m_h; }
};
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); }
operator Z3_optimize() const { return m_opt; }
void add(expr const& e) {
assert(e.is_bool());
Z3_optimize_assert(ctx(), m_opt, e);
}
handle add(expr const& e, unsigned weight) {
assert(e.is_bool());
std::stringstream strm;
strm << weight;
return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
}
handle add(expr const& e, char const* weight) {
assert(e.is_bool());
return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
}
handle maximzie(expr const& e) {
return handle(Z3_optimize_maximize(ctx(), m_opt, e));
}
handle minimize(expr const& 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); }
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(); }
expr lower(handle const& h) {
Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
check_error();
return expr(ctx(), r);
}
expr upper(handle const& h) {
Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
check_error();
return expr(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; }
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) {
Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
p.check_error();