From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sun, 10 Jul 2011 17:23:29 +0000 (+0000)
Subject: changing the sat solver remove clauses constants
X-Git-Tag: cvc5-1.0.0~8511
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=abc169cbdba1d3fdc1400f74a4c93b747cae0575;p=cvc5.git

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
---

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):
     //