Moved parameters to the right file. Almost clean.

src/tactic/sls/sls_compilation_settings.h

@@ -22,10 +22,7 @@ Notes:
 #ifndef _SLS_COMPILATION_SETTINGS_H_
 #define _SLS_COMPILATION_SETTINGS_H_
 
-// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
+// should we use unsat-structures as done in SLS 4 SAT?
 #define _REAL_RS_ 0
 
-// shall we use early pruning for incremental update?
-#define _EARLY_PRUNE_ 1
-
 #endif

src/tactic/sls/sls_engine.cpp

@@ -70,6 +70,8 @@ void sls_engine::updt_params(params_ref const & _p) {
     m_restart_next = m_restart_base;
     m_restart_init = p.restart_init();
 
+    m_early_prune = p.early_prune();
+
     // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT.
     if (m_walksat_repick && !m_walksat)
         NOT_IMPLEMENTED_YET();
@@ -117,7 +119,7 @@ double sls_engine::top_score() {
 
     m_tracker.set_top_sum(top_sum);
 
-    return top_sum / (double)sz;
+    return top_sum;
 }
 
 double sls_engine::rescore() {
@@ -129,21 +131,21 @@ double sls_engine::rescore() {
 double sls_engine::serious_score(func_decl * fd, const mpz & new_value) {
     m_evaluator.serious_update(fd, new_value);
     m_stats.m_incr_evals++;
-    return (m_tracker.get_top_sum() / m_assertions.size());
+    return m_tracker.get_top_sum();
 }
 
 double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) {
     m_evaluator.update(fd, new_value);
     m_stats.m_incr_evals++;
-    return (m_tracker.get_top_sum() / m_assertions.size());
+    return m_tracker.get_top_sum();
 }
 
 double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) {
     m_stats.m_incr_evals++;
     if (m_evaluator.update_prune(fd, new_value))
-        return (m_tracker.get_top_sum() / m_assertions.size());
+        return m_tracker.get_top_sum();
     else
-        return 0.0;
+        return -DBL_MAX;
 }
 
 // checks whether the score outcome of a given move is better than the previous score
@@ -160,11 +162,11 @@ bool sls_engine::what_if(
     m_mpz_manager.set(old_value, m_tracker.get_value(fd));
 #endif
 
-#if _EARLY_PRUNE_
+    double r;
-    double r = incremental_score_prune(fd, temp);
+    if (m_early_prune)
-#else
+        r = incremental_score_prune(fd, temp);
-    double r = incremental_score(fd, temp);
+    else
-#endif   
+        r = incremental_score(fd, temp);
 #ifdef Z3DEBUG
     TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
             " --> " << r << std::endl;);
@@ -342,11 +344,8 @@ double sls_engine::find_best_move(
             if (what_if(fd, i, temp, new_score, best_const, best_value))
                 move = MV_INV;
         }
-
         // reset to what it was before
-        double check = incremental_score(fd, old_value);
+        incremental_score(fd, old_value);
-        // Andreas: does not hold anymore now that we use top level score caching
-        //SASSERT(check == score);
     }
 
     m_mpz_manager.del(old_value);
@@ -381,9 +380,8 @@ double sls_engine::find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double
                 }
             }
         }
-
         // reset to what it was before
-        double check = incremental_score(fd, old_value);
+        incremental_score(fd, old_value);
     }
 
     m_mpz_manager.del(old_value);
@@ -408,7 +406,10 @@ lbool sls_engine::search() {
         checkpoint();
         m_stats.m_moves++;
         if (m_stats.m_moves % m_restart_base == 0)
+        {
             m_tracker.ucb_forget(m_assertions);
+            //score = rescore();
+        }
 
 #if _REAL_RS_
         //m_tracker.debug_real(g, m_stats.m_moves);
@@ -425,7 +426,7 @@ lbool sls_engine::search() {
         if (m_wp && m_tracker.get_random_uint(10) < m_wp)
         {
             mk_random_move(to_evaluate);
-            score = m_tracker.get_top_sum() / sz;
+            score = m_tracker.get_top_sum();
             continue;
         }
 
@@ -465,7 +466,7 @@ lbool sls_engine::search() {
             else
                 m_evaluator.randomize_local(to_evaluate);
 
-            score = m_tracker.get_top_sum() / m_assertions.size();
+            score = m_tracker.get_top_sum();
 
             // update assertion weights if a weigthing is enabled (sp < 1024)
             if (m_paws)
@@ -513,7 +514,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
         assert_expr(g->form(i));    
 
     verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl;
-    verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl;
 
     lbool res = operator()();
 

src/tactic/sls/sls_engine.h

@@ -81,8 +81,7 @@ protected:
     unsigned        m_restart_base;
     unsigned        m_restart_next;
     unsigned        m_restart_init;
-
+    unsigned        m_early_prune;
-    ptr_vector<mpz> m_old_values;
 
     typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type;
 

src/tactic/sls/sls_evaluator.h

@@ -554,9 +554,7 @@ public:
                 if (m_tracker.is_top_expr(cur))
                     m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
                 m_tracker.set_score(cur, new_score);
-#if _EARLY_PRUNE_
                 m_tracker.set_score_prune(cur, new_score);
-#endif            
 
                 if (m_tracker.has_uplinks(cur)) {
                     ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
@@ -599,9 +597,6 @@ public:
                 if (m_tracker.is_top_expr(cur))
                     m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
                 m_tracker.set_score(cur, new_score);
-#if _EARLY_PRUNE_
-                m_tracker.set_score_prune(cur, new_score);
-#endif            
                 if (m_tracker.has_uplinks(cur)) {
                     ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
                     for (unsigned j = 0; j < ups.size(); j++) {

src/tactic/sls/sls_params.pyg

@@ -8,19 +8,15 @@ def_module_params('sls',
 						('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'),
 						('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'),
 						('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'),
-						('walksat_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'),
 						('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'),
 						('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'),
 						('paws_init', UINT, 40, 'initial/minimum assertion weights'),
 						('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'),
-						('wp', UINT, 100, 'random walk with probability wp / 1024'),
+						('wp', UINT, 0, 'random walk with probability wp / 1024'),
 						('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'),
 						('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'),
 						('restart_base', UINT, 100, 'base restart interval given by moves per run'),
 						('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
 						('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'),
-						('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
 						('random_seed', UINT, 0, 'random seed')
 			  ))

src/tactic/sls/sls_tracker.h

@@ -44,11 +44,9 @@ class sls_tracker {
         unsynch_mpz_manager * m;
         mpz value;
         double score;
-#if _EARLY_PRUNE_
         double score_prune;
         unsigned has_pos_occ;
         unsigned has_neg_occ;
-#endif
         unsigned distance; // max distance from any root
         unsigned touched;
         value_score & operator=(const value_score & other) {
@@ -122,6 +120,7 @@ public:
         m_paws_init = p.paws_init();
     }
 
+    /* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently.
     unsigned get_formula_size() {
         return m_scores.size();
     }
@@ -145,7 +144,7 @@ public:
         }
 
         return sum / count;   
-    }
+    }*/
 
     inline void adapt_top_sum(expr * e, double add, double sub) {
         m_top_sum += m_weights.find(e) * (add - sub);
@@ -417,6 +416,8 @@ public:
         }
     }
 
+    /* Andreas: Used this at some point to have values for the non-top-level expressions.
+                However, it did not give better performance but even cause some additional m/o - is not used currently.
     void initialize_recursive(init_proc proc, expr_mark visited, expr * e) {
         if (m_manager.is_and(e) || m_manager.is_or(e)) {
             app * a = to_app(e);
@@ -445,7 +446,7 @@ public:
         find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e));
         expr_fast_mark1 visited;
         quick_for_each_expr(ffd_proc, visited, e);
-    }
+    }*/
 
     void initialize(ptr_vector<expr> const & as) {
         init_proc proc(m_manager, *this);
@@ -455,8 +456,6 @@ public:
             expr * e = as[i];
             if (!m_top_expr.contains(e))
                 m_top_expr.insert(e);
-            else
-                printf("this is already in ...\n");
             for_each_expr(proc, visited, e);
         }
 
@@ -464,7 +463,6 @@ public:
 
         for (unsigned i = 0; i < sz; i++) {
             expr * e = as[i];
-            // Andreas: Maybe not fully correct.
             ptr_vector<func_decl> t;
             m_constants_occ.insert_if_not_there(e, t);
             find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e));
@@ -488,15 +486,16 @@ public:
         for (unsigned i = 0; i < sz; i++)
         {
             expr * e = as[i];
-        	if (!m_weights.contains(e))
+
+            // initialize weights
+            if (!m_weights.contains(e))
         		m_weights.insert(e, m_paws_init);
+
+            // positive/negative occurences used for early pruning
+            setup_occs(as[i]);
         }
 
-#if _EARLY_PRUNE_
+        // initialize ucb total touched value (individual ones are always initialized to 1)
-        for (unsigned i = 0; i < sz; i++)
-            setup_occs(as[i]);
-#endif
-
         m_touched = m_ucb_init ? as.size() : 1;
     }
 
@@ -738,7 +737,6 @@ public:
             SASSERT(!negated);
             app * a = to_app(n);
             expr * const * args = a->get_args();
-            // Andreas: Seems to have no effect. Probably it is still too similar to the original version.
             double max = 0.0;
             for (unsigned i = 0; i < a->get_num_args(); i++) {
                 double cur = get_score(args[i]);
@@ -764,7 +762,6 @@ public:
             const mpz & v1 = get_value(arg1);
             
             if (negated) {                    
-                //res = (m_mpz_manager.eq(v0, v1)) ? 0.5 * (m_bv_util.get_bv_size(arg0) - 1.0) / m_bv_util.get_bv_size(arg0) : 1.0;
                 res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0;
                 TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << 
                                         m_mpz_manager.to_string(v1) << std::endl; );
@@ -1051,10 +1048,8 @@ public:
 //            for (unsigned i = 0; i < m_where_false.size(); i++) {
 //                expr * e = m_list_false[i];
                 vscore = m_scores.find(e);
-                double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
+                //double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
-#if _UCT_ == 3
+                double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + (get_random_uint(8) * 0.0000002); 
-            double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16)); 
-#endif
                 if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
             }
             if (pos == static_cast<unsigned>(-1))