diff options
Diffstat (limited to 'src/theory/shared_data.h')
-rw-r--r-- | src/theory/shared_data.h | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h index 64b7f5ab1..0b21eedae 100644 --- a/src/theory/shared_data.h +++ b/src/theory/shared_data.h @@ -72,13 +72,15 @@ private: SharedData* d_proofNext; /** - * The equality that justifies this node being equal to - * the node at d_proofNext. Not valid if this is proof root. + * In order to precisely reconstruct the equality that justifies this node + * being equal to the node at d_proofNext, we need to know whether this edge + * has been switched. Value is meaningless at the proof root. */ - Node d_equality; + bool d_edgeReversed; /** - * The theory that can explain d_equality. Not valid if this is proof root. + * The theory that can explain the equality of this node and the node at + * d_proofNext. Not valid if this is proof root. */ theory::Theory* d_explainingTheory; @@ -157,14 +159,24 @@ public: void setProofNext(SharedData* pData) { makeCurrent(); d_proofNext = pData; } /** - * Get the equality associated with the link in the proof tree. + * Get the edge reversed property of this node */ - Node getEquality() const { return d_equality; } + bool getEdgeReversed() const { return d_edgeReversed; } /** - * Set the equality associated with the link in the proof tree. + * Set the edge reversed flag to value */ - void setEquality(TNode eq) { makeCurrent(); d_equality = eq; } + void setEdgeReversed(bool value) { makeCurrent(); d_edgeReversed = value; } + + /** + * Get the original equality that created the link from this node to the next + * proof node. + */ + Node getEquality() const { + return d_edgeReversed + ? NodeManager::currentNM()->mkNode(kind::EQUAL, d_proofNext->getRep(), d_rep) + : NodeManager::currentNM()->mkNode(kind::EQUAL, d_rep, d_proofNext->getRep()); + } /** * Get the explaining theory |