na

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

cmake/msvc_legacy_quirks.cmake

@@ -183,7 +183,5 @@ foreach (_build_type ${_build_types_as_upper})
     # See https://msdn.microsoft.com/en-us/library/ms235442.aspx
     string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /NXCOMPAT")
 
-    # per GitHub issue #2380, enable checksum
-    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /RELEASE")
   endif()
 endforeach()

src/sat/sat_config.cpp

@@ -61,9 +61,10 @@ namespace sat {
         else if (s == symbol("random"))
             m_phase = PS_RANDOM;
         else
-            throw sat_param_exception("invalid phase selection strategy");
+            throw sat_param_exception("invalid phase selection strategy: always_false, always_true, basic_caching, caching, random");
 
         m_rephase_base      = p.rephase_base();
+        m_reorder_base      = p.reorder_base();
         m_search_sat_conflicts = p.search_sat_conflicts();
         m_search_unsat_conflicts = p.search_unsat_conflicts();
         m_phase_sticky      = p.phase_sticky();

src/sat/sat_config.h

@@ -91,6 +91,7 @@ namespace sat {
         unsigned           m_search_unsat_conflicts;
         bool               m_phase_sticky;
         unsigned           m_rephase_base;
+        unsigned           m_reorder_base;
         bool               m_propagate_prefetch;
         restart_strategy   m_restart;
         bool               m_restart_fast;

src/sat/sat_params.pyg

@@ -7,6 +7,7 @@ def_module_params('sat',
                           ('search.unsat.conflicts', UINT, 400, 'period for solving for unsat (in number of conflicts)'),
                           ('search.sat.conflicts', UINT, 400, 'period for solving for sat (in number of conflicts)'),
 	                  ('rephase.base', UINT, 1000, 'number of conflicts per rephase '),                          
+	                  ('reorder.base', UINT, UINT_MAX, 'number of conflicts per random reorder '),                          
                           ('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
                           ('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'),
                           ('restart.initial', UINT, 2, 'initial restart (number of conflicts)'),

src/sat/sat_solver.cpp

@@ -1230,6 +1230,7 @@ namespace sat {
                 else if (do_cleanup(false)) continue;
                 else if (should_gc()) do_gc();
                 else if (should_rephase()) do_rephase();
+                else if (should_reorder()) do_reorder();
                 else if (should_restart()) do_restart(!m_config.m_restart_fast);
                 else if (should_simplify()) do_simplify();
                 else if (!decide()) is_sat = final_check();
@@ -1806,6 +1807,8 @@ namespace sat {
         m_best_phase_size         = 0;
         m_rephase_lim             = 0;
         m_rephase_inc             = 0;
+        m_reorder_lim             = 0;
+        m_reorder_inc             = 0;
         m_conflicts_since_restart = 0;
         m_force_conflict_analysis = false;
         m_restart_threshold       = m_config.m_restart_initial;
@@ -3146,6 +3149,25 @@ namespace sat {
         m_rephase_lim += m_rephase_inc;
     }
 
+    bool solver::should_reorder() {
+        return m_conflicts_since_init > m_reorder_lim;
+    }
+
+    void solver::do_reorder() {
+        IF_VERBOSE(1, verbose_stream() << "(reorder)\n");
+        m_activity_inc = 128;
+        svector<bool_var> vars;
+        for (bool_var v = num_vars(); v-- > 0; ) {
+            vars.push_back(v);
+        }
+        shuffle(vars.size(), vars.c_ptr(), m_rand);
+        for (bool_var v : vars) {
+            update_activity(v, m_rand(10));
+        }
+        m_reorder_inc += m_config.m_reorder_base;
+        m_reorder_lim += m_reorder_inc;
+    }
+
     void solver::updt_phase_counters() {
         m_phase_counter++;
         if (should_toggle_search_state()) {

src/sat/sat_solver.h

@@ -146,6 +146,8 @@ namespace sat {
         unsigned                m_best_phase_size;
         unsigned                m_rephase_lim;
         unsigned                m_rephase_inc;
+        unsigned                m_reorder_lim;
+        unsigned                m_reorder_inc;
         var_queue               m_case_split_queue;
         unsigned                m_qhead;
         unsigned                m_scope_lvl;
@@ -562,6 +564,8 @@ namespace sat {
         bool is_two_phase() const;
         bool should_rephase();
         void do_rephase();
+        bool should_reorder();
+        void do_reorder();
         svector<char> m_diff_levels;
         unsigned num_diff_levels(unsigned num, literal const * lits);
         bool     num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue);

src/smt/theory_seq.cpp

@@ -5961,7 +5961,7 @@ void theory_seq::add_lt_axiom(expr* n) {
     add_axiom(lt, eq, e1xcy);
     add_axiom(lt, eq, emp2, ltdc);
     add_axiom(lt, eq, emp2, e2xdz);
-    if (e1->get_id() <= e2->get_id()) {
+    if (e1->get_id() <= e2->get_id() || true) {
         literal gt = mk_literal(m_util.str.mk_lex_lt(e2, e1));
         add_axiom(lt, eq, gt);
         add_axiom(~eq, ~lt);