diff options
Diffstat (limited to 'src/theory/arrays/array_proof_reconstruction.cpp')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 40 |
1 files changed, 22 insertions, 18 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 } } |