diff options
author | Guy <katz911@gmail.com> | 2016-03-24 16:56:13 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-03-24 16:56:13 -0700 |
commit | 399788b6e81f9718e7870ef0b8061a77fb22b9cf (patch) | |
tree | 5953146e657760a357d1abaf987df049f150a3c3 /src/theory/arrays/array_proof_reconstruction.cpp | |
parent | ea75c6f2b6e3a374efdccbfc9a01074609c13a57 (diff) |
Refactored the equality engine in order to remove theory-specific logic from equality path reconstruction
Diffstat (limited to 'src/theory/arrays/array_proof_reconstruction.cpp')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp new file mode 100644 index 000000000..b2e8c3ab3 --- /dev/null +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -0,0 +1,121 @@ +/********************* */ +/*! \file array_proof_reconstruction.h + ** \verbatim + ** + ** \brief Array-specific proof construction logic to be used during the + ** equality engine's path reconstruction + **/ + +#include "theory/arrays/array_proof_reconstruction.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine) + : d_equalityEngine(equalityEngine) { +} + +void ArrayProofReconstruction::notify(eq::MergeReasonType 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 (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; + childProof->d_node = reason; + proof->d_children.push_back(childProof); + } + break; + } + + case eq::MERGED_ARRAYS_ROW: { + // 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). + + if (proof) { + if (a.getNumChildren() == 2) { + // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k). + + // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be + // false in the first case and true in the second case. + bool currentNodeIsUnchangedArray; + + Assert(a.getNumChildren() == 2); + Assert(b.getNumChildren() == 2); + + if (a[0].getKind() == kind::VARIABLE || a[0].getKind() == kind::SKOLEM) { + currentNodeIsUnchangedArray = true; + } else if (b[0].getKind() == kind::VARIABLE || b[0].getKind() == kind::SKOLEM) { + currentNodeIsUnchangedArray = false; + } else { + Assert(a[0].getKind() == kind::STORE); + Assert(b[0].getKind() == kind::STORE); + + if (a[0][0] == b[0]) { + currentNodeIsUnchangedArray = false; + } else if (b[0][0] == a[0]) { + currentNodeIsUnchangedArray = true; + } else { + Unreachable(); + } + } + + Node indexOne = currentNodeIsUnchangedArray ? a[1] : a[0][1]; + Node indexTwo = currentNodeIsUnchangedArray ? b[0][1] : b[1]; + + // Some assertions to ensure that the theory of arrays behaves as expected + Assert(a[1] == b[1]); + if (currentNodeIsUnchangedArray) { + Assert(a[0] == b[0][0]); + } else { + Assert(a[0][0] == b[0]); + } + + Debug("pf::ee") << "Getting explanation for ROW guard: " + << indexOne << " != " << indexTwo << std::endl; + + eq::EqProof* childProof = new eq::EqProof; + d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof); + proof->d_children.push_back(childProof); + } else { + // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), + + Node indexOne = a; + Node indexTwo = b; + + Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl + << "The reason for the edge is: " << reason << std::endl; + + 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); + proof->d_children.push_back(childProof); + } + } + break; + } + + case eq::MERGED_ARRAYS_ROW1: { + // No special handling required at this time + break; + } + + default: + break; + } +} + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |