projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8f5e1c6) | patch
changing the sat solver remove clauses constants
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Sun, 10 Jul 2011 17:23:29 +0000 (17:23 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Sun, 10 Jul 2011 17:23:29 +0000 (17:23 +0000)
commitabc169cbdba1d3fdc1400f74a4c93b747cae0575
tree3ee268f17d5f9787d66fe9a4c3509e4edd04113atree
parent8f5e1c68701aa2a805fe656f5c580fc74b310606commit | 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
src/prop/minisat/core/Solver.cc diff | blob | history