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

author	Guy <katz911@gmail.com>
	Wed, 23 Mar 2016 19:07:59 +0000 (12:07 -0700)
committer	Guy <katz911@gmail.com>
	Wed, 23 Mar 2016 19:07:59 +0000 (12:07 -0700)
commit	aa9aa46b77f048f2865c29e40ed946371fd115ef
tree	254f392449a03901f7acb7a65e9499193d07ac9a	tree
parent	786cd2dd5b1c53f650c891d6dfbf299a62840848	commit \| diff

squash-merge from proof branch

51 files changed:

proofs/signatures/Makefile.am		diff \| blob \| history
proofs/signatures/example-arrays.plf		diff \| blob \| history
proofs/signatures/th_arrays.plf		diff \| blob \| history
proofs/signatures/th_base.plf		diff \| blob \| history
proofs/signatures/th_int.plf	[new file with mode: 0644]	blob
proofs/signatures/th_lra.plf	[new file with mode: 0644]	blob
proofs/signatures/th_real.plf	[new file with mode: 0644]	blob
src/Makefile.am		diff \| blob \| history
src/options/bv_options		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/arith_proof.cpp	[new file with mode: 0644]	blob
src/proof/arith_proof.h	[new file with mode: 0644]	blob
src/proof/array_proof.cpp	[new file with mode: 0644]	blob
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/proof_manager.cpp		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/sat_proof.h		diff \| blob \| history
src/proof/sat_proof_implementation.h		diff \| blob \| history
src/proof/skolemization_manager.cpp	[new file with mode: 0644]	blob
src/proof/skolemization_manager.h	[new file with mode: 0644]	blob
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/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_check_proof.cpp		diff \| blob \| history
src/theory/arrays/array_info.cpp		diff \| blob \| history
src/theory/arrays/array_info.h		diff \| blob \| history
src/theory/arrays/kinds		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.h		diff \| blob \| history
src/theory/bv/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/theory.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_types.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history

RSS Atom