diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-10 17:23:29 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-10 17:23:29 +0000 |
| commit | abc169cbdba1d3fdc1400f74a4c93b747cae0575 (patch) | |
| tree | 3ee268f17d5f9787d66fe9a4c3509e4edd04113a | |
| parent | 8f5e1c68701aa2a805fe656f5c580fc74b310606 (diff) | |
changing the sat solver remove clauses constants
with these we get closer to yices on uf and it seems better on lra
vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471
vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 1ec9b0962..8e98f32c0 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -75,7 +75,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo // Parameters (the rest): // - , learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + , learntsize_factor(1), learntsize_inc(1.5) // Parameters (experimental): // |