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

author	Liana Hadarean <lianahady@gmail.com>
	Fri, 28 Oct 2011 19:24:38 +0000 (19:24 +0000)
committer	Liana Hadarean <lianahady@gmail.com>
	Fri, 28 Oct 2011 19:24:38 +0000 (19:24 +0000)
commit	b084a7efa9d65ec2f7475caa8486f8fd4cbafbd5
tree	e118097c88787b7f2899bb8b2cbf865d058ef6bf	tree
parent	9547a48a7cdab8786c080779930de9c39655c52b	commit \| diff

merged the proofgen3 branch into trunk:
    - can now output LFSC checkable resolution proofs
    - added configuration option  --enable-proof
    - added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof.

25 files changed:

config/build-type		diff \| blob \| history
config/cvc4.m4		diff \| blob \| history
configure.ac		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/main/usage.h		diff \| blob \| history
src/proof/Makefile	[new file with mode: 0644]	blob
src/proof/Makefile.am	[new file with mode: 0644]	blob
src/proof/cnf_proof.cpp	[new file with mode: 0644]	blob
src/proof/cnf_proof.h	[new file with mode: 0644]	blob
src/proof/proof.h	[new file with mode: 0644]	blob
src/proof/proof_manager.cpp	[new file with mode: 0644]	blob
src/proof/proof_manager.h	[new file with mode: 0644]	blob
src/proof/sat_proof.cpp	[new file with mode: 0644]	blob
src/proof/sat_proof.h	[new file with mode: 0644]	blob
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/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/util/configuration.cpp		diff \| blob \| history
src/util/configuration.h		diff \| blob \| history
src/util/configuration_private.h		diff \| blob \| history
src/util/options.cpp		diff \| blob \| history
src/util/options.h		diff \| blob \| history

RSS Atom