Current version for relocating.

src/tactic/sls/sls_evaluator.h

@@ -78,7 +78,11 @@ public:
             case OP_AND: {
                 m_mpz_manager.set(result, m_one);
                 for (unsigned i = 0; i < n_args; i++)
+#if _DIRTY_UP_
+                    if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) && !m_tracker.is_top_expr(args[i]))  {
+#else
                     if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result))  {
+#endif
                         m_mpz_manager.set(result, m_zero);
                         break;
                     }
@@ -86,7 +90,11 @@ public:
             }
             case OP_OR: {
                 for (unsigned i = 0; i < n_args; i++)
+#if _DIRTY_UP_
+                    if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) || m_tracker.is_top_expr(args[i]))  {
+#else
                     if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
+#endif
                         m_mpz_manager.set(result, m_one);
                         break;
                     }
@@ -94,9 +102,16 @@ public:
             }
             case OP_NOT: {
                 SASSERT(n_args == 1);
+#if _DIRTY_UP_
+                if (m_tracker.is_top_expr(args[0]))
+                    m_mpz_manager.set(result, m_zero);
+                else
+                    m_mpz_manager.set(result, (m_mpz_manager.is_zero(m_tracker.get_value(args[0]))) ? m_one : m_zero);
+#else
                 const mpz & child = m_tracker.get_value(args[0]);
                 SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child));                
                 m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero);
+#endif
                 break;
             }
             case OP_EQ: {
@@ -542,7 +557,8 @@ public:
                 m_tracker.set_value(cur, new_value);
 
 #if _REAL_RS_ || _REAL_PBFS_
-                if (!m_tracker.has_uplinks(cur))
+                //if (!m_tracker.has_uplinks(cur))
+                if (m_tracker.is_top_expr(cur))
                 {
                     if (m_mpz_manager.eq(new_value,m_one))
                         m_tracker.make_assertion(cur);
@@ -554,7 +570,8 @@ public:
 #if _EARLY_PRUNE_
                 new_score = m_tracker.score(cur);
 #if _CACHE_TOP_SCORE_
-                if (!m_tracker.has_uplinks(cur))
+                //if (!m_tracker.has_uplinks(cur))
+                if (m_tracker.is_top_expr(cur))
                     m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
 #endif
                 m_tracker.set_score(cur, new_score);
@@ -562,7 +579,8 @@ public:
 #else
 #if _CACHE_TOP_SCORE_
                 new_score = m_tracker.score(cur);
-                if (!m_tracker.has_uplinks(cur))
+                //if (!m_tracker.has_uplinks(cur))
+                if (m_tracker.is_top_expr(cur))
                     m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
                 m_tracker.set_score(cur, new_score);
 #else
@@ -611,7 +629,8 @@ public:
 #if _EARLY_PRUNE_
                 new_score = m_tracker.score(cur);
 #if _CACHE_TOP_SCORE_
-                if (!m_tracker.has_uplinks(cur))
+                //if (!m_tracker.has_uplinks(cur))
+                if (m_tracker.is_top_expr(cur))
                     m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
 #endif
                 m_tracker.set_score(cur, new_score);
@@ -619,7 +638,8 @@ public:
 #else
 #if _CACHE_TOP_SCORE_
                 new_score = m_tracker.score(cur);
-                if (!m_tracker.has_uplinks(cur))
+                //if (!m_tracker.has_uplinks(cur))
+                if (m_tracker.is_top_expr(cur))
                     m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
                 m_tracker.set_score(cur, new_score);
 #else
@@ -704,7 +724,8 @@ public:
 
             new_score = m_tracker.score(cur); 
 #if _CACHE_TOP_SCORE_
-            if (!m_tracker.has_uplinks(cur))
+            //if (!m_tracker.has_uplinks(cur))
+            if (m_tracker.is_top_expr(cur))
                 m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
 #endif
             prune_score = m_tracker.get_score_prune(cur);
@@ -745,7 +766,8 @@ public:
 
 #if _CACHE_TOP_SCORE_
                     new_score = m_tracker.score(cur); 
-                    if (!m_tracker.has_uplinks(cur))
+                    //if (!m_tracker.has_uplinks(cur))
+                    if (m_tracker.is_top_expr(cur))
                         m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
                     m_tracker.set_score(cur, new_score);
 #else
@@ -833,44 +855,7 @@ public:
     }
 #endif
 
-    void randomize_local(expr * e, unsigned int flip) {
+    void randomize_local(ptr_vector<func_decl> & unsat_constants) {
-        ptr_vector<func_decl> & unsat_constants = m_tracker.get_constants(e);
-
-        // Randomize _one_ candidate:
-        unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size();
-        func_decl * fd = unsat_constants[r];
-#if _PERC_CHANGE_
-        sort * srt = fd->get_range();
-        mpz temp;
-
-        if (m_manager.is_bool(srt))
-            m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
-        else
-        {
-            mpz temp2, mask;
-            unsigned bv_sz = m_bv_util.get_bv_size(srt);
-            m_mpz_manager.set(temp, m_tracker.get_value(fd));
-
-            for (unsigned bit = 0; bit < bv_sz; bit++)
-                if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_)
-                {
-                    m_mpz_manager.set(mask, m_powers(bit));
-                    m_mpz_manager.bitwise_xor(temp, mask, temp2);
-                    m_mpz_manager.set(temp, temp2);
-                }
-            m_mpz_manager.del(mask);
-            m_mpz_manager.del(temp2);
-        }
-#else
-        mpz temp = m_tracker.get_random(fd->get_range());
-#endif
-        update(fd, temp);
-        m_mpz_manager.del(temp);
-    } 
-
-     void randomize_local(goal_ref const & g, unsigned int flip) {
-        ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g, flip);
-
         // Randomize _all_ candidates:
 
         //// bool did_something = false;
@@ -927,6 +912,15 @@ public:
                         tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;
                         tout << "Locally randomized model: " << std::endl; 
                         m_tracker.show_model(tout); );
+
+    }
+
+    void randomize_local(expr * e) {
+        randomize_local(m_tracker.get_constants(e));
+    } 
+
+     void randomize_local(goal_ref const & g, unsigned int flip) {
+        randomize_local(m_tracker.get_unsat_constants(g, flip));
     } 
 };
 

src/tactic/sls/sls_tactic.cpp

@@ -34,6 +34,8 @@ Notes:
 #include"propagate_values_tactic.h"
 #include"sls_tactic.h"
 #include"nnf_tactic.h"
+#include"luby.h"
+#include "ctx_simplify_tactic.h"
 
 // which unsatisfied assertion is selected? only works with _FOCUS_ > 0
 // 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score
@@ -43,9 +45,23 @@ Notes:
 // 0 = all terms (GSAT), 1 = only one top level assertion (WSAT), 2 = only one bottom level atom
 #define _FOCUS_ 1
 
+// probability of choosing the same assertion again in the next step
+#define _PERC_STICKY_ 0
+
+// do we use dirty unit propagation to get rid of nested top level assertions?
+#define _DIRTY_UP_ 0
+
 // do we use restarts?
-// 0 = no, otherwise the value defines the maximum number of moves
+// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time
-#define _RESTARTS_ 0
+#define _RESTARTS_ 3
+// limit of moves/plateaus/seconds until first restart occurs
+#define _RESTART_LIMIT_ 10
+// 0 = initialize with all zero, 1 initialize with random value
+#define _RESTART_INIT_ 0
+// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid
+#define _RESTART_SCHEME_ 1
+// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3
+#define _RESTART_CONST_ARMIN_ 3.0
 
 // timelimit
 #define _TIMELIMIT_ 3600
@@ -66,38 +82,58 @@ Notes:
 // 2 = yes, by squaring it
 // 3 = yes, by setting it to zero
 // 4 = by progessively increasing weight (_TIMELIMIT_ needs to be set appropriately!)
-#define _WEIGHT_DIST_ 0
+#define _WEIGHT_DIST_ 1
 
 // the factor used for _WEIGHT_DIST_ = 1
 #define _WEIGHT_DIST_FACTOR_ 0.25
 
+// shall we toggle the weight after each restart?
+#define _WEIGHT_TOGGLE_ 0
+
 // do we use intensification steps in local minima? if so, how many?
 #define _INTENSIFICATION_ 0
 #define _INTENSIFICATION_TRIES_ 0
 
+// what is the percentage of random moves in plateaus (instead of full randomization)?
+#define _PERC_PLATEAU_MOVES_ 0
+
+// shall we repick clause when randomizing in a plateau or use the current one?
+#define _REPICK_ 1
+
 // do we use some UCT-like scheme for assertion-selection? overrides _BFS_
-#define _UCT_ 0
+#define _UCT_ 1
 
 // how much diversification is used in the UCT-scheme?
-#define _UCT_CONSTANT_ 0.01
+#define _UCT_CONSTANT_ 10.0
 
 // is uct clause selection probabilistic similar to variable selection in sparrow?
+// 0 = no, 1 = yes, use uct-value, 2 = yes, use score-value (_UCT_CONSTANT_ = 0.0) with squared score
 #define _PROBABILISTIC_UCT_ 0
 
+// additive constants for probabilistic uct > 0
+#define _UCT_EPS_ 0.0001
+
+// shall we reset _UCT_ touched values after restart?
+#define _UCT_RESET_ 0
+
+// how shall we initialize the _UCT_ total touched counter?
+// 0 = initialize with one, 1 = initialize with number of assertions
+#define _UCT_INIT_ 1
+
 // shall we use addition/subtraction?
 #define _USE_ADDSUB_ 1
 
 // shall we try multilication and division by 2?
-#define _USE_MUL2DIV2_ 1
+#define _USE_MUL2DIV2_ 0
 
 // shall we try multiplication by 3?
-#define _USE_MUL3_ 1
+#define _USE_MUL3_ 0
 
 // shall we try unary minus (= inverting and incrementing)
-#define _USE_UNARY_MINUS_ 1
+#define _USE_UNARY_MINUS_ 0
 
 // is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0
-#define _UNIFORM_RANDOM_ 1
+#define _UNIFORM_RANDOM_ 0
 
 // should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
 #define _REAL_RS_ 0
@@ -124,13 +160,21 @@ Notes:
 #define _CACHE_TOP_SCORE_ 1
 
 
-#if ((_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1) || _BFS_ && (_UCT_ ||_UNIFORM_RANDOM_ ||_REAL_RS_ ||_REAL_PBFS_)
+#if ((_BFS_ > 0) + (_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1)
     InvalidConfiguration;
 #endif
 #if (_PROBABILISTIC_UCT_ && !_UCT_)
     InvalidConfiguration;
 #endif
-
+#if (_PERM_RSTEP_ && !_TYPE_RSTEP_)
+    InvalidConfiguration;
+#endif
+#if (_PERC_CHANGE_ == 50)
+    InvalidConfiguration;
+#endif
+#if (_PERC_STICKY_ && !_FOCUS_)
+    InvalidConfiguration;
+#endif
 
 #include"sls_params.hpp"
 #include"sls_evaluator.h"
@@ -180,6 +224,7 @@ class sls_tactic : public tactic {
         sls_tracker     m_tracker;
         sls_evaluator   m_evaluator;
 
+        unsigned		m_restart_limit;
         unsigned        m_max_restarts;
         unsigned        m_plateau_limit;
 
@@ -208,6 +253,41 @@ class sls_tactic : public tactic {
             m_mpz_manager.del(m_two);
         }        
 
+        double get_restart_armin(unsigned cnt_restarts)
+        {
+            unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts));
+            unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2;
+            //printf("armin: %f\n", pow(1.1, inner_id + 1));
+            return pow(_RESTART_CONST_ARMIN_, inner_id + 1);
+        }
+
+        inline unsigned check_restart(unsigned curr_value)
+        {
+            if (curr_value > m_restart_limit)
+            {
+#if _RESTART_SCHEME_ == 4
+                m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1);
+#elif _RESTART_SCHEME_ == 3
+                m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_;
+#elif _RESTART_SCHEME_ == 2
+                m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_;
+#elif _RESTART_SCHEME_ == 1
+                if (m_stats.m_restarts & 1)
+                    m_restart_limit += _RESTART_LIMIT_;
+                else
+                    m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_;
+#else
+                    m_restart_limit += _RESTART_LIMIT_;
+#endif
+#if _WEIGHT_TOGGLE_
+                    printf("Setting weight: %f\n", _WEIGHT_DIST_FACTOR_ * (((m_stats.m_restarts & 2) == 0) + 1));
+                m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_ * (((m_stats.m_restarts & 2) == 0) + 1));
+#endif
+                return 0;
+            }
+            return 1;
+        }
+
         ast_manager & m() const { return m_manager; }
 
         void set_cancel(bool f) { m_cancel = f; }
@@ -435,12 +515,10 @@ class sls_tactic : public tactic {
                 NOT_IMPLEMENTED_YET();
         }
 
-        void mk_random_move(goal_ref const & g) {
+        void mk_random_move(ptr_vector<func_decl> & unsat_constants)
+        {
             unsigned rnd_mv = 0;
-            if (m_stats.m_moves > 10000)
-                rnd_mv = 0;
 
-            ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g, m_stats.m_moves);                
             unsigned ucc = unsat_constants.size(); 
             unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc;
             func_decl * fd = unsat_constants[rc];
@@ -503,6 +581,10 @@ class sls_tactic : public tactic {
             m_mpz_manager.del(new_value);
         }
 
+        void mk_random_move(goal_ref const & g) {
+            mk_random_move(m_tracker.get_unsat_constants(g, m_stats.m_moves));                
+        }
+
         // will use VNS to ignore some possible moves and increase the flips per second
         double find_best_move_vns(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score, 
                               unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) {
@@ -875,6 +957,130 @@ class sls_tactic : public tactic {
             unsigned new_const = (unsigned)-1, new_bit = 0;        
             mpz new_value;
             move_type move;
+            unsigned plateau_cnt = 0;
+
+            score = rescore(g);
+            unsigned sz = g->size();
+#if _PERC_STICKY_
+            expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);    
+#endif
+
+#if _RESTARTS_ == 1
+            while (check_restart(m_stats.m_moves) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
+#elif _RESTARTS_ == 2
+            while (check_restart(plateau_cnt) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
+#elif _RESTARTS_ == 3
+            while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
+#else
+            while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
+#endif
+                checkpoint();
+                m_stats.m_moves++;
+
+#if _REAL_RS_ || _REAL_PBFS_
+                //m_tracker.debug_real(g, m_stats.m_moves);
+#endif
+
+#if _FOCUS_
+#if _PERC_STICKY_
+                if (m_tracker.get_random_uint(16) % 100 >= _PERC_STICKY_ || m_mpz_manager.eq(m_tracker.get_value(e), m_one))
+                e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);    
+#else
+                expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);    
+#endif
+                if (!e)
+                {
+                    res = l_true;
+                    goto bailout;
+                }
+                ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants_walksat(e);
+#else
+                ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants_gsat(g, sz);
+                if (!to_evaluate.size())
+                {
+                    res = l_true;
+                    goto bailout;
+                }
+#endif
+
+#if _TYPE_RSTEP_
+                if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_)
+                {
+#if _TYPE_RSTEP_ == 1
+                    m_evaluator.randomize_local(to_evaluate);
+#elif _TYPE_RSTEP_ == 2
+                    mk_random_move(to_evaluate);
+#endif
+#if _CACHE_TOP_SCORE_
+                    score = m_tracker.get_top_sum() / g->size();
+#else
+                    score = top_score(g);
+#endif
+                }
+                continue;
+#endif
+
+#if _WEIGHT_DIST_ == 4
+                m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
+#endif       
+                old_score = score;
+                new_const = (unsigned)-1;
+
+#if _VNS_
+                score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move);
+#else
+                score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move);
+#endif
+
+                if (new_const == static_cast<unsigned>(-1)) {
+                    score = old_score;
+                    plateau_cnt++;
+#if _INTENSIFICATION_
+                    handle_plateau(g, score);
+                    //handle_plateau(g);
+                    //e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);    
+                    //to_evaluate = m_tracker.get_unsat_constants_walksat(e);
+#else
+#if _PERC_PLATEAU_MOVES_
+                    if (m_tracker.get_random_uint(8) % 100 < _PERC_PLATEAU_MOVES_)
+                        mk_random_move(to_evaluate);
+                    else
+#endif
+#if _REPICK_
+                    m_evaluator.randomize_local(g, m_stats.m_moves);
+#else
+                    m_evaluator.randomize_local(to_evaluate);
+#endif
+#endif
+
+#if _CACHE_TOP_SCORE_
+                    score = m_tracker.get_top_sum() / g->size();
+#else
+                    score = top_score(g);
+#endif
+                } else {
+                    func_decl * fd = to_evaluate[new_const];              
+#if _REAL_RS_ || _REAL_PBFS_
+                    score = serious_score(g, fd, new_value);
+#else
+                    score = incremental_score(g, fd, new_value);    
+#endif
+                }
+            }
+
+            bailout:
+            m_mpz_manager.del(new_value);
+
+            return res;
+        }    
+
+        // main search loop
+        lbool search_old(goal_ref const & g) {        
+            lbool res = l_undef;
+            double score = 0.0, old_score = 0.0;
+            unsigned new_const = (unsigned)-1, new_bit = 0;        
+            mpz new_value;
+            move_type move;
             
             score = rescore(g);
             TRACE("sls", tout << "Starting search, initial score   = " << std::setprecision(32) << score << std::endl;
@@ -887,12 +1093,12 @@ class sls_tactic : public tactic {
 
             // Andreas: Why do we only allow so few plateaus?
 #if _RESTARTS_
-            while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
+            while (m_stats.m_stopwatch.get_current_seconds() < 200 * (m_stats.m_restarts + 1) * 0.2) {
+            //while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
 #else
             while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && (_RESTARTS_ == 0 || m_stats.m_moves < _RESTARTS_)) {                
 #endif
                 do {
-                    if (m_stats.m_moves == 5590)
                     checkpoint();
 
 #if _WEIGHT_DIST_ == 4
@@ -1072,7 +1278,11 @@ class sls_tactic : public tactic {
 
             verbose_stream() << "_BFS_ " << _BFS_ << std::endl;
             verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl;
+            verbose_stream() << "_PERC_STICKY_ " << _PERC_STICKY_ << std::endl;
             verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << std::endl;
+            verbose_stream() << "_RESTART_LIMIT_ " << _RESTART_LIMIT_ << std::endl;
+            verbose_stream() << "_RESTART_INIT_ " << _RESTART_INIT_ << std::endl;
+            verbose_stream() << "_RESTART_SCHEME_ " << _RESTART_SCHEME_ << std::endl;
             verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl;
             verbose_stream() << "_SCORE_AND_AVG_ " << _SCORE_AND_AVG_ << std::endl;
             verbose_stream() << "_SCORE_OR_MUL_ " << _SCORE_OR_MUL_ << std::endl;
@@ -1081,9 +1291,14 @@ class sls_tactic : public tactic {
             verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl;
             verbose_stream() << "_INTENSIFICATION_ " << _INTENSIFICATION_ << std::endl;
             verbose_stream() << "_INTENSIFICATION_TRIES_ " << _INTENSIFICATION_TRIES_ << std::endl;
+            verbose_stream() << "_PERC_PLATEAU_MOVES_ " << _PERC_PLATEAU_MOVES_ << std::endl;
+            verbose_stream() << "_REPICK_ " << _REPICK_ << std::endl;
             verbose_stream() << "_UCT_ " << _UCT_ << std::endl;
             verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl;
+            verbose_stream() << "_UCT_RESET_ " << _UCT_RESET_ << std::endl;
+            verbose_stream() << "_UCT_INIT_ " << _UCT_INIT_ << std::endl;
             verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl;
+            verbose_stream() << "_UCT_EPS_ " << std::fixed << std::setprecision(4) << _UCT_EPS_ << std::endl;
             verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl;
             verbose_stream() << "_USE_MUL2DIV2_ " << _USE_MUL2DIV2_ << std::endl;
             verbose_stream() << "_USE_MUL3_ " << _USE_MUL3_ << std::endl;
@@ -1100,20 +1315,29 @@ class sls_tactic : public tactic {
             
 #if _WEIGHT_DIST_ == 4
             m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
+#endif
+#if _WEIGHT_TOGGLE_
+            m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_);
 #endif
             m_tracker.initialize(g);
             lbool res = l_undef;
         
+            m_restart_limit = _RESTART_LIMIT_;
+
             do {
                 checkpoint();
-                // Andreas: I think restarts are too impotant to ignore 99% of them are happening...
-                //if ((m_stats.m_restarts % 100) == 0)                        
-                    report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
 
+                report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
                 res = search(g);
 
                 if (res == l_undef)
-                    m_tracker.randomize();
+                {
+#if _RESTART_INIT_
+                    m_tracker.randomize(g);
+#else
+                    m_tracker.reset(g);
+#endif
+                }
             }
             while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts);
         
@@ -1121,6 +1345,13 @@ class sls_tactic : public tactic {
 
             if (res == l_true) {    
                 report_tactic_progress("Number of flips:", m_stats.m_moves);
+                for (unsigned i = 0; i < g->size(); i++)
+                    if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
+                    {
+                        verbose_stream() << "Terminated before all assertions were SAT!" << std::endl;
+                        NOT_IMPLEMENTED_YET(); 
+                    }
+
                 if (m_produce_models) {
                     model_ref mdl = m_tracker.get_model();
                     mc = model2model_converter(mdl.get());
@@ -1183,12 +1414,17 @@ public:
     }
 
     virtual void cleanup() {        
-        imp * d = alloc(imp, m, m_params, m_stats);
+        imp * d = m_imp;
         #pragma omp critical (tactic_cancel)
         {
-            std::swap(d, m_imp);
+            d = m_imp;
         }
         dealloc(d);
+        d = alloc(imp, m, m_params, m_stats);
+        #pragma omp critical (tactic_cancel) 
+        {
+            m_imp = d;
+        }
     }
     
     virtual void collect_statistics(statistics & st) const {
@@ -1246,6 +1482,9 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
     // conservative gaussian elimination. 
     gaussian_p.set_uint("gaussian_max_occs", 2); 
 
+    params_ref ctx_p;
+    ctx_p.set_uint("max_depth", 32);
+    ctx_p.set_uint("max_steps", 5000000);
     return and_then(and_then(mk_simplify_tactic(m),                             
                              mk_propagate_values_tactic(m),
                              using_params(mk_solve_eqs_tactic(m), gaussian_p),
@@ -1254,6 +1493,10 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
                              using_params(mk_simplify_tactic(m), simp2_p)),
                         using_params(mk_simplify_tactic(m), hoist_p),
                         mk_max_bv_sharing_tactic(m),
+                        // Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this?
+                        //mk_ctx_simplify_tactic(m, ctx_p),
+                        // Andreas: This one at least eliminates top level duplicates ...
+                        mk_simplify_tactic(m),
                         // Andreas: How does a NNF actually look like? Can it contain ITE operators?
                         mk_nnf_tactic(m, p));
 }

src/tactic/sls/sls_tracker.h

@@ -65,6 +65,7 @@ private:
     typedef obj_map<expr, value_score> scores_type;    
     typedef obj_map<expr, ptr_vector<expr> > uplinks_type;    
     typedef obj_map<expr, ptr_vector<func_decl> > occ_type;
+    obj_hashtable<expr>	  m_top_expr;
     scores_type           m_scores;
     uplinks_type          m_uplinks;
     entry_point_type      m_entry_points;
@@ -82,7 +83,7 @@ private:
 #if _CACHE_TOP_SCORE_
     double				  m_top_sum;
 #endif
-#if _WEIGHT_DIST_ == 4
+#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_
     double				  m_weight_dist_factor;
 #endif
 
@@ -104,7 +105,7 @@ public:
         m_mpz_manager.del(m_two);            
     }
 
-#if _WEIGHT_DIST_ == 4
+#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_
     inline void set_weight_dist_factor(double val) {
         m_weight_dist_factor = val;
     }
@@ -213,11 +214,62 @@ public:
         return m_uplinks.contains(n);
     }
 
+    inline bool is_top_expr(expr * n) {
+        return m_top_expr.contains(n);
+    }
+
     inline ptr_vector<expr> & get_uplinks(expr * n) {
         SASSERT(m_uplinks.contains(n));
         return m_uplinks.find(n);
     }
 
+#if _REAL_RS_ || _REAL_PBFS_
+    void debug_real(goal_ref const & g, unsigned flip)
+    {
+        unsigned count = 0;
+        for (unsigned i = 0; i < g->size(); i++)
+        {
+            expr * e = g->form(i);
+            if (m_mpz_manager.eq(get_value(e),m_one) && m_where_false.contains(e))
+            {
+                printf("iteration %d: ", flip);
+                printf("form %d is sat but in unsat list at position %d of %d\n", i, m_where_false.find(e), m_where_false.size());
+                exit(4);
+            }
+
+            if (m_mpz_manager.eq(get_value(e),m_zero) && !m_where_false.contains(e))
+            {
+                printf("iteration %d: ", flip);
+                printf("form %d is unsat but not in unsat list\n", i);
+                exit(4);
+            }
+
+            if (m_mpz_manager.eq(get_value(e),m_zero) && m_where_false.contains(e))
+            {
+                unsigned pos = m_where_false.find(e);
+                expr * q = m_list_false[pos];
+                if (q != e)
+                {
+                    printf("iteration %d: ", flip);
+                    printf("form %d is supposed to be at pos %d in unsat list but something else was there\n", i, pos);
+                    exit(4);
+                }
+            }
+
+            if (m_mpz_manager.eq(get_value(e),m_zero))
+                count++;
+        }
+
+        // should be true now that duplicate assertions are removed
+        if (count != m_where_false.size())
+        {
+                printf("iteration %d: ", flip);
+                printf("%d are unsat but list is of size %d\n", count, m_where_false.size());
+                exit(4);
+        }
+    }
+#endif
+
     void initialize(app * n) {
         // Build score table
         if (!m_scores.contains(n)) {
@@ -352,6 +404,10 @@ public:
         unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) {
             expr * e = g->form(i);
+            if (!m_top_expr.contains(e))
+                m_top_expr.insert(e);
+            else
+                printf("this is already in ...\n");
             // Andreas: Maybe not fully correct.
 #if _FOCUS_ == 2
             initialize_recursive(proc, visited, e);
@@ -380,9 +436,11 @@ public:
 
 #if _REAL_RS_ || _REAL_PBFS_
         m_list_false = new expr*[sz];
-        for (unsigned i = 0; i < sz; i++)
+        //for (unsigned i = 0; i < sz; i++)
-              if (m_mpz_manager.eq(get_value(g->form(i)),m_zero))
+        //{
-                break_assertion(g->form(i));
+        //	if (m_mpz_manager.eq(get_value(g->form(i)),m_zero))
+        //		break_assertion(g->form(i));
+        //}
 #endif
 
 #if _EARLY_PRUNE_
@@ -391,7 +449,7 @@ public:
 #endif
 
 #if _UCT_
-        m_touched = 1;
+        m_touched = _UCT_INIT_ ? g->size() : 1;
 #endif
     }
 
@@ -407,7 +465,11 @@ public:
                 expr * q = m_list_false[m_where_false.size()];
                 m_list_false[pos] = q;
                 m_where_false.find(q) = pos;
+                //printf("Moving %d from %d to %d\n", q, m_where_false.size(), pos);
             }
+            //else
+                //printf("Erasing %d from %d to %d\n", e, pos);
+//			m_list_false[m_where_false.size()] = 0;
 //			printf("Going in %d\n", m_where_false.size());
         }
         //if (m_unsat_expr.contains(e))
@@ -416,8 +478,10 @@ public:
 
     void break_assertion(expr * e)
     {
+        //printf("I'm broken... that's still fine.\n");
         if (!m_where_false.contains(e))
         {
+            //printf("This however is not so cool...\n");
             unsigned pos = m_where_false.size();
             m_list_false[pos] = e;
             m_where_false.insert(e, pos);
@@ -522,7 +586,7 @@ public:
             NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
     }    
 
-    void randomize() {
+    void randomize(goal_ref const & g) {
         TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
 
         for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
@@ -534,6 +598,28 @@ public:
         }
 
         TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); );
+
+#if _UCT_RESET_
+        m_touched = _UCT_INIT_ ? g->size() : 1;
+        for (unsigned i = 0; i < g->size(); i++)
+            m_scores.find(g->form(i)).touched = 1;
+#endif
+    }              
+
+    void reset(goal_ref const & g) {
+        TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
+
+        for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
+            mpz temp = m_zero;
+            set_value(it->m_value, temp);
+            m_mpz_manager.del(temp);
+        }
+
+#if _UCT_RESET_
+        m_touched = _UCT_INIT_ ? g->size() : 1;
+        for (unsigned i = 0; i < g->size(); i++)
+            m_scores.find(g->form(i)).touched = 1;
+#endif
     }              
 
 #if _EARLY_PRUNE_
@@ -591,12 +677,20 @@ public:
 #if _SCORE_AND_AVG_
             double sum = 0.0;
             for (unsigned i = 0; i < a->get_num_args(); i++)
+#if _DIRTY_UP_
+                sum += is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
+#else
                 sum += get_score(args[i]);
+#endif
             res = sum / (double) a->get_num_args();
 #else
             double min = 1.0;
             for (unsigned i = 0; i < a->get_num_args(); i++) {
+#if _DIRTY_UP_
+                double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
+#else
                 double cur = get_score(args[i]);
+#endif
                 if (cur < min) min = cur;
             }
             res = min;
@@ -610,14 +704,22 @@ public:
 #if _SCORE_OR_MUL_
             double inv = 1.0;
             for (unsigned i = 0; i < a->get_num_args(); i++) {
+#if _DIRTY_UP_
+                double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
+#else
                 double cur = get_score(args[i]);
+#endif
                 inv *= (1.0 - get_score(args[i]));
             }
             res = 1.0 - inv;
 #else
             double max = 0.0;
             for (unsigned i = 0; i < a->get_num_args(); i++) {
+#if _DIRTY_UP_
+                double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
+#else
                 double cur = get_score(args[i]);
+#endif
                 if (cur > max) max = cur;
             }
             res = max;
@@ -772,7 +874,11 @@ public:
             expr * child = a->get_arg(0);
             if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF.
                 NOT_IMPLEMENTED_YET();
+#if _DIRTY_UP_
+            res = is_top_expr(child) ? 0.0 : score_bool(child, true);
+#else
             res = score_bool(child, true);
+#endif
         }
         else if (m_manager.is_distinct(n)) {
             app * a = to_app(n);
@@ -803,7 +909,11 @@ public:
         if (afid == m_bv_util.get_family_id())
 #endif
 #if _WEIGHT_DIST_ == 1
+#if _WEIGHT_TOGGLE_
+        if (res < 1.0) res *= m_weight_dist_factor;
+#else
         if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_;
+#endif
 #elif _WEIGHT_DIST_ == 2
         res *= res;
 #elif _WEIGHT_DIST_ == 3
@@ -900,6 +1010,10 @@ public:
     }
 
     ptr_vector<func_decl> & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) {
+        if (sz == 1)
+            return get_constants();
+        m_temp_constants.reset();
+
         for (unsigned i = 0; i < sz; i++) {
             expr * q = g->form(i);
             if (m_mpz_manager.eq(get_value(q), m_one))
@@ -945,7 +1059,7 @@ public:
     }
 
     ptr_vector<func_decl> & get_unsat_constants_walksat(expr * e) {
-            if (!e)
+            if (!e || m_temp_constants.size())
                 return m_temp_constants;
             ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
             unsigned sz = this_decls.size();
@@ -1033,11 +1147,16 @@ public:
 #if _PROBABILISTIC_UCT_
             double sum_score = 0.0;
             unsigned start_index = get_random_uint(16) % sz;
+            
             for (unsigned i = start_index; i < sz; i++)
             {
                 expr * e = g->form(i);
                 vscore = m_scores.find(e);
-                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); 
+#if _PROBABILISTIC_UCT_ == 2
+                double q = vscore.score * vscore.score; 
+#else
+                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; 
+#endif
                 if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
                     sum_score += q;
                     if (rand() <= (q * RAND_MAX / sum_score) + 1)
@@ -1048,7 +1167,11 @@ public:
             {
                 expr * e = g->form(i);
                 vscore = m_scores.find(e);
-                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); 
+#if _PROBABILISTIC_UCT_ == 2
+                double q = vscore.score * vscore.score; 
+#else
+                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; 
+#endif
                 if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
                     sum_score += q;
                     if (rand() <= (q * RAND_MAX / sum_score) + 1)
@@ -1059,6 +1182,8 @@ public:
             double max = -1.0;
             for (unsigned i = 0; i < sz; i++) {
                 expr * e = g->form(i);
+//            for (unsigned i = 0; i < m_where_false.size(); i++) {
+//                expr * e = m_list_false[i];
                 vscore = m_scores.find(e);
 #if _UCT_ == 1
                 double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); 
@@ -1078,6 +1203,7 @@ public:
             m_scores.find(g->form(pos)).touched = flip; 
 #endif
             expr * e = g->form(pos);
+//            expr * e = m_list_false[pos];
 
 #elif _BFS_ == 3
             unsigned int pos = -1;
@@ -1120,7 +1246,6 @@ public:
             sz = m_where_false.size();
             if (sz == 0)
                 return m_temp_constants;
-            else
             expr * e = m_list_false[get_random_uint(16) % sz];
 #elif _REAL_PBFS_
             //unsigned pos = m_false_list[flip % m_cnt_false];
@@ -1154,6 +1279,142 @@ public:
 #endif
         }
     }
+    
+
+    expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) {
+        unsigned sz = g->size();
+
+        if (sz == 1)
+            return g->form(0);
+
+        m_temp_constants.reset();
+#if _FOCUS_ == 1
+#if _UCT_
+        unsigned pos = -1;
+        value_score vscore;
+#if _PROBABILISTIC_UCT_
+        double sum_score = 0.0;
+        unsigned start_index = get_random_uint(16) % sz;
+            
+        for (unsigned i = start_index; i < sz; i++)
+        {
+            expr * e = g->form(i);
+            vscore = m_scores.find(e);
+#if _PROBABILISTIC_UCT_ == 2
+            double q = vscore.score * vscore.score + _UCT_EPS_; 
+#else
+            double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; 
+#endif
+            if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
+                sum_score += q;
+                if (rand() <= (q * RAND_MAX / sum_score) + 1)
+                    pos = i;
+            }	
+        }
+        for (unsigned i = 0; i < start_index; i++)
+        {
+            expr * e = g->form(i);
+            vscore = m_scores.find(e);
+#if _PROBABILISTIC_UCT_ == 2
+            double q = vscore.score * vscore.score + _UCT_EPS_; 
+#else
+            double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_; 
+#endif
+            if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
+                sum_score += q;
+                if (rand() <= (q * RAND_MAX / sum_score) + 1)
+                    pos = i;
+            }	
+        }
+#else
+        double max = -1.0;
+            for (unsigned i = 0; i < sz; i++) {
+                expr * e = g->form(i);
+//            for (unsigned i = 0; i < m_where_false.size(); i++) {
+//                expr * e = m_list_false[i];
+                vscore = m_scores.find(e);
+#if _UCT_ == 1
+            double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); 
+#elif _UCT_ == 2
+            double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; 
+#endif
+            if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
+            }
+#endif
+        if (pos == static_cast<unsigned>(-1))
+            return 0;
+
+#if _UCT_ == 1
+        m_scores.find(g->form(pos)).touched++;
+        m_touched++;
+#elif _UCT_ == 2
+        m_scores.find(g->form(pos)).touched = flip; 
+#endif
+//        return m_list_false[pos];
+        return g->form(pos);
+
+#elif _BFS_ == 3
+        unsigned int pos = -1;
+        double max = -1.0;
+        for (unsigned i = 0; i < sz; i++) {
+            expr * e = g->form(i);
+               double q = get_score(e);
+            if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
+        if (pos == static_cast<unsigned>(-1))
+            return 0;
+        return g->form(pos);
+#elif _BFS_ == 2
+        unsigned int pos = -1;
+        double min = 2.0;
+        for (unsigned i = 0; i < sz; i++) {
+            expr * e = g->form(i);
+               double q = get_score(e);
+            if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; }
+        }
+        if (pos == static_cast<unsigned>(-1))
+            return 0;
+        return g->form(pos);
+#elif _BFS_ == 1
+        unsigned int pos = flip % sz;
+        return get_unsat_assertion(g, sz, pos);
+#elif _UNIFORM_RANDOM_
+        unsigned cnt_unsat = 0, pos = -1;
+        for (unsigned i = 0; i < sz; i++)
+            if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;	
+        if (pos == static_cast<unsigned>(-1))
+            return 0;
+        return g->form(pos);
+#elif _REAL_RS_
+        //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
+        //expr * e = get_unsat_assertion(g, sz, pos);
+        //expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()];
+        sz = m_where_false.size();
+        if (sz == 0)
+            return 0;
+        return m_list_false[get_random_uint(16) % sz];
+#elif _REAL_PBFS_
+        //unsigned pos = m_false_list[flip % m_cnt_false];
+        //expr * e = get_unsat_assertion(g, sz, pos);
+        //expr * e = m_unsat_expr[flip % m_unsat_expr.size()];
+        sz = m_where_false.size();
+        if (sz == 0)
+            return0;
+        else
+            return m_list_false[flip % sz];
+#else
+        unsigned int pos = get_random_uint(16) % sz;
+        return get_unsat_assertion(g, sz, pos);
+#endif
+        return g->form(pos);
+#elif _FOCUS_ == 2
+#if _BFS_
+        unsigned int pos = flip % sz;
+#else
+        unsigned int pos = get_random_uint(16) % sz;
+#endif
+        return get_unsat_constants_crsat(g, sz, pos);
+#endif
+    }
 };
 
 #endif