From abc169cbdba1d3fdc1400f74a4c93b747cae0575 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sun, 10 Jul 2011 17:23:29 +0000 Subject: [PATCH] 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 --- src/prop/minisat/core/Solver.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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): // -- 2.30.2