summaryrefslogtreecommitdiff
path: root/src/proof/arith_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/arith_proof.cpp')
-rw-r--r--src/proof/arith_proof.cpp173
1 files changed, 93 insertions, 80 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 03de1ca4f..dd3ac0bde 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -14,12 +14,14 @@
** \todo document this file
**/
+#include "proof/arith_proof.h"
+
+#include <memory>
+#include <stack>
-#include "proof/theory_proof.h"
#include "proof/proof_manager.h"
-#include "proof/arith_proof.h"
+#include "proof/theory_proof.h"
#include "theory/arith/theory_arith.h"
-#include <stack>
namespace CVC4 {
@@ -70,56 +72,64 @@ void ProofArith::toStream(std::ostream& out) {
Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl;
//AJR : carry this further?
ProofLetMap map;
- toStreamLFSC(out, ProofManager::getArithProof(), d_proof, map);
+ toStreamLFSC(out, ProofManager::getArithProof(), *d_proof, map);
}
-void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) {
+void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf,
+ const ProofLetMap& map) {
Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl;
- pf->debug_print("lfsc-arith");
+ pf.debug_print("lfsc-arith");
Debug("lfsc-arith") << std::endl;
- toStreamRecLFSC( out, tp, pf, 0, map );
+ toStreamRecLFSC(out, tp, pf, 0, map);
}
-Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) {
- Debug("pf::arith") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
- pf->debug_print("pf::arith");
+Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf, unsigned tb,
+ const ProofLetMap& map) {
+ Debug("pf::arith") << std::endl
+ << std::endl
+ << "toStreamRecLFSC called. tb = " << tb
+ << " . proof:" << std::endl;
+ pf.debug_print("pf::arith");
Debug("pf::arith") << std::endl;
if(tb == 0) {
- Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.size() >= 2);
+ Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS);
+ Assert(!pf.d_node.isNull());
+ Assert(pf.d_children.size() >= 2);
int neg = -1;
- theory::eq::EqProof subTrans;
- subTrans.d_id = theory::eq::MERGED_THROUGH_TRANS;
- subTrans.d_node = pf->d_node;
+ std::shared_ptr<theory::eq::EqProof> subTrans =
+ std::make_shared<theory::eq::EqProof>();
+ subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS;
+ subTrans->d_node = pf.d_node;
size_t i = 0;
- while (i < pf->d_children.size()) {
+ while (i < pf.d_children.size()) {
// Look for the negative clause, with which we will form a contradiction.
- if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) {
+ if(!pf.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) {
Assert(neg < 0);
neg = i;
++i;
}
// Handle congruence closures over equalities.
- else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) {
+ else if (pf.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) {
Debug("pf::arith") << "Handling congruence over equalities" << std::endl;
// Gather the sequence of consecutive congruence closures.
- std::vector<const theory::eq::EqProof *> congruenceClosures;
+ std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures;
unsigned count;
Debug("pf::arith") << "Collecting congruence sequence" << std::endl;
for (count = 0;
- i + count < pf->d_children.size() &&
- pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
- pf->d_children[i + count]->d_node.isNull();
+ i + count < pf.d_children.size() &&
+ pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
+ pf.d_children[i + count]->d_node.isNull();
++count) {
Debug("pf::arith") << "Found a congruence: " << std::endl;
- pf->d_children[i+count]->debug_print("pf::arith");
- congruenceClosures.push_back(pf->d_children[i+count]);
+ pf.d_children[i+count]->debug_print("pf::arith");
+ congruenceClosures.push_back(pf.d_children[i+count]);
}
Debug("pf::arith") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
@@ -133,9 +143,9 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
targetAppearsBefore = false;
}
- if ((i + count >= pf->d_children.size()) ||
- (!pf->d_children[i + count]->d_node.isNull() &&
- pf->d_children[i + count]->d_node.getKind() == kind::NOT)) {
+ if ((i + count >= pf.d_children.size()) ||
+ (!pf.d_children[i + count]->d_node.isNull() &&
+ pf.d_children[i + count]->d_node.getKind() == kind::NOT)) {
Debug("pf::arith") << "Target does not appear after" << std::endl;
targetAppearsAfter = false;
}
@@ -144,37 +154,37 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
Assert(targetAppearsBefore != targetAppearsAfter);
// Begin breaking up the congruences and ordering the equalities correctly.
- std::vector<theory::eq::EqProof *> orderedEqualities;
+ std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities;
// Insert target clause first.
if (targetAppearsBefore) {
- orderedEqualities.push_back(pf->d_children[i - 1]);
+ orderedEqualities.push_back(pf.d_children[i - 1]);
// The target has already been added to subTrans; remove it.
- subTrans.d_children.pop_back();
+ subTrans->d_children.pop_back();
} else {
- orderedEqualities.push_back(pf->d_children[i + count]);
+ orderedEqualities.push_back(pf.d_children[i + count]);
}
// Start with the congruence closure closest to the target clause, and work our way back/forward.
if (targetAppearsBefore) {
for (unsigned j = 0; j < count; ++j) {
- if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
- orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]);
- if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
- orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]);
+ if (pf.d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+ orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + j]->d_children[0]);
+ if (pf.d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+ orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + j]->d_children[1]);
}
} else {
for (unsigned j = 0; j < count; ++j) {
- if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
- orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]);
- if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
- orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]);
+ if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+ orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + count - 1 - j]->d_children[0]);
+ if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+ orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + count - 1 - j]->d_children[1]);
}
}
// Copy the result into the main transitivity proof.
- subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
+ subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
// Increase i to skip over the children that have been processed.
i += count;
@@ -185,7 +195,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
// Else, just copy the child proof as is
else {
- subTrans.d_children.push_back(pf->d_children[i]);
+ subTrans->d_children.push_back(pf.d_children[i]);
++i;
}
}
@@ -193,16 +203,16 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
Node n1;
std::stringstream ss;
- //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
- Debug("pf::arith") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
- if(pf->d_children.size() > 2) {
- n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
+ //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
+ Debug("pf::arith") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
+ if(pf.d_children.size() > 2) {
+ n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
} else {
- n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
- Debug("pf::arith") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
+ n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map);
+ Debug("pf::arith") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
}
- Node n2 = pf->d_children[neg]->d_node;
+ Node n2 = pf.d_children[neg]->d_node;
Assert(n2.getKind() == kind::NOT);
out << "(clausify_false (contra _ ";
Debug("pf::arith") << "\nhave proven: " << n1 << std::endl;
@@ -228,12 +238,14 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
return Node();
}
- switch(pf->d_id) {
+ switch(pf.d_id) {
case theory::eq::MERGED_THROUGH_CONGRUENCE: {
Debug("pf::arith") << "\nok, looking at congruence:\n";
- pf->debug_print("pf::arith");
+ pf.debug_print("pf::arith");
std::stack<const theory::eq::EqProof*> stk;
- for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
+ for (const theory::eq::EqProof* pf2 = &pf;
+ pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
+ pf2 = pf2->d_children[0].get()) {
Assert(!pf2->d_node.isNull());
Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE);
Assert(pf2->d_children.size() == 2);
@@ -245,10 +257,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
const theory::eq::EqProof* pf2 = stk.top();
stk.pop();
Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
- Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map);
+ Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map);
out << " ";
std::stringstream ss;
- Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+ Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
Debug("pf::arith") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
pf2->debug_print("pf::arith");
Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
@@ -316,7 +328,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
out << " ";
ss.str("");
- n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+ n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
Debug("pf::arith") << "\nok, in cong[" << stk.size() << "]" << "\n";
Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
Debug("pf::arith") << " " << n1 << "\n";
@@ -373,27 +385,27 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
}
case theory::eq::MERGED_THROUGH_REFLEXIVITY:
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.empty());
+ Assert(!pf.d_node.isNull());
+ Assert(pf.d_children.empty());
out << "(refl _ ";
- tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map);
+ tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map);
out << ")";
- return eqNode(pf->d_node, pf->d_node);
+ return eqNode(pf.d_node, pf.d_node);
case theory::eq::MERGED_THROUGH_EQUALITY:
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.empty());
- out << ProofManager::getLitName(pf->d_node.negate());
- return pf->d_node;
+ Assert(!pf.d_node.isNull());
+ Assert(pf.d_children.empty());
+ out << ProofManager::getLitName(pf.d_node.negate());
+ return pf.d_node;
case theory::eq::MERGED_THROUGH_TRANS: {
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.size() >= 2);
+ Assert(!pf.d_node.isNull());
+ Assert(pf.d_children.size() >= 2);
std::stringstream ss;
Debug("pf::arith") << "\ndoing trans proof[[\n";
- pf->debug_print("pf::arith");
+ pf.debug_print("pf::arith");
Debug("pf::arith") << "\n";
- Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+ Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
Debug("pf::arith") << "\ndoing trans proof, got n1 " << n1 << "\n";
if(tb == 1) {
Debug("pf::arith") << "\ntrans proof[0], got n1 " << n1 << "\n";
@@ -405,7 +417,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
std::map<size_t, Node> childToStream;
- for(size_t i = 1; i < pf->d_children.size(); ++i) {
+ for(size_t i = 1; i < pf.d_children.size(); ++i) {
std::stringstream ss1(ss.str()), ss2;
ss.str("");
@@ -415,7 +427,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
if (childToStream.find(i) != childToStream.end())
n2 = childToStream[i];
else {
- n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map);
+ n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map);
childToStream[i] = n2;
}
@@ -446,9 +458,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
bool sequenceOver = false;
size_t j = i + 1;
- while (j < pf->d_children.size() && !sequenceOver) {
+ while (j < pf.d_children.size() && !sequenceOver) {
std::stringstream dontCare;
- nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map );
+ nodeAfterEqualitySequence = toStreamRecLFSC(
+ dontCare, tp, *(pf.d_children[j]), tb + 1, map);
if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
@@ -466,17 +479,17 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
Debug("pf::arith") << "Equality sequence of even length" << std::endl;
Debug("pf::arith") << "n1 is: " << n1 << std::endl;
Debug("pf::arith") << "n2 is: " << n2 << std::endl;
- Debug("pf::arith") << "pf-d_node is: " << pf->d_node << std::endl;
+ Debug("pf::arith") << "pf-d_node is: " << pf.d_node << std::endl;
Debug("pf::arith") << "Next node is: " << nodeAfterEqualitySequence << std::endl;
ss << "(trans _ _ _ _ ";
- // If the sequence is at the very end of the transitivity proof, use pf->d_node to guide us.
+ // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
if (!sequenceOver) {
- if (match(n1[0], pf->d_node[0])) {
+ if (match(n1[0], pf.d_node[0])) {
n1 = eqNode(n1[0], n1[0]);
ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
- } else if (match(n1[1], pf->d_node[1])) {
+ } else if (match(n1[1], pf.d_node[1])) {
n1 = eqNode(n1[1], n1[1]);
ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
} else {
@@ -572,7 +585,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
Warning() << "0 proves " << n1 << "\n";
Warning() << "1 proves " << n2 << "\n\n";
- pf->debug_print("pf::arith",0);
+ pf.debug_print("pf::arith",0);
//toStreamRec(Warning.getStream(), pf, 0);
Warning() << "\n\n";
Unreachable();
@@ -613,11 +626,11 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
}
default:
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.empty());
- Debug("pf::arith") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl;
+ Assert(!pf.d_node.isNull());
+ Assert(pf.d_children.empty());
+ Debug("pf::arith") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl;
AlwaysAssert(false);
- return pf->d_node;
+ return pf.d_node;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback