summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arrays/array_proof_reconstruction.cpp40
-rw-r--r--src/theory/arrays/array_proof_reconstruction.h13
-rw-r--r--src/theory/arrays/theory_arrays.cpp39
-rw-r--r--src/theory/arrays/theory_arrays.h9
-rw-r--r--src/theory/uf/equality_engine.cpp19
-rw-r--r--src/theory/uf/equality_engine.h30
-rw-r--r--src/theory/uf/equality_engine_types.h24
7 files changed, 107 insertions, 67 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index b2e8c3ab3..c8a6716f5 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -1,10 +1,10 @@
/********************* */
/*! \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"
@@ -16,16 +16,26 @@ ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equ
: 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.
@@ -33,10 +43,9 @@ void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reaso
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).
@@ -103,16 +112,11 @@ void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reaso
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
}
}
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
index 8afc0d3f7..6502b0e6b 100644
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ b/src/theory/arrays/array_proof_reconstruction.h
@@ -26,10 +26,21 @@ class ArrayProofReconstruction : public eq::PathReconstructionNotify {
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 */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 37854ee90..8d97eb89d 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -129,9 +129,17 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
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() {
@@ -665,7 +673,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
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());
}
}
@@ -751,7 +759,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
}
// 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);
@@ -1367,7 +1375,7 @@ void TheoryArrays::check(Effort e) {
<< "\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;
}
@@ -1669,7 +1677,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
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);
}
}
@@ -1976,7 +1984,7 @@ void TheoryArrays::propagate(RowLemmaType lem)
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;
}
@@ -1986,7 +1994,7 @@ void TheoryArrays::propagate(RowLemmaType lem)
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;
}
@@ -2230,15 +2238,22 @@ void TheoryArrays::conflict(TNode a, TNode b) {
}
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 */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 6d2bb9e73..14e5a622a 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -125,6 +125,15 @@ class TheoryArrays : public Theory {
/** 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,
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index d4a1e5ca4..20d0d85a8 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -93,6 +93,8 @@ void EqualityEngine::init() {
d_trueId = getNodeId(d_true);
d_falseId = getNodeId(d_false);
+
+ d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
}
EqualityEngine::~EqualityEngine() throw(AssertionException) {
@@ -389,7 +391,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const
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;
@@ -407,7 +409,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, Me
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);
@@ -420,7 +422,7 @@ void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
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
@@ -888,7 +890,7 @@ void EqualityEngine::backtrack() {
}
-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));
@@ -1089,7 +1091,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
// 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;
@@ -1711,12 +1713,16 @@ size_t EqualityEngine::getSize(TNode t) {
}
-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;
@@ -2221,7 +2227,6 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{
Debug( c ) << ")" << std::endl;
}
-
} // Namespace uf
} // Namespace theory
} // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 97abfccf1..7bc645c24 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -149,7 +149,7 @@ public:
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;
};
@@ -231,7 +231,7 @@ private:
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;
@@ -274,6 +274,9 @@ private:
/** 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.
@@ -304,7 +307,7 @@ private:
// 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;
@@ -313,7 +316,7 @@ private:
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 */
@@ -323,7 +326,7 @@ private:
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; }
@@ -348,7 +351,7 @@ private:
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);
@@ -520,7 +523,7 @@ private:
/**
* 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.
@@ -744,7 +747,7 @@ public:
* 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.
@@ -759,7 +762,7 @@ public:
* 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.
@@ -851,7 +854,12 @@ public:
/**
* 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();
};
/**
@@ -895,7 +903,7 @@ class EqProof
{
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;
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 0c2c3e354..5bf9db436 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -67,14 +67,11 @@ enum MergeReasonType {
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) {
@@ -91,20 +88,11 @@ 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;
}
@@ -117,9 +105,9 @@ default:
*/
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)
{}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback