namespace CVC4 {
+unsigned ProofArray::d_reasonRow;
+unsigned ProofArray::d_reasonRow1;
+unsigned ProofArray::d_reasonExt;
+
inline static Node eqNode(TNode n1, TNode n2) {
return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
}
return true;
}
+void ProofArray::setRowMergeTag(unsigned tag) {
+ d_reasonRow = tag;
+}
+
+void ProofArray::setRow1MergeTag(unsigned tag) {
+ d_reasonRow1 = tag;
+}
+
+void ProofArray::setExtMergeTag(unsigned tag) {
+ d_reasonExt = tag;
+}
+
void ProofArray::toStream(std::ostream& out) {
Trace("pf::array") << "; Print Array proof..." << std::endl;
//AJR : carry this further?
Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
}
-void ProofArray::registerSkolem(Node equality, Node skolem) {
- d_nodeToSkolem[equality] = skolem;
-}
-
Node ProofArray::toStreamRecLFSC(std::ostream& out,
TheoryProof* tp,
theory::eq::EqProof* pf,
unsigned tb,
const LetMap& map) {
+ Debug("gk::temp") << "d_reasonExt = " << d_reasonExt << std::endl;
+ Debug("gk::temp") << "d_reasonRow = " << d_reasonRow << std::endl;
+ Debug("gk::temp") << "d_reasonRow1 = " << d_reasonRow1 << std::endl;
+
Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
pf->debug_print("pf::array");
Debug("pf::array") << std::endl;
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();
+ 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");
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 == theory::eq::MERGED_ARRAYS_EXT) {
+ if (pf->d_children[neg]->d_id == d_reasonExt) {
// The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
// (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6
return Node();
}
- switch(pf->d_id) {
- case 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");
std::stack<const theory::eq::EqProof*> stk;
} else {
Debug("mgd") << "SIDE IS 1\n";
if(!match(pf2->d_node, n1[1])) {
- Debug("mgd") << "IN BAD CASE, our first subproof is\n";
- pf2->d_children[0]->debug_print("mgd");
+ Debug("mgd") << "IN BAD CASE, our first subproof is\n";
+ pf2->d_children[0]->debug_print("mgd");
}
Assert(match(pf2->d_node, n1[1]));
side = 1;
b2 << kind::PARTIAL_APPLY_UF;
b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator());
}
- b2.append(n1[1-side].begin(), n1[1-side].end());
+ b2.append(n1[1-side].begin(), n1[1-side].end());
} else if (n1[1-side].getKind() == kind::PARTIAL_SELECT_0) {
b2 << kind::PARTIAL_SELECT_1;
} else {
b1.append(n1.begin(), n1.end());
n1 = b1;
Debug("mgd") << "New n1: " << n1 << std::endl;
- // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) {
- // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
- // b1.clear(kind::PARTIAL_SELECT_1);
- // b1.append(n1.begin(), n1.end());
- // n1 = b1;
- // Debug("mgd") << "New n1: " << n1 << std::endl;
- // } else
+ // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) {
+ // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
+ // b1.clear(kind::PARTIAL_SELECT_1);
+ // b1.append(n1.begin(), n1.end());
+ // n1 = b1;
+ // Debug("mgd") << "New n1: " << n1 << std::endl;
+ // } else
} else if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) {
if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
b2.append(n2.begin(), n2.end());
n2 = b2;
Debug("mgd") << "New n2: " << n2 << std::endl;
- // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) {
- // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
- // b2.clear(kind::PARTIAL_SELECT_1);
- // b2.append(n2.begin(), n2.end());
- // n2 = b2;
- // Debug("mgd") << "New n2: " << n2 << std::endl;
- // } else
+ // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) {
+ // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
+ // b2.clear(kind::PARTIAL_SELECT_1);
+ // b2.append(n2.begin(), n2.end());
+ // n2 = b2;
+ // Debug("mgd") << "New n2: " << n2 << std::endl;
+ // } else
} else if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) {
if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
return n;
}
- case theory::eq::MERGED_THROUGH_REFLEXIVITY:
+ 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);
out << ")";
return eqNode(pf->d_node, pf->d_node);
+ }
- case theory::eq::MERGED_THROUGH_EQUALITY:
+ 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;
+ }
- case theory::eq::MERGED_THROUGH_TRANS: {
+ else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) {
bool firstNeg = false;
bool secondNeg = false;
// Both elements of the transitivity rule are equalities/iffs
{
if(n1[0] == n2[0]) {
- if(tb == 1) { Debug("mgdx") << "case 1\n"; }
- n1 = eqNode(n1[1], n2[1]);
- ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str();
+ if(tb == 1) { Debug("mgdx") << "case 1\n"; }
+ n1 = eqNode(n1[1], n2[1]);
+ ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str();
} else if(n1[1] == n2[1]) {
if(tb == 1) { Debug("mgdx") << "case 2\n"; }
n1 = eqNode(n1[0], n2[0]);
ss << ss1.str() << (secondNeg ? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2.str() << ")";
} else if(n1[0] == n2[1]) {
- if(tb == 1) { Debug("mgdx") << "case 3\n"; }
- if(!firstNeg && !secondNeg) {
- n1 = eqNode(n2[0], n1[1]);
- ss << ss2.str() << " " << ss1.str();
- } else if (firstNeg) {
- n1 = eqNode(n1[1], n2[0]);
- ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")";
- } else {
- Assert(secondNeg);
- n1 = eqNode(n1[1], n2[0]);
- ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")";
- }
- if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; }
+ if(tb == 1) { Debug("mgdx") << "case 3\n"; }
+ if(!firstNeg && !secondNeg) {
+ n1 = eqNode(n2[0], n1[1]);
+ ss << ss2.str() << " " << ss1.str();
+ } else if (firstNeg) {
+ n1 = eqNode(n1[1], n2[0]);
+ ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")";
+ } else {
+ Assert(secondNeg);
+ n1 = eqNode(n1[1], n2[0]);
+ ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")";
+ }
+ if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; }
} else if(n1[1] == n2[0]) {
if(tb == 1) { Debug("mgdx") << "case 4\n"; }
n1 = eqNode(n1[0], n2[1]);
return n1;
}
- case theory::eq::MERGED_ARRAYS_ROW: {
+ else if (pf->d_id == d_reasonRow) {
Debug("mgd") << "row lemma: " << pf->d_node << std::endl;
Assert(pf->d_node.getKind() == kind::EQUAL);
// if (subproof[0][1] == t3) {
- Debug("pf::array") << "Dont need symmetry!" << std::endl;
- out << ss.str();
+ Debug("pf::array") << "Dont need symmetry!" << std::endl;
+ out << ss.str();
// } else {
// Debug("pf::array") << "Need symmetry!" << std::endl;
// out << "(negsymm _ _ _ " << ss.str() << ")";
}
}
- case theory::eq::MERGED_ARRAYS_ROW1: {
+ 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;
return ret;
}
- case theory::eq::MERGED_ARRAYS_EXT: {
+ else if (pf->d_id == d_reasonExt) {
theory::eq::EqProof *child_proof;
Assert(pf->d_node.getKind() == kind::NOT);
return pf->d_node;
}
- default:
+ 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;
unsigned tb,
const LetMap& map);
- std::hash_map<Node, Node, NodeHashFunction> d_nodeToSkolem;
+ /** Merge tag for ROW applications */
+ static unsigned d_reasonRow;
+ /** Merge tag for ROW1 applications */
+ static unsigned d_reasonRow1;
+ /** Merge tag for EXT applications */
+ static unsigned d_reasonExt;
public:
ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {}
//it is simply an equality engine proof
static void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map);
void registerSkolem(Node equality, Node skolem);
+
+ static void setRowMergeTag(unsigned tag);
+ static void setRow1MergeTag(unsigned tag);
+ static void setExtMergeTag(unsigned tag);
};
namespace theory {
return n1;
}
- case theory::eq::MERGED_ARRAYS_ROW: {
- Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW encountered in UF_PROOF" << std::endl;
- Unreachable();
-
- Debug("pf::uf") << "row lemma: " << pf->d_node << std::endl;
- Assert(pf->d_node.getKind() == kind::EQUAL);
- 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]);
- Debug("pf::uf") << "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;
- Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
- }
- out << "(row _ _ ";
- tp->printTerm(t2.toExpr(), out, map);
- out << " ";
- tp->printTerm(t3.toExpr(), out, map);
- out << " ";
- tp->printTerm(t1.toExpr(), out, map);
- out << " ";
- tp->printTerm(t4.toExpr(), out, map);
- out << " " << ProofManager::getLitName(t2.eqNode(t3)) << ")";
- return ret;
- }
-
- case theory::eq::MERGED_ARRAYS_ROW1: {
- Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW1 encountered in UF_PROOF" << std::endl;
- Unreachable();
-
- Debug("pf::uf") << "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]);
- Debug("pf::uf") << "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;
- Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
- }
- out << "(row1 _ _ ";
- tp->printTerm(t1.toExpr(), out, map);
- out << " ";
- tp->printTerm(t2.toExpr(), out, map);
- out << " ";
- tp->printTerm(t3.toExpr(), out, map);
- out << ")";
- return ret;
- }
-
default:
Assert(!pf->d_node.isNull());
Assert(pf->d_children.empty());
/********************* */
/*! \file array_proof_reconstruction.h
- ** \verbatim
- **
- ** \brief Array-specific proof construction logic to be used during the
- ** equality engine's path reconstruction
- **/
+** \verbatim
+**
+** \brief Array-specific proof construction logic to be used during the
+** equality engine's path reconstruction
+**/
#include "theory/arrays/array_proof_reconstruction.h"
: d_equalityEngine(equalityEngine) {
}
-void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b,
+void ArrayProofReconstruction::setRowMergeTag(unsigned tag) {
+ d_reasonRow = tag;
+}
+
+void ArrayProofReconstruction::setRow1MergeTag(unsigned tag) {
+ d_reasonRow1 = tag;
+}
+
+void ArrayProofReconstruction::setExtMergeTag(unsigned tag) {
+ d_reasonExt = tag;
+}
+
+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;
- switch (reasonType) {
-
- case eq::MERGED_ARRAYS_EXT: {
+ 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.
childProof->d_node = reason;
proof->d_children.push_back(childProof);
}
- break;
}
- case eq::MERGED_ARRAYS_ROW: {
+ else if (reasonType == d_reasonRow) {
// ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
// The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
// or ((a[i]:=t)[k] == a[k]) because (i != k).
proof->d_children.push_back(childProof);
}
}
- break;
- }
- case eq::MERGED_ARRAYS_ROW1: {
- // No special handling required at this time
- break;
}
- default:
- break;
+ else if (reasonType == d_reasonRow1) {
+ // No special handling required at this time
}
}
public:
ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
- void notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b,
+ void notify(unsigned reasonType, Node reason, Node a, Node b,
std::vector<TNode>& equalities, eq::EqProof* proof) const;
+ void setRowMergeTag(unsigned tag);
+ void setRow1MergeTag(unsigned tag);
+ void setExtMergeTag(unsigned tag);
+
private:
+ /** Merge tag for ROW applications */
+ unsigned d_reasonRow;
+ /** Merge tag for ROW1 applications */
+ unsigned d_reasonRow1;
+ /** Merge tag for EXT applications */
+ unsigned d_reasonExt;
+
const eq::EqualityEngine* d_equalityEngine;
}; /* class ArrayProofReconstruction */
d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
}
- d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW, &d_proofReconstruction);
- d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW1, &d_proofReconstruction);
- d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_EXT, &d_proofReconstruction);
+ d_reasonRow = d_equalityEngine.getFreshMergeReasonType();
+ d_reasonRow1 = d_equalityEngine.getFreshMergeReasonType();
+ d_reasonExt = d_equalityEngine.getFreshMergeReasonType();
+
+ d_proofReconstruction.setRowMergeTag(d_reasonRow);
+ d_proofReconstruction.setRow1MergeTag(d_reasonRow1);
+ d_proofReconstruction.setExtMergeTag(d_reasonExt);
+
+ d_equalityEngine.addPathReconstructionTrigger(d_reasonRow, &d_proofReconstruction);
+ d_equalityEngine.addPathReconstructionTrigger(d_reasonRow1, &d_proofReconstruction);
+ d_equalityEngine.addPathReconstructionTrigger(d_reasonExt, &d_proofReconstruction);
}
TheoryArrays::~TheoryArrays() {
if (ni != node) {
preRegisterTermInternal(ni);
}
- d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1);
+ d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1);
Assert(++it == stores->end());
}
}
}
// Apply RIntro1 Rule
- d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, eq::MERGED_ARRAYS_ROW1);
+ d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
}
d_infoMap.addStore(node, node);
<< "\teq = " << eq << std::endl
<< "\treason = " << fact << std::endl;
- d_equalityEngine.assertEquality(eq, false, fact, eq::MERGED_ARRAYS_EXT);
+ d_equalityEngine.assertEquality(eq, false, fact, d_reasonExt);
++d_numProp;
}
d_infoMap.setRIntro1Applied(s);
Node ni = nm->mkNode(kind::SELECT, s, s[1]);
preRegisterTermInternal(ni);
- d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1);
+ d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1);
}
}
if (!bjExists) {
preRegisterTermInternal(bj);
}
- d_equalityEngine.assertEquality(aj_eq_bj, true, reason, eq::MERGED_ARRAYS_ROW);
+ d_equalityEngine.assertEquality(aj_eq_bj, true, reason, d_reasonRow);
++d_numProp;
return;
}
Node i_eq_j = i.eqNode(j);
Node reason = nm->mkNode(kind::OR, i_eq_j, aj_eq_bj);
d_permRef.push_back(reason);
- d_equalityEngine.assertEquality(i_eq_j, true, reason, eq::MERGED_ARRAYS_ROW);
+ d_equalityEngine.assertEquality(i_eq_j, true, reason, d_reasonRow);
++d_numProp;
return;
}
}
if (!d_inCheckModel) {
- if (proof) { proof->debug_print("pf::array"); }
- ProofArray* proof_array = d_proofsEnabled ? new ProofArray( proof ) : NULL;
+ ProofArray* proof_array = NULL;
+
+ if (d_proofsEnabled) {
+ proof->debug_print("pf::array");
+ proof_array = new ProofArray( proof );
+ proof_array->setRowMergeTag(d_reasonRow);
+ proof_array->setRow1MergeTag(d_reasonRow1);
+ proof_array->setExtMergeTag(d_reasonExt);
+ }
+
d_out->conflict(d_conflictNode, proof_array);
}
d_conflict = true;
}
-
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
/** conflicts in setModelVal */
IntStat d_numSetModelValConflicts;
+ // Merge reason types
+
+ /** Merge tag for ROW applications */
+ unsigned d_reasonRow;
+ /** Merge tag for ROW1 applications */
+ unsigned d_reasonRow1;
+ /** Merge tag for EXT applications */
+ unsigned d_reasonExt;
+
public:
TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
d_trueId = getNodeId(d_true);
d_falseId = getNodeId(d_false);
+
+ d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
}
EqualityEngine::~EqualityEngine() throw(AssertionException) {
return d_equalityNodes[nodeId];
}
-void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) {
Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl;
enqueue(MergeCandidate(t1Id, t2Id, pid, reason));
}
-void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) {
Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead");
assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid);
propagate();
}
-void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) {
Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
if (polarity) {
// If two terms are already equal, don't assert anything
}
-void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
+void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) {
Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl;
EqualityEdgeId edge = d_equalityEdges.size();
d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason));
// The current node
currentNode = bfsQueue[currentIndex].nodeId;
EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
- MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
+ unsigned reasonType = d_equalityEdges[currentEdge].getReasonType();
Node reason = d_equalityEdges[currentEdge].getReason();
Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
}
-void EqualityEngine::addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify) {
+void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) {
// Currently we can only inform one callback per trigger
Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end());
d_pathReconstructionTriggers[trigger] = notify;
}
+unsigned EqualityEngine::getFreshMergeReasonType() {
+ return d_freshMergeReasonType++;
+}
+
void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
{
Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
Debug( c ) << ")" << std::endl;
}
-
} // Namespace uf
} // Namespace theory
} // Namespace CVC4
virtual ~PathReconstructionNotify() {}
- virtual void notify(MergeReasonType reasonType, Node reason, Node a, Node b,
+ virtual void notify(unsigned reasonType, Node reason, Node a, Node b,
std::vector<TNode>& equalities, EqProof* proof) const = 0;
};
KindMap d_congruenceKindsInterpreted;
/** Objects that need to be notified during equality path reconstruction */
- std::map<MergeReasonType, const PathReconstructionNotify*> d_pathReconstructionTriggers;
+ std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
/** Map from nodes to their ids */
__gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
/** Memory for the use-list nodes */
std::vector<UseListNode> d_useListNodes;
+ /** A fresh merge reason type to return upon request */
+ unsigned d_freshMergeReasonType;
+
/**
* We keep a list of asserted equalities. Not among original terms, but
* among the class representatives.
// The next edge
EqualityEdgeId d_nextId;
// Type of reason for this equality
- MergeReasonType d_mergeType;
+ unsigned d_mergeType;
// Reason of this equality
TNode d_reason;
EqualityEdge():
d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {}
- EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason):
+ EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, unsigned type, TNode reason):
d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {}
/** Returns the id of the next edge */
EqualityNodeId getNodeId() const { return d_nodeId; }
/** The reason of this edge */
- MergeReasonType getReasonType() const { return d_mergeType; }
+ unsigned getReasonType() const { return d_mergeType; }
/** The reason of this edge */
TNode getReason() const { return d_reason; }
std::vector<EqualityEdgeId> d_equalityGraph;
/** Add an edge to the equality graph */
- void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason);
+ void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason);
/** Returns the equality node of the given node */
EqualityNode& getEqualityNode(TNode node);
/**
* Adds an equality of terms t1 and t2 to the database.
*/
- void assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+ void assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
/**
* Adds a trigger equality to the database with the trigger node and polarity for notification.
* asserting the negated predicate
* @param reason the reason to keep for building explanations
*/
- void assertPredicate(TNode p, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+ void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
/**
* Adds predicate p and q and makes them equal.
* asserting the negated equality
* @param reason the reason to keep for building explanations
*/
- void assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+ void assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
/**
* Returns the current representative of the term t.
/**
* Marks an object for merge type based notification during equality path reconstruction.
*/
- void addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify);
+ void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify);
+
+ /**
+ * Returns a fresh merge reason type tag for the client to use.
+ */
+ unsigned getFreshMergeReasonType();
};
/**
{
public:
EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
- MergeReasonType d_id;
+ unsigned d_id;
Node d_node;
std::vector< EqProof * > d_children;
void debug_print( const char * c, unsigned tb = 0 ) const;
MERGED_THROUGH_REFLEXIVITY,
/** Equality was merged to false, due to both sides of equality being a constant */
MERGED_THROUGH_CONSTANTS,
-
/** (for proofs only) Equality was merged due to transitivity */
MERGED_THROUGH_TRANS,
- /** Theory specific proof rules */
- MERGED_ARRAYS_ROW,
- MERGED_ARRAYS_ROW1,
- MERGED_ARRAYS_EXT
+ /** Reason types beyond this constant are theory specific reasons */
+ NUMBER_OF_MERGE_REASONS
};
inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
case MERGED_THROUGH_CONSTANTS:
out << "constants disequal";
break;
- // (for proofs only)
case MERGED_THROUGH_TRANS:
out << "transitivity";
break;
- case MERGED_ARRAYS_ROW:
- out << "arrays ROW";
- break;
- case MERGED_ARRAYS_ROW1:
- out << "arrays ROW1";
- break;
- case MERGED_ARRAYS_EXT:
- out << "arrays EXT";
- break;
-default:
+
+ default:
out << "[theory]";
break;
}
*/
struct MergeCandidate {
EqualityNodeId t1Id, t2Id;
- MergeReasonType type;
+ unsigned type;
TNode reason;
- MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason)
+ MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason)
: t1Id(x), t2Id(y), type(type), reason(reason)
{}
};
projects / cvc5.git / commitdiff