From faa59ba7f90020c06677e705b0c9b237abf40b59 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Dec 2013 14:14:44 -0800
Subject: [PATCH] debugging multi-objective interface and pb revisions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp |  2 +-
 src/opt/opt_cmds.cpp            | 32 ++++++++++++++++++++++++++------
 src/smt/theory_pb.cpp           |  8 ++++----
 3 files changed, 31 insertions(+), 11 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 976a66664..47575be7e 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -689,7 +689,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
     if (!m_global_decls) {
         m_func_decls_stack.push_back(sf_pair(s, f));
     }
-    TRACE("cmd_context", tout << "new sort decl\n" << mk_pp(f, m()) << "\n";);
+    TRACE("cmd_context", tout << "new function decl\n" << mk_pp(f, m()) << "\n";);
 }
 
 void cmd_context::insert(symbol const & s, psort_decl * p) {
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index 7691787ce..8cf432e7b 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -35,16 +35,27 @@ Notes:
 class opt_context {
     cmd_context& ctx;
     scoped_ptr<opt::context> m_opt;
+    hashtable<symbol, symbol_hash_proc, symbol_eq_proc> m_ids;    
+
 public:
     opt_context(cmd_context& ctx): ctx(ctx) {}
     opt::context& operator()() { 
         if (!m_opt) {
-            m_opt = alloc(opt::context, ctx.m());
             decl_plugin * p = alloc(opt::objective_decl_plugin);
-            ctx.register_plugin(symbol("objective"), p, true);            
+            ctx.register_plugin(symbol("objective"), p, true);
+            m_opt = alloc(opt::context, ctx.m());
         }
         return *m_opt;
     }
+
+    bool contains(symbol const& s) const { return m_ids.contains(s); }
+
+    void insert(symbol const& s) { m_ids.insert(s); }
+
+    sort* obj_sort(cmd_context& ctx) {
+        return ctx.m().mk_sort(ctx.m().get_family_id(symbol("objective")), opt::OBJECTIVE_SORT);
+    }
+    
 };
 
 
@@ -121,6 +132,10 @@ public:
 
     virtual void execute(cmd_context & ctx) {
         m_opt_ctx().add_soft_constraint(m_formula, m_weight, m_id);
+        if (!m_opt_ctx.contains(m_id)) {
+            ctx.insert(m_id, 0, ctx.m().mk_const(m_id, m_opt_ctx.obj_sort(ctx)));
+            m_opt_ctx.insert(m_id);
+        }
         reset(ctx);
     }
 
@@ -255,12 +270,14 @@ private:
 class execute_cmd : public parametric_cmd {
 protected:
     expr * m_objective;
+    unsigned m_idx;
     opt_context& m_opt_ctx;
 public:
     execute_cmd(opt_context& opt_ctx):
         parametric_cmd("optimize"),
-        m_opt_ctx(opt_ctx),
-        m_objective(0)
+        m_objective(0),
+        m_idx(0),
+        m_opt_ctx(opt_ctx)
     {}
 
     virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
@@ -271,10 +288,11 @@ public:
     }
 
     virtual char const * get_main_descr() const { return "check sat modulo objective function";}
-    virtual char const * get_usage() const { return "(<keyword> <value>)*"; }
+    virtual char const * get_usage() const { return "<objective> (<keyword> <value>)*"; }
     virtual void prepare(cmd_context & ctx) {
         parametric_cmd::prepare(ctx);
         reset(ctx);
+        m_opt_ctx(); // ensure symbol table is updated.
     }
     virtual void failure_cleanup(cmd_context & ctx) {
         reset(ctx);
@@ -284,16 +302,18 @@ public:
             ctx.m().dec_ref(m_objective);
         }
         m_objective = 0;
+        m_idx = 0;
     }
 
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
-        if (m_objective == 0) return CPK_EXPR;
+        if (m_idx == 0) return CPK_EXPR;
         return parametric_cmd::next_arg_kind(ctx);
     }
 
     virtual void set_next_arg(cmd_context & ctx, expr * arg) {
         m_objective = arg;
         ctx.m().inc_ref(arg);
+        ++m_idx;
     }
 
     virtual void execute(cmd_context & ctx) {
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 46a8eb443..79db388f4 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -550,8 +550,8 @@ namespace smt {
     void theory_pb::assign_eh(bool_var v, bool is_true) {
         context& ctx = get_context();
         ptr_vector<ineq>* ineqs = 0;
-        literal lit(v, !is_true);
-        if (m_watch.find(lit.index(), ineqs)) {
+        literal nlit(v, is_true);
+        if (m_watch.find(nlit.index(), ineqs)) {
             for (unsigned i = 0; i < ineqs->size(); ++i) {
                 if (assign_watch(v, is_true, *ineqs, i)) {
                     // i was removed from watch list.
@@ -1283,8 +1283,8 @@ namespace smt {
             UNREACHABLE();
             return false;
         case l_false:
-            add_assign(c, m_ineq_literals, false_literal);
-            break;
+            //add_assign(c, m_ineq_literals, false_literal);
+            //break;
         default: {
             app_ref tmp = m_lemma.to_expr(ctx, get_manager());
             internalize_atom(tmp, false);