From 0e68cfe050946d1ed9544dffcbd5e75be0e6f22f Mon Sep 17 00:00:00 2001 From: Guy Date: Fri, 16 Sep 2016 16:26:30 -0700 Subject: [PATCH] Handling a corner case where a ROW's guard is a constant disequality. If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality --- src/theory/arrays/array_proof_reconstruction.cpp | 2 +- src/theory/uf/equality_engine.cpp | 9 ++++++++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 8dd7fe782..9cba0592e 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -107,7 +107,7 @@ 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) { + if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS && childProof->d_children.size() != 0) { // The proof has two children, explaining why each index is a (different) constant. Assert(childProof->d_children.size() == 2); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index f98ad556f..5d929a708 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -987,7 +987,14 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec } if (eqp) { - if(eqp->d_children.size() == 1) { + if (eqp->d_children.size() == 0) { + // Corner case where this is actually a disequality between two constants + Debug("pf::ee") << "Encountered a constant disequality (not a transitivity proof): " + << eqp->d_node << std::endl; + Assert(eqp->d_node[0][0].isConst()); + Assert(eqp->d_node[0][1].isConst()); + eqp->d_id = MERGED_THROUGH_CONSTANTS; + } else if (eqp->d_children.size() == 1) { // The transitivity proof has just one child. Simplify. EqProof* temp = eqp->d_children[0]; eqp->d_children.clear(); -- 2.30.2