From 3f8083dfa692b24a4525f548b3673fa274394dca Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 Sep 2014 09:32:38 -0700
Subject: [PATCH] fix push/pop bugs in optimize context, add example to c++,
 fix bug in arithemtic bounds axiom addition

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/example.cpp    | 25 ++++++++++++++++++++++++-
 src/opt/opt_context.cpp     |  9 +++++++++
 src/smt/theory_arith_core.h |  1 +
 3 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 7ffa04709..454f3ebae 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -972,7 +972,29 @@ void substitute_example() {
     std::cout << new_f << std::endl;
 }
 
-
+void opt_example() {
+    context c;
+    optimize opt(c);
+    params p(c);
+    p.set("priority",c.str_symbol("pareto"));
+    opt.set(p);
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    opt.add(10 >= x && x >= 0);
+    opt.add(10 >= y && y >= 0);
+    opt.add(x + y <= 11);
+    optimize::handle h1 = opt.maximize(x);
+    optimize::handle h2 = opt.maximize(y);
+    check_result r = sat;
+    while (true) {
+        if (sat == opt.check()) {
+            std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n";
+        }
+        else {
+            break;
+        }
+    }
+}
 
 int main() {
     try {
@@ -1012,6 +1034,7 @@ int main() {
         expr_vector_example(); std::cout << "\n";
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";
+        opt_example(); std::cout << "\n";
         std::cout << "done\n";
     }
     catch (exception & ex) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index d931afbff..9098a1323 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -139,6 +139,7 @@ namespace opt {
         for (; it != end; ++it) {
             dealloc(it->m_value);
         }
+        m_maxsmts.reset();
     }
 
     void context::push() {
@@ -149,21 +150,29 @@ namespace opt {
         for (unsigned i = 0; i < n; ++i) {
             m_scoped_state.pop();
         }
+        m_model.reset();
+        reset_maxsmts();
+        m_optsmt.reset();        
+        m_hard_constraints.reset();
     }
 
     void context::set_hard_constraints(ptr_vector<expr>& fmls) {
         m_scoped_state.set(fmls);
+        m_model.reset();
     }
 
     void context::add_hard_constraint(expr* f) { 
         m_scoped_state.add(f);
+        m_model.reset();
     }
 
     unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { 
+        m_model.reset();
         return m_scoped_state.add(f, w, id);
     }
 
     unsigned context::add_objective(app* t, bool is_max) {
+        m_model.reset();
         return m_scoped_state.add(t, is_max);
     }
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index b80a1f415..366054d79 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3090,6 +3090,7 @@ namespace smt {
         SASSERT(m_to_patch.empty());
         m_to_check.reset();
         m_in_to_check.reset();
+        m_new_atoms.reset();
         CASSERT("arith", wf_rows());
         CASSERT("arith", wf_columns());
         CASSERT("arith", valid_row_assignment());