Create placeholders to optimization methods

scripts/mk_util.py

@@ -59,7 +59,7 @@ SHOW_CPPS = True
 VS_X64 = False
 ONLY_MAKEFILES = False
 Z3PY_SRC_DIR=None
-VS_PROJ = True
+VS_PROJ = False
 TRACE = False
 DOTNET_ENABLED=False
 JAVA_ENABLED=False

src/opt/opt_cmds.cpp

@@ -18,37 +18,18 @@ Notes:
 #include "opt_cmds.h"
 #include "cmd_context.h"
 #include "ast_pp.h"
-#include "smt_solver.h"
-#include "fu_malik.h"
 
-class opt_context {
-    ast_manager& m;
-    expr_ref_vector m_formulas;
-    vector<rational> m_weights;
+#include "opt_context.h"
 
-public:
-    opt_context(ast_manager& m):
-        m(m),
-        m_formulas(m)        
-    {}
-
-    void add_formula(expr* f, rational const& w) {
-        m_formulas.push_back(f);
-        m_weights.push_back(w);
-    }
-        
-    expr_ref_vector const & formulas() const { return m_formulas; }
-    vector<rational> const& weights() const { return m_weights; }
-};
 
 class assert_weighted_cmd : public cmd {
-    opt_context* m_opt_ctx;
+    opt::context* m_opt_ctx;
     unsigned   m_idx;
     expr_ref   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),
@@ -95,12 +76,11 @@ public:
     }
 
     virtual void execute(cmd_context & ctx) {
-        m_opt_ctx->add_formula(m_formula, m_weight);
+        m_opt_ctx->add_soft_constraint(m_formula, m_weight);
         reset(ctx);
     }
 
     virtual void finalize(cmd_context & ctx) { 
-        std::cout << "FINALIZE\n";
     }
 
 };
@@ -111,19 +91,16 @@ public:
 // to do the feasibility check.
 class min_maximize_cmd : public cmd {
     bool m_is_max;
-    expr_ref m_term;
-    opt_context* m_opt_ctx;
+    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_term(ctx.m()),
         m_opt_ctx(opt_ctx)
     {}
 
     virtual void reset(cmd_context & ctx) { 
-        m_term = 0;
     }
 
     virtual char const * get_usage() const { return "<term>"; }
@@ -134,7 +111,9 @@ 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) {
-        m_term = 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);
     }
 
     virtual void failure_cleanup(cmd_context & ctx) {
@@ -142,58 +121,45 @@ public:
     }
 
     virtual void execute(cmd_context & ctx) {
-        ast_manager& m = m_term.get_manager();
-        std::cout << "TODO: " << mk_pp(m_term, ctx.m()) << "\n";
-        // Here is how to retrieve the soft constraints
-        expr_ref_vector const& fmls = m_opt_ctx->formulas();
-        vector<rational> const& ws  = m_opt_ctx->weights();
+    }
 
-        // TODO: move most functionaltiy to separate module, because it is going to grow..
-        ref<solver> s;
-        symbol logic;
-        params_ref p;
-        p.set_bool("model", true);
-        p.set_bool("unsat_core", true);        
-        s = mk_smt_solver(m, p, logic);
+
+};
+
+class optimize_cmd : public cmd {
+    opt::context* m_opt_ctx;
+public:
+    optimize_cmd(opt::context* opt_ctx):
+        cmd("optimize"),
+        m_opt_ctx(opt_ctx)
+    {}
+    virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";}
+    virtual unsigned get_arity() const { return 0; }
+    virtual void prepare(cmd_context & ctx) {}
+    virtual void failure_cleanup(cmd_context & ctx) {
+        reset(ctx);
+    }
+
+    virtual void execute(cmd_context & ctx) {
 
         ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx.end_assertions();
         for (; it != end; ++it) {
-            s->assert_expr(*it);
-        }
-        expr_ref_vector fmls_copy(fmls);
-        if (is_maxsat_problem(ws)) {
-            lbool is_sat = opt::fu_malik_maxsat(*s, fmls_copy);
-            std::cout << "is-sat: " << is_sat << "\n";
-            if (is_sat == l_true) {
-                for (unsigned i = 0; i < fmls_copy.size(); ++i) {
-                    std::cout << mk_pp(fmls_copy[i].get(), m) << "\n";
-                }
-            }
-        }
-        else {
-            NOT_IMPLEMENTED_YET();
+            m_opt_ctx->add_hard_constraint(*it);
         }
+        m_opt_ctx->optimize();
 
-        // handle optimization criterion.        
+  
     }
-
 private:
 
-    bool is_maxsat_problem(vector<rational> const& ws) const {
-        for (unsigned i = 0; i < ws.size(); ++i) {
-            if (!ws[i].is_one()) {
-                return false;
-            }
-        }
-        return true;
-    }
 
 };
 
 void install_opt_cmds(cmd_context & ctx) {
-    opt_context* opt_ctx = alloc(opt_context, ctx.m());
+    opt::context* opt_ctx = alloc(opt::context, ctx.m());
     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

@@ -0,0 +1,94 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    opt_context.cpp
+
+Abstract:
+    Facility for running optimization problem.
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-10-16
+
+Notes:
+
+--*/
+
+
+#include "opt_context.h"
+#include "smt_solver.h"
+#include "fu_malik.h"
+#include "weighted_maxsat.h"
+#include "optimize_objectives.h"
+#include "ast_pp.h"
+
+namespace opt {
+
+    void context::optimize() {
+
+        expr_ref_vector const& fmls = m_soft_constraints;
+
+        ref<solver> s;
+        symbol logic;
+        params_ref p;
+        p.set_bool("model", true);
+        p.set_bool("unsat_core", true);        
+        s = mk_smt_solver(m, p, logic);
+
+        for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+            s->assert_expr(m_hard_constraints[i].get());
+        }
+
+        expr_ref_vector fmls_copy(fmls);
+        lbool is_sat;
+        if (!fmls.empty()) {
+            if (is_maxsat_problem()) {
+                is_sat = opt::fu_malik_maxsat(*s, fmls_copy);
+            }
+            else {
+                is_sat = weighted_maxsat(*s, fmls_copy, m_weights);
+            }
+            std::cout << "is-sat: " << is_sat << "\n";
+            if (is_sat != l_true) {
+                return;
+            }
+            for (unsigned i = 0; i < fmls_copy.size(); ++i) {
+                std::cout << "Satisfying soft constraint: " << mk_pp(fmls_copy[i].get(), m) << "\n";
+            }            
+        }
+
+        if (!m_objectives.empty()) {
+            vector<optional<rational> > values;
+            for (unsigned i = 0; i < fmls_copy.size(); ++i) {
+                s->assert_expr(fmls_copy[i].get());
+            }
+            is_sat = optimize_objectives(*s, m_objectives, m_is_max, values);
+            std::cout << "is-sat: " << is_sat << "\n";
+            if (is_sat != l_true) {
+                return;
+            }
+            for (unsigned i = 0; i < values.size(); ++i) {
+                // display
+            }
+        }     
+
+        if (m_objectives.empty() && m_soft_constraints.empty()) {
+            is_sat = s->check_sat(0,0);
+            std::cout << "nothing to optimize: is-sat " << is_sat << "\n";
+        }
+
+    }
+        
+    bool context::is_maxsat_problem() const {
+        vector<rational> const& ws  = m_weights;
+        for (unsigned i = 0; i < ws.size(); ++i) {
+            if (!ws[i].is_one()) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+}

src/opt/opt_context.h

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    opt_context.h
+
+Abstract:
+    Facility for running optimization problem.
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-10-16
+
+Notes:
+
+--*/
+#ifndef _OPT_CONTEXT_H_
+#define _OPT_CONTEXT_H_
+
+#include "ast.h"
+
+namespace opt {
+
+    class context {
+        ast_manager& m;
+        expr_ref_vector m_hard_constraints;
+        expr_ref_vector  m_soft_constraints;
+        vector<rational> m_weights;
+
+        expr_ref_vector m_objectives;
+        svector<bool>   m_is_max;
+
+    public:
+        context(ast_manager& m):
+            m(m),
+            m_hard_constraints(m),
+            m_soft_constraints(m),
+            m_objectives(m)
+        {}
+
+        void add_soft_constraint(expr* f, rational const& w) {
+            m_soft_constraints.push_back(f);
+            m_weights.push_back(w);
+        }
+
+        void add_objective(expr* t, bool is_max) {
+            m_objectives.push_back(t);
+            m_is_max.push_back(is_max);
+        }
+
+        void add_hard_constraint(expr* f) {
+            m_hard_constraints.push_back(f);
+        }
+
+        void optimize();
+
+    private:
+        bool is_maxsat_problem() const;
+
+    };
+
+
+}
+
+#endif

src/opt/optimize_objectives.cpp

@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    optimize_objectives.cpp
+
+Abstract:
+   
+    Objective optimization method.
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-10-16
+
+Notes:
+
+--*/
+
+
+#include "optimize_objectives.h"
+
+namespace opt {
+
+    /*
+        Enumerate locally optimal assignments until fixedpoint.
+    */
+    lbool mathsat_style_opt(solver& s, 
+                          expr_ref_vector& objectives, svector<bool> const& is_max,
+                          vector<optional<rational> >& values) {
+        lbool is_sat;
+        is_sat = s.check_sat(0,0);
+        if (is_sat != l_true) {
+            return is_sat;
+        }
+        // assume that s is instrumented to produce locally optimal assignments.
+
+        while (is_sat != l_false) {
+            model_ref model;
+            s.get_model(model);
+            // extract values for objectives.
+            // store them in values.
+            // assert there must be something better.
+            is_sat = s.check_sat(0,0);
+        }
+        return l_true;
+
+    }
+
+    /**
+       Takes solver with hard constraints added.
+       Returns an optimal assignment to objective functions.
+    */
+    
+    lbool optimize_objectives(solver& s, 
+                          expr_ref_vector& objectives, svector<bool> const& is_max,
+                          vector<optional<rational> >& values) {
+        return mathsat_style_opt(s, objectives, is_max, values);
+    }
+}

src/opt/optimize_objectives.h

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    optimize_objectives.h
+
+Abstract:
+   
+    Objective optimization method.
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-10-16
+
+Notes:
+
+--*/
+#ifndef _OPT_OBJECTIVES_H_
+#define _OPT_OBJECTIVES_H_
+
+#include "solver.h"
+
+namespace opt {
+    /**
+       Takes solver with hard constraints added.
+       Returns an optimal assignment to objective functions.
+    */
+    
+    lbool optimize_objectives(solver& s, 
+                          expr_ref_vector& objectives, svector<bool> const& is_max,
+                          vector<optional<rational> >& values);
+};
+
+#endif

src/opt/plan.txt

@@ -7,3 +7,11 @@ Similar to muz\fp\dl_cmds:
    Identifier is optional and used to group constraints together. 
    The F# sample illustrates what is meant.
 
+Next steps:
+        - replace solver by opt_solver.
+        - create a file called opt_solver, copy most from smt_solver into it.
+            Add some functions to enable/disable post-optimization on feasiable state.
+        - Add methods to theory_arith.h to enable/disable post-optimization
+        - Add method(s) to theory_arith.h to register objective functions.
+        - Add post-optimization step to theory_arith_core.h
+        - (Figure out how to do multi-objective in this framework directly besides naive loop)

src/opt/weighted_maxsat.cpp

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    weighted_maxsat.h
+
+Abstract:
+    Weighted MAXSAT module
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-10-16
+
+Notes:
+
+--*/
+
+#include "weighted_maxsat.h"
+
+namespace opt {
+    /**
+       Takes solver with hard constraints added.
+       Returns a maximal satisfying subset of weighted soft_constraints
+       that are still consistent with the solver state.
+    */
+    
+    lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
+        NOT_IMPLEMENTED_YET();
+        return l_false;
+    }
+};
+

src/opt/weighted_maxsat.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    weighted_maxsat.h
+
+Abstract:
+   Weighted MAXSAT module
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-10-16
+
+Notes:
+
+--*/
+#ifndef _OPT_WEIGHTED_MAX_SAT_H_
+#define _OPT_WEIGHTED_MAX_SAT_H_
+
+#include "solver.h"
+
+namespace opt {
+    /**
+       Takes solver with hard constraints added.
+       Returns a maximal satisfying subset of weighted soft_constraints
+       that are still consistent with the solver state.
+    */
+    
+    lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights);
+};
+
+#endif