From c6fbe38f780e9b45bcafea816d22bf52dae91b0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Jun 2017 23:56:50 -0500 Subject: [PATCH] disable anti-exploration by default Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Solver.cs | 8 ++++++++ src/sat/sat_config.cpp | 2 +- src/sat/sat_params.pyg | 3 ++- src/sat/sat_solver.cpp | 4 ++-- 4 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index d2c63ecce..40da086ce 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -196,6 +196,14 @@ namespace Microsoft.Z3 } } + /// + /// Assert a lemma (or multiple) into the solver. + /// + public void AddLemma(IEnumerable constraints) + { + AssertLemma(constraints.ToArray()); + } + /// /// The number of assertions in the solver. /// diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 3d803d164..559317976 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -141,7 +141,7 @@ namespace sat { else { throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'"); } - m_anti_exploration = m_branching_heuristic != BH_VSIDS; + m_anti_exploration = p.branching_anti_exploration(); m_step_size_init = 0.40; m_step_size_dec = 0.000001; m_step_size_min = 0.06; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index c60ceee07..211b3b2bd 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -10,6 +10,7 @@ def_module_params('sat', ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), + ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), ('random_seed', UINT, 0, 'random seed'), ('burst_search', UINT, 100, 'number of conflicts before first global simplification'), @@ -22,7 +23,7 @@ def_module_params('sat', ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('core.minimize', BOOL, False, 'minimize computed core'), - ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('threads', UINT, 1, 'number of parallel threads to use'), + ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('threads', UINT, 1, 'number of parallel threads to use'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.check', BOOL, False, 'build up internal proof and check'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 36cf9b526..0341b9269 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1194,9 +1194,9 @@ namespace sat { return l_true; if (!resolve_conflict()) return l_false; - if (m_conflicts > m_config.m_max_conflicts) + if (m_conflicts > m_config.m_max_conflicts) return l_undef; - if (m_conflicts_since_restart > m_restart_threshold) + if (m_conflicts_since_restart > m_restart_threshold) return l_undef; if (at_base_lvl()) { cleanup(); // cleaner may propagate frozen clauses