debugging opt

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

src/ast/rewriter/pb_rewriter_def.h

@@ -141,7 +141,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
         for (unsigned i = 0; i < args.size(); ++i) {
             args[i].second = PBU::numeral::one();
         }
-        k = PBU::numeral::one();
+        k = PBU::numeral(args.size());
         return l_undef;
     }
     

src/opt/opt_context.cpp

@@ -310,10 +310,13 @@ namespace opt {
                      mk_solve_eqs_tactic(m),
                      mk_elim_uncnstr_tactic(m),
                      mk_simplify_tactic(m));   
-        tactic_ref tac2 = mk_elim01_tactic(m);
-        tactic_ref tac3 = mk_lia2card_tactic(m);
         opt_params optp(m_params);
         if (optp.elim_01()) {
+            tactic_ref tac2 = mk_elim01_tactic(m);
+            tactic_ref tac3 = mk_lia2card_tactic(m);
+            params_ref lia_p;
+            lia_p.set_bool("compile_equality", optp.pb_compile_equality());
+            tac3->updt_params(lia_p);
             m_simplify = and_then(tac0.get(), tac2.get(), tac3.get());
         }
         else {

src/opt/opt_params.pyg

@@ -10,7 +10,8 @@ def_module_params('opt',
                           ('print_all_models', BOOL, False, 'display all intermediary models for satisfiable constraints'),
                           ('debug_conflict', BOOL, False, 'debug conflict resolution'),
                           ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'iwmax' (iterative), 'bwmax' (bisection)"),
-                          ('elim_01', BOOL, True, 'eliminate 01 variables')
+                          ('elim_01', BOOL, True, 'eliminate 01 variables'),
+                          ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)')
 
                           ))
 

src/opt/weighted_maxsat.cpp

@@ -266,7 +266,6 @@ namespace smt {
             m_min_cost_atoms.reset();
             m_propagate = false;
             m_assigned.reset();
-            m_stats.reset();
         }
 
         virtual theory * mk_fresh(context * new_ctx) { return 0; }
@@ -300,6 +299,7 @@ namespace smt {
         }
 
         expr_ref mk_block() {
+            ++m_stats.m_num_blocks;
             ast_manager& m = get_manager();
             expr_ref_vector disj(m);
             compare_cost compare_cost(*this);
@@ -445,6 +445,8 @@ namespace opt {
             m_weights.append(weights);
             m_assignment.reset();
             m_assignment.resize(m_soft.size(), false);
+            m_lower.reset();
+            m_upper.reset();
         }
 
         smt::theory_weighted_maxsat* get_theory() const {
@@ -686,18 +688,28 @@ namespace opt {
             return is_sat;
         }
 
+        expr* mk_not(expr* e) {
+            if (m.is_not(e, e)) {
+                return e;
+            }
+            else {
+                return m.mk_not(e);
+            }
+        }
+
         lbool pb_simplify_solve() {
+            TRACE("opt", s.display(tout); tout << "\n";
+                  for (unsigned i = 0; i < m_soft.size(); ++i) {
+                      tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n";
+                  }
+                  );
             pb_util u(m);
             expr_ref fml(m), val(m);
             expr_ref_vector nsoft(m);
             m_lower = m_upper = rational::zero();
-            rational minw(0);
             for (unsigned i = 0; i < m_soft.size(); ++i) {
                 m_upper += m_weights[i];
-                if (m_weights[i] < minw || minw.is_zero()) {
+                nsoft.push_back(mk_not(m_soft[i].get()));
-                    minw = m_weights[i];
-                }
-                nsoft.push_back(m.mk_not(m_soft[i].get()));
             }
             solver::scoped_push _s1(s);
             lbool is_sat = l_true;
@@ -711,17 +723,18 @@ namespace opt {
                     is_sat = l_undef;
                 }
                 if (is_sat == l_true) {
-                    rational old_upper = m_upper;
                     m_upper = rational::zero();
                     for (unsigned i = 0; i < m_soft.size(); ++i) {
                         VERIFY(m_model->eval(m_soft[i].get(), val));
-                        m_assignment[i] = !m.is_false(val);
+                        TRACE("opt", tout << "eval " << mk_pp(m_soft[i].get(), m) << " " << val << "\n";);
+                        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";);
+                    TRACE("opt", tout << "new upper: " << m_upper << "\n";);
-                    fml = u.mk_le(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper - minw);
+                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";);
+                    fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
                     was_sat = true;
                 }
             }            
@@ -729,6 +742,7 @@ namespace opt {
                 is_sat = l_true;
                 m_lower = m_upper;
             }
+            TRACE("opt", tout << "lower: " << m_lower << "\n";);
             return is_sat;
         }
 
@@ -777,6 +791,20 @@ namespace opt {
                 asms.append(ans);
                 asms.append(am);
                 lbool is_sat = s.check_sat(asms.size(), asms.c_ptr());
+                TRACE("opt", 
+                      tout << "\nassumptions: ";
+                      for (unsigned i = 0; i < asms.size(); ++i) {
+                          tout << mk_pp(asms[i].get(), m) << " ";
+                      }
+                      tout << "\n" << is_sat << "\n";
+                      tout << "upper: " << m_upper << "\n";
+                      tout << "lower: " << m_lower << "\n";
+                      if (is_sat == l_true) {
+                          model_ref mdl;
+                          s.get_model(mdl);
+                          model_smt2_pp(tout, m, *(mdl.get()), 0);
+                      });
+
                 if (m_cancel && is_sat != l_false) {
                     is_sat = l_undef;
                 }
@@ -784,17 +812,24 @@ namespace opt {
                     m_upper = m_lower;
                     updt_model(s);
                     for (unsigned i = 0; i < block.size(); ++i) {
-                        VERIFY(m_model->eval(block[i].get(), val));
+                        VERIFY(m_model->eval(m_soft[i].get(), val));
-                        m_assignment[i] = m.is_false(val);
+                        TRACE("opt", tout << mk_pp(block[i].get(), m) << " " << val << "\n";);
+                        m_assignment[i] = m.is_true(val);
                     }
                 }
-                if (is_sat != l_false) {                    
+                if (is_sat != l_false) {
                     return is_sat;
                 }
                 s.get_unsat_core(core);
                 if (core.empty()) {
                     return l_false;
                 }
+                TRACE("opt",
+                      tout << "core: ";
+                      for (unsigned i = 0; i < core.size(); ++i) {
+                          tout << mk_pp(core[i],m) << " ";
+                      }
+                      tout << "\n";);
                 uint_set A;
                 for (unsigned i = 0; i < core.size(); ++i) {
                     unsigned j;
@@ -834,6 +869,7 @@ namespace opt {
                 if (is_sat != l_true) {
                     return is_sat;
                 }
+                TRACE("opt", tout << "new bound: " << k << " lower: " << m_lower << "\n";);
                 m_lower += k;
                 expr_ref B_le_k(m), B_ge_k(m);
                 B_le_k = u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k);
@@ -1031,7 +1067,9 @@ namespace opt {
                         rational& k) {
             pb_util u(m);
             lbool is_sat = bound(al, ws, bs, k);
-            if (is_sat != l_true) return is_sat;
+            if (is_sat != l_true || !k.is_zero()) {
+                return is_sat;
+            }
             expr_ref_vector al2(m);
             al2.append(al);
             // w_j*b_j > k
@@ -1054,8 +1092,14 @@ namespace opt {
                 m_solver.assert_expr(al[i]);
             }
             for (unsigned i = 0; i < bs.size(); ++i) {
-                nbs.push_back(m.mk_not(bs[i]));
+                nbs.push_back(mk_not(bs[i]));
             }    
+            TRACE("opt", 
+                  m_solver.display(tout);
+                  tout << "\n";
+                  for (unsigned i = 0; i < bs.size(); ++i) {
+                      tout << mk_pp(bs[i], m) << " " << ws[i] << "\n";
+                  });
             m_imp->re_init(nbs, ws); 
             lbool is_sat = m_imp->pb_simplify_solve();
             k = m_imp->m_lower;
@@ -1105,7 +1149,7 @@ namespace opt {
             }
             else {
                 SASSERT(result.size() == 1);
-                goal* r = result[0];
+                goal_ref r = result[0];
                 solver::scoped_push _s(m_solver);
                 // TBD ptr_vector<expr> asms;
                 for (unsigned i = 0; i < r->size(); ++i) {

src/smt/params/theory_pb_params.h

@@ -31,7 +31,7 @@ struct theory_pb_params {
         m_pb_conflict_frequency(0),
         m_pb_learn_complements(true),
         m_pb_enable_compilation(true),
-        m_pb_enable_simplex(false)    
+        m_pb_enable_simplex(false)
     {}
     
     void updt_params(params_ref const & p);

src/smt/theory_pb.cpp

@@ -388,16 +388,13 @@ namespace smt {
             }
         }
         
-        // m_simplex.display(std::cout);
         literal_vector lits;
         for (unsigned i = 0; i < explains.size(); ++i) {
             literal lit(explains[i]);
             if (lit != null_literal) {
-                //std::cout << lit << " ";
                 lits.push_back(~lit);
             }
         }
-        //std::cout << "\n";
 
         m_stats.m_num_conflicts++;
         justification* js = 0;
@@ -799,8 +796,11 @@ namespace smt {
                 unsigned slack = info.m_slack;
                 if (is_true) {
                     update_bound(slack, literal(v), true, coeff);
+                    if (c->is_eq()) {
+                        update_bound(slack, literal(v), false, coeff);
+                    }
                 }
-                else {
+                else if (c->is_ge()) {
                     m_mpq_inf_mgr.sub(coeff, std::make_pair(mpq(1),mpq(0)), coeff);
                     update_bound(slack, ~literal(v), false, coeff);
                 }
@@ -1678,10 +1678,14 @@ namespace smt {
                 if (!conseq.sign() && j->get_from_theory() == get_id()) {                    
                     pbj = dynamic_cast<pb_justification*>(j);
                 }
-                if (pbj && pbj->get_ineq().is_ge()) {
+                if (pbj && pbj->get_ineq().is_eq()) {
                     // only resolve >= that are positive consequences.
                     pbj = 0;
                 }
+                if (pbj && pbj->get_ineq().lit() == conseq) {
+                    // can't resolve against literal representing inequality.
+                    pbj = 0;
+                }
                 if (pbj) {
                     // weaken the lemma and resolve.
                     TRACE("pb", display(tout << "resolve with inequality", pbj->get_ineq(), true););

src/tactic/arith/lia2card_tactic.cpp

@@ -33,12 +33,13 @@ public:
     pb_util                          m_pb;
     mutable ptr_vector<expr>         m_todo;
     expr_set                         m_01s;
-
+    bool                             m_compile_equality;
     
     lia2card_tactic(ast_manager & _m, params_ref const & p):
         m(_m),
         a(m),
-        m_pb(m) {
+        m_pb(m),
+        m_compile_equality(false) {
     }
 
     virtual ~lia2card_tactic() {
@@ -49,6 +50,7 @@ public:
         
     void updt_params(params_ref const & p) {
         m_params = p;
+        m_compile_equality = p.get_bool("compile_equality", false);
     }
     
     virtual void operator()(goal_ref const & g, 
@@ -64,6 +66,7 @@ public:
         
         bound_manager bounds(m);
         bounds(*g);
+
         
         bound_manager::iterator bit = bounds.begin(), bend = bounds.end();
         for (; bit != bend; ++bit) {
@@ -175,11 +178,12 @@ public:
     }
 
     expr* mk_eq(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
-#if 1
+        if (m_compile_equality) {
-        return m.mk_and(mk_ge(sz, weights, args, w), mk_le(sz, weights, args, w));
+            return m_pb.mk_eq(sz, weights, args, w);
-#else
+        }
-        return m_pb.mk_eq(sz, weights, args, w);
+        else {
-#endif
+            return m.mk_and(mk_ge(sz, weights, args, w), mk_le(sz, weights, args, w));
+        }
     }
     
     expr* mk_ge(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
@@ -270,6 +274,8 @@ public:
     }
         
     virtual void collect_param_descrs(param_descrs & r) {
+        r.insert("compile_equality", CPK_BOOL, 
+                 "(default:false) compile equalities into pseudo-Boolean equality");
     }
         
     virtual void cleanup() {

src/tactic/arith/purify_arith_tactic.cpp

@@ -707,7 +707,7 @@ public:
 
     virtual void collect_param_descrs(param_descrs & r) {
         r.insert("complete", CPK_BOOL, 
-                 "(default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a functio. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root");
+                 "(default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root");
         r.insert("elim_root_objects", CPK_BOOL,
                  "(default: true) eliminate root objects.");
         r.insert("elim_inverses", CPK_BOOL,