fix local search encoding bug

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

src/opt/opt_context.cpp

@@ -721,8 +721,8 @@ namespace opt {
         }
 
         goal_ref g(alloc(goal, m, true, false));
-        for (unsigned i = 0; i < fmls.size(); ++i) {
+        for (expr* fml : fmls) {
-            g->assert_expr(fmls[i].get());
+            g->assert_expr(fml);
         }
         tactic_ref tac0 = 
             and_then(mk_simplify_tactic(m, m_params), 

src/sat/ba_solver.h

@@ -453,7 +453,6 @@ namespace sat {
         bool validate_resolvent();
 
         void display(std::ostream& out, ineq& p, bool values = false) const;
-        void display(std::ostream& out, constraint const& c, bool values) const;
         void display(std::ostream& out, card const& c, bool values) const;
         void display(std::ostream& out, pb const& p, bool values) const;
         void display(std::ostream& out, xr const& c, bool values) const;
@@ -500,6 +499,7 @@ namespace sat {
         virtual bool is_blocked(literal l, ext_constraint_idx idx);
 
         ptr_vector<constraint> const & constraints() const { return m_constraints; }
+        void display(std::ostream& out, constraint const& c, bool values) const;
 
         virtual bool validate();
 

src/sat/sat_local_search.cpp

@@ -104,7 +104,7 @@ namespace sat {
             coeff_vector& falsep = m_vars[v].m_watch[!is_true];
             for (unsigned i = 0; i < falsep.size(); ++i) {
                 constraint& c = m_constraints[falsep[i].m_constraint_id];
-                SASSERT(falsep[i].m_coeff == 1);
+                //SASSERT(falsep[i].m_coeff == 1);
                 // will --slack
                 if (c.m_slack <= 0) {
                     dec_slack_score(v);
@@ -113,7 +113,7 @@ namespace sat {
                 }
             }
             for (unsigned i = 0; i < truep.size(); ++i) {
-                SASSERT(truep[i].m_coeff == 1);
+                //SASSERT(truep[i].m_coeff == 1);
                 constraint& c = m_constraints[truep[i].m_constraint_id];
                 // will --true_terms_count[c]
                 // will ++slack
@@ -139,7 +139,8 @@ namespace sat {
 
     void local_search::reinit() {
 
-        if (!m_is_pb) {
+        IF_VERBOSE(10, verbose_stream() << "(sat-local-search reinit)\n";);
+        if (true || !m_is_pb) {
             //
             // the following methods does NOT converge for pseudo-boolean
             // can try other way to define "worse" and "better"
@@ -156,8 +157,7 @@ namespace sat {
             }
         }
 
-        for (unsigned i = 0; i < m_constraints.size(); ++i) {
+        for (constraint & c : m_constraints) {
-            constraint& c = m_constraints[i];
             c.m_slack = c.m_k;
         }
         
@@ -216,31 +216,43 @@ namespace sat {
     }
     
     void local_search::verify_solution() const {
-        for (unsigned i = 0; i < m_constraints.size(); ++i) {
+        for (constraint const& c : m_constraints) 
-            verify_constraint(m_constraints[i]);
+            verify_constraint(c);
-        }
     }
 
-    void local_search::verify_unsat_stack() const {
+    void local_search::verify_unsat_stack() const {        
-        for (unsigned i = 0; i < m_unsat_stack.size(); ++i) {
+        for (unsigned i : m_unsat_stack) {
-            constraint const& c = m_constraints[m_unsat_stack[i]];
+            constraint const& c = m_constraints[i];
             SASSERT(c.m_k < constraint_value(c));
         }
     }
 
+    unsigned local_search::constraint_coeff(constraint const& c, literal l) const {
+        for (auto const& pb : m_vars[l.var()].m_watch[is_pos(l)]) {
+            if (pb.m_constraint_id == c.m_id) return pb.m_coeff;
+        }
+        UNREACHABLE();
+        return 0;
+    }
+
+
     unsigned local_search::constraint_value(constraint const& c) const {
         unsigned value = 0;
         for (unsigned i = 0; i < c.size(); ++i) {
-            value += is_true(c[i]) ? 1 : 0;
+            literal t = c[i];
+            if (is_true(t)) {
+                value += constraint_coeff(c, t);
+            }
         }
         return value;
     }
 
     void local_search::verify_constraint(constraint const& c) const {
         unsigned value = constraint_value(c);
+        IF_VERBOSE(11, display(verbose_stream() << "verify ", c););
+        TRACE("sat", display(verbose_stream() << "verify ", c););
         if (c.m_k < value) {
-            IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c);
+            IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c) << "value: " << value << "\n";);
-                       verbose_stream() << "value: " << value << "\n";);
             UNREACHABLE();
         }
     }
@@ -252,7 +264,7 @@ namespace sat {
     // ~c <= k
     void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) {
         unsigned id = m_constraints.size();
-        m_constraints.push_back(constraint(k));
+        m_constraints.push_back(constraint(k, id));
         for (unsigned i = 0; i < sz; ++i) {
             m_vars.reserve(c[i].var() + 1);
             literal t(~c[i]);            
@@ -264,14 +276,15 @@ namespace sat {
         }
     }
 
+    // c * coeffs <= k
     void local_search::add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) {
         unsigned id = m_constraints.size();
-        m_constraints.push_back(constraint(k));
+        m_constraints.push_back(constraint(k, id));
         for (unsigned i = 0; i < sz; ++i) {
             m_vars.reserve(c[i].var() + 1);            
-            literal t(~c[i]);            
+            literal t(c[i]);            
             m_vars[t.var()].m_watch[is_pos(t)].push_back(pbcoeff(id, coeffs[i]));
-            m_constraints.back().push(t); // add coefficient to constraint?
+            m_constraints.back().push(t);
         }
         if (sz == 1 && k == 0) {
             m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100;
@@ -359,7 +372,7 @@ namespace sat {
                         
                         lits.reset();
                         coeffs.reset();
-                        for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]), coeffs.push_back(1);
+                        for (literal l : c) lits.push_back(~l), coeffs.push_back(1);
                         lits.push_back(c.lit()); coeffs.push_back(k);
                         add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);
                     }
@@ -889,21 +902,27 @@ namespace sat {
         }
     }
 
-    void local_search::display(std::ostream& out) const {
+    std::ostream& local_search::display(std::ostream& out) const {
         for (constraint const& c : m_constraints) {
             display(out, c);
         }        
         for (bool_var v = 0; v < num_vars(); ++v) {
             display(out, v, m_vars[v]);
         }
+        return out;
     }
     
-    void local_search::display(std::ostream& out, constraint const& c) const {
+    std::ostream& local_search::display(std::ostream& out, constraint const& c) const {
-        out << c.m_literals << " <= " << c.m_k << " lhs value: " << constraint_value(c) << "\n";
+        for (literal l : c) {
+            unsigned coeff = constraint_coeff(c, l);
+            if (coeff > 1) out << coeff << " * ";
+            out << l << " ";
+        }
+        return out << " <= " << c.m_k << " lhs value: " << constraint_value(c) << "\n";
     }
     
-    void local_search::display(std::ostream& out, unsigned v, var_info const& vi) const {
+    std::ostream& local_search::display(std::ostream& out, unsigned v, var_info const& vi) const {
-        out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n";
+        return out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n";
     }
 
     bool local_search::check_goodvar() {

src/sat/sat_local_search.h

@@ -99,11 +99,12 @@ namespace sat {
         };
 
         struct constraint {
+            unsigned        m_id;
             unsigned        m_k;
             int             m_slack;
             unsigned        m_size;
             literal_vector  m_literals;
-            constraint(unsigned k) : m_k(k), m_slack(0), m_size(0) {}
+            constraint(unsigned k, unsigned id) : m_id(id), m_k(k), m_slack(0), m_size(0) {}
             void push(literal l) { m_literals.push_back(l); ++m_size; }
             unsigned size() const { return m_size; }
             literal const& operator[](unsigned idx) const { return m_literals[idx]; }
@@ -232,6 +233,8 @@ namespace sat {
 
         unsigned constraint_value(constraint const& c) const;
 
+        unsigned constraint_coeff(constraint const& c, literal l) const;
+
         void print_info(std::ostream& out);
 
         void extract_model();
@@ -240,11 +243,11 @@ namespace sat {
 
         void add_clause(unsigned sz, literal const* c);
 
-        void display(std::ostream& out) const;
+        std::ostream& display(std::ostream& out) const;
 
-        void display(std::ostream& out, constraint const& c) const;
+        std::ostream& display(std::ostream& out, constraint const& c) const;
 
-        void display(std::ostream& out, unsigned v, var_info const& vi) const;
+        std::ostream& display(std::ostream& out, unsigned v, var_info const& vi) const;
 
     public:
 

src/sat/tactic/goal2sat.cpp

@@ -517,7 +517,10 @@ struct goal2sat::imp {
             mk_clause(~l1, ~l2, l);
             m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
             m_result_stack.push_back(sign ? ~l : l);
-            if (root) mk_clause(~l);
+            if (root) {
+                m_result_stack.reset();
+                mk_clause(~l);
+            }
         }
     }
 
@@ -586,7 +589,10 @@ struct goal2sat::imp {
             mk_clause(~l1, ~l2, l);
             m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
             m_result_stack.push_back(sign ? ~l : l);
-            if (root) mk_clause(~l);
+            if (root) {
+                mk_clause(~l);
+                m_result_stack.reset();
+            }
         }
     }
 
@@ -808,7 +814,7 @@ struct goal2sat::imp {
                 }                
                 f = m.mk_or(fmls.size(), fmls.c_ptr());
             }
-            TRACE("goal2sat", tout << mk_pp(f, m) << "\n";);
+            TRACE("goal2sat", tout << f << "\n";);
             process(f);
         skip_dep:
             ;

src/shell/opt_frontend.cpp

@@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "opt/opt_context.h"
 #include "ast/ast_util.h"
 #include "ast/arith_decl_plugin.h"
+#include "ast/ast_pp.h"
 #include "util/gparams.h"
 #include "util/timeout.h"
 #include "ast/reg_decl_plugins.h"
@@ -99,21 +100,20 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
         case l_false: std::cout << "unsat\n"; break;
         case l_undef: std::cout << "unknown\n"; break;
         }
-        DEBUG_CODE(
+        
-            if (false && r == l_true) {
+        if (r != l_false && gparams::get().get_bool("model_validate", false)) {
-                model_ref mdl;
+            model_ref mdl;
-                opt.get_model(mdl);
+            opt.get_model(mdl);
-                expr_ref_vector hard(m);
+            expr_ref_vector hard(m);
-                opt.get_hard_constraints(hard);
+            opt.get_hard_constraints(hard);
-                for (unsigned i = 0; i < hard.size(); ++i) {
+            for (expr* h : hard) {
-                    std::cout << "validate: " << i << "\n";
+                expr_ref tmp(m);
-                    expr_ref tmp(m);
+                VERIFY(mdl->eval(h, tmp));
-                    VERIFY(mdl->eval(hard[i].get(), tmp));
+                if (!m.is_true(tmp)) {
-                    if (!m.is_true(tmp)) {
+                    std::cout << mk_pp(h, m) << " " << tmp << "\n";
-                        std::cout << tmp << "\n";
-                    }
                 }
-            });
+            }
+        }
     }
     catch (z3_exception & ex) {
         std::cerr << ex.msg() << "\n";

src/tactic/arith/lia2card_tactic.cpp

@@ -213,7 +213,9 @@ public:
                 new_pr = m.mk_rewrite(g->form(i), new_curr);
                 new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
             }
+            // IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";);
             g->update(i, new_curr, new_pr, g->dep(i));
+
         }
         for (expr* a : axioms) {
             g->assert_expr(a);

src/tactic/generic_model_converter.cpp

@@ -53,21 +53,6 @@ void generic_model_converter::operator()(model_ref & md) {
             break;
         case instruction::ADD:
             ev(e.m_def, val);
-            if (e.m_f->get_name() == symbol("FOX-PIT-17")) {
-                IF_VERBOSE(0, verbose_stream() << e.m_f->get_name() << " " << e.m_def << " -> " << val << "\n";);
-                ptr_vector<expr> ts;
-                ts.push_back(e.m_def);
-                while (!ts.empty()) {
-                    app* t = to_app(ts.back());
-                    ts.pop_back();
-                    if (t->get_num_args() > 0) {
-                        ts.append(t->get_num_args(), t->get_args());
-                    }
-                    expr_ref tmp(m);
-                    ev(t, tmp);
-                    IF_VERBOSE(0, verbose_stream() << mk_pp(t, m) << " -> " << tmp << "\n";);                    
-                }
-            }
             TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
             arity = e.m_f->get_arity();
             reset_ev = false;