plenty of new stuff

src/sat/tactic/sat_tactic.cpp

@@ -66,6 +66,8 @@ class sat_tactic : public tactic {
             CASSERT("sat_solver", m_solver.check_invariant());
             IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
             TRACE("sat_dimacs", m_solver.display_dimacs(tout););
+			//m_solver.display_dimacs(std::cerr);
+            //exit(0);
 
             lbool r = m_solver.check();
             if (r == l_false) {

src/tactic/portfolio/default_tactic.cpp

@@ -33,6 +33,7 @@ Notes:
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
                                         cond(mk_is_qfbv_probe(),  mk_qfbv_sls_tactic(m),
+  //                                      cond(mk_is_qfbv_probe(),  mk_qfbv_tactic(m),
                                         cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
                                         cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
                                         cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -43,6 +43,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
     if (logic=="QF_UF")
         return mk_qfuf_tactic(m, p);
     else if (logic=="QF_BV")
+   //     return mk_qfbv_tactic(m, p);
         return mk_qfbv_sls_tactic(m, p);
     else if (logic=="QF_IDL")
         return mk_qfidl_tactic(m, p);

src/tactic/sls/sls_evaluator.h

@@ -34,6 +34,9 @@ class sls_evaluator {
     powers              & m_powers;
     expr_ref_buffer       m_temp_exprs;
     vector<ptr_vector<expr> > m_traversal_stack;
+#if _EARLY_PRUNE_
+    vector<ptr_vector<expr> > m_traversal_stack_bool;
+#endif
 
 public:
     sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) : 
@@ -519,11 +522,15 @@ public:
         }    
     }
 
-    void run_update(unsigned cur_depth) {
+    void run_serious_update(unsigned cur_depth) {
         // precondition: m_traversal_stack contains the entry point(s)
         expr_fast_mark1 visited;
         mpz new_value;
 
+#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
+		double new_score;
+#endif
+
         SASSERT(cur_depth < m_traversal_stack.size());
         while (cur_depth != static_cast<unsigned>(-1)) {
             ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
@@ -533,8 +540,92 @@ public:
 
                 (*this)(to_app(cur), new_value);
                 m_tracker.set_value(cur, new_value);
-                m_tracker.set_score(cur, m_tracker.score(cur));
 
+#if _REAL_RS_ || _REAL_PBFS_
+				if (!m_tracker.has_uplinks(cur))
+				{
+					if (m_mpz_manager.eq(new_value,m_one))
+						m_tracker.make_assertion(cur);
+					else
+						m_tracker.break_assertion(cur);
+				}
+#endif
+
+#if _EARLY_PRUNE_
+				new_score = m_tracker.score(cur);
+#if _CACHE_TOP_SCORE_
+				if (!m_tracker.has_uplinks(cur))
+					m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
+#endif
+				m_tracker.set_score(cur, new_score);
+				m_tracker.set_score_prune(cur, new_score);
+#else
+#if _CACHE_TOP_SCORE_
+				new_score = m_tracker.score(cur);
+				if (!m_tracker.has_uplinks(cur))
+					m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
+				m_tracker.set_score(cur, new_score);
+#else
+				m_tracker.set_score(cur, m_tracker.score(cur));
+#endif
+#endif			
+                if (m_tracker.has_uplinks(cur)) {
+                    ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
+                    for (unsigned j = 0; j < ups.size(); j++) {
+                        expr * next = ups[j];
+                        unsigned next_d = m_tracker.get_distance(next);
+                        SASSERT(next_d < cur_depth);
+                        if (!visited.is_marked(next)) {
+                            m_traversal_stack[next_d].push_back(next);
+                            visited.mark(next);
+                        }
+                    }
+                }
+            }
+
+            cur_depth_exprs.reset();
+            cur_depth--;
+        }
+
+        m_mpz_manager.del(new_value);
+    }
+
+    void run_update(unsigned cur_depth) {
+        // precondition: m_traversal_stack contains the entry point(s)
+        expr_fast_mark1 visited;
+        mpz new_value;
+
+#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
+		double new_score;
+#endif
+
+        SASSERT(cur_depth < m_traversal_stack.size());
+        while (cur_depth != static_cast<unsigned>(-1)) {
+            ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
+
+            for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
+                expr * cur = cur_depth_exprs[i];
+
+                (*this)(to_app(cur), new_value);
+                m_tracker.set_value(cur, new_value);
+#if _EARLY_PRUNE_
+				new_score = m_tracker.score(cur);
+#if _CACHE_TOP_SCORE_
+				if (!m_tracker.has_uplinks(cur))
+					m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
+#endif
+				m_tracker.set_score(cur, new_score);
+				m_tracker.set_score_prune(cur, new_score);
+#else
+#if _CACHE_TOP_SCORE_
+				new_score = m_tracker.score(cur);
+				if (!m_tracker.has_uplinks(cur))
+					m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
+				m_tracker.set_score(cur, new_score);
+#else
+				m_tracker.set_score(cur, m_tracker.score(cur));
+#endif
+#endif			
                 if (m_tracker.has_uplinks(cur)) {
                     ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
                     for (unsigned j = 0; j < ups.size(); j++) {
@@ -569,8 +660,11 @@ public:
             m_traversal_stack[cur_depth].push_back(ep);
             if (cur_depth > max_depth) max_depth = cur_depth;
         }
-
+#if _REAL_RS_ || _REAL_PBFS_
+		run_serious_update(max_depth);
+#else
         run_update(max_depth);
+#endif
     }
 
     void update(func_decl * fd, const mpz & new_value) {
@@ -584,6 +678,196 @@ public:
         run_update(cur_depth);
     }
 
+    void serious_update(func_decl * fd, const mpz & new_value) {
+        m_tracker.set_value(fd, new_value);
+        expr * ep = m_tracker.get_entry_point(fd);
+        unsigned cur_depth = m_tracker.get_distance(ep);
+        if (m_traversal_stack.size() <= cur_depth) 
+            m_traversal_stack.resize(cur_depth+1);
+        m_traversal_stack[cur_depth].push_back(ep);
+
+        run_serious_update(cur_depth);
+    }
+
+#if _EARLY_PRUNE_
+    unsigned run_update_bool_prune(unsigned cur_depth) {
+        expr_fast_mark1 visited;
+
+		double prune_score, new_score;
+		unsigned pot_benefits = 0;
+ 		SASSERT(cur_depth < m_traversal_stack_bool.size());
+ 
+        ptr_vector<expr> & cur_depth_exprs = m_traversal_stack_bool[cur_depth];
+
+        for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
+            expr * cur = cur_depth_exprs[i];
+
+			new_score = m_tracker.score(cur); 
+#if _CACHE_TOP_SCORE_
+			if (!m_tracker.has_uplinks(cur))
+				m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
+#endif
+			prune_score = m_tracker.get_score_prune(cur);
+            m_tracker.set_score(cur, new_score);
+
+			if ((new_score > prune_score) && (m_tracker.has_pos_occ(cur)))
+				pot_benefits = 1;
+			if ((new_score <= prune_score) && (m_tracker.has_neg_occ(cur)))
+				pot_benefits = 1;
+
+            if (m_tracker.has_uplinks(cur)) {
+                ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
+                for (unsigned j = 0; j < ups.size(); j++) {
+                    expr * next = ups[j];
+                    unsigned next_d = m_tracker.get_distance(next);
+                    SASSERT(next_d < cur_depth);
+                    if (!visited.is_marked(next)) {
+						m_traversal_stack_bool[next_d].push_back(next);
+                        visited.mark(next);
+                    }
+                }
+            }
+			else
+			{
+			}
+		}
+
+		cur_depth_exprs.reset();
+        cur_depth--;
+ 
+		while (cur_depth != static_cast<unsigned>(-1)) {
+			ptr_vector<expr> & cur_depth_exprs = m_traversal_stack_bool[cur_depth];
+			if (pot_benefits)
+			{
+				unsigned cur_size = cur_depth_exprs.size();
+				for (unsigned i = 0; i < cur_size; i++) {
+					expr * cur = cur_depth_exprs[i];
+
+#if _CACHE_TOP_SCORE_
+					new_score = m_tracker.score(cur); 
+					if (!m_tracker.has_uplinks(cur))
+						m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
+					m_tracker.set_score(cur, new_score);
+#else
+					m_tracker.set_score(cur, m_tracker.score(cur));
+#endif
+					if (m_tracker.has_uplinks(cur)) {
+						ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
+						for (unsigned j = 0; j < ups.size(); j++) {
+							expr * next = ups[j];
+							unsigned next_d = m_tracker.get_distance(next);
+							SASSERT(next_d < cur_depth);
+							if (!visited.is_marked(next)) {
+								m_traversal_stack_bool[next_d].push_back(next);
+								visited.mark(next);
+							}
+						}
+					}
+				}
+			}
+			cur_depth_exprs.reset();
+			cur_depth--;
+		}
+
+		return pot_benefits;
+    }
+
+    void run_update_prune(unsigned max_depth) {
+        // precondition: m_traversal_stack contains the entry point(s)
+        expr_fast_mark1 visited;
+        mpz new_value;
+
+		unsigned cur_depth = max_depth;
+        SASSERT(cur_depth < m_traversal_stack.size());
+        while (cur_depth != static_cast<unsigned>(-1)) {
+            ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
+
+            for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
+                expr * cur = cur_depth_exprs[i];
+
+                (*this)(to_app(cur), new_value);
+                m_tracker.set_value(cur, new_value);
+				// should always have uplinks ...
+                if (m_tracker.has_uplinks(cur)) {
+                    ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
+                    for (unsigned j = 0; j < ups.size(); j++) {
+                        expr * next = ups[j];
+                        unsigned next_d = m_tracker.get_distance(next);
+                        SASSERT(next_d < cur_depth);
+                        if (!visited.is_marked(next)) {
+							if (m_manager.is_bool(next))
+								m_traversal_stack_bool[max_depth].push_back(next);
+							else
+								m_traversal_stack[next_d].push_back(next);
+                            visited.mark(next);
+                        }
+                    }
+                }
+            }
+
+            cur_depth_exprs.reset();
+            cur_depth--;
+        }
+
+        m_mpz_manager.del(new_value);
+    }
+
+    unsigned update_prune(func_decl * fd, const mpz & new_value) {
+        m_tracker.set_value(fd, new_value);
+        expr * ep = m_tracker.get_entry_point(fd);
+        unsigned cur_depth = m_tracker.get_distance(ep);
+
+		if (m_traversal_stack_bool.size() <= cur_depth)
+            m_traversal_stack_bool.resize(cur_depth+1);
+		if (m_traversal_stack.size() <= cur_depth) 
+				m_traversal_stack.resize(cur_depth+1);
+
+		if (m_manager.is_bool(ep))
+	        m_traversal_stack_bool[cur_depth].push_back(ep);
+		else
+		{
+	        m_traversal_stack[cur_depth].push_back(ep);
+			run_update_prune(cur_depth);
+		}
+		return run_update_bool_prune(cur_depth);
+    }
+#endif
+
+	void randomize_local(expr * e, unsigned int flip) {
+        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);
 
@@ -603,8 +887,37 @@ public:
         // 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
+
+#if _REAL_RS_ || _REAL_PBFS_
+		serious_update(fd, temp);
+#else
 		update(fd, temp);
+#endif
         m_mpz_manager.del(temp);
 
         TRACE("sls", /*tout << "Randomization candidates: ";

src/tactic/sls/sls_tactic.cpp

@@ -35,16 +35,102 @@ Notes:
 #include"sls_tactic.h"
 #include"nnf_tactic.h"
 
-#define _CNF_ 0
+// which unsatisfied assertion is selected? only works with _FOCUS_ > 0
-#define _BFS_ 1
+// 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score
+#define _BFS_ 0
+
+// how many terms are considered for variable selection?
+// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT), 2 = only one bottom level atom
 #define _FOCUS_ 1
+
+// do we use restarts?
+// 0 = no, otherwise the value defines the maximum number of moves
 #define _RESTARTS_ 0
-#define _TIMELIMIT_ 30
+
+// timelimit
+#define _TIMELIMIT_ 3600
+
+// should score of conjunctions be calculated by average rather than max?
 #define _SCORE_AND_AVG_ 0
+
+// should score of discunctions be calculated by multiplication of the inverse score rather than min?
 #define _SCORE_OR_MUL_ 0
+
+// do we use some kind of variable neighbourhood-search?
+// 0 = no, 1 = only consider flipping bits if no better score can be obtained otherwise, 2 = only consider flipping bits until a better score can be obtained
 #define _VNS_ 0
-#define _WEIGHT_DIST_ 3
+
-#define _WEIGHT_DIST_FACTOR_ 0.1
+// do we reduce the score of unsatisfied literals?
+// 0 = no
+// 1 = yes, by multiplying it with some factor
+// 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
+
+// the factor used for _WEIGHT_DIST_ = 1
+#define _WEIGHT_DIST_FACTOR_ 0.25
+
+// do we use intensification steps in local minima? if so, how many?
+#define _INTENSIFICATION_ 0
+#define _INTENSIFICATION_TRIES_ 0
+
+// do we use some UCT-like scheme for assertion-selection? overrides _BFS_
+#define _UCT_ 0
+
+// how much diversification is used in the UCT-scheme?
+#define _UCT_CONSTANT_ 0.01
+
+// is uct clause selection probabilistic similar to variable selection in sparrow?
+#define _PROBABILISTIC_UCT_ 0
+
+// shall we use addition/subtraction?
+#define _USE_ADDSUB_ 1
+
+// shall we try multilication and division by 2?
+#define _USE_MUL2DIV2_ 1
+
+// shall we try multiplication by 3?
+#define _USE_MUL3_ 1
+
+// shall we try unary minus (= inverting and incrementing)
+#define _USE_UNARY_MINUS_ 1
+
+// is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0
+#define _UNIFORM_RANDOM_ 1
+
+// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
+#define _REAL_RS_ 0
+#define _REAL_PBFS_ 0
+
+// how many bits do we neglect in each iteration?
+#define _SKIP_BITS_ 0
+
+// when randomizing local, what is the probability for changing a single bit?
+// 0 = use standard scheme and pick a new value at random (= 50), otherwise the value (as int) gives the percentage
+#define _PERC_CHANGE_ 0
+
+// do we use random steps for noise?
+// 0 = no, 1 = randomize local, 2 = make random move
+#define _TYPE_RSTEP_ 0
+
+// with what probability _PERM_STEP_/1000 will the random step happen? 
+#define _PERM_RSTEP_ 0
+
+// shall we use early pruning for incremental update?
+#define _EARLY_PRUNE_ 1
+
+// shall we use caching for top_score?
+#define _CACHE_TOP_SCORE_ 1
+
+
+#if ((_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1) || _BFS_ && (_UCT_ ||_UNIFORM_RANDOM_ ||_REAL_RS_ ||_REAL_PBFS_)
+	InvalidConfiguration;
+#endif
+#if (_PROBABILISTIC_UCT_ && !_UCT_)
+	InvalidConfiguration;
+#endif
+
 
 #include"sls_params.hpp"
 #include"sls_evaluator.h"
@@ -57,12 +143,17 @@ class sls_tactic : public tactic {
         stopwatch       m_stopwatch;    
         unsigned        m_full_evals;
         unsigned        m_incr_evals;
-        unsigned        m_moves, m_flips, m_incs, m_decs, m_invs;
+        unsigned        m_moves, m_flips, m_incs, m_decs, m_invs, m_umins, m_mul2s, m_mul3s, m_div2s;
+
         stats() :
             m_restarts(0),
             m_full_evals(0),
             m_incr_evals(0),
             m_moves(0),
+			m_umins(0),
+			m_mul2s(0),
+			m_mul3s(0),
+			m_div2s(0),
             m_flips(0),
             m_incs(0),
             m_decs(0),
@@ -92,7 +183,9 @@ class sls_tactic : public tactic {
         unsigned        m_max_restarts;
         unsigned        m_plateau_limit;
 
-        typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type;        
+		ptr_vector<mpz> m_old_values;
+		
+        typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV, MV_UMIN, MV_MUL2, MV_MUL3, MV_DIV2 } move_type;        
 
         imp(ast_manager & m, params_ref const & p, stats & s) : 
             m_manager(m),
@@ -175,12 +268,19 @@ class sls_tactic : public tactic {
             double top_sum = 0.0;
             unsigned sz = g->size();
 			for (unsigned i = 0; i < sz; i++) {
-                top_sum += m_tracker.get_score(g->form(i));
+				expr * e = g->form(i);
+                top_sum += m_tracker.get_score(e);
             }
+
 			TRACE("sls_top", tout << "Score distribution:"; 
                                     for (unsigned i = 0; i < sz; i++)
                                         tout << " " << m_tracker.get_score(g->form(i));
                                     tout << " AVG: " << top_sum / (double) sz << std::endl; );
+
+#if _CACHE_TOP_SCORE_
+			m_tracker.set_top_sum(top_sum);
+#endif
+
             return top_sum / (double) sz;
             #endif
         }
@@ -191,12 +291,41 @@ class sls_tactic : public tactic {
             return top_score(g);
         }
 
+        double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
+			m_evaluator.serious_update(fd, new_value);
+            m_stats.m_incr_evals++;
+#if _CACHE_TOP_SCORE_
+			return (m_tracker.get_top_sum() / g->size());
+#else
+            return top_score(g);
+#endif
+        }
+
         double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
 			m_evaluator.update(fd, new_value);
             m_stats.m_incr_evals++;
+#if _CACHE_TOP_SCORE_
+			return (m_tracker.get_top_sum() / g->size());
+#else
             return top_score(g);
+#endif
         }
 
+#if _EARLY_PRUNE_
+        double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) {
+            m_stats.m_incr_evals++;
+			if (m_evaluator.update_prune(fd, new_value))
+#if _CACHE_TOP_SCORE_
+				return (m_tracker.get_top_sum() / g->size());
+#else
+	            return top_score(g);
+#endif
+			else
+				return 0.0;
+        }
+#endif
+
+		// checks whether the score outcome of a given move is better than the previous score
         bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, 
                         double & best_score, unsigned & best_const, mpz & best_value) {
 
@@ -205,8 +334,11 @@ class sls_tactic : public tactic {
             m_mpz_manager.set(old_value, m_tracker.get_value(fd));
             #endif
 
+#if _EARLY_PRUNE_
+            double r = incremental_score_prune(g, fd, temp);
+#else
             double r = incremental_score(g, fd, temp);
-        
+#endif   
             #ifdef Z3DEBUG
             TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << 
                                         " --> " << r << std::endl; );
@@ -214,6 +346,22 @@ class sls_tactic : public tactic {
             m_mpz_manager.del(old_value);
             #endif
 
+//            if (r >= best_score) {
+            if (r > best_score) {
+                best_score = r;
+                best_const = fd_inx;            
+                m_mpz_manager.set(best_value, temp);
+                return true;
+            }
+
+            return false;
+        }
+
+		// same as what_if, but only applied to the score of a specific atom, not the total score
+        bool what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp, 
+                        double & best_score, unsigned & best_const, mpz & best_value) {
+            m_evaluator.update(fd, temp);
+			double r = m_tracker.get_score(e);
             if (r >= best_score) {
                 best_score = r;
                 best_const = fd_inx;            
@@ -224,6 +372,34 @@ class sls_tactic : public tactic {
             return false;
         }
 
+        void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result) {
+            mpz temp, mask, mask2;
+            m_mpz_manager.add(old_value, add_value, temp);
+            m_mpz_manager.set(mask, m_powers(bv_sz));
+            m_mpz_manager.bitwise_not(bv_sz, mask, mask2);
+            m_mpz_manager.bitwise_and(temp, mask2, result);
+			m_mpz_manager.del(temp);
+			m_mpz_manager.del(mask);
+			m_mpz_manager.del(mask2);
+
+		}
+
+		// Andreas: do we really need all those temporary mpzs?
+		void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result) {
+            mpz temp, mask, mask2;
+            m_mpz_manager.mul(old_value, m_two, temp);
+            m_mpz_manager.set(mask, m_powers(bv_sz));
+            m_mpz_manager.bitwise_not(bv_sz, mask, mask2);
+            m_mpz_manager.bitwise_and(temp, mask2, result);
+			m_mpz_manager.del(temp);
+			m_mpz_manager.del(mask);
+			m_mpz_manager.del(mask2);
+        }
+
+        void mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result) {
+            m_mpz_manager.div(old_value, m_two, result);
+        }
+
 		void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) {
             unsigned shift;        
             m_mpz_manager.add(old_value, m_one, incremented);
@@ -261,24 +437,37 @@ class sls_tactic : public tactic {
 
         void mk_random_move(goal_ref const & g) {
             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];
+
+			mpz new_value;
+
+			sort * srt = fd->get_range();
+            if (m_manager.is_bool(srt))
+				m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
+			else
+			{
+#if _USE_ADDSUB_
 	            if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv=2;
 	            if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++;
 				move_type mt = (move_type) rnd_mv;
 
 				// inversion doesn't make sense, let's do a flip instead.
 				if (mt == MV_INV) mt = MV_FLIP;
-
+#else
-			ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g, m_stats.m_moves);                
+				mt = MV_FLIP;
-            unsigned ucc = unsat_constants.size(); 
+#endif
-            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];
-            mpz new_value;
 				unsigned bit = 0;
 
 				switch (mt)
 				{
 					case MV_FLIP: {
-                unsigned bv_sz = m_bv_util.get_bv_size(fd->get_range());
+					unsigned bv_sz = m_bv_util.get_bv_size(srt);
 					bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz;
 					mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value);
 					break;
@@ -296,8 +485,6 @@ class sls_tactic : public tactic {
 					NOT_IMPLEMENTED_YET();
 				}
 
-            m_evaluator.update(fd, new_value);            
-
 				TRACE("sls", tout << "Randomization candidates: ";
 							 for (unsigned i = 0; i < unsat_constants.size(); i++)
 								 tout << unsat_constants[i]->get_name() << ", ";
@@ -310,10 +497,13 @@ class sls_tactic : public tactic {
 							 case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break;
 							 }
 							 tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); );            
+			}
 
+			m_evaluator.update(fd, new_value);            
 			m_mpz_manager.del(new_value);
 		}
 
+		// 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) {
             mpz old_value, temp;
@@ -359,6 +549,7 @@ class sls_tactic : public tactic {
                 SASSERT(check == score);
             }
 
+			// we can either check the condition once in the beginning or check it repeatedly after every bit
 #if _VNS_ == 1
 			for (unsigned j = 1; j < max_bv_sz && new_score <= score; j++)
 #else
@@ -390,9 +581,13 @@ class sls_tactic : public tactic {
             return new_score;
         }        
 
+		// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
         double find_best_move(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score, 
                               unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) {
             mpz old_value, temp;
+#if _USE_MUL3_ || _USE_UNARY_MINUS_
+			mpz temp2;
+#endif
             unsigned bv_sz;
             double new_score = score;
 
@@ -403,7 +598,11 @@ class sls_tactic : public tactic {
                 m_mpz_manager.set(old_value, m_tracker.get_value(fd));
 
                 // first try to flip every bit
+#if _SKIP_BITS_
+				for (unsigned j = (i + m_stats.m_moves) % (_SKIP_BITS_ + 1); j < bv_sz && new_score < 1.0; j+=(_SKIP_BITS_ + 1)) {
+#else
 				for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) {
+#endif
 					// What would happen if we flipped bit #i ?                
                     mk_flip(srt, old_value, j, temp);                
 
@@ -414,6 +613,7 @@ class sls_tactic : public tactic {
                 }
 
                 if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
+#if _USE_ADDSUB_
 					if (!m_mpz_manager.is_even(old_value)) { 
                         // for odd values, try +1
                         mk_inc(bv_sz, old_value, temp);
@@ -426,16 +626,99 @@ class sls_tactic : public tactic {
                         if (what_if(g, fd, i, temp, new_score, best_const, best_value))
                             move = MV_DEC;
                     }
-
+#endif
                     // try inverting
                     mk_inv(bv_sz, old_value, temp);
                     if (what_if(g, fd, i, temp, new_score, best_const, best_value))
                         move = MV_INV;
+
+#if _USE_UNARY_MINUS_
+                    mk_inc(bv_sz, temp, temp2);
+                    if (what_if(g, fd, i, temp2, new_score, best_const, best_value))
+                        move = MV_UMIN;
+#endif
+
+#if _USE_MUL2DIV2_
+                    // try multiplication by 2
+                    mk_mul2(bv_sz, old_value, temp);
+                    if (what_if(g, fd, i, temp, new_score, best_const, best_value))
+                        move = MV_MUL2;
+
+#if _USE_MUL3_
+                    // try multiplication by 3
+                    mk_add(bv_sz, old_value, temp, temp2);
+                    if (what_if(g, fd, i, temp2, new_score, best_const, best_value))
+                        move = MV_MUL3;
+#endif
+
+                    // try division by 2
+                    mk_div2(bv_sz, old_value, temp);
+                    if (what_if(g, fd, i, temp, new_score, best_const, best_value))
+                        move = MV_DIV2;
+#endif
                 }
 
                 // reset to what it was before
                 double check = incremental_score(g, fd, old_value);
-                SASSERT(check == score);
+				// Andreas: does not hold anymore now that we use top level score caching
+                //SASSERT(check == score);
+            }
+
+            m_mpz_manager.del(old_value);
+            m_mpz_manager.del(temp);
+#if _USE_MUL3_
+            m_mpz_manager.del(temp2);
+#endif
+			return new_score;
+        }        
+
+		// same as find_best_move but only considers the score of the current expression instead of the overall score
+		double find_best_move_local(expr * e, ptr_vector<func_decl> & to_evaluate,
+                              unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) {
+            mpz old_value, temp;
+            unsigned bv_sz;
+			double new_score = m_tracker.get_score(e);
+			// Andreas: tie breaking not implemented yet
+			// double tie_score = top_score(g);
+            for (unsigned i = 0; i < to_evaluate.size(); i++) {
+                func_decl * fd = to_evaluate[i];
+                sort * srt = fd->get_range();
+                bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
+                m_mpz_manager.set(old_value, m_tracker.get_value(fd));
+
+                // first try to flip every bit
+                for (unsigned j = 0; j < bv_sz; j++) {
+                    // What would happen if we flipped bit #i ?                
+                    mk_flip(srt, old_value, j, temp);                
+
+                    if (what_if_local(e, fd, i, temp, new_score, best_const, best_value)) {
+                        new_bit = j;
+                        move = MV_FLIP;
+                    }
+                }
+
+                if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
+                    if (!m_mpz_manager.is_even(old_value)) { 
+                        // for odd values, try +1
+                        mk_inc(bv_sz, old_value, temp);
+                        if (what_if_local(e, fd, i, temp, new_score, best_const, best_value))
+                            move = MV_INC;
+                    }
+                    else { 
+                        // for even values, try -1
+                        mk_dec(bv_sz, old_value, temp);
+                        if (what_if_local(e, fd, i, temp, new_score, best_const, best_value))
+                            move = MV_DEC;
+                    }
+
+                    // try inverting
+                    mk_inv(bv_sz, old_value, temp);
+                    if (what_if_local(e, fd, i, temp, new_score, best_const, best_value))
+                        move = MV_INV;
+                }
+
+                // reset to what it was before
+	            m_evaluator.update(fd, old_value);
             }
 
             m_mpz_manager.del(old_value);
@@ -443,6 +726,149 @@ class sls_tactic : public tactic {
             return new_score;
         }        
 
+		// first try of intensification ... does not seem to be efficient
+		bool handle_plateau(goal_ref const & g)
+		{
+			unsigned sz = g->size();
+#if _BFS_
+			unsigned pos = m_stats.m_moves % sz;
+#else
+			unsigned pos = m_tracker.get_random_uint(16) % sz;
+#endif
+			expr * e = m_tracker.get_unsat_assertion(g, sz, pos);
+	        if (!e)
+				return 0;
+
+			expr * q = m_tracker.get_unsat_expression(e);
+			ptr_vector<func_decl> & to_evaluate = m_tracker.get_constants(q);
+			for (unsigned i = 0; i < to_evaluate.size(); i++)
+			{
+				m_tracker.get_value(to_evaluate[i]);
+				m_old_values.push_back( & m_tracker.get_value(to_evaluate[i]));
+			}            
+			unsigned new_const = (unsigned)-1, new_bit = 0;        
+            mpz new_value;
+            move_type move;
+			for (unsigned i = 0; i < _INTENSIFICATION_TRIES_; i++)
+			{
+				// Andreas: Could be extended to use (best) score but this is computationally more expensive.
+                find_best_move_local(q, to_evaluate, new_const, new_value, new_bit, move);
+
+                if (new_const == static_cast<unsigned>(-1)) {
+					// Andreas: Actually this should never happen.
+					NOT_IMPLEMENTED_YET();
+                } else {
+                    m_stats.m_moves++;
+                    func_decl * fd = to_evaluate[new_const];
+
+                    switch (move) {
+                    case MV_FLIP: m_stats.m_flips++; break;
+                    case MV_INC: m_stats.m_incs++; break;
+                    case MV_DEC: m_stats.m_decs++; break;
+                    case MV_INV: m_stats.m_invs++; break;
+                    case MV_UMIN: m_stats.m_umins++; break;
+					case MV_MUL2: m_stats.m_mul2s++; break;
+					case MV_MUL3: m_stats.m_mul3s++; break;
+					case MV_DIV2: m_stats.m_div2s++; break;
+                    }
+                    
+					m_evaluator.update(fd, new_value);
+                }
+
+				if (m_mpz_manager.is_one(m_tracker.get_value(q)))
+					return 1;
+			}
+
+			for (unsigned i = 0; i < to_evaluate.size(); i++)
+				m_tracker.set_value(to_evaluate[i], * m_old_values[i]);
+
+			m_old_values.reset();
+
+			return 0;
+		}
+
+		// what_if version needed in the context of 2nd intensification try, combining local and global score
+        bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp, 
+                        double & best_score, mpz & best_value, unsigned i) {
+        
+            double global_score = incremental_score(g, fd, temp);
+			double local_score = m_tracker.get_score(e);
+            double new_score = i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_;
+
+			if (new_score >= best_score) {
+                best_score = new_score;
+                m_mpz_manager.set(best_value, temp);
+                return true;
+            }
+
+            return false;
+        }
+
+		// find_best_move version needed in the context of 2nd intensification try
+        double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i)
+		{
+			mpz old_value, temp;
+            double best_score = 0;
+
+            sort * srt = fd->get_range();
+            unsigned bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
+            m_mpz_manager.set(old_value, m_tracker.get_value(fd));
+
+			for (unsigned j = 0; j < bv_sz && best_score < 1.0; j++) {
+                mk_flip(srt, old_value, j, temp);                
+                what_if(g, e, fd, temp, best_score, best_value, i); 
+            }
+
+            m_mpz_manager.del(old_value);
+            m_mpz_manager.del(temp);
+
+			return best_score;
+        }        
+
+		// second try to use intensification ... also not very effective
+		bool handle_plateau(goal_ref const & g, double old_score)
+		{
+			unsigned sz = g->size();
+#if _BFS_
+			unsigned new_const = m_stats.m_moves % sz;
+#else
+			unsigned new_const = m_tracker.get_random_uint(16) % sz;
+#endif
+			expr * e = m_tracker.get_unsat_assertion(g, sz, new_const);
+	        if (!e)
+				return 0;
+
+			expr * q = m_tracker.get_unsat_expression(e);
+			ptr_vector<func_decl> & to_evaluate = m_tracker.get_constants(q);
+
+			new_const = m_tracker.get_random_uint(16) % to_evaluate.size();
+			func_decl * fd = to_evaluate[new_const];
+
+			mpz new_value;
+			//m_mpz_manager.set(new_value, m_tracker.get_value(fd));
+			unsigned new_bit = 0;        
+			double global_score = old_score, local_score = m_tracker.get_score(q), new_score = old_score;
+			
+			for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++)
+			{
+                new_score = find_best_move_local(g, q, fd, new_value, i);
+
+                m_stats.m_moves++;
+                m_stats.m_flips++;
+
+				global_score = incremental_score(g, fd, new_value);
+     			local_score = m_tracker.get_score(q);
+
+				SASSERT(new_score == i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_);
+
+				if (m_mpz_manager.is_one(m_tracker.get_value(q)))
+					return 1;
+			}
+
+			return 0;
+		}
+
+		// main search loop
 		lbool search(goal_ref const & g) {        
             lbool res = l_undef;
             double score = 0.0, old_score = 0.0;
@@ -463,16 +889,48 @@ class sls_tactic : public tactic {
 #if _RESTARTS_
 			while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
 #else
-			while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {                
+			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
+					m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
+#endif
+            
+#if _TYPE_RSTEP_
+					if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_)
+					{
+#if _TYPE_RSTEP_ == 1
+						m_evaluator.randomize_local(g, m_stats.m_moves);
+#elif _TYPE_RSTEP_ == 2
+						mk_random_move(g);
+#endif
+                        score = top_score(g);
+
+	                    if (score >= 1.0) {
+	                        bool all_true = true;
+	                        for (unsigned i = 0; i < g->size() && all_true; i++)
+	                            if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
+	                                all_true=false;
+	                        if (all_true) {
+	                            res = l_true; // sat
+	                            goto bailout;
+							} else
+								TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;);
+						}
+					}
+#endif
                     old_score = score;
                     new_const = (unsigned)-1;
                         
 					ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves);
-
+					if (!to_evaluate.size())
+					{
+						res = l_true;
+						goto bailout;
+					}
                     TRACE("sls_constants", tout << "Evaluating these constants: " << std::endl;
                                             for (unsigned i = 0 ; i < to_evaluate.size(); i++)
                                                 tout << to_evaluate[i]->get_name() << std::endl; );
@@ -525,9 +983,17 @@ class sls_tactic : public tactic {
                         case MV_INC: m_stats.m_incs++; break;
                         case MV_DEC: m_stats.m_decs++; break;
                         case MV_INV: m_stats.m_invs++; break;
+                        case MV_UMIN: m_stats.m_umins++; break;
+						case MV_MUL2: m_stats.m_mul2s++; break;
+						case MV_MUL3: m_stats.m_mul3s++; break;
+						case MV_DIV2: m_stats.m_div2s++; break;
                         }
                     
+#if _REAL_RS_ || _REAL_PBFS_
+						score = serious_score(g, fd, new_value);
+#else
 						score = incremental_score(g, fd, new_value);    
+#endif
 
                         TRACE("sls", tout << "Score distribution:"; 
                                         for (unsigned i = 0; i < g->size(); i++)
@@ -535,9 +1001,10 @@ class sls_tactic : public tactic {
                                         tout << " TOP: " << score << std::endl; );                        
                     }
 
-                    if (score >= 1.0) {
+                    if (score >= 0.99999) {
+//                    if (score >= 1.0) {
                         // score could theoretically be imprecise.
-						// Andreas: Can it only be imprecise in one direction?
+						// Andreas: it seems using top level score caching can make the score unprecise also in the other direction!
                         bool all_true = true;
                         for (unsigned i = 0; i < g->size() && all_true; i++)
                             if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
@@ -568,10 +1035,26 @@ class sls_tactic : public tactic {
 					// Andreas: Right now, a useless assignment is created in case of a restart. But we don't want to use restarts anyway.
                     //if (plateau_cnt < m_plateau_limit) {
                         TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl; );
+#if _INTENSIFICATION_
+						handle_plateau(g, score);
+						//handle_plateau(g);
+#else
 						m_evaluator.randomize_local(g, m_stats.m_moves);
+#endif
 						//mk_random_move(g);
                         score = top_score(g);
-                    //}
+
+	                    if (score >= 1.0) {
+	                        bool all_true = true;
+	                        for (unsigned i = 0; i < g->size() && all_true; i++)
+	                            if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
+	                                all_true=false;
+	                        if (all_true) {
+	                            res = l_true; // sat
+	                            goto bailout;
+                        } else
+                            TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;);
+                    }
                 }
             }
 
@@ -587,6 +1070,37 @@ class sls_tactic : public tactic {
                 return;
             }
 
+			verbose_stream() << "_BFS_ " << _BFS_ << std::endl;
+			verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl;
+			verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << 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;
+			verbose_stream() << "_VNS_ " << _VNS_ << std::endl;
+			verbose_stream() << "_WEIGHT_DIST_ " << _WEIGHT_DIST_ << std::endl;
+			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() << "_UCT_ " << _UCT_ << std::endl;
+			verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl;
+			verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << 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;
+			verbose_stream() << "_USE_UNARY_MINUS_ " << _USE_UNARY_MINUS_ << std::endl;
+			verbose_stream() << "_UNIFORM_RANDOM_ " << _UNIFORM_RANDOM_ << std::endl;
+			verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl;
+			verbose_stream() << "_REAL_PBFS_ " << _REAL_PBFS_ << std::endl;
+			verbose_stream() << "_SKIP_BITS_ " << _SKIP_BITS_ << std::endl;
+			verbose_stream() << "_PERC_CHANGE_ " << _PERC_CHANGE_ << std::endl;
+			verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << std::endl;
+			verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl;
+			verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl;
+			verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl;
+			
+#if _WEIGHT_DIST_ == 4
+					m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
+#endif
             m_tracker.initialize(g);
             lbool res = l_undef;
         
@@ -745,13 +1259,8 @@ 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),
-#if _CNF_
-						// Andreas: We will probably never use this. CNF sucks.
-                        mk_cnf_tactic(m, p));
-#else
 						// Andreas: How does a NNF actually look like? Can it contain ITE operators?
                         mk_nnf_tactic(m, p));
-#endif
 }
 
 tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {

src/tactic/sls/sls_tracker.h

@@ -31,18 +31,29 @@ class sls_tracker {
     mpz                   m_zero, m_one, m_two;
 	    
     struct value_score { 
-        value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { };
+#if _EARLY_PRUNE_
+		value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1), score_prune(0.0), has_pos_occ(0), has_neg_occ(0) { };
+#else
+		value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1) { };
+#endif
         ~value_score() { if (m) m->del(value); }
         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) {
             SASSERT(m == 0 || m == other.m);
             if (m) m->set(value, 0); else m = other.m;
             m->set(value, other.value);
             score = other.score;
             distance = other.distance;
+			touched = other.touched;
             return *this;
         }
     };
@@ -60,6 +71,20 @@ private:
     ptr_vector<func_decl> m_constants;
     ptr_vector<func_decl> m_temp_constants;
     occ_type              m_constants_occ;
+#if _UCT_
+	unsigned              m_touched;
+#endif
+#if _REAL_RS_ || _REAL_PBFS_
+	ptr_vector<expr>	  m_unsat_expr;
+	obj_map<expr, unsigned>	m_where_false;
+	expr**					m_list_false;
+#endif
+#if _CACHE_TOP_SCORE_
+	double				  m_top_sum;
+#endif
+#if _WEIGHT_DIST_ == 4
+	double				  m_weight_dist_factor;
+#endif
 
 public:    
     sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) :
@@ -79,6 +104,26 @@ public:
         m_mpz_manager.del(m_two);            
     }
 
+#if _WEIGHT_DIST_ == 4
+	inline void set_weight_dist_factor(double val) {
+		m_weight_dist_factor = val;
+	}
+#endif
+
+#if _CACHE_TOP_SCORE_
+	inline void adapt_top_sum(double add, double sub) {
+		m_top_sum += add - sub;
+	}
+
+	inline void set_top_sum(double new_score) {
+		m_top_sum = new_score;
+	}
+
+	inline double get_top_sum() {
+		return m_top_sum;
+	}
+#endif
+
     inline void set_value(expr * n, const mpz & r) {
         SASSERT(m_scores.contains(n));
         m_mpz_manager.set(m_scores.find(n).value, r);
@@ -123,6 +168,28 @@ public:
         return get_score(ep);
     }
 
+#if _EARLY_PRUNE_
+    inline void set_score_prune(expr * n, double score) {
+        SASSERT(m_scores.contains(n));
+        m_scores.find(n).score_prune = score;
+    }
+
+	inline double & get_score_prune(expr * n) {
+        SASSERT(m_scores.contains(n));
+        return m_scores.find(n).score_prune;
+    }
+
+	inline unsigned has_pos_occ(expr * n) {
+        SASSERT(m_scores.contains(n));
+        return m_scores.find(n).has_pos_occ;
+ 	}
+
+	inline unsigned has_neg_occ(expr * n) {
+        SASSERT(m_scores.contains(n));
+        return m_scores.find(n).has_neg_occ;
+ 	}
+#endif
+
     inline unsigned get_distance(expr * n) {
         SASSERT(m_scores.contains(n));
         return m_scores.find(n).distance;
@@ -297,7 +364,7 @@ public:
         for (unsigned i = 0; i < sz; i++) {
             expr * e = g->form(i);
 			// Andreas: Maybe not fully correct.
-#if _FOCUS_ == 2
+#if _FOCUS_ == 2 || _INTENSIFICATION_
 			initialize_recursive(e);
 #endif
             ptr_vector<func_decl> t;
@@ -310,8 +377,57 @@ public:
         calculate_expr_distances(g);
 
         TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); );
+
+#if _REAL_RS_ || _REAL_PBFS_
+		m_list_false = new expr*[sz];
+        for (unsigned i = 0; i < sz; i++)
+	  		if (m_mpz_manager.eq(get_value(g->form(i)),m_zero))
+				break_assertion(g->form(i));
+#endif
+
+#if _EARLY_PRUNE_
+        for (unsigned i = 0; i < sz; i++)
+	  		setup_occs(g->form(i));
+#endif
+
+#if _UCT_
+		m_touched = 1;
+#endif
     }
 
+#if _REAL_RS_ || _REAL_PBFS_
+	void make_assertion(expr * e)
+	{
+		if (m_where_false.contains(e))
+		{
+			unsigned pos = m_where_false.find(e);
+			m_where_false.erase(e);
+			if (pos != m_where_false.size())
+			{
+				expr * q = m_list_false[m_where_false.size()];
+				m_list_false[pos] = q;
+				m_where_false.find(q) = pos;
+			}
+//			printf("Going in %d\n", m_where_false.size());
+		}
+		//if (m_unsat_expr.contains(e))
+			//m_unsat_expr.erase(e);
+	}
+
+	void break_assertion(expr * e)
+	{
+		if (!m_where_false.contains(e))
+		{
+			unsigned pos = m_where_false.size();
+			m_list_false[pos] = e;
+			m_where_false.insert(e, pos);
+	//		printf("Going in %d\n", m_where_false.size());
+		}
+		//if (!m_unsat_expr.contains(e))
+			//m_unsat_expr.push_back(e);
+	}
+#endif
+
     void show_model(std::ostream & out) {
         unsigned sz = get_num_constants();
         for (unsigned i = 0; i < sz; i++) {
@@ -420,6 +536,41 @@ public:
         TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); );
     }              
 
+#if _EARLY_PRUNE_
+	void setup_occs(expr * n, bool negated = false) {
+		if (m_manager.is_bool(n))
+		{
+			if (m_manager.is_and(n) || m_manager.is_or(n))
+			{
+	            SASSERT(!negated);
+	            app * a = to_app(n);
+	            expr * const * args = a->get_args();
+	            for (unsigned i = 0; i < a->get_num_args(); i++)
+					setup_occs(args[i]);
+			}
+			else if (m_manager.is_not(n))
+			{
+	            SASSERT(!negated);
+	            app * a = to_app(n);
+	            SASSERT(a->get_num_args() == 1);
+	            expr * child = a->get_arg(0);
+	            if (m_manager.is_and(child) || m_manager.is_or(child))
+	                NOT_IMPLEMENTED_YET();
+				setup_occs(child, true);
+			}
+			else
+			{
+				if (negated)
+					m_scores.find(n).has_neg_occ = 1;
+				else
+					m_scores.find(n).has_pos_occ = 1;
+			}
+		}
+        else
+            NOT_IMPLEMENTED_YET();
+    }
+#endif
+
     double score_bool(expr * n, bool negated = false) {
         TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; );
 
@@ -648,6 +799,7 @@ public:
 #if _WEIGHT_DIST_
 		app * a = to_app(n);
 		family_id afid = a->get_family_id();
+
 		if (afid == m_bv_util.get_family_id())
 #endif
 #if _WEIGHT_DIST_ == 1
@@ -656,9 +808,10 @@ public:
 		res *= res;
 #elif _WEIGHT_DIST_ == 3
 		if (res < 1.0) res = 0.0;
+#elif _WEIGHT_DIST_ == 4
+		if (res < 1.0) res *= m_weight_dist_factor;
 #endif
 
-
         TRACE("sls_score", tout << "SCORE = " << res << std::endl; );
         return res;
     }
@@ -708,6 +861,44 @@ public:
             NOT_IMPLEMENTED_YET();
     }    
 
+	expr * get_unsat_expression(expr * e) {
+		if (m_manager.is_bool(e)) {
+			if (m_manager.is_and(e) || m_manager.is_or(e)) {
+				app * a = to_app(e);
+				expr * const * args = a->get_args();
+			    // Andreas: might be used for guided branching
+				//for (unsigned i = 0; i < a->get_num_args(); i++) {
+					//double cur = get_score(args[i]);
+				//}
+				// Andreas: A random number is better here since reusing flip will cause patterns.
+				unsigned int sz = a->get_num_args();
+				unsigned int pos = get_random_uint(16) % sz;
+				for (unsigned int i = pos; i < sz; i++) {
+	                expr * q = args[i];
+	                if (m_mpz_manager.neq(get_value(q), m_one))
+			            return get_unsat_expression(q);
+				}
+				for (unsigned int i = 0; i < pos; i++) {
+					expr * q = args[i];
+	                if (m_mpz_manager.neq(get_value(q), m_one))
+			            return get_unsat_expression(q);
+	            }
+	        }
+		}
+		return e;
+	}
+
+	ptr_vector<func_decl> & get_constants(expr * e) {
+        ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
+        unsigned sz = this_decls.size();
+        for (unsigned i = 0; i < sz; i++) {
+            func_decl * fd = this_decls[i];
+            if (!m_temp_constants.contains(fd))
+                m_temp_constants.push_back(fd);
+        }
+        return m_temp_constants;
+	}
+
 	ptr_vector<func_decl> & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) {
         for (unsigned i = 0; i < sz; i++) {
             expr * q = g->form(i);
@@ -743,7 +934,6 @@ public:
             // Andreas: I should probably fix this. If this is the case then the formula is SAT anyway but this is not checked in the first iteration.
 			if (!q)
 				return m_temp_constants;
-
 			ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
             unsigned sz2 = this_decls.size();
             for (unsigned j = 0; j < sz2; j++) {
@@ -754,6 +944,19 @@ public:
 	        return m_temp_constants;
 	}
 
+	ptr_vector<func_decl> & get_unsat_constants_walksat(expr * e) {
+			if (!e)
+				return m_temp_constants;
+			ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
+            unsigned sz = this_decls.size();
+            for (unsigned j = 0; j < sz; j++) {
+                func_decl * fd = this_decls[j];
+                if (!m_temp_constants.contains(fd))
+                    m_temp_constants.push_back(fd);
+            }
+	        return m_temp_constants;
+	}
+
 	ptr_vector<func_decl> & go_deeper(expr * e) {
 			if (m_manager.is_bool(e)) {
 				if (m_manager.is_and(e)) {
@@ -816,40 +1019,134 @@ public:
         unsigned sz = g->size();
 
         if (sz == 1) {
+			if (m_mpz_manager.eq(get_value(g->form(0)), m_one))
+				return m_temp_constants;
+			else
 	            return get_constants();
         }
         else {
             m_temp_constants.reset();
 #if _FOCUS_ == 1
-#if _BFS_ == 3
+#if _UCT_
-			unsigned int pos = 0;
+			unsigned pos = -1;
-			double max = get_score(g->form(0));
+			value_score vscore;
-            unsigned sz = g->size();
+#if _PROBABILISTIC_UCT_
-            for (unsigned i = 1; i < sz; i++) {
+			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 (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);
+                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); 
+				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);
+				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 m_temp_constants;
+
+#if _UCT_ == 1
+			m_scores.find(g->form(pos)).touched++;
+			m_touched++;
+#elif _UCT_ == 2
+			m_scores.find(g->form(pos)).touched = flip; 
+#endif
+			expr * e = 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 m_temp_constants;
+			expr * e = g->form(pos);
 #elif _BFS_ == 2
-			unsigned int pos = 0;
+			unsigned int pos = -1;
-			double min = get_score(g->form(0));
+			double min = 2.0;
-            unsigned sz = g->size();
+            for (unsigned i = 0; i < sz; i++) {
-            for (unsigned i = 1; 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 m_temp_constants;
+			expr * e = g->form(pos);
 #elif _BFS_ == 1
-			unsigned int pos = flip % m_constants.size();
+			// I guess it was buggy ...
+			// unsigned int pos = flip % m_constants.size();
+			unsigned int pos = flip % sz;
+			expr * e = 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 m_temp_constants;
+			expr * e = 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 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];
+			//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)
+				return m_temp_constants;
+			else
+				expr * e = m_list_false[flip % sz];
 #else
-			unsigned int pos = get_random_uint(16) % m_constants.size();
+			// I guess it was buggy ...
+			// unsigned int pos = get_random_uint(16) % m_constants.size();
+			unsigned int pos = get_random_uint(16) % sz;
+			expr * e = get_unsat_assertion(g, sz, pos);
 #endif
-			return get_unsat_constants_walksat(g, sz, pos);
+			return get_unsat_constants_walksat(e);
 #elif _FOCUS_ == 2
 #if _BFS_
-			unsigned int pos = flip % m_constants.size();
+			// I guess it was buggy ...
+			// unsigned int pos = flip % m_constants.size();
+			unsigned int pos = flip % sz;
 #else
-			unsigned int pos = get_random_uint(16) % m_constants.size();
+			// I guess it was buggy ...
+			// unsigned int pos = get_random_uint(16) % m_constants.size();
+			unsigned int pos = get_random_uint(16) % sz;
 #endif
 			return get_unsat_constants_crsat(g, sz, pos);
 #else

versions/z3-wsat-0.01.txt

@@ -10,3 +10,5 @@ No restarts.
 #define _TIMELIMIT_ 300
 #define _SCORE_AND_AVG_ 0
 #define _SCORE_OR_MUL_ 0
+
+BUGGY VERSION! Uses wrong value for modulo operation in assertion selection.

versions/z3-wsat-0.01b.txt

@@ -10,3 +10,5 @@ No restarts.
 #define _TIMELIMIT_ 300
 #define _SCORE_AND_AVG_ 0
 #define _SCORE_OR_MUL_ 0
+
+BUGGY VERSION! Uses wrong value for modulo operation in assertion selection.