This clarifies the memory ownership of EqProofs.
** \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 {
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;
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;
}
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;
// 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;
}
}
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;
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);
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";
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";
}
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";
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("");
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;
}
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]))) {
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 {
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();
}
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;
}
}
#ifndef __CVC4__ARITH__PROOF_H
#define __CVC4__ARITH__PROOF_H
+#include <memory>
#include <unordered_set>
#include "expr/expr.h"
//proof object outputted by TheoryArith
class ProofArith : public Proof {
-private:
- static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
-public:
- ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {}
- //it is simply an equality engine proof
- theory::eq::EqProof * d_proof;
- void toStream(std::ostream& out);
- static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
+ public:
+ ProofArith(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {}
+ void toStream(std::ostream& out) override;
+ private:
+ static void toStreamLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf,
+ const ProofLetMap& map);
+ static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf,
+ unsigned tb, const ProofLetMap& map);
+ // it is simply an equality engine proof
+ std::shared_ptr<theory::eq::EqProof> d_proof;
};
-
namespace theory {
namespace arith {
class TheoryArith;
return true;
}
-ProofArray::ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1,
- unsigned ext)
+ProofArray::ProofArray(std::shared_ptr<theory::eq::EqProof> pf, unsigned row,
+ unsigned row1, unsigned ext)
: d_proof(pf), d_reasonRow(row), d_reasonRow1(row1), d_reasonExt(ext) {}
void ProofArray::toStream(std::ostream& out) {
void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) {
Trace("pf::array") << "; Print Array proof..." << std::endl;
- toStreamLFSC(out, ProofManager::getArrayProof(), d_proof, map);
+ toStreamLFSC(out, ProofManager::getArrayProof(), *d_proof, map);
Debug("pf::array") << "; Print Array proof done!" << std::endl;
}
void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp,
- theory::eq::EqProof* pf, const ProofLetMap& map) {
+ const theory::eq::EqProof& pf,
+ const ProofLetMap& map) {
Debug("pf::array") << "Printing array proof in LFSC : " << std::endl;
ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt);
- pf->debug_print("pf::array", 0, &proofPrinter);
+ pf.debug_print("pf::array", 0, &proofPrinter);
Debug("pf::array") << std::endl;
toStreamRecLFSC(out, tp, pf, 0, map);
Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
}
-Node ProofArray::toStreamRecLFSC(std::ostream& out,
- TheoryProof* tp,
- theory::eq::EqProof* pf,
- unsigned tb,
+Node ProofArray::toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf, unsigned tb,
const ProofLetMap& map) {
-
- Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
+ Debug("pf::array") << std::endl
+ << std::endl
+ << "toStreamRecLFSC called. tb = " << tb
+ << " . proof:" << std::endl;
ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt);
- pf->debug_print("pf::array", 0, &proofPrinter);
+ pf.debug_print("pf::array", 0, &proofPrinter);
Debug("pf::array") << 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()) {
- if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
- pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+ while (i < pf.d_children.size()) {
+ if (pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
+ pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
// 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::array") << "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::array") << "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::array") << "Found a congruence: " << std::endl;
- pf->d_children[i + count]->debug_print("pf::array", 0, &proofPrinter);
- congruenceClosures.push_back(pf->d_children[i + count]);
+ pf.d_children[i + count]->debug_print("pf::array", 0, &proofPrinter);
+ congruenceClosures.push_back(pf.d_children[i + count]);
}
Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
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::array") << "Target does not appear after" << std::endl;
targetAppearsAfter = false;
}
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;
// 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;
}
}
bool disequalityFound = (neg >= 0);
if (!disequalityFound) {
Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
- Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
- Assert(pf->d_node.getKind() == kind::EQUAL);
- Assert(pf->d_node.getNumChildren() == 2);
- Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+ Debug("pf::array") << "Proof for: " << pf.d_node << std::endl;
+ Assert(pf.d_node.getKind() == kind::EQUAL);
+ Assert(pf.d_node.getNumChildren() == 2);
+ Assert (pf.d_node[0].isConst() && pf.d_node[1].isConst());
}
Node n1;
std::stringstream ss, ss2;
- //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
- Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
- if(!disequalityFound || pf->d_children.size() > 2) {
- n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
+ //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
+ Debug("mgdx") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
+ if(!disequalityFound || pf.d_children.size() > 2) {
+ n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
} else {
- n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
- Debug("mgdx") << "\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("mgdx") << "\nsubTrans unique child "
+ << subTrans->d_children[0]->d_id
+ << " was proven\ngot: " << n1 << std::endl;
}
out << "(clausify_false (contra _ ";
if (disequalityFound) {
- Node n2 = pf->d_children[neg]->d_node;
+ Node n2 = pf.d_children[neg]->d_node;
Assert(n2.getKind() == kind::NOT);
Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
Debug("mgdx") << "n2 is " << n2 << std::endl;
- Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
+ Debug("mgdx") << "n2->d_id is " << pf.d_children[neg]->d_id << std::endl;
Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
- if ((pf->d_children[neg]->d_id == d_reasonExt) ||
- (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) {
+ if ((pf.d_children[neg]->d_id == d_reasonExt) ||
+ (pf.d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) {
// Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
out << ss.str();
out << " ";
- toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+ toStreamRecLFSC(ss2, tp, *pf.d_children[neg], 1, map);
out << ss2.str();
} else if (n2[0].getKind() == kind::APPLY_UF) {
out << "(trans _ _ _ _ ";
out << " " << ProofManager::getLitName(n2[0]);
}
} else {
- Node n2 = pf->d_node;
+ Node n2 = pf.d_node;
Assert(n2.getKind() == kind::EQUAL);
Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
return Node();
}
- if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
+ if (pf.d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
Debug("mgd") << "\nok, looking at congruence:\n";
- pf->debug_print("mgd", 0, &proofPrinter);
+ pf.debug_print("mgd", 0, &proofPrinter);
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]) {
- Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl;
-
+ for (const theory::eq::EqProof* pf2 = &pf;
+ pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
+ pf2 = pf2->d_children[0].get()) {
+ Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node
+ << std::endl;
Assert(!pf2->d_node.isNull());
Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF ||
pf2->d_node.getKind() == kind::BUILTIN ||
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("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
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("mgd") << "\nok, in cong[" << stk.size() << "]" << "\n";
Debug("mgd") << "looking at " << pf2->d_node << "\n";
return n;
}
- else if (pf->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.empty());
+ else if (pf.d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+ 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);
}
- else if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY) {
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.empty());
- Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf->d_node.negate() << " ) = " <<
- ProofManager::getLitName(pf->d_node.negate()) << std::endl;
- out << ProofManager::getLitName(pf->d_node.negate());
- return pf->d_node;
+ else if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY) {
+ Assert(!pf.d_node.isNull());
+ Assert(pf.d_children.empty());
+ Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf.d_node.negate() << " ) = " <<
+ ProofManager::getLitName(pf.d_node.negate()) << std::endl;
+ out << ProofManager::getLitName(pf.d_node.negate());
+ return pf.d_node;
}
- else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
- Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
- Assert(pf->d_node.getKind() == kind::NOT);
- Node n = pf->d_node[0];
+ else if (pf.d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
+ Debug("pf::array") << "Proof for: " << pf.d_node << std::endl;
+ Assert(pf.d_node.getKind() == kind::NOT);
+ Node n = pf.d_node[0];
Assert(n.getKind() == kind::EQUAL);
Assert(n.getNumChildren() == 2);
Assert(n[0].isConst() && n[1].isConst());
n[0].toExpr(),
n[1].toExpr(),
map);
- return pf->d_node;
+ return pf.d_node;
}
- else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) {
+ else if (pf.d_id == theory::eq::MERGED_THROUGH_TRANS) {
bool firstNeg = false;
bool secondNeg = false;
- 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("mgd") << "\ndoing trans proof[[\n";
- pf->debug_print("mgd", 0, &proofPrinter);
+ pf.debug_print("mgd", 0, &proofPrinter);
Debug("mgd") << "\n";
- pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node);
+ pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node);
- 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("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
if(tb == 1) {
Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n";
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("");
// and not turn them into (a[x]=true), because that will mess up the congruence application
// later.
- if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
- pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+ if (pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
+ pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
// It is possible that we've already converted the i'th child to stream. If so,
// use previously stored result. Otherwise, convert and store.
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;
}
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]))) {
Debug("pf::array") << "Equality sequence of even length" << std::endl;
Debug("pf::array") << "n1 is: " << n1 << std::endl;
Debug("pf::array") << "n2 is: " << n2 << std::endl;
- Debug("pf::array") << "pf-d_node is: " << pf->d_node << std::endl;
+ Debug("pf::array") << "pf-d_node is: " << pf.d_node << std::endl;
Debug("pf::array") << "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 {
Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
Warning() << "0 proves " << n1 << "\n";
Warning() << "1 proves " << n2 << "\n\n";
- pf->debug_print("mgdx", 0, &proofPrinter);
+ pf.debug_print("mgdx", 0, &proofPrinter);
//toStreamRec(Warning.getStream(), pf, 0);
Warning() << "\n\n";
Unreachable();
return n1;
}
- else if (pf->d_id == d_reasonRow) {
- Debug("mgd") << "row lemma: " << pf->d_node << std::endl;
- Assert(pf->d_node.getKind() == kind::EQUAL);
+ else if (pf.d_id == d_reasonRow) {
+ Debug("mgd") << "row lemma: " << pf.d_node << std::endl;
+ Assert(pf.d_node.getKind() == kind::EQUAL);
- if (pf->d_node[1].getKind() == kind::SELECT) {
+ if (pf.d_node[1].getKind() == kind::SELECT) {
// This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof explains why (i != k).
TNode t1, t2, t3, t4;
Node ret;
- if(pf->d_node[1].getKind() == kind::SELECT &&
- pf->d_node[1][0].getKind() == kind::STORE &&
- pf->d_node[0].getKind() == kind::SELECT &&
- pf->d_node[0][0] == pf->d_node[1][0][0] &&
- pf->d_node[0][1] == pf->d_node[1][1]) {
- t2 = pf->d_node[1][0][1];
- t3 = pf->d_node[1][1];
- t1 = pf->d_node[0][0];
- t4 = pf->d_node[1][0][2];
- ret = pf->d_node[1].eqNode(pf->d_node[0]);
+ if(pf.d_node[1].getKind() == kind::SELECT &&
+ pf.d_node[1][0].getKind() == kind::STORE &&
+ pf.d_node[0].getKind() == kind::SELECT &&
+ pf.d_node[0][0] == pf.d_node[1][0][0] &&
+ pf.d_node[0][1] == pf.d_node[1][1]) {
+ t2 = pf.d_node[1][0][1];
+ t3 = pf.d_node[1][1];
+ t1 = pf.d_node[0][0];
+ t4 = pf.d_node[1][0][2];
+ ret = pf.d_node[1].eqNode(pf.d_node[0]);
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
} else {
- Assert(pf->d_node[0].getKind() == kind::SELECT &&
- pf->d_node[0][0].getKind() == kind::STORE &&
- pf->d_node[1].getKind() == kind::SELECT &&
- pf->d_node[1][0] == pf->d_node[0][0][0] &&
- pf->d_node[1][1] == pf->d_node[0][1]);
- t2 = pf->d_node[0][0][1];
- t3 = pf->d_node[0][1];
- t1 = pf->d_node[1][0];
- t4 = pf->d_node[0][0][2];
- ret = pf->d_node;
+ Assert(pf.d_node[0].getKind() == kind::SELECT &&
+ pf.d_node[0][0].getKind() == kind::STORE &&
+ pf.d_node[1].getKind() == kind::SELECT &&
+ pf.d_node[1][0] == pf.d_node[0][0][0] &&
+ pf.d_node[1][1] == pf.d_node[0][1]);
+ t2 = pf.d_node[0][0][1];
+ t3 = pf.d_node[0][1];
+ t1 = pf.d_node[1][0];
+ t4 = pf.d_node[0][0][2];
+ ret = pf.d_node;
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
}
// inner index != outer index
// t3 is the outer index
- Assert(pf->d_children.size() == 1);
+ Assert(pf.d_children.size() == 1);
std::stringstream ss;
- Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+ Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
out << "(row _ _ ";
tp->printTerm(t2.toExpr(), out, map);
out << " ";
- Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node
+ Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf.d_children[0]->d_node
<< ". t3 is: " << t3 << std::endl
<< "subproof is: " << subproof << std::endl;
} else {
Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl;
- Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node << std::endl;
+ Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf.d_children[0]->d_node << std::endl;
// This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k])
TNode t1, t2, t3, t4;
Node ret;
- // pf->d_node is an equality, i==k.
- t1 = pf->d_node[0];
- t2 = pf->d_node[1];
+ // pf.d_node is an equality, i==k.
+ t1 = pf.d_node[0];
+ t2 = pf.d_node[1];
- // pf->d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))),
+ // pf.d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))),
// or its symmetrical version.
unsigned side;
- if (pf->d_children[0]->d_node[0][0].getKind() == kind::SELECT &&
- pf->d_children[0]->d_node[0][0][0].getKind() == kind::STORE) {
+ if (pf.d_children[0]->d_node[0][0].getKind() == kind::SELECT &&
+ pf.d_children[0]->d_node[0][0][0].getKind() == kind::STORE) {
side = 0;
- } else if (pf->d_children[0]->d_node[0][1].getKind() == kind::SELECT &&
- pf->d_children[0]->d_node[0][1][0].getKind() == kind::STORE) {
+ } else if (pf.d_children[0]->d_node[0][1].getKind() == kind::SELECT &&
+ pf.d_children[0]->d_node[0][1][0].getKind() == kind::STORE) {
side = 1;
}
else {
Debug("pf::array") << "Side is: " << side << std::endl;
// The array's index and element types will come from the subproof...
- t3 = pf->d_children[0]->d_node[0][side][0][0];
- t4 = pf->d_children[0]->d_node[0][side][0][2];
- ret = pf->d_node;
+ t3 = pf.d_children[0]->d_node[0][side][0][0];
+ t4 = pf.d_children[0]->d_node[0][side][0][2];
+ ret = pf.d_node;
// The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
- bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]);
+ bool swap = (t2 == pf.d_children[0]->d_node[0][side][0][1]);
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
- Assert(pf->d_children.size() == 1);
+ Assert(pf.d_children.size() == 1);
std::stringstream ss;
- Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+ Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
}
}
- else if (pf->d_id == d_reasonRow1) {
- Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl;
- Assert(pf->d_node.getKind() == kind::EQUAL);
+ else if (pf.d_id == d_reasonRow1) {
+ Debug("mgd") << "row1 lemma: " << pf.d_node << std::endl;
+ Assert(pf.d_node.getKind() == kind::EQUAL);
TNode t1, t2, t3;
Node ret;
- if(pf->d_node[1].getKind() == kind::SELECT &&
- pf->d_node[1][0].getKind() == kind::STORE &&
- pf->d_node[1][0][1] == pf->d_node[1][1] &&
- pf->d_node[1][0][2] == pf->d_node[0]) {
- t1 = pf->d_node[1][0][0];
- t2 = pf->d_node[1][0][1];
- t3 = pf->d_node[0];
- ret = pf->d_node[1].eqNode(pf->d_node[0]);
+ if(pf.d_node[1].getKind() == kind::SELECT &&
+ pf.d_node[1][0].getKind() == kind::STORE &&
+ pf.d_node[1][0][1] == pf.d_node[1][1] &&
+ pf.d_node[1][0][2] == pf.d_node[0]) {
+ t1 = pf.d_node[1][0][0];
+ t2 = pf.d_node[1][0][1];
+ t3 = pf.d_node[0];
+ ret = pf.d_node[1].eqNode(pf.d_node[0]);
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
} else {
- Assert(pf->d_node[0].getKind() == kind::SELECT &&
- pf->d_node[0][0].getKind() == kind::STORE &&
- pf->d_node[0][0][1] == pf->d_node[0][1] &&
- pf->d_node[0][0][2] == pf->d_node[1]);
- t1 = pf->d_node[0][0][0];
- t2 = pf->d_node[0][0][1];
- t3 = pf->d_node[1];
- ret = pf->d_node;
+ Assert(pf.d_node[0].getKind() == kind::SELECT &&
+ pf.d_node[0][0].getKind() == kind::STORE &&
+ pf.d_node[0][0][1] == pf.d_node[0][1] &&
+ pf.d_node[0][0][2] == pf.d_node[1]);
+ t1 = pf.d_node[0][0][0];
+ t2 = pf.d_node[0][0][1];
+ t3 = pf.d_node[1];
+ ret = pf.d_node;
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
}
out << "(row1 _ _ ";
return ret;
}
- else if (pf->d_id == d_reasonExt) {
- theory::eq::EqProof *child_proof;
-
- Assert(pf->d_node.getKind() == kind::NOT);
- Assert(pf->d_node[0].getKind() == kind::EQUAL);
- Assert(pf->d_children.size() == 1);
-
- child_proof = pf->d_children[0];
+ else if (pf.d_id == d_reasonExt) {
+ Assert(pf.d_node.getKind() == kind::NOT);
+ Assert(pf.d_node[0].getKind() == kind::EQUAL);
+ Assert(pf.d_children.size() == 1);
+ std::shared_ptr<theory::eq::EqProof> child_proof = pf.d_children[0];
Assert(child_proof->d_node.getKind() == kind::NOT);
Assert(child_proof->d_node[0].getKind() == kind::EQUAL);
- Debug("mgd") << "EXT lemma: " << pf->d_node << std::endl;
+ Debug("mgd") << "EXT lemma: " << pf.d_node << std::endl;
TNode t1, t2, t3;
t1 = child_proof->d_node[0][0];
t2 = child_proof->d_node[0][1];
- t3 = pf->d_node[0][0][1];
+ t3 = pf.d_node[0][0][1];
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
out << ProofManager::getArrayProof()->skolemToLiteral(t3.toExpr());
out << ")";
- return pf->d_node;
+ return pf.d_node;
}
else {
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.empty());
- Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl;
+ Assert(!pf.d_node.isNull());
+ Assert(pf.d_children.empty());
+ Debug("mgd") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl;
AlwaysAssert(false);
- return pf->d_node;
+ return pf.d_node;
}
}
#ifndef __CVC4__ARRAY__PROOF_H
#define __CVC4__ARRAY__PROOF_H
+#include <memory>
#include <unordered_set>
#include "expr/expr.h"
// Proof object outputted by TheoryARRAY.
class ProofArray : public Proof {
public:
- ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1,
- unsigned ext);
+ ProofArray(std::shared_ptr<theory::eq::EqProof> pf, unsigned row,
+ unsigned row1, unsigned ext);
void registerSkolem(Node equality, Node skolem);
void toStream(std::ostream& out);
void toStream(std::ostream& out, const ProofLetMap& map);
- void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf,
- const ProofLetMap& map);
-
private:
+ void toStreamLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf, const ProofLetMap& map);
+
Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
- theory::eq::EqProof* pf, unsigned tb,
+ const theory::eq::EqProof& pf, unsigned tb,
const ProofLetMap& map);
- // it is simply an equality engine proof
- theory::eq::EqProof* d_proof;
+ // It is simply an equality engine proof.
+ std::shared_ptr<theory::eq::EqProof> d_proof;
/** Merge tag for ROW applications */
unsigned d_reasonRow;
** \todo document this file
**/
+#include "proof/uf_proof.h"
+
+#include <stack>
#include "proof/proof_manager.h"
#include "proof/simplify_boolean_node.h"
-#include "proof/theory_proof.h"
-#include "proof/uf_proof.h"
#include "theory/uf/theory_uf.h"
-#include <stack>
namespace CVC4 {
void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) {
Trace("theory-proof-debug") << "; Print UF proof..." << std::endl;
//AJR : carry this further?
- toStreamLFSC(out, ProofManager::getUfProof(), d_proof, map);
+ toStreamLFSC(out, ProofManager::getUfProof(), *d_proof, map);
}
-void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) {
+void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf,
+ const ProofLetMap& map) {
Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl;
Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl;
- pf->debug_print("lfsc-uf");
+ pf.debug_print("lfsc-uf");
Debug("lfsc-uf") << std::endl;
toStreamRecLFSC( out, tp, pf, 0, map );
}
-Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) {
- Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
- pf->debug_print("pf::uf");
+Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf,
+ unsigned tb, const ProofLetMap& map) {
+ Debug("pf::uf") << std::endl
+ << std::endl
+ << "toStreamRecLFSC called. tb = " << tb
+ << " . proof:" << std::endl;
+ pf.debug_print("pf::uf");
Debug("pf::uf") << std::endl;
if (tb == 0) {
// Special case: false was an input, so the proof is just "false".
- if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
- pf->d_node == NodeManager::currentNM()->mkConst(false)) {
+ if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
+ pf.d_node == NodeManager::currentNM()->mkConst(false)) {
out << "(clausify_false ";
out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode());
out << ")" << std::endl;
return Node();
}
- 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()) {
- pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+ while (i < pf.d_children.size()) {
+ pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
// 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);
- Node node = pf->d_children[i]->d_node[0];
+ Node node = pf.d_children[i]->d_node[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::uf") << "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::uf") << "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::uf") << "Found a congruence: " << std::endl;
- pf->d_children[i+count]->debug_print("pf::uf");
- congruenceClosures.push_back(pf->d_children[i+count]);
+ pf.d_children[i+count]->debug_print("pf::uf");
+ congruenceClosures.push_back(pf.d_children[i+count]);
}
Debug("pf::uf") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
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::uf") << "Target does not appear after" << std::endl;
targetAppearsAfter = false;
}
targetAppearsBefore = false;
// 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;
// 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;
}
}
bool disequalityFound = (neg >= 0);
if (!disequalityFound) {
Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
- Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl;
- Assert(pf->d_node.getKind() == kind::EQUAL);
- Assert(pf->d_node.getNumChildren() == 2);
- Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+ Debug("pf::uf") << "Proof for: " << pf.d_node << std::endl;
+ Assert(pf.d_node.getKind() == kind::EQUAL);
+ Assert(pf.d_node.getNumChildren() == 2);
+ Assert (pf.d_node[0].isConst() && pf.d_node[1].isConst());
}
Node n1;
std::stringstream ss;
- Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
+ Debug("pf::uf") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
- if(!disequalityFound || subTrans.d_children.size() >= 2) {
- n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
+ if(!disequalityFound || subTrans->d_children.size() >= 2) {
+ n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
} else {
- n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
- Debug("pf::uf") << "\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::uf") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
}
Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
out << "(clausify_false (contra _ ";
if (disequalityFound) {
- Node n2 = pf->d_children[neg]->d_node;
+ Node n2 = pf.d_children[neg]->d_node;
Assert(n2.getKind() == kind::NOT);
Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
}
} else {
- Node n2 = pf->d_node;
+ Node n2 = pf.d_node;
Assert(n2.getKind() == kind::EQUAL);
Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
return Node();
}
- switch(pf->d_id) {
+ switch(pf.d_id) {
case theory::eq::MERGED_THROUGH_CONGRUENCE: {
Debug("pf::uf") << "\nok, looking at congruence:\n";
- pf->debug_print("pf::uf");
+ pf.debug_print("pf::uf");
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);
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::uf") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
pf2->debug_print("pf::uf");
Debug("pf::uf") << "looking at " << pf2->d_node << "\n";
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::uf") << "\nok, in cong[" << stk.size() << "]" << "\n";
Debug("pf::uf") << "looking at " << pf2->d_node << "\n";
Debug("pf::uf") << " " << n1 << "\n";
}
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::uf") << "\ndoing trans proof[[\n";
- pf->debug_print("pf::uf");
+ pf.debug_print("pf::uf");
Debug("pf::uf") << "\n";
- pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node);
+ pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node);
- 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::uf") << "\ndoing trans proof, got n1 " << n1 << "\n";
if(tb == 1) {
Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n";
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("");
- pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+ pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
// It is possible that we've already converted the i'th child to stream. If so,
// use previously stored result. Otherwise, convert and store.
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;
}
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]))) {
Debug("pf::uf") << "Equality sequence of even length" << std::endl;
Debug("pf::uf") << "n1 is: " << n1 << std::endl;
Debug("pf::uf") << "n2 is: " << n2 << std::endl;
- Debug("pf::uf") << "pf-d_node is: " << pf->d_node << std::endl;
+ Debug("pf::uf") << "pf-d_node is: " << pf.d_node << std::endl;
Debug("pf::uf") << "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 {
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::uf",0);
+ pf.debug_print("pf::uf",0);
//toStreamRec(Warning.getStream(), pf, 0);
Warning() << "\n\n";
Unreachable();
// We want to prove b1 = b2, and we know that ((b1), (b2)) or ((not b1), (not b2))
if (n1.getKind() == kind::NOT) {
Assert(n2.getKind() == kind::NOT);
- Assert(pf->d_node[0] == n1[0] || pf->d_node[0] == n2[0]);
- Assert(pf->d_node[1] == n1[0] || pf->d_node[1] == n2[0]);
+ Assert(pf.d_node[0] == n1[0] || pf.d_node[0] == n2[0]);
+ Assert(pf.d_node[1] == n1[0] || pf.d_node[1] == n2[0]);
Assert(n1[0].getKind() == kind::BOOLEAN_TERM_VARIABLE);
Assert(n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE);
- if (pf->d_node[0] == n1[0]) {
+ if (pf.d_node[0] == n1[0]) {
ss << "(false_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") ";
ss << "(pred_refl_neg _ " << ss2.str() << ")";
} else {
ss << "(false_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") ";
ss << "(pred_refl_neg _ " << ss1.str() << ")";
}
- n1 = pf->d_node;
+ n1 = pf.d_node;
} else if (n1.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
Assert(n2.getKind() == kind::BOOLEAN_TERM_VARIABLE);
- Assert(pf->d_node[0] == n1 || pf->d_node[0] == n2);
- Assert(pf->d_node[1] == n1 || pf->d_node[2] == n2);
+ Assert(pf.d_node[0] == n1 || pf.d_node[0] == n2);
+ Assert(pf.d_node[1] == n1 || pf.d_node[2] == n2);
- if (pf->d_node[0] == n1) {
+ if (pf.d_node[0] == n1) {
ss << "(true_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") ";
ss << "(pred_refl_pos _ " << ss2.str() << ")";
} else {
ss << "(true_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") ";
ss << "(pred_refl_pos _ " << ss1.str() << ")";
}
- n1 = pf->d_node;
+ n1 = pf.d_node;
} else {
}
default:
- Assert(!pf->d_node.isNull());
- Assert(pf->d_children.empty());
- Debug("pf::uf") << "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::uf") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl;
AlwaysAssert(false);
- return pf->d_node;
+ return pf.d_node;
}
}
#ifndef __CVC4__UF__PROOF_H
#define __CVC4__UF__PROOF_H
+#include <memory>
#include <unordered_set>
#include "expr/expr.h"
-#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
#include "theory/uf/equality_engine.h"
+#include "util/proof.h"
namespace CVC4 {
-//proof object outputted by TheoryUF
+// proof object outputted by TheoryUF
class ProofUF : public Proof {
-private:
- static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
-public:
- ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {}
- //it is simply an equality engine proof
- theory::eq::EqProof * d_proof;
- void toStream(std::ostream& out);
- void toStream(std::ostream& out, const ProofLetMap& map);
- static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
+ public:
+ ProofUF(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {}
+ void toStream(std::ostream& out) override;
+ void toStream(std::ostream& out, const ProofLetMap& map) override;
+
+ private:
+ static void toStreamLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf,
+ const ProofLetMap& map);
+ static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+ const theory::eq::EqProof& pf, unsigned tb,
+ const ProofLetMap& map);
+
+ // it is simply an equality engine proof
+ std::shared_ptr<theory::eq::EqProof> d_proof;
};
-
namespace theory {
namespace uf {
class TheoryUF;
#include "theory/arrays/array_proof_reconstruction.h"
+#include <memory>
+
namespace CVC4 {
namespace theory {
namespace arrays {
d_reasonExt = tag;
}
-void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Node b,
- std::vector<TNode>& equalities, eq::EqProof* proof) const {
-
+void ArrayProofReconstruction::notify(
+ unsigned reasonType, Node reason, Node a, Node b,
+ std::vector<TNode>& equalities, eq::EqProof* proof) const {
Debug("pf::array") << "ArrayProofReconstruction::notify( "
<< reason << ", " << a << ", " << b << std::endl;
if (reasonType == d_reasonExt) {
if (proof) {
- // Todo: here we assume that a=b is an assertion. We should probably call explain()
- // recursively, to explain this.
- eq::EqProof* childProof = new eq::EqProof;
+ // Todo: here we assume that a=b is an assertion. We should probably call
+ // explain() recursively, to explain this.
+ std::shared_ptr<eq::EqProof> childProof = std::make_shared<eq::EqProof>();
childProof->d_node = reason;
proof->d_children.push_back(childProof);
}
Debug("pf::ee") << "Getting explanation for ROW guard: "
<< indexOne << " != " << indexTwo << std::endl;
+ std::shared_ptr<eq::EqProof> childProof =
+ std::make_shared<eq::EqProof>();
+ d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities,
+ childProof.get());
- eq::EqProof* childProof = new eq::EqProof;
- d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof);
-
- // It could be that the guard condition is a constant disequality. In this case,
- // we need to change it to a different format.
+ // It could be that the guard condition is a constant disequality. In
+ // this case, we need to change it to a different format.
bool haveNegChild = false;
for (unsigned i = 0; i < childProof->d_children.size(); ++i) {
if (childProof->d_children[i]->d_node.getKind() == kind::NOT)
}
}
- eq::EqProof* constantDisequalityProof = new eq::EqProof;
+ std::shared_ptr<eq::EqProof> constantDisequalityProof =
+ std::make_shared<eq::EqProof>();
constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
constantDisequalityProof->d_node =
NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
// Middle is where we need to insert the new disequality
- std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin();
+ std::vector<std::shared_ptr<eq::EqProof>>::iterator middle =
+ childProof->d_children.begin();
++middle;
childProof->d_children.insert(middle, constantDisequalityProof);
Assert(reason.getNumChildren() == 2);
Debug("pf::ee") << "Getting explanation for ROW guard: " << reason[1] << std::endl;
- eq::EqProof* childProof = new eq::EqProof;
- d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false, equalities, childProof);
+ std::shared_ptr<eq::EqProof> childProof =
+ std::make_shared<eq::EqProof>();
+ d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false,
+ equalities, childProof.get());
proof->d_children.push_back(childProof);
}
}
ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
void notify(unsigned reasonType, Node reason, Node a, Node b,
- std::vector<TNode>& equalities, eq::EqProof* proof) const;
+ std::vector<TNode>& equalities,
+ eq::EqProof* proof) const override;
void setRowMergeTag(unsigned tag);
void setRow1MergeTag(unsigned tag);
#include "theory/arrays/theory_arrays.h"
#include <map>
+#include <memory>
#include "expr/kind.h"
#include "options/arrays_options.h"
}/* TheoryArrays::propagate(TNode) */
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) {
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions,
+ eq::EqProof* proof) {
// Do the work
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
return explanation;
}
-Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
-{
+Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
++d_numExplain;
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel())
+ << "TheoryArrays::explain(" << literal << ")" << std::endl;
std::vector<TNode> assumptions;
explain(literal, assumptions, proof);
return mkAnd(assumptions);
}
-
/////////////////////////////////////////////////////////////////////////////
// SHARING
/////////////////////////////////////////////////////////////////////////////
void TheoryArrays::conflict(TNode a, TNode b) {
Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
- eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
+ std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ?
+ std::make_shared<eq::EqProof>() : nullptr;
- d_conflictNode = explain(a.eqNode(b), proof);
+ d_conflictNode = explain(a.eqNode(b), proof.get());
if (!d_inCheckModel) {
ProofArray* proof_array = NULL;
bool propagate(TNode literal);
/** Explain why this literal is true by adding assumptions */
- void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof);
+ void explain(TNode literal, std::vector<TNode>& assumptions,
+ eq::EqProof* proof);
/** For debugging only- checks invariants about when things are preregistered*/
context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
void preRegisterTerm(TNode n);
void propagate(Effort e);
- Node explain(TNode n, eq::EqProof *proof);
+ Node explain(TNode n, eq::EqProof* proof);
Node explain(TNode n);
/////////////////////////////////////////////////////////////////////////////
return out.str();
}
-void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const {
- Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
+void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
+ std::vector<TNode>& equalities,
+ EqProof* eqp) const {
+ Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2
+ << ", " << (polarity ? "true" : "false") << ")"
+ << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
// The terms must be there already
Assert(hasTerm(t1) && hasTerm(t2));;
for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
EqualityPair toExplain = d_deducedDisequalityReasons[i];
- EqProof* eqpc = NULL;
+ std::shared_ptr<EqProof> eqpc;
// If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
if (eqp && toExplain.first != toExplain.second) {
- eqpc = new EqProof;
+ eqpc = std::make_shared<EqProof>();
}
- getExplanation(toExplain.first, toExplain.second, equalities, eqpc);
+ getExplanation(toExplain.first, toExplain.second, equalities, eqpc.get());
if (eqpc) {
Debug("pf::ee") << "Child proof is:" << std::endl;
eqpc->debug_print("pf::ee", 1);
if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) {
- std::vector<EqProof *> orderedChildren;
+ std::vector<std::shared_ptr<EqProof>> orderedChildren;
bool nullCongruenceFound = false;
for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
eqp->d_id = MERGED_THROUGH_CONSTANTS;
} else if (eqp->d_children.size() == 1) {
// The transitivity proof has just one child. Simplify.
- EqProof* temp = eqp->d_children[0];
+ std::shared_ptr<EqProof> temp = eqp->d_children[0];
eqp->d_children.clear();
*eqp = *temp;
- delete temp;
}
Debug("pf::ee") << "Disequality explanation final proof: " << std::endl;
}
}
-void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp) const {
- Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" << std::endl;
+void EqualityEngine::explainPredicate(TNode p, bool polarity,
+ std::vector<TNode>& assertions,
+ EqProof* eqp) const {
+ Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")"
+ << std::endl;
// Must have the term
Assert(hasTerm(p));
// Get the explanation
- getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, eqp);
+ getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions,
+ eqp);
}
-void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const {
-
+void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id,
+ std::vector<TNode>& equalities,
+ EqProof* eqp) const {
Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
// We can only explain the nodes that got merged
Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
- std::vector<EqProof *> eqp_trans;
+ std::vector<std::shared_ptr<EqProof>> eqp_trans;
// Reconstruct the path
do {
Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
Debug("equality") << d_name << " reason type = " << reasonType << std::endl;
- EqProof* eqpc = NULL;
+ std::shared_ptr<EqProof> eqpc;;
// Make child proof if a proof is being constructed
if (eqp) {
- eqpc = new EqProof;
+ eqpc = std::make_shared<EqProof>();
eqpc->d_id = reasonType;
}
Debug("equality") << push;
Debug("equality") << "Explaining left hand side equalities" << std::endl;
- EqProof * eqpc1 = eqpc ? new EqProof : NULL;
- getExplanation(f1.a, f2.a, equalities, eqpc1);
+ std::shared_ptr<EqProof> eqpc1 =
+ eqpc ? std::make_shared<EqProof>() : nullptr;
+ getExplanation(f1.a, f2.a, equalities, eqpc1.get());
Debug("equality") << "Explaining right hand side equalities" << std::endl;
- EqProof * eqpc2 = eqpc ? new EqProof : NULL;
- getExplanation(f1.b, f2.b, equalities, eqpc2);
+ std::shared_ptr<EqProof> eqpc2 =
+ eqpc ? std::make_shared<EqProof>() : nullptr;
+ getExplanation(f1.b, f2.b, equalities, eqpc2.get());
if( eqpc ){
eqpc->d_children.push_back( eqpc1 );
eqpc->d_children.push_back( eqpc2 );
// Explain why a = b constant
Debug("equality") << push;
- EqProof * eqpc1 = eqpc ? new EqProof : NULL;
- getExplanation(eq.a, eq.b, equalities, eqpc1);
+ std::shared_ptr<EqProof> eqpc1 =
+ eqpc ? std::make_shared<EqProof>() : nullptr;
+ getExplanation(eq.a, eq.b, equalities, eqpc1.get());
if( eqpc ){
eqpc->d_children.push_back( eqpc1 );
}
for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) {
EqualityNodeId childId = getNodeId(interpreted[i]);
Assert(isConstant(childId));
- EqProof * eqpcc = eqpc ? new EqProof : NULL;
- getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
+ std::shared_ptr<EqProof> eqpcc =
+ eqpc ? std::make_shared<EqProof>() : nullptr;
+ getExplanation(childId, getEqualityNode(childId).getFind(),
+ equalities, eqpcc.get());
if( eqpc ) {
eqpc->d_children.push_back( eqpcc );
if (eqpc) {
//apply proof reconstruction processing (when eqpc is non-null)
if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
- d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
- equalities, eqpc);
+ d_pathReconstructionTriggers.find(reasonType)
+ ->second->notify(reasonType, reason, a, b, equalities,
+ eqpc.get());
}
if (reasonType == MERGED_THROUGH_EQUALITY) {
eqpc->d_node = reason;
if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
if(eqpc->d_node.isNull()) {
Assert(eqpc->d_children.size() == 1);
- EqProof *p = eqpc;
+ std::shared_ptr<EqProof> p = eqpc;
eqpc = p->d_children[0];
- delete p;
} else {
Assert(eqpc->d_children.empty());
}
if (eqp) {
if(eqp_trans.size() == 1) {
*eqp = *eqp_trans[0];
- delete eqp_trans[0];
} else {
eqp->d_id = MERGED_THROUGH_TRANS;
eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
#include <deque>
#include <queue>
+#include <memory>
#include <unordered_map>
#include <vector>
virtual ~PathReconstructionNotify() {}
virtual void notify(unsigned reasonType, Node reason, Node a, Node b,
- std::vector<TNode>& equalities, EqProof* proof) const = 0;
+ std::vector<TNode>& equalities,
+ EqProof* proof) const = 0;
};
/**
* imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
* else.
*/
- void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const;
+ void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof* eqp) const;
/**
* Print the equality graph.
* Returns the reasons (added when asserting) that imply it
* in the assertions vector.
*/
- void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const;
+ void explainEquality(TNode t1, TNode t2, bool polarity,
+ std::vector<TNode>& assertions,
+ EqProof* eqp = nullptr) const;
/**
* Get an explanation of the predicate being true or false.
* Returns the reasons (added when asserting) that imply imply it
* in the assertions vector.
*/
- void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const;
+ void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions,
+ EqProof* eqp = nullptr) const;
/**
* Add term to the set of trigger terms with a corresponding tag. The notify class will get
EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
unsigned d_id;
Node d_node;
- std::vector< EqProof * > d_children;
- void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const;
+ std::vector<std::shared_ptr<EqProof>> d_children;
+ void debug_print(const char* c, unsigned tb = 0,
+ PrettyPrinter* prettyPrinter = nullptr) const;
};/* class EqProof */
} // Namespace eq
#include "theory/uf/theory_uf.h"
+#include <memory>
+
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
}/* TheoryUF::computeCareGraph() */
void TheoryUF::conflict(TNode a, TNode b) {
- eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
- d_conflictNode = explain(a.eqNode(b),pf);
+ std::shared_ptr<eq::EqProof> pf =
+ d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
+ d_conflictNode = explain(a.eqNode(b), pf.get());
ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
d_out->conflict(d_conflictNode, puf);
d_conflict = true;
projects / cvc5.git / commitdiff