add bvmax tactic, add proviso for non-0 lower bounds in elim01

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

src/cmd_context/cmd_context.cpp

@@ -1376,6 +1376,9 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             throw cmd_exception(ex.msg());
         }
         get_opt()->set_status(r);
+        if (r != l_false) {
+            get_opt()->display_assignment(regular_stream());
+        }
     }
     else if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
@@ -1580,6 +1583,9 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
     else if (m_solver) {
         m_solver->collect_statistics(st);
     }
+    else if (m_opt) {
+        m_opt->collect_statistics(st);
+    }
     st.display_smt2(regular_stream());
 }
 

src/cmd_context/cmd_context.h

@@ -121,6 +121,7 @@ public:
     virtual void cancel() = 0;
     virtual lbool optimize() = 0;
     virtual void set_hard_constraints(ptr_vector<expr> & hard) = 0;
+    virtual void display_assignment(std::ostream& out) = 0;
 };
 
 class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {

src/opt/opt_context.h

@@ -122,8 +122,7 @@ namespace opt {
         virtual void get_unsat_core(ptr_vector<expr> & r) {}
         virtual std::string reason_unknown() const { return std::string("unknown"); }
 
-        void display_assignment(std::ostream& out);
+        virtual void display_assignment(std::ostream& out);
-        void display_range_assignment(std::ostream& out);
         static void collect_param_descrs(param_descrs & r);
         void updt_params(params_ref& p);
 

src/opt/opt_solver.cpp

@@ -44,6 +44,7 @@ namespace opt {
         m_logic = l;
         if (m_logic != symbol::null)
             m_context.set_logic(m_logic);
+        m_params.m_relevancy_lvl = 0;
     }
 
     unsigned opt_solver::m_dump_count = 0;

src/opt/weighted_maxsat.cpp

@@ -29,6 +29,9 @@ Notes:
 #include "tactic.h"
 #include "model_smt2_pp.h"
 #include "pb_sls.h"
+#include "qfbv_tactic.h"
+#include "card2bv_tactic.h"
+#include "tactic2solver.h"
 
 namespace smt {
 
@@ -450,6 +453,7 @@ namespace opt {
         volatile bool    m_cancel;
         params_ref       m_params;
         opt_solver       m_solver;
+        ref<solver>      m_sat_solver;
         scoped_ptr<imp>  m_imp;
         smt::pb_sls      m_sls;
 
@@ -511,6 +515,9 @@ namespace opt {
             if (m_engine == symbol("pwmax")) {
                 return pb_solve();
             }
+            if (m_engine == symbol("bvmax")) {
+                return pb2sat_solve();
+            }
             if (m_engine == symbol("wpm2")) {
                 return wpm2_solve();
             }
@@ -520,7 +527,11 @@ namespace opt {
             if (m_engine == symbol("sls")) {
                 return sls_solve();
             }
-            return incremental_solve();
+            if (m_engine == symbol::null || m_engine == symbol("wmax")) {
+                return incremental_solve();
+            }
+            IF_VERBOSE(0, verbose_stream() << "(unknown engine " << m_engine << " using default 'wmax')\n";);
+            return incremental_solve();            
         }
 
         rational get_lower() const {
@@ -535,6 +546,25 @@ namespace opt {
             mdl = m_model.get();
         }
 
+        void set_cancel(bool f) {
+            if (m_sat_solver) {
+                m_sat_solver->set_cancel(f);
+            }
+            m_sls.set_cancel(f);
+            m_cancel = f;
+            m_solver.set_cancel(f);
+            m_imp->m_cancel = f;        
+            m_imp->m_solver.set_cancel(f);
+        }
+
+        void collect_statistics(statistics& st) const {
+            m_solver.collect_statistics(st);
+            if (m_sat_solver) {
+                m_sat_solver->collect_statistics(st);
+            }
+        }
+
+
         class scoped_ensure_theory {
             smt::theory_weighted_maxsat* m_wth;
         public:
@@ -732,7 +762,6 @@ namespace opt {
 
 
         // convert bounds constraint into pseudo-Boolean
-
         lbool pb_solve() {
             pb_util u(m);
             expr_ref fml(m), val(m);
@@ -778,6 +807,63 @@ namespace opt {
             return is_sat;
         }
 
+        //
+        // convert bounds constraint into pseudo-Boolean, 
+        // then treat pseudo-Booleans as bit-vectors and
+        // sorting circuits.
+        //
+        lbool pb2sat_solve() {
+            pb_util u(m);
+            expr_ref fml(m), val(m);
+            app_ref b(m);
+            expr_ref_vector nsoft(m);
+            m_lower = m_upper = rational::zero();
+            tactic_ref pb2bv = mk_card2bv_tactic(m, m_params);
+            tactic_ref bv2sat = mk_qfbv_tactic(m, m_params);
+            tactic_ref tac = and_then(pb2bv.get(), bv2sat.get());
+            m_sat_solver = mk_tactic2solver(m, tac.get(), m_params);
+            unsigned sz = s.get_num_assertions();
+            for (unsigned i = 0; i < sz; ++i) {
+                m_sat_solver->assert_expr(s.get_assertion(i));
+            }
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
+                m_upper += m_weights[i];
+                b = m.mk_fresh_const("b", m.mk_bool_sort());
+                // TODO: s.mc().insert(b->get_decl());
+                fml = m.mk_or(m_soft[i].get(), b);
+                m_sat_solver->assert_expr(fml);
+                nsoft.push_back(b);
+            }
+            lbool is_sat = l_true;
+            bool was_sat = false;
+            while (l_true == is_sat) {
+                is_sat = m_sat_solver->check_sat(0,0);
+                if (m_cancel) {
+                    is_sat = l_undef;
+                }
+                if (is_sat == l_true) {
+                    m_sat_solver->get_model(m_model);
+                    m_upper = rational::zero();
+                    for (unsigned i = 0; i < m_soft.size(); ++i) {
+                        VERIFY(m_model->eval(nsoft[i].get(), val));
+                        m_assignment[i] = !m.is_true(val);
+                        if (!m_assignment[i]) {
+                            m_upper += m_weights[i];
+                        }
+                    }                    
+                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";);
+                    fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
+                    m_sat_solver->assert_expr(fml);
+                    was_sat = true;
+                }
+            }            
+            if (is_sat == l_false && was_sat) {
+                is_sat = l_true;
+                m_lower = m_upper;
+            }
+            return is_sat;
+        }
+
         expr* mk_not(expr* e) {
             if (m.is_not(e, e)) {
                 return e;
@@ -1285,14 +1371,10 @@ namespace opt {
         return m_imp->m_assignment[idx];
     }
     void wmaxsmt::set_cancel(bool f) {
-        m_imp->m_sls.set_cancel(f);
+        m_imp->set_cancel(f);
-        m_imp->m_cancel = f;
-        m_imp->m_solver.set_cancel(f);
-        m_imp->m_imp->m_cancel = f;        
-        m_imp->m_imp->m_solver.set_cancel(f);
     }
     void wmaxsmt::collect_statistics(statistics& st) const {
-        m_imp->m_solver.collect_statistics(st);
+        m_imp->collect_statistics(st);
     }
     void wmaxsmt::get_model(model_ref& mdl) {
         m_imp->get_model(mdl);

src/sat/sat_solver.cpp

@@ -686,7 +686,7 @@ namespace sat {
     //
     // -----------------------
     lbool solver::check() {
-        IF_VERBOSE(0, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";);
+        IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";);
         SASSERT(scope_lvl() == 0);
 #ifdef CLONE_BEFORE_SOLVING
         if (m_mc.empty()) {

src/smt/theory_pb.cpp

@@ -1558,6 +1558,8 @@ namespace smt {
         }
     }
 
+    static unsigned s_min_l_size = UINT_MAX;
+        
     //
     // modeled after sat_solver/smt_context
     //
@@ -1731,6 +1733,12 @@ namespace smt {
         m_lemma.prune(false);
 
         IF_VERBOSE(4, display(verbose_stream() << "lemma2: ", m_lemma););
+        //unsigned l_size = m_ineq_literals.size() + ((is_true==l_false)?0:m_lemma.size());
+        //if (s_min_l_size >= l_size) {
+        //    verbose_stream() << "(pb.conflict min size: " << l_size << ")\n";
+        //    s_min_l_size = l_size;        
+        //}
+        //IF_VERBOSE(1, verbose_stream() << "(pb.conflict " << m_ineq_literals.size() << " " << m_lemma.size() << "\n";);
         switch(is_true) {
         case l_true:
             UNREACHABLE();

src/tactic/arith/elim01_tactic.cpp

@@ -167,6 +167,7 @@ public:
         expr_ref_vector axioms(m);
         bounds(*g);
         
+        rational zero(0);
         bound_manager::iterator bit = bounds.begin(), bend = bounds.end();
         for (; bit != bend; ++bit) {
             if (!is_app(*bit)) continue;
@@ -174,9 +175,14 @@ public:
             bool s1, s2;
             rational lo, hi;
             if (a.is_int(x) && 
-                bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() &&
+                bounds.has_lower(x, lo, s1) && !s1 && zero <= lo &&
-                bounds.has_upper(x, hi, s2) && !s2 && hi <= m_max_hi) {
+                bounds.has_upper(x, hi, s2) && !s2 && hi <= m_max_hi && lo <= hi) {
-                add_variable(b2i, sub, x, hi.get_unsigned(), axioms);
+                add_variable(b2i, sub, x, lo.get_unsigned(), hi.get_unsigned(), axioms);
+            }
+            else if (a.is_int(x)) {
+                TRACE("pb", tout << "Not adding variable " << mk_pp(x, m) << " has lower: " 
+                      << bounds.has_lower(x, lo, s1) << " " << lo << " has upper: " 
+                      << bounds.has_upper(x, hi, s2) << " " << hi << "\n";);
             }
         }
                
@@ -209,6 +215,7 @@ public:
     void add_variable(bool2int_model_converter* b2i,
                       expr_safe_replace& sub,
                       app* x,
+                      unsigned min_value,
                       unsigned max_value,
                       expr_ref_vector& axioms) {
         std::string name = x->get_decl()->get_name().str();
@@ -242,6 +249,9 @@ public:
         if ((max_value & (max_value + 1)) != 0) {
             axioms.push_back(a.mk_le(sum, a.mk_numeral(rational(max_value), true)));
         }
+        if (min_value > 0) {
+            axioms.push_back(a.mk_ge(sum, a.mk_numeral(rational(min_value), true)));
+        }
     }
                       
 };