allow for alternating

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

src/ast/sls/sat_ddfw.cpp

@@ -564,6 +564,7 @@ namespace sat {
             double w = calculate_transfer_weight(cn.m_weight);
             transfer_weight(from_idx, to_idx, w);
         }
+        //verbose_stream() << m_shifts << " " << m_flips << " " << shifted << "\n";
         if (!shifted)
             m_reinit_next = m_flips;
         // DEBUG_CODE(invariant(););

src/ast/sls/sat_ddfw.h

@@ -88,7 +88,6 @@ namespace sat {
         svector<double>      m_scores;      // reward -> score
         svector<lbool>       m_model;       // var -> best assignment
         unsigned             m_init_weight = 2; 
-        
         vector<unsigned_vector> m_use_list;
         unsigned_vector  m_flat_use_list;
         unsigned_vector  m_use_list_index;
@@ -96,6 +95,7 @@ namespace sat {
         indexed_uint_set m_unsat;
         indexed_uint_set m_unsat_vars;  // set of variables that are in unsat clauses
         random_gen       m_rand;
+        uint64_t         m_last_flips_for_shift = 0;
         unsigned         m_num_non_binary_clauses = 0;
         unsigned         m_restart_count = 0, m_reinit_count = 0;
         uint64_t         m_restart_next = 0, m_reinit_next = 0;

src/ast/sls/sls_euf_plugin.cpp

@@ -39,11 +39,13 @@ namespace sls {
 
     void euf_plugin::initialize() {
         sls_params sp(ctx.get_params());
-        m_incremental = sp.euf_incremental();
+        m_incremental_mode = sp.euf_incremental();
+        m_incremental = 1 == m_incremental_mode;
         IF_VERBOSE(2, verbose_stream() << "sls.euf: incremental " << m_incremental << "\n");
     }
 
     void euf_plugin::start_propagation() {
+        if (m_incremental_mode == 2)
             m_incremental = !m_incremental;
         m_g = alloc(euf::egraph, m);
         std::function<void(std::ostream&, void*)> dj = [&](std::ostream& out, void* j) {
@@ -100,6 +102,7 @@ namespace sls {
         g.explain<size_t>(explain, nullptr);
         g.end_explain();
         double reward = -1;
+        bool has_flipped = false;
         TRACE("enf",
             for (auto p : explain) {
                 sat::literal l = to_literal(p);
@@ -115,6 +118,7 @@ namespace sls {
             if (!lits.contains(~l))
                 lits.push_back(~l);
 
+
             if (ctx.reward(l.var()) > reward)
                 n = 0, reward = ctx.reward(l.var());
 
@@ -122,7 +126,6 @@ namespace sls {
                 flit = l;
         }
 
-        ctx.add_clause(lits);
 
         if (flit == sat::null_literal)
             return;
@@ -167,8 +170,6 @@ namespace sls {
                 g.new_diseq(g.find(e), to_ptr(lit));
             else 
                 g.merge(g.find(x), g.find(y), to_ptr(lit));                      
-            
-            // g.merge(g.find(e), g.find(!lit.sign()), to_ptr(lit));
         }
         else if (!lit.sign() && m.is_distinct(e)) {
             auto n = to_app(e)->get_num_args();

src/ast/sls/sls_euf_plugin.h

@@ -43,6 +43,7 @@ namespace sls {
 
 
         bool m_incremental = false;
+        unsigned m_incremental_mode = 0;
         stats m_stats;
 
         scoped_ptr<euf::egraph> m_g;

src/params/sls_params.pyg

@@ -22,7 +22,7 @@ def_module_params('sls',
                         ('early_prune', BOOL, 1, 'use early pruning for score prediction'),
                         ('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
                         ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
-                        ('euf_incremental', BOOL, False, 'use incremental EUF resolver'), 
+                        ('euf_incremental', UINT, 0, '0 non-incremental, 1 incremental, 2 alternating EUF resolver'), 
                         ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
                         ('random_seed', UINT, 0, 'random seed')
               ))