dealing with cancel

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/opt_cmds.cpp

@@ -170,11 +170,16 @@ public:
         reset(ctx);
     }
 
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
+        return parametric_cmd::next_arg_kind(ctx);
+    }
+
+
     virtual void execute(cmd_context & ctx) {
         params_ref p = ctx.params().merge_default_params(ps());
         opt::context& opt = m_opt_ctx();
         opt.updt_params(p);
-        unsigned timeout   = p.get_uint("timeout", UINT_MAX);
+        unsigned timeout = p.get_uint("timeout", UINT_MAX);
 
         ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx.end_assertions();

src/opt/opt_context.cpp

@@ -26,7 +26,6 @@ Notes:
 #include "opt_context.h"
 #include "fu_malik.h"
 #include "weighted_maxsat.h"
-#include "optimize_objectives.h"
 #include "ast_pp.h"
 #include "opt_solver.h"
 #include "arith_decl_plugin.h"
@@ -39,7 +38,8 @@ namespace opt {
         m(m),
         m_hard_constraints(m),
         m_soft_constraints(m),
-        m_objectives(m)
+        m_objectives(m),
+        m_opt_objectives(m)
     {
         m_params.set_bool("model", true);
         m_params.set_bool("unsat_core", true);
@@ -83,8 +83,7 @@ namespace opt {
             for (unsigned i = 0; i < fmls_copy.size(); ++i) {
                 s->assert_expr(fmls_copy[i].get());
             }
-            optimize_objectives obj(m, get_opt_solver(*s)); // TBD: make an attribute
+            is_sat = m_opt_objectives(get_opt_solver(*s), m_objectives, values);
-            is_sat = obj(m_objectives, values);
             std::cout << "is-sat: " << is_sat << std::endl;
 
             if (is_sat != l_true) {
@@ -126,12 +125,14 @@ namespace opt {
         if (m_solver) {
             m_solver->cancel();
         }
+        m_opt_objectives.set_cancel(true);
     }
 
     void context::reset_cancel() {
         if (m_solver) {
             m_solver->reset_cancel();
         }
+        m_opt_objectives.set_cancel(false);
     }
 
     void context::add_objective(app* t, bool is_max) {

src/opt/opt_context.h

@@ -27,6 +27,7 @@ Notes:
 
 #include "ast.h"
 #include "solver.h"
+#include "optimize_objectives.h"
 
 namespace opt {
 
@@ -41,7 +42,7 @@ namespace opt {
         svector<bool>    m_is_max;
         ref<solver>      m_solver;
         params_ref       m_params;
-        
+        optimize_objectives m_opt_objectives;
     public:
         context(ast_manager& m);
 

src/opt/optimize_objectives.cpp

@@ -67,28 +67,28 @@ namespace opt {
         ast_manager& m = objectives.get_manager();
         arith_util autil(m);
 
-        s.reset_objectives();
+        s->reset_objectives();
         values.reset();
         // First check_sat call to initialize theories
-        lbool is_sat = s.check_sat(0, 0);
+        lbool is_sat = s->check_sat(0, 0);
         if (is_sat == l_false) {
             return is_sat;
         }
 
-        opt_solver::scoped_push _push(s);
+        opt_solver::scoped_push _push(*s);
 
-        opt_solver::toggle_objective _t(s, true);
+        opt_solver::toggle_objective _t(*s, true);
 
         for (unsigned i = 0; i < objectives.size(); ++i) {
-            s.add_objective(objectives[i].get());
+            s->add_objective(objectives[i].get());
             values.push_back(inf_eps(rational(-1),inf_rational(0)));
         }
 
-        is_sat = s.check_sat(0, 0);
+        is_sat = s->check_sat(0, 0);
         
                 
         while (is_sat == l_true && !m_cancel) {
-            set_max(values, s.get_objective_values());
+            set_max(values, s->get_objective_values());
             IF_VERBOSE(1, 
                        for (unsigned i = 0; i < values.size(); ++i) {
                            verbose_stream() << values[i] << " ";
@@ -99,11 +99,11 @@ namespace opt {
 
             for (unsigned i = 0; i < objectives.size(); ++i) {
                 inf_eps const& v = values[i];
-                disj.push_back(s.block_lower_bound(i, v));
+                disj.push_back(s->block_lower_bound(i, v));
             }
             constraint = m.mk_or(disj.size(), disj.c_ptr());
-            s.assert_expr(constraint);
+            s->assert_expr(constraint);
-            is_sat = s.check_sat(0, 0);
+            is_sat = s->check_sat(0, 0);
         }      
 
         
@@ -117,7 +117,8 @@ namespace opt {
        Takes solver with hard constraints added.
        Returns an optimal assignment to objective functions.
     */
-    lbool optimize_objectives::operator()(app_ref_vector& objectives, vector<inf_eps>& values) {
+    lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector<inf_eps>& values) {
+        s = &solver;
         return basic_opt(objectives, values);
     }
 

src/opt/optimize_objectives.h

@@ -29,12 +29,12 @@ namespace opt {
 
     class optimize_objectives {
         ast_manager& m;
-        opt_solver& s;
+        opt_solver*  s;
         volatile bool m_cancel;
     public:
-        optimize_objectives(ast_manager& m, opt_solver& s): m(m), s(s), m_cancel(false) {}
+        optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {}
 
-        lbool operator()(app_ref_vector& objectives, vector<inf_eps>& values);
+        lbool operator()(opt_solver& s, app_ref_vector& objectives, vector<inf_eps>& values);
 
         void set_cancel(bool f);