mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

disable anti-exploration by default

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-19 23:56:50 -05:00
parent ce592d7716
commit c6fbe38f78
4 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/dotnet/Solver.cs
View file

@ -196,6 +196,14 @@ namespace Microsoft.Z3
} }
} }
/// <summary>
/// Assert a lemma (or multiple) into the solver.
/// </summary>
public void AddLemma(IEnumerable<BoolExpr> constraints)
{
AssertLemma(constraints.ToArray());
}
/// <summary> /// <summary>
/// The number of assertions in the solver. /// The number of assertions in the solver.
/// </summary> /// </summary>

2
src/sat/sat_config.cpp
View file

@ -141,7 +141,7 @@ namespace sat {
else { else {
throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'"); 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_init = 0.40;
m_step_size_dec = 0.000001; m_step_size_dec = 0.000001;
m_step_size_min = 0.06; m_step_size_min = 0.06;

3
src/sat/sat_params.pyg
View file

@ -10,6 +10,7 @@ def_module_params('sat',
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), ('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_freq', DOUBLE, 0.01, 'frequency of random case splits'),
('random_seed', UINT, 0, 'random seed'), ('random_seed', UINT, 0, 'random seed'),
('burst_search', UINT, 100, 'number of conflicts before first global simplification'), ('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'), ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
('core.minimize', BOOL, False, 'minimize computed core'), ('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'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
('drat.check', BOOL, False, 'build up internal proof and check'), ('drat.check', BOOL, False, 'build up internal proof and check'),

4
src/sat/sat_solver.cpp
View file

@ -1194,9 +1194,9 @@ namespace sat {
return l_true; return l_true;
if (!resolve_conflict()) if (!resolve_conflict())
return l_false; return l_false;
if (m_conflicts > m_config.m_max_conflicts) if (m_conflicts > m_config.m_max_conflicts)
return l_undef; return l_undef;
if (m_conflicts_since_restart > m_restart_threshold) if (m_conflicts_since_restart > m_restart_threshold)
return l_undef; return l_undef;
if (at_base_lvl()) { if (at_base_lvl()) {
cleanup(); // cleaner may propagate frozen clauses cleanup(); // cleaner may propagate frozen clauses