diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 51 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 |
2 files changed, 55 insertions, 1 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 11c3dc081..6dfd14157 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -101,8 +101,59 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, 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); + + // It could be that the guard condition is a constant disequality. In this case, + // we need to change it to a different format. + if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { + // The proof has two children, explaining why each index is a (different) constant. + Assert(childProof->d_children.size() == 2); + + Node constantOne, constantTwo; + // Each subproof explains why one of the indices is constant. + + if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantOne = childProof->d_children[0]->d_node; + } else { + Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY); + if ((childProof->d_children[0]->d_node[0] == indexOne) || + (childProof->d_children[0]->d_node[0] == indexTwo)) { + constantOne = childProof->d_children[0]->d_node[1]; + } else { + constantOne = childProof->d_children[0]->d_node[0]; + } + } + + if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantTwo = childProof->d_children[1]->d_node; + } else { + Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY); + if ((childProof->d_children[1]->d_node[0] == indexOne) || + (childProof->d_children[1]->d_node[0] == indexTwo)) { + constantTwo = childProof->d_children[1]->d_node[1]; + } else { + constantTwo = childProof->d_children[1]->d_node[0]; + } + } + + eq::EqProof* constantDisequalityProof = new eq::EqProof; + constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS; + constantDisequalityProof->d_node = + NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate(); + + // Middle is where we need to insert the new disequality + std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin(); + ++middle; + + childProof->d_children.insert(middle, constantDisequalityProof); + + childProof->d_id = theory::eq::MERGED_THROUGH_TRANS; + childProof->d_node = + NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate(); + } + proof->d_children.push_back(childProof); } else { // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6add1b55f..28a08630e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -829,7 +829,8 @@ void TheoryArrays::propagate(Effort e) Node TheoryArrays::explain(TNode literal) { - return explain(literal, NULL); + Node explanation = explain(literal, NULL); + return explanation; } Node TheoryArrays::explain(TNode literal, eq::EqProof *proof) @@ -1394,6 +1395,7 @@ void TheoryArrays::check(Effort e) { break; default: Unreachable(); + break; } } @@ -2231,6 +2233,7 @@ bool TheoryArrays::dischargeLemmas() void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; + if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b), proof); } else { |