local updates

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

src/opt/pb_sls.cpp

@@ -20,49 +20,11 @@ Notes:
 #include "smt_literal.h"
 #include "ast_pp.h"
 #include "th_rewriter.h"
+#include "sat_sls.h"
 
 namespace smt {
     struct pb_sls::imp {
 
-        struct index_set {
-            unsigned_vector m_elems;
-            unsigned_vector m_index;
-            
-            unsigned num_elems() const { return m_elems.size(); }
-
-            void reset() { m_elems.reset(); m_index.reset(); }
-
-            bool empty() const { return m_elems.empty(); }
-
-            bool contains(unsigned idx) const {
-                return 
-                    (idx < m_index.size()) && 
-                    (m_index[idx] < m_elems.size()) && 
-                    (m_elems[m_index[idx]] == idx);
-            }
-
-            void insert(unsigned idx) {
-                m_index.reserve(idx+1);
-                if (!contains(idx)) {
-                    m_index[idx] = m_elems.size();
-                    m_elems.push_back(idx);
-                }
-            }
-
-            void remove(unsigned idx) {
-                if (!contains(idx)) return;
-                unsigned pos = m_index[idx];
-                m_elems[pos] = m_elems.back();
-                m_index[m_elems[pos]] = pos;
-                m_elems.pop_back();
-            }
-
-            unsigned choose(random_gen& rnd) const {
-                SASSERT(!empty());
-                return m_elems[rnd(num_elems())];
-            }
-        };
-
         struct clause {
             literal_vector    m_lits;
             scoped_mpz_vector m_weights;
@@ -112,8 +74,8 @@ namespace smt {
         expr_ref_vector  m_trail;
         obj_map<expr, unsigned> m_decl2var; // map declarations to Boolean variables.
         ptr_vector<expr> m_var2decl;        // reverse map
-        index_set        m_hard_false;           // list of hard clauses that are false.
+        sat::index_set        m_hard_false;           // list of hard clauses that are false.
-        index_set        m_soft_false;           // list of soft clauses that are false.
+        sat::index_set        m_soft_false;           // list of soft clauses that are false.
         unsigned         m_max_flips;            // maximal number of flips
         unsigned         m_non_greedy_percent;   // percent of moves to do non-greedy style
         random_gen       m_rng;

src/sat/sat_mus.cpp

@@ -36,6 +36,7 @@ namespace sat {
         m_core.append(m_mus);                
         s.m_core.reset();
         s.m_core.append(m_core);
+        m_model.reset();
     }
 
     lbool mus::operator()() {
@@ -47,10 +48,11 @@ namespace sat {
         literal_vector& mus = m_mus;
         core.append(s.get_core());
         
+
         while (!core.empty()) {
             TRACE("sat", 
                   tout << "core: " << core << "\n";
-                  tout << "mus:  " << mus << "\n";);
+                  tout << "mus:  " << mus  << "\n";);
 
             if (s.m_cancel) {
                 set_core();
@@ -76,7 +78,8 @@ namespace sat {
                 }
                 sz = core.size();
                 core.append(mus);
-                rmr();
+                measure_mr();
+                // rmr();
                 core.resize(sz);
                 break;
             }
@@ -97,10 +100,31 @@ namespace sat {
         }
         TRACE("sat", tout << "new core: " << mus << "\n";);
         set_core();
+<<<<<<< HEAD
         IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << core << ")\n";);
+=======
+        IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << m_core << ")\n";);
+>>>>>>> 180b0d4ec915c84b770bb609fae4e462118cde50
         return l_true;
     }
 
+    void mus::measure_mr() {
+        model const& m2 = s.get_model();
+        if (!m_model.empty()) {
+            unsigned n = 0;
+            for (unsigned i = 0; i < m_model.size(); ++i) {
+                if (m2[i] != m_model[i]) ++n;
+            }
+            std::cout << "model diff: " << n << " out of " << m_model.size() << "\n";
+        }
+        m_model.reset();
+        m_model.append(m2);        
+    }
+
+    // 
+    // TBD: eager model rotation allows rotating the same clause 
+    // several times with respect to different models.
+    // 
     void mus::rmr() {
         return;
 #if 0
@@ -148,16 +172,33 @@ namespace sat {
         watch_list const& wlist = s.get_wlist(lit);
         watch_list::const_iterator it  = wlist.begin();
         watch_list::const_iterator end = wlist.end();
-        for (; it != end; ++it) {
+        unsigned num_cand = 0;
+        for (; it != end && num_cand <= 1; ++it) {
             switch (it->get_kind()) {
             case watched::BINARY:
+                if (it->is_learned()) {
+                    break;
+                }
                 lit2 = it->get_literal();
+                if (value_at(lit2, model) == l_true) {
+                    break;
+                }
+                IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << ") ";);
                 TRACE("sat", tout << ~lit << " " << lit2 << "\n";);
+                ++num_cand;
                 break;
             case watched::TERNARY:
                 lit2 = it->get_literal1();
                 lit3 = it->get_literal2();
-                TRACE("sat", tout << ~lit << " " << lit2 << " " << lit3 << "\n";);
+                if (value_at(lit2, model) == l_true) {
+                    break;
+                }
+                if (value_at(lit3, model) == l_true) {
+                    break;
+                }
+
+                IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << " " << lit3 << ") ";);
+                ++num_cand;
                 break;
             case watched::CLAUSE: {
                 clause_offset cls_off = it->get_clause_offset();
@@ -165,15 +206,23 @@ namespace sat {
                 if (c.is_learned()) {
                     break;
                 }
+                ++num_cand;
+                IF_VERBOSE(1, verbose_stream() << c << " ";);
                 TRACE("sat", tout << c << "\n";);
                 break;
             }
             case watched::EXT_CONSTRAINT:
                 TRACE("sat", tout << "external constraint - should avoid rmr\n";);
-                m_toswap.resize(sz);
                 return;
             }
         }
+        if (num_cand > 1) {
+            m_toswap.resize(sz);
+        }
+        else {
+            IF_VERBOSE(1, verbose_stream() << "wlist size: " << num_cand << " " << m_core.size() << "\n";);
+        }
+
     }
 
 }

src/sat/sat_mus.h

@@ -24,6 +24,8 @@ namespace sat {
         literal_vector m_core;
         literal_vector m_mus;
         literal_vector m_toswap;        
+        model m_model;
+
         solver& s;
     public:
         mus(solver& s);
@@ -32,6 +34,7 @@ namespace sat {
     private:
         lbool mus2();
         void rmr();
+        void measure_mr();
         bool has_single_unsat(literal& assumption_lit);
         void find_swappable(literal lit);
         void reset();

src/sat/sat_sls.cpp

@@ -0,0 +1,96 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sat_sls.cpp
+
+Abstract:
+   
+    SLS for clauses in SAT solver
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2014-12-8
+
+Notes:
+
+--*/
+
+#include "sat_sls.h"
+
+namespace sat {
+
+    bool index_set::contains(unsigned idx) const {
+        return 
+            (idx < m_index.size()) && 
+            (m_index[idx] < m_elems.size()) && 
+            (m_elems[m_index[idx]] == idx);
+    }
+        
+    void index_set::insert(unsigned idx) {
+        m_index.reserve(idx+1);
+        if (!contains(idx)) {
+            m_index[idx] = m_elems.size();
+            m_elems.push_back(idx);
+        }
+    }
+        
+    void index_set::remove(unsigned idx) {
+        if (!contains(idx)) return;
+        unsigned pos = m_index[idx];
+        m_elems[pos] = m_elems.back();
+        m_index[m_elems[pos]] = pos;
+        m_elems.pop_back();
+    }
+        
+    unsigned index_set::choose(random_gen& rnd) const {
+        SASSERT(!empty());
+        return m_elems[rnd(num_elems())];
+    }
+
+    sls::sls(solver& s): s(s) {
+
+    }
+
+    sls::~sls() {
+        
+    }
+
+#if 0
+    bool_var sls::pick_flip() {
+        unsigned clause_idx = m_false.choose(m_rand);
+        clause const& c = m_clauses[clause_idx];
+        unsigned result =  UINT_MAX;
+        m_min_vars.reset();
+        for (unsigned i = 0; i < c.size(); ++i) {
+            
+        }
+    }
+
+    void sls::flip(bool_var v) {
+
+    }
+
+    bool sls::local_search() {
+        for (unsigned i = 0; !m_false.empty() && i < m_max_flips; ++i) {
+            flip(pick_flip());
+        }        
+        return m_false.empty();
+    }
+
+#endif
+
+    lbool sls::operator()() {
+#if 0
+        for (unsigned i = 0; i < m_max_tries; ++i) {
+            if (local_search()) {
+                return l_true;
+            }
+        }
+#endif
+        return l_undef;
+    }
+
+};
+

src/sat/sat_sls.h

@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sat_sls.h
+
+Abstract:
+   
+    SLS for clauses in SAT solver
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2014-12-8
+
+Notes:
+
+--*/
+#ifndef _SAT_SLS_H_
+#define _SAT_SLS_H_
+
+#include "util.h"
+#include "sat_simplifier.h"
+
+namespace sat {
+
+    class index_set {
+        unsigned_vector m_elems;
+        unsigned_vector m_index;        
+    public:
+        unsigned num_elems() const { return m_elems.size(); }        
+        void reset() { m_elems.reset(); m_index.reset(); }        
+        bool empty() const { return m_elems.empty(); }        
+        bool contains(unsigned idx) const;        
+        void insert(unsigned idx);        
+        void remove(unsigned idx);        
+        unsigned choose(random_gen& rnd) const;
+    };
+
+    class sls {
+        solver& s;
+        random_gen m_rand;
+        unsigned   m_max_tries;
+        unsigned   m_max_flips;
+        index_set  m_false;
+        use_list   m_use_list;
+        vector<clause> m_clauses;
+    public:
+        sls(solver& s);
+        ~sls();        
+        lbool operator()();
+    private:
+        bool local_search();
+        bool_var pick_flip();
+        void flip(bool_var v);
+    };
+
+};
+
+#endif

src/sat/sat_solver.cpp

@@ -48,6 +48,8 @@ namespace sat {
         m_scope_lvl(0),
         m_params(p) {
         m_config.updt_params(p);
+        m_conflicts_since_gc      = 0;
+        m_next_simplify           = 0;
     }
 
     solver::~solver() {
@@ -924,10 +926,8 @@ namespace sat {
         m_conflicts_since_restart = 0;
         m_restart_threshold       = m_config.m_restart_initial;
         m_luby_idx                = 1;
-        m_conflicts_since_gc      = 0;
         m_gc_threshold            = m_config.m_gc_initial;
         m_min_d_tk                = 1.0;
-        m_next_simplify           = 0;
         m_stopwatch.reset();
         m_stopwatch.start();
         m_core.reset();
@@ -1667,6 +1667,10 @@ namespace sat {
         }        
         reset_unmark(old_size);
         if (m_config.m_minimize_core) {
+            // TBD: 
+            // apply optional clause minimization by detecting subsumed literals.
+            // initial experiment suggests it has no effect.
+
             m_mus(); // ignore return value on cancelation.
         }
     }

src/shell/dimacs_frontend.cpp

@@ -101,7 +101,7 @@ static void track_clauses(sat::solver const& src,
     sat::clause * const * end = src.end_clauses();
     svector<sat::solver::bin_clause> bin_clauses;
     src.collect_bin_clauses(bin_clauses, false);
-    tracking_clauses.reserve(2*src.num_vars() + (end - it) + bin_clauses.size());
+    tracking_clauses.reserve(2*src.num_vars() + static_cast<unsigned>(end - it) + bin_clauses.size());
 
     for (sat::bool_var v = 1; v < src.num_vars(); ++v) {
         if (src.value(v) != l_undef) {
@@ -114,7 +114,7 @@ static void track_clauses(sat::solver const& src,
     for (; it != end; ++it) {
         lits.reset();
         sat::clause& cls = *(*it);
-        lits.append(cls.end()-cls.begin(), cls.begin());
+        lits.append(static_cast<unsigned>(cls.end()-cls.begin()), cls.begin());
         track_clause(dst, lits, assumptions, tracking_clauses);
     }
     for (unsigned i = 0; i < bin_clauses.size(); ++i) {

src/tactic/arith/card2bv_tactic.cpp

@@ -22,6 +22,7 @@ Notes:
 #include"ast_smt2_pp.h"
 #include"expr_substitution.h"
 #include"card2bv_tactic.h"
+#include"pb_rewriter.h"
 
 namespace pb {
     unsigned card2bv_rewriter::get_num_bits(func_decl* f) {
@@ -58,43 +59,8 @@ namespace pb {
             return BR_DONE;
         }
         else if (f->get_family_id() == pb.get_family_id()) {
-            expr_ref zero(m), a(m), b(m);
+            // return mk_shannon(f, sz, args, result);
-            expr_ref_vector es(m);
+            return mk_bv(f, sz, args, result);
-            unsigned bw = get_num_bits(f);
-            zero = bv.mk_numeral(rational(0), bw);
-            for (unsigned i = 0; i < sz; ++i) {
-                es.push_back(m.mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero));
-            }
-            switch (es.size()) {
-            case 0:  a = zero; break;
-            case 1:  a = es[0].get(); break;
-            default:
-                a = es[0].get();
-                for (unsigned i = 1; i < es.size(); ++i) {
-                    a = bv.mk_bv_add(a, es[i].get());
-                }
-                break;
-            }
-            b = bv.mk_numeral(pb.get_k(f), bw);
-            
-            switch (f->get_decl_kind()) {
-            case OP_AT_MOST_K:
-            case OP_PB_LE:
-                UNREACHABLE();
-                result = bv.mk_ule(a, b);
-                return BR_DONE;
-            case OP_AT_LEAST_K:
-                UNREACHABLE();
-            case OP_PB_GE:
-                result = bv.mk_ule(b, a);
-                return BR_DONE;
-            case OP_PB_EQ:
-                result = m.mk_eq(a, b);
-                return BR_DONE;
-            default:
-                UNREACHABLE();
-            }
-            return BR_FAILED;
         }
         // NSB: review
         // we should remove this code and rely on a layer above to deal with 
@@ -136,6 +102,62 @@ namespace pb {
             return BR_FAILED;
     }
 
+
+    br_status card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+        expr_ref zero(m), a(m), b(m);
+        expr_ref_vector es(m);
+        unsigned bw = get_num_bits(f);
+        zero = bv.mk_numeral(rational(0), bw);
+        for (unsigned i = 0; i < sz; ++i) {
+            es.push_back(m.mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero));
+        }
+        switch (es.size()) {
+        case 0:  a = zero; break;
+        case 1:  a = es[0].get(); break;
+        default:
+            a = es[0].get();
+            for (unsigned i = 1; i < es.size(); ++i) {
+                a = bv.mk_bv_add(a, es[i].get());
+            }
+            break;
+        }
+        b = bv.mk_numeral(pb.get_k(f), bw);
+        
+        switch (f->get_decl_kind()) {
+        case OP_AT_MOST_K:
+        case OP_PB_LE:
+            UNREACHABLE();
+            result = bv.mk_ule(a, b);
+            break;
+        case OP_AT_LEAST_K:
+            UNREACHABLE();
+        case OP_PB_GE:
+            result = bv.mk_ule(b, a);
+            break;
+        case OP_PB_EQ:
+            result = m.mk_eq(a, b);
+            break;
+        default:
+            UNREACHABLE();
+        }
+        return BR_DONE;
+    }
+
+    br_status card2bv_rewriter::mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+        pb_rewriter rw(m);
+        if (sz == 0) {
+            rw.mk_app_core(f, sz, args, result);
+            return BR_DONE;
+        }
+        expr_ref r1(m), r2(m);
+        ptr_vector<expr> new_args(sz, args);
+        new_args[0] = m.mk_true();
+        rw.mk_app_core(f, sz, new_args.c_ptr(), r1);
+        new_args[0] = m.mk_false();
+        rw.mk_app_core(f, sz, new_args.c_ptr(), r2);
+        result = m.mk_ite(args[0], r1, r2);
+        return BR_REWRITE_FULL;        
+    }
 };
 
 template class rewriter_tpl<pb::card2bv_rewriter_cfg>;

src/tactic/arith/card2bv_tactic.h

@@ -35,6 +35,8 @@ namespace pb {
         pb_util      pb;
         bv_util      bv;
         unsigned get_num_bits(func_decl* f);
+        br_status mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
+        br_status mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
     public:
         card2bv_rewriter(ast_manager& m);
         br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);

src/test/hilbert_basis.cpp

@@ -540,6 +540,33 @@ static void tst19() {
     saturate_basis(hb);    
 }
 
+static void test_A_5_5_3() {
+    hilbert_basis hb;
+    for (unsigned i = 0; i < 15; ++i) {
+        vector<rational> v;
+        for (unsigned j = 0; j < 5; ++j) {
+            for (unsigned k = 0; k < 15; ++k) {
+                v.push_back(rational(k == i));                
+            }
+        }
+        hb.add_ge(v, R(0));
+    }
+    for (unsigned i = 1; i <= 15; ++i) {
+        vector<rational> v;
+        for (unsigned k = 1; k <= 5; ++k) {
+            for (unsigned l = 1; l <= 5; ++l) {
+                for (unsigned j = 1; j <= 3; ++j) {
+                    bool one = ((j*k <= i) && (((i - j) % 3) == 0); // fixme
+                    v.push_back(rational(one));
+                }
+            }
+        }
+        hb.add_ge(v, R(0));
+    }
+    // etc.
+    saturate_basis(hb);
+}
+
 void tst_hilbert_basis() {
     std::cout << "hilbert basis test\n";
 //    tst3();
@@ -547,6 +574,9 @@ void tst_hilbert_basis() {
 
     g_use_ordered_support = true;
 
+    test_A_5_5_3();
+    return;
+
     tst18();
     return;