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

author	Guy <katz911@gmail.com>
	Thu, 2 Jun 2016 00:46:24 +0000 (17:46 -0700)
committer	Guy <katz911@gmail.com>
	Thu, 2 Jun 2016 00:46:24 +0000 (17:46 -0700)
commit	4dac1ec234ee0d0885f058b4b35a7eeba2ca5007
tree	aae1792c05c0a67c521160226deb451ca861822c	tree
parent	de0dd1dc966b05467f1a5443ff33094262f5076a	commit \| diff

Merge from proof branch

50 files changed:

proofs/signatures/th_arrays.plf		diff \| blob \| history
proofs/signatures/th_bv.plf		diff \| blob \| history
proofs/signatures/th_bv_bitblast.plf		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/options/Makefile.am		diff \| blob \| history
src/proof/arith_proof.cpp		diff \| blob \| history
src/proof/arith_proof.h		diff \| blob \| history
src/proof/array_proof.cpp		diff \| blob \| history
src/proof/array_proof.h		diff \| blob \| history
src/proof/bitvector_proof.cpp		diff \| blob \| history
src/proof/bitvector_proof.h		diff \| blob \| history
src/proof/cnf_proof.cpp		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/lemma_proof.cpp	[new file with mode: 0644]	blob
src/proof/lemma_proof.h	[new file with mode: 0644]	blob
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/proof_output_channel.cpp	[new file with mode: 0644]	blob
src/proof/proof_output_channel.h	[new file with mode: 0644]	blob
src/proof/proof_utils.cpp		diff \| blob \| history
src/proof/proof_utils.h		diff \| blob \| history
src/proof/sat_proof_implementation.h		diff \| blob \| history
src/proof/skolemization_manager.h		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
src/proof/theory_proof.h		diff \| blob \| history
src/proof/uf_proof.cpp		diff \| blob \| history
src/proof/uf_proof.h		diff \| blob \| history
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/minisat.cpp		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine_check_proof.cpp		diff \| blob \| history
src/theory/arrays/array_proof_reconstruction.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/abstraction.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
test/regress/regress0/aufbv/Makefile.am		diff \| blob \| history

RSS Atom