mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

fix #1625

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-18 14:03:32 -07:00
parent bc3719f436
commit e5b14ab682
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2292,6 +2292,7 @@ namespace z3 {
class optimize : public object { class optimize : public object {
Z3_optimize m_opt; Z3_optimize m_opt;
public: public:
class handle { class handle {
unsigned m_h; unsigned m_h;
@ -2300,6 +2301,17 @@ namespace z3 {
unsigned h() const { return m_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(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
optimize(optimize& o):object(c) {
Z3_optimize_inc_ref(o.ctx(), o.m_opt);
m_opt = o.m_opt;
}
optimize& operator=(optimize const& o) {
Z3_optimize_inc_rec(o.ctx(), o.m_opt);
Z3_optimize_dec_ref(ctx(), m_opt);
m_opt = o.m_opt;
m_ctx = o.m_ctx;
return *this;
}
~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) {