summaryrefslogtreecommitdiff
path: root/src/proof/cnf_proof.cpp
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2011-10-28 19:24:38 +0000
committerLiana Hadarean <lianahady@gmail.com>2011-10-28 19:24:38 +0000
commitb084a7efa9d65ec2f7475caa8486f8fd4cbafbd5 (patch)
treee118097c88787b7f2899bb8b2cbf865d058ef6bf /src/proof/cnf_proof.cpp
parent9547a48a7cdab8786c080779930de9c39655c52b (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.
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r--src/proof/cnf_proof.cpp9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
new file mode 100644
index 000000000..2bf146661
--- /dev/null
+++ b/src/proof/cnf_proof.cpp
@@ -0,0 +1,9 @@
+#include "cnf_proof.h"
+using namespace CVC4::prop;
+
+namespace CVC4 {
+CnfProof::CnfProof(CnfStream* stream) :
+ d_cnfStream(stream) {}
+
+
+} /* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback