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

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Tue, 9 Nov 2010 21:57:06 +0000 (21:57 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Tue, 9 Nov 2010 21:57:06 +0000 (21:57 +0000)
commit	df5f7fe03fda041429548bcb39abb8916ca2e291
tree	46b08f3e35ee9c3d4c551d82f3e7e36582383f39	tree
parent	1f07775e9205b3f9e172a1ad218a9015b7265b58	commit \| diff

Lemmas on demand work, push-pop, some cleanup.

41 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/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/bitvector.cpp	[deleted file]	blob \| history
src/util/bitvector.h		diff \| blob \| history
src/util/integer_cln_imp.cpp	[deleted file]	blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.cpp	[deleted file]	blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/options.cpp		diff \| blob \| history
src/util/options.h		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/lemmas/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/fischer3-mutex-16.smt	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/fs_not_sc_seen.induction.smt	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/mode_cntrl.induction.smt	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/pursuit-safety-8.smt	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt	[new file with mode: 0644]	blob
test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/test.00.cvc	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/test.01.cvc	[new file with mode: 0644]	blob
test/unit/prop/cnf_stream_black.h		diff \| blob \| history
test/unit/theory/theory_arith_white.h		diff \| blob \| history

RSS Atom