diff options
| author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
| commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
| tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/prop/cnf_stream.cpp | |
| parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) | |
squash-merge from proof branch
Diffstat (limited to 'src/prop/cnf_stream.cpp')
| -rw-r--r-- | src/prop/cnf_stream.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9bc352f9b..7409c7222 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -674,7 +674,8 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, - TNode from) { + TNode from, + theory::TheoryId ownerTheory) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -684,6 +685,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; + d_cnfProof->setExplainerTheory(ownerTheory); if (proof_id != RULE_INVALID) { d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion); d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id); @@ -695,7 +697,10 @@ void TseitinCnfStream::convertAndAssert(TNode node, }); convertAndAssert(node, negated); - PROOF(if (d_cnfProof) d_cnfProof->popCurrentAssertion(); ); + PROOF + (if (d_cnfProof) { + d_cnfProof->popCurrentAssertion(); + }); } void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { |