alternate

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

src/ast/sls/sat_ddfw.cpp

@@ -256,8 +256,9 @@ namespace sat {
         m_use_list_index.push_back(m_flat_use_list.size());
     }
 
-    void ddfw::flip(bool_var v) {
+    bool ddfw::flip(bool_var v) {
         ++m_flips;
+        bool new_unsat = false;
         literal lit = literal(v, !value(v));
         literal nlit = ~lit;
         SASSERT(is_true(lit));
@@ -273,6 +274,7 @@ namespace sat {
                     verbose_stream() << "flipping unit clause " << ci << "\n";
 #endif
                 m_unsat.insert_fresh(cls_idx);
+                new_unsat = true;
                 auto const& c = get_clause(cls_idx);
                 for (literal l : c) {
                     inc_reward(l, w);
@@ -314,6 +316,7 @@ namespace sat {
         }
         value(v) = !value(v);
         update_reward_avg(v);
+        return new_unsat;
     }
 
     bool ddfw::should_reinit_weights() {

src/ast/sls/sat_ddfw.h

@@ -252,7 +252,7 @@ namespace sat {
 
         void remove_assumptions();
 
-        void flip(bool_var v);
+        bool flip(bool_var v);
 
         inline double get_reward(bool_var v) const { return m_vars[v].m_reward; }
 

src/ast/sls/sls_context.h

@@ -65,7 +65,7 @@ namespace sls {
         virtual vector<sat::clause_info> const& clauses() const = 0;
         virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
         virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
-        virtual void flip(sat::bool_var v) = 0;
+        virtual bool flip(sat::bool_var v) = 0;
         virtual double reward(sat::bool_var v) = 0;
         virtual double get_weigth(unsigned clause_idx) = 0;
         virtual bool is_true(sat::literal lit) = 0;
@@ -167,7 +167,7 @@ namespace sls {
         sat::literal mk_literal(expr* e);
         void add_clause(expr* f);
         void add_clause(sat::literal_vector const& lits);
-        void flip(sat::bool_var v) { s.flip(v); }
+        bool flip(sat::bool_var v) { return s.flip(v); }
         double reward(sat::bool_var v) { return s.reward(v); }
         indexed_uint_set const& unsat() const { return s.unsat(); }
         unsigned rand() { return m_rand(); }

src/ast/sls/sls_euf_plugin.cpp

@@ -44,6 +44,7 @@ namespace sls {
     }
 
     void euf_plugin::start_propagation() {
+        m_incremental = !m_incremental;
         m_g = alloc(euf::egraph, m);
         std::function<void(std::ostream&, void*)> dj = [&](std::ostream& out, void* j) {
             out << "lit " << to_literal(reinterpret_cast<size_t*>(j));
@@ -111,16 +112,18 @@ namespace sls {
 
             if (ctx.is_unit(l))
                 continue;
-            lits.push_back(~l);
-            //verbose_stream() << "reward " << l << " " << ctx.reward(l.var()) << "\n";
-            
+            if (!lits.contains(~l))
+                lits.push_back(~l);
+
             if (ctx.reward(l.var()) > reward)
                 n = 0, reward = ctx.reward(l.var());
+
             if (ctx.rand(++n) == 0)
                 flit = l;
         }
-        //verbose_stream() << "conflict: " << lits << " flip " << flit << "\n";
+
         ctx.add_clause(lits);
+
         if (flit == sat::null_literal)
             return;
         do {
@@ -132,7 +135,7 @@ namespace sls {
         while (slit != flit);
         // flip the last literal on the replay stack
         IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
-        ctx.flip(flit.var());
+        ctx.flip(flit.var());        
         m_replay_stack.back().neg();
     }
 

src/ast/sls/sls_smt_solver.cpp

@@ -87,7 +87,7 @@ namespace sls {
         vector<sat::clause_info> const& clauses() const override { return m_ddfw.clauses(); }
         sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw.get_clause_info(idx); }
         ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
-        void flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false;  m_ddfw.flip(v); }
+        bool flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false;  return m_ddfw.flip(v); }
         double reward(sat::bool_var v) override { return m_ddfw.get_reward(v); }
         double get_weigth(unsigned clause_idx) override { return m_ddfw.get_clause_info(clause_idx).m_weight; }
         bool is_true(sat::literal lit) override { return m_ddfw.get_value(lit.var()) != lit.sign(); }

src/sat/smt/sls_solver.cpp

@@ -125,7 +125,7 @@ namespace sls {
         vector<sat::clause_info> const& clauses() const override { return m_ddfw->clauses(); }
         sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw->get_clause_info(idx); }
         ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw->use_list(lit); }
-        void flip(sat::bool_var v) override { m_ddfw->flip(v); }
+        bool flip(sat::bool_var v) override { return m_ddfw->flip(v); }
         double reward(sat::bool_var v) override { return m_ddfw->get_reward(v); }
         double get_weigth(unsigned clause_idx) override { return m_ddfw->get_clause_info(clause_idx).m_weight; }
         bool is_true(sat::literal lit) override { return m_ddfw->get_value(lit.var()) != lit.sign(); }