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

author	Alex Ozdemir <aozdemir@hmc.edu>
	Sat, 16 Mar 2019 01:51:47 +0000 (18:51 -0700)
committer	Andres Noetzli <andres.noetzli@gmail.com>
	Sat, 16 Mar 2019 01:51:47 +0000 (01:51 +0000)
commit	5d0a5a729680a1db3f44e31037955390e86440ce
tree	d2f85ff47f75935439a14f514a5133d1dd6d5cad	tree
parent	2989780f0242d14712927bd4c01c4a521a8fe399	commit \| diff

Enable CryptoMiniSat-backed BV proofs (#2847)

* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
* Specifically, CNF proofs broke when proving tautological clauses.
Now they don't.

20 files changed:

proofs/signatures/CMakeLists.txt		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/options/bv_options.toml		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/proof/bitvector_proof.cpp		diff \| blob \| history
src/proof/bitvector_proof.h		diff \| blob \| history
src/proof/clausal_bitvector_proof.cpp		diff \| blob \| history
src/proof/clausal_bitvector_proof.h		diff \| blob \| history
src/proof/cnf_proof.cpp		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/drat/drat_proof.cpp		diff \| blob \| history
src/proof/er/er_proof.cpp		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
test/regress/regress0/bv/ackermann2.smt2		diff \| blob \| history
test/regress/regress0/bv/core/slice-12.smt		diff \| blob \| history
test/regress/regress0/bv/temp.lrat	[new file with mode: 0644]	blob
test/unit/proof/drat_proof_black.h		diff \| blob \| history
test/unit/proof/lrat_proof_black.h		diff \| blob \| history

RSS Atom