tidy & todo notes

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

src/opt/fu_malik.cpp

@@ -37,13 +37,13 @@ namespace opt {
 
     class fu_malik {
         ast_manager& m;
-        ::solver& s;
+        solver& s;
         expr_ref_vector m_soft;
         expr_ref_vector m_aux;
 
     public:
 
-        fu_malik(ast_manager& m, ::solver& s, expr_ref_vector const& soft):
+        fu_malik(ast_manager& m, solver& s, expr_ref_vector const& soft):
             m(m),
             s(s),
             m_soft(soft),
@@ -132,7 +132,7 @@ namespace opt {
 
     };
     
-    lbool fu_malik_maxsat(::solver& s, expr_ref_vector& soft_constraints) {
+    lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints) {
         ast_manager& m = soft_constraints.get_manager();
         lbool is_sat = s.check_sat(0,0);
         if (!soft_constraints.empty() && is_sat == l_true) {

src/opt/fu_malik.h

@@ -28,7 +28,7 @@ namespace opt {
        that are still consistent with the solver state.
     */
     
-    lbool fu_malik_maxsat(::solver& s, expr_ref_vector& soft_constraints);
+    lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints);
 };
 
 #endif

src/opt/opt_cmds.cpp

@@ -14,12 +14,26 @@ Author:
 
 Notes:
 
+    TODO:
+    - integrate with parameters. 
+      Parameter infrastructure lets us control setttings, such as 
+      timeouts and control which backend optimization approach to 
+      use during experiments.
+
+    - Display statistics properly on exit when configured to do so.
+      Also add appropriate statistics tracking to opt::context
+
+    - Deal with push/pop (later)
+
+    - Revisit weighted constraints if we want to group them using identifiers.
+
 --*/
 #include "opt_cmds.h"
 #include "cmd_context.h"
 #include "ast_pp.h"
-
 #include "opt_context.h"
+#include "cancel_eh.h"
+#include "scoped_ctrl_c.h"
 
 
 class opt_context {
@@ -37,13 +51,13 @@ public:
 
 
 class assert_weighted_cmd : public cmd {
-    opt_context* m_opt_ctx;
-    unsigned   m_idx;
-    expr*      m_formula;
-    rational   m_weight;
+    opt_context& m_opt_ctx;
+    unsigned     m_idx;
+    expr*        m_formula;
+    rational     m_weight;
 
 public:
-    assert_weighted_cmd(cmd_context& ctx, opt_context* opt_ctx):
+    assert_weighted_cmd(cmd_context& ctx, opt_context& opt_ctx):
         cmd("assert-weighted"),
         m_opt_ctx(opt_ctx),
         m_idx(0),
@@ -52,7 +66,7 @@ public:
     {}
 
     virtual ~assert_weighted_cmd() {
-        dealloc(m_opt_ctx);
+        dealloc(&m_opt_ctx);
     }
 
     virtual void reset(cmd_context & ctx) { 
@@ -94,7 +108,7 @@ public:
     }
 
     virtual void execute(cmd_context & ctx) {
-        (*m_opt_ctx)().add_soft_constraint(m_formula, m_weight);
+        m_opt_ctx().add_soft_constraint(m_formula, m_weight);
         reset(ctx);
     }
 
@@ -103,23 +117,18 @@ public:
 
 };
 
-// what amounts to check-sat, but uses the *single* objective function.
-// alternative is to register multiple objective functions using
-// minimize/maximize and then use check-sat or some variant of it 
-// to do the feasibility check.
 class min_maximize_cmd : public cmd {
-    bool m_is_max;
-    opt_context* m_opt_ctx;
+    bool         m_is_max;
+    opt_context& m_opt_ctx;
 
 public:
-    min_maximize_cmd(cmd_context& ctx, opt_context* opt_ctx, bool is_max):
+    min_maximize_cmd(cmd_context& ctx, opt_context& opt_ctx, bool is_max):
         cmd(is_max?"maximize":"minimize"),
         m_is_max(is_max),
         m_opt_ctx(opt_ctx)
     {}
 
-    virtual void reset(cmd_context & ctx) { 
-    }
+    virtual void reset(cmd_context & ctx) { }
 
     virtual char const * get_usage() const { return "<term>"; }
     virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";}
@@ -129,9 +138,7 @@ public:
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; }
 
     virtual void set_next_arg(cmd_context & ctx, expr * t) {
-        // TODO: type check objective term. It should pass basic sanity being
-        // integer, real (, bit-vector) or other supported objective function type.
-        (*m_opt_ctx)().add_objective(t, m_is_max);
+        m_opt_ctx().add_objective(t, m_is_max);
     }
 
     virtual void failure_cleanup(cmd_context & ctx) {
@@ -140,14 +147,12 @@ public:
 
     virtual void execute(cmd_context & ctx) {
     }
-
-
 };
 
 class optimize_cmd : public cmd {
-    opt_context* m_opt_ctx;
+    opt_context& m_opt_ctx;
 public:
-    optimize_cmd(opt_context* opt_ctx):
+    optimize_cmd(opt_context& opt_ctx):
         cmd("optimize"),
         m_opt_ctx(opt_ctx)
     {}
@@ -159,25 +164,33 @@ public:
     }
 
     virtual void execute(cmd_context & ctx) {
-
+        opt::context& opt = m_opt_ctx();
         ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx.end_assertions();
         for (; it != end; ++it) {
-            (*m_opt_ctx)().add_hard_constraint(*it);
+            opt.add_hard_constraint(*it);
+        }
+        cancel_eh<opt::context> eh(opt);
+        {
+            scoped_ctrl_c ctrlc(eh);
+            cmd_context::scoped_watch sw(ctx);
+            try {
+                opt.optimize();
+            }
+            catch (z3_error& ex) {
+                ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
+            }
+            catch (z3_exception& ex) {
+                ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
+            }
         }
-        (*m_opt_ctx)().optimize();
-
-  
     }
-private:
-
-
 };
 
 void install_opt_cmds(cmd_context & ctx) {
     opt_context* opt_ctx = alloc(opt_context, ctx);
-    ctx.insert(alloc(assert_weighted_cmd, ctx, opt_ctx));
-    ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, true));
-    ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, false));
-    ctx.insert(alloc(optimize_cmd, opt_ctx));
+    ctx.insert(alloc(assert_weighted_cmd, ctx, *opt_ctx));
+    ctx.insert(alloc(min_maximize_cmd, ctx, *opt_ctx, true));
+    ctx.insert(alloc(min_maximize_cmd, ctx, *opt_ctx, false));
+    ctx.insert(alloc(optimize_cmd, *opt_ctx));
 }

src/opt/opt_context.cpp

@@ -14,6 +14,13 @@ Author:
 
 Notes:
 
+    TODO:
+
+    - there are race conditions for cancelation.
+    - it would also be a good idea to maintain a volatile bool to track
+      cancelation and then bail out of loops inside optimize() and derived
+      functions.
+
 --*/
 
 #include "opt_context.h"
@@ -95,4 +102,16 @@ namespace opt {
         return true;
     }
 
+    void context::cancel() {
+        if (m_solver) {
+            m_solver->cancel();
+        }
+    }
+
+    void context::reset_cancel() {
+        if (m_solver) {
+            m_solver->reset_cancel();
+        }
+    }
+
 }

src/opt/opt_context.h

@@ -14,6 +14,13 @@ Author:
 
 Notes:
 
+    TODO:
+
+    - type check objective term and assertions. It should pass basic sanity being
+      integer, real (, bit-vector) or other supported objective function type.
+
+    - add appropriate statistics tracking to opt::context
+
 --*/
 #ifndef _OPT_CONTEXT_H_
 #define _OPT_CONTEXT_H_
@@ -31,7 +38,7 @@ namespace opt {
 
         expr_ref_vector m_objectives;
         svector<bool>   m_is_max;
-        ref<::solver>     m_solver;
+        ref<solver>     m_solver;
 
     public:
         context(ast_manager& m):
@@ -55,12 +62,15 @@ namespace opt {
             m_hard_constraints.push_back(f);
         }
 
-        void set_solver(::solver* s) {
+        void set_solver(solver* s) {
             m_solver = s;
         }
 
         void optimize();
 
+        void cancel();
+        void reset_cancel();
+
     private:
         bool is_maxsat_problem() const;
 

src/smt/theory_opt.h

@@ -28,11 +28,11 @@ namespace smt {
     public:
         virtual bool maximize(theory_var v) { UNREACHABLE(); return false; };
         virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; }
-		virtual inf_eps_rational<rational> get_objective_value(theory_var v) { 
+        virtual inf_eps_rational<rational> get_objective_value(theory_var v) { 
             UNREACHABLE(); 
             inf_eps_rational<rational> r(rational(1), rational(0)); 
             return r; 
-		}
+        }
     };
 }