From: Dejan Jovanović Date: Fri, 20 Aug 2010 18:23:53 +0000 (+0000) Subject: updating the minisat restart parameters after running some experiments X-Git-Tag: cvc5-1.0.0~8882 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=314e777887f32c8cf656dbc56f370da6dd0bf76e;p=cvc5.git updating the minisat restart parameters after running some experiments --- diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 39978ab5e..e8efe3d03 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -42,8 +42,8 @@ static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls confl static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true); -static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); -static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false)); +static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 25, IntRange(1, INT32_MAX)); +static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false)); static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); diff --git a/src/prop/sat.h b/src/prop/sat.h index 8581cd9a0..7229b3565 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -233,8 +233,6 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_minisat = new Minisat::SimpSolver(this, d_context); // Setup the verbosity d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1; - // Do not delete the satisfied clauses, just the learnt ones - d_minisat->remove_satisfied = false; // No random choices if(Debug.isOn("no_rnd_decisions")){