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

author	Morgan Deters <mdeters@gmail.com>
	Sat, 29 Oct 2011 05:21:49 +0000 (05:21 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Sat, 29 Oct 2011 05:21:49 +0000 (05:21 +0000)
commit	02f4f0500849bc719cb45bbc771bea90eb6e96f8
tree	6df8a696dba89732dc17d30e80b1d326edf36a5c	tree
parent	b695ce10f294b2469434656fb2c5dc8e6d701c5d	commit \| diff

Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof(), a few other things..

18 files changed:

src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/proof/proof.h		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/sat_proof.cpp		diff \| blob \| history
src/proof/sat_proof.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/proof.h	[new file with mode: 0644]	blob
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/boolean.cvc		diff \| blob \| history
test/regress/regress0/hole6.cvc		diff \| blob \| history
test/regress/regress0/wiki.05.cvc		diff \| blob \| history
test/regress/run_regression		diff \| blob \| history