From 670f56e5e4fad8990f00ab7878a450cb08a9a746 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 21 Dec 2013 07:09:39 -0800
Subject: [PATCH] adjust benchmark generation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_solver.cpp      |  8 ++++----
 src/opt/opt_solver.h        |  2 +-
 src/opt/weighted_maxsat.cpp | 11 +++++++----
 src/smt/theory_pb.cpp       | 13 ++++++++++++-
 4 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index eb97d49b0..c437e48f1 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -38,12 +38,13 @@ namespace opt {
         m_context(mgr, m_params),
         m(mgr),
         m_dump_benchmarks(false),
-        m_dump_count(0),
         m_fm(m) {
         m_logic = l;
         if (m_logic != symbol::null)
             m_context.set_logic(m_logic);
     }
+
+    unsigned opt_solver::m_dump_count = 0;
     
     opt_solver::~opt_solver() {
     }
@@ -119,15 +120,14 @@ namespace opt {
                 tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";
             }
         });
-
-        lbool r = m_context.check(num_assumptions, assumptions);
         if (dump_benchmarks()) {
             std::stringstream file_name;
             file_name << "opt_solver" << ++m_dump_count << ".smt2";
             std::ofstream buffer(file_name.str().c_str());
-            to_smt2_benchmark(buffer, "opt_solver", "QF_BV");
+            to_smt2_benchmark(buffer, "opt_solver", "");
             buffer.close();
         }
+        lbool r = m_context.check(num_assumptions, assumptions);
         return r;
     }
 
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 141108d0a..eb5812317 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -48,7 +48,7 @@ namespace opt {
         svector<smt::theory_var>  m_objective_vars;
         vector<inf_eps>     m_objective_values;
         bool                m_dump_benchmarks;
-        unsigned            m_dump_count;
+        static unsigned     m_dump_count;
         statistics          m_stats;
         filter_model_converter m_fm;
     public:
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 0619953b9..b9a9cfbcc 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -246,9 +246,7 @@ namespace smt {
                 }
             }
             m_propagate = false;
-        }
-        
-
+        }       
 
         bool is_optimal() const {
             return m_cost < m_min_cost;
@@ -755,7 +753,7 @@ namespace opt {
             pb_util u(m);
             lbool is_sat = bound(al, ws, bs, k);
             if (is_sat != l_true) return is_sat;
-#if 1
+#if 0
             rational mininc(0);
             for (unsigned i = 0; i < ws.size(); ++i) {
                 if (mininc.is_zero() || mininc > ws[i]) {
@@ -795,6 +793,7 @@ namespace opt {
                 nbs.push_back(m.mk_not(bs[i]));
             }            
             m_imp = alloc(imp, m, m_solver, nbs, ws); // race condition.
+            m_imp->updt_params(m_params);
             lbool is_sat = m_imp->pb_solve();
             k = m_imp->m_lower;
             m_solver.pop_core(1);
@@ -804,6 +803,10 @@ namespace opt {
         void updt_params(params_ref& p) {
             opt_params _p(p);
             m_engine = _p.wmaxsat_engine();        
+            m_solver.updt_params(p);
+            if (m_imp) {
+                m_imp->updt_params(p);
+            }
         }
 
     };
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 755bc4c2c..df71ce969 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -388,8 +388,8 @@ namespace smt {
         c->prune();
         TRACE("pb", display(tout, *c););
 
-        
         literal lit(abv);
+        
         switch(is_true) {
         case l_false: 
             lit = ~lit;
@@ -405,6 +405,17 @@ namespace smt {
 
         // TBD: special cases: k == 1, or args.size() == 1
             
+        if (c->k().is_one()) {
+            literal_vector& lits = get_lits();
+            lits.push_back(~lit);
+            for (unsigned i = 0; i < c->size(); ++i) {
+                lits.push_back(c->lit(i));
+                SASSERT(c->coeff(i).is_one());
+                ctx.mk_th_axiom(get_id(), lit, ~c->lit(i));
+            }
+            ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+            return true;
+        }
         
         
         // maximal coefficient: