diff options
author | guykatzz <katz911@gmail.com> | 2016-09-16 17:18:56 -0700 |
---|---|---|
committer | guykatzz <katz911@gmail.com> | 2016-09-16 17:18:56 -0700 |
commit | 53d625529c90c81b46a08811e4143552095fff9a (patch) | |
tree | 4c7359c2a9af6d35d6c64b2a09876b12f302108e /src/theory/arrays/array_proof_reconstruction.cpp | |
parent | 4745737174f9d48e68aa59823f25c0b3ce31cc3c (diff) |
In a ROW guard proof, if the transitivity proof does not have a disequality, we can deduce that it is a constant-disequality proof and process it accordingly
Diffstat (limited to 'src/theory/arrays/array_proof_reconstruction.cpp')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 9cba0592e..5ecccdd53 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -107,7 +107,14 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, // 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 && childProof->d_children.size() != 0) { + bool haveNegChild = false; + for (unsigned i = 0; i < childProof->d_children.size(); ++i) { + if (childProof->d_children[i]->d_node.getKind() == kind::NOT) + haveNegChild = true; + } + + if ((childProof->d_children.size() != 0) && + (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS || !haveNegChild)) { // The proof has two children, explaining why each index is a (different) constant. Assert(childProof->d_children.size() == 2); @@ -117,7 +124,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, 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); + Assert(childProof->d_children[0]->d_node.getKind() == kind::EQUAL); 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]; @@ -129,7 +136,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, 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); + Assert(childProof->d_children[1]->d_node.getKind() == kind::EQUAL); 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]; |