git.libre-soc.org Git - cvc5.git/commit

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Wed, 17 Aug 2011 15:20:19 +0000 (15:20 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Wed, 17 Aug 2011 15:20:19 +0000 (15:20 +0000)
commit	32e1d3558f17d12f2631175776209a5f8cabbdd9
tree	ebc20658d5375b17f13b5c83d3dc7ee078029f96	tree
parent	41dc1b3685b9258660dab571f8f8b56deb0fb095	commit \| diff

new implementation of lemmas on demand
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>

14 files changed:

src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/core/SolverTypes.h		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/sat.cpp		diff \| blob \| history
src/prop/sat.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
test/unit/prop/cnf_stream_black.h		diff \| blob \| history