From cd93cdd819155da8b6fc98127f63512e042e6d08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 Jul 2019 14:40:20 +0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- cmake/msvc_legacy_quirks.cmake | 2 -- src/sat/sat_config.cpp | 3 ++- src/sat/sat_config.h | 1 + src/sat/sat_params.pyg | 1 + src/sat/sat_solver.cpp | 22 ++++++++++++++++++++++ src/sat/sat_solver.h | 4 ++++ src/smt/theory_seq.cpp | 2 +- 7 files changed, 31 insertions(+), 4 deletions(-) diff --git a/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake index 09ee90d2a..0831346ab 100644 --- a/cmake/msvc_legacy_quirks.cmake +++ b/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() diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 5e903ecce..76fb1d3a3 100644 --- a/src/sat/sat_config.cpp +++ b/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(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 0c1eb48cc..86835b073 100644 --- a/src/sat/sat_config.h +++ b/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; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 59738db5c..7fefb7711 100644 --- a/src/sat/sat_params.pyg +++ b/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)'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0a6722b04..722b91b26 100644 --- a/src/sat/sat_solver.cpp +++ b/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 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()) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index a44b91749..f817cb190 100644 --- a/src/sat/sat_solver.h +++ b/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 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); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e51082ab7..8a29648e9 100644 --- a/src/smt/theory_seq.cpp +++ b/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);