Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls

Conflicts:
	src/tactic/sls/sls_tactic.cpp

src/tactic/sls/sls_compilation_settings.h

@@ -0,0 +1,168 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sls_compilation_constants.h
+
+Abstract:
+
+    Stochastic Local Search (SLS) compilation constants
+
+Author:
+
+    Christoph (cwinter) 2014-03-19
+
+Notes:
+
+    This file should go away completely once we have evaluated all options.
+
+--*/
+
+#ifndef _SLS_COMPILATION_SETTINGS_H_
+#define _SLS_COMPILATION_SETTINGS_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
+#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
+
+// 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, 1 = use #moves, 2 = use #plateaus, 3 = use time
+#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, 5 = minisat
+#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
+
+// 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
+
+// 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_ 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_ 1
+
+// how much diversification is used in the UCT-scheme?
+#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
+
+// do we gradually reduce the touched values of _UCT_?
+#define _UCT_FORGET_ 0
+#define _UCT_FORGET_FACTOR_ 0.5
+
+// shall we use addition/subtraction?
+#define _USE_ADDSUB_ 1
+
+// shall we try multilication and division by 2?
+#define _USE_MUL2DIV2_ 0
+
+// shall we try multiplication by 3?
+#define _USE_MUL3_ 0
+
+// shall we try unary minus (= inverting and incrementing)
+#define _USE_UNARY_MINUS_ 0
+
+// is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0
+#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
+#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 ((_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
+
+#endif

src/tactic/sls/sls_engine.h

@@ -0,0 +1,159 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sls_engine.h
+
+Abstract:
+
+    A Stochastic Local Search (SLS) engine
+
+Author:
+
+    Christoph (cwinter) 2014-03-19
+
+Notes:
+
+--*/
+#ifndef _SLS_ENGINE_H_
+#define _SLS_ENGINE_H_
+
+#include"stopwatch.h"
+#include"lbool.h"
+#include"model_converter.h"
+
+#include"sls_compilation_settings.h"
+#include"sls_tracker.h"
+#include"sls_evaluator.h"
+
+class sls_engine {
+public:
+    class stats {
+    public:
+        unsigned        m_restarts;
+        stopwatch       m_stopwatch;
+        unsigned        m_full_evals;
+        unsigned        m_incr_evals;
+        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),
+            m_invs(0) {
+            m_stopwatch.reset();
+            m_stopwatch.start();
+        }
+        void reset() {
+            m_full_evals = m_flips = m_incr_evals = 0;
+            m_stopwatch.reset();
+            m_stopwatch.start();
+        }
+    };
+
+protected:
+    ast_manager   & m_manager;
+    stats           m_stats;
+    unsynch_mpz_manager m_mpz_manager;
+    powers          m_powers;
+    mpz             m_zero, m_one, m_two;
+    bool            m_produce_models;
+    volatile bool   m_cancel;
+    bv_util         m_bv_util;
+    sls_tracker     m_tracker;
+    sls_evaluator   m_evaluator;
+
+    unsigned		m_restart_limit;
+    unsigned        m_max_restarts;
+    unsigned        m_plateau_limit;
+
+    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;
+
+public:    
+    sls_engine(ast_manager & m, params_ref const & p);
+    ~sls_engine();
+
+    ast_manager & m() const { return m_manager; }
+
+    void set_cancel(bool f) { m_cancel = f; }
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
+
+    void updt_params(params_ref const & _p);
+
+    stats const & get_stats(void) { return m_stats; }
+    void reset_statistics(void) { m_stats.reset(); }    
+
+    bool full_eval(goal_ref const & g, model & mdl);
+    
+
+    void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result);
+    void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result);
+    void mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result);
+    void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented);
+    void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented);
+    void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
+    void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);    
+
+    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);
+    
+    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);
+    
+    
+    
+    bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp,
+                 double & best_score, mpz & best_value, unsigned i);
+    
+    double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i);
+    
+
+    lbool search(goal_ref const & g);    
+
+    void operator()(goal_ref const & g, model_converter_ref & mc);
+
+protected:
+    void checkpoint();
+    lbool search_old(goal_ref const & g);
+    double get_restart_armin(unsigned cnt_restarts);    
+
+    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);
+
+    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);
+
+    double top_score(goal_ref const & g);
+    double rescore(goal_ref const & g);
+    double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
+    double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
+
+#if _EARLY_PRUNE_
+    double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value);
+#endif
+
+    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);
+
+    void mk_random_move(ptr_vector<func_decl> & unsat_constants);
+    void mk_random_move(goal_ref const & g);
+
+    bool handle_plateau(goal_ref const & g);
+    bool handle_plateau(goal_ref const & g, double old_score);
+
+    inline unsigned check_restart(unsigned curr_value);
+};
+
+#endif

src/tactic/sls/sls_evaluator.h

@@ -20,6 +20,9 @@ Notes:
 #ifndef _SLS_EVALUATOR_H_
 #define _SLS_EVALUATOR_H_
 
+#include"model_evaluator.h"
+
+#include"sls_compilation_settings.h"
 #include"sls_powers.h"
 #include"sls_tracker.h"
 

src/tactic/sls/sls_tracker.h

@@ -20,6 +20,12 @@ Notes:
 #ifndef _SLS_TRACKER_H_
 #define _SLS_TRACKER_H_
 
+#include"goal.h"
+#include"model.h"
+
+#include"sls_compilation_settings.h"
+#include"sls_powers.h"
+
 class sls_tracker {
     ast_manager         & m_manager;
     unsynch_mpz_manager & m_mpz_manager;
@@ -1201,7 +1207,7 @@ public:
 //                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); 
+                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched)/vscore.touched); 
 #elif _UCT_ == 2
                 double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; 
 #elif _UCT_ == 3
@@ -1351,7 +1357,7 @@ public:
 //                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); 
+                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched);
 #elif _UCT_ == 2
             double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; 
 #elif _UCT_ == 3