From: Andrew Reynolds Date: Fri, 18 Sep 2020 15:07:12 +0000 (-0500) Subject: Logic exception for arrays indexed by arrays (#5073) X-Git-Tag: cvc5-1.0.0~2838 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f714e763e57a8e7fc32c6bd0fbab279eac2f993;p=cvc5.git Logic exception for arrays indexed by arrays (#5073) This throws a logic exception when a term of array type whose index is also an array is registered to the theory of arrays. It refactors the preRegisterTermInternal method of arrays so that all non-equality terms are added to the equality engine in the same block of code, which also checks for the type. Fixes #4237. FYI @barrettcw --- diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3dc19d39b..28953ab05 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -643,115 +643,131 @@ void TheoryArrays::preRegisterTermInternal(TNode node) return; } Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; - switch (node.getKind()) { - case kind::EQUAL: + Kind nk = node.getKind(); + if (nk == kind::EQUAL) + { // Add the trigger for equality // NOTE: note that if the equality is true or false already, it might not be added d_equalityEngine->addTriggerPredicate(node); - break; - case kind::SELECT: { + return; + } + else if (d_equalityEngine->hasTerm(node)) + { // Invariant: array terms should be preregistered before being added to the equality engine - if (d_equalityEngine->hasTerm(node)) + Assert(nk != kind::SELECT + || d_isPreRegistered.find(node) != d_isPreRegistered.end()); + return; + } + // add to equality engine and the may equality engine + TypeNode nodeType = node.getType(); + if (nodeType.isArray()) + { + // index type should not be an array, otherwise we throw a logic exception + if (nodeType.getArrayIndexType().isArray()) { - Assert(d_isPreRegistered.find(node) != d_isPreRegistered.end()); - return; + std::stringstream ss; + ss << "Arrays cannot be indexed by array types, offending array type is " + << nodeType; + throw LogicException(ss.str()); } - // Reads - TNode store = d_equalityEngine->getRepresentative(node[0]); - - // The may equal needs the store - d_mayEqualEqualityEngine.addTerm(store); + d_mayEqualEqualityEngine.addTerm(node); + } + d_equalityEngine->addTerm(node); - if (node.getType().isArray()) - { - d_mayEqualEqualityEngine.addTerm(node); - d_equalityEngine->addTerm(node); - } - else + switch (node.getKind()) + { + case kind::SELECT: { - d_equalityEngine->addTerm(node); - } - Assert((d_isPreRegistered.insert(node), true)); + // Reads + TNode store = d_equalityEngine->getRepresentative(node[0]); - Assert(d_equalityEngine->getRepresentative(store) == store); - d_infoMap.addIndex(store, node[1]); + // The may equal needs the store + d_mayEqualEqualityEngine.addTerm(store); - // Synchronize d_constReadsContext with SAT context - Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); - while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { - d_constReadsContext->push(); - } + Assert((d_isPreRegistered.insert(node), true)); - // Record read in sharing data structure - TNode index = d_equalityEngine->getRepresentative(node[1]); - if (!options::arraysWeakEquivalence() && index.isConst()) { - CTNodeList* temp; - CNodeNListMap::iterator it = d_constReads.find(index); - if (it == d_constReads.end()) { - temp = new(true) CTNodeList(d_constReadsContext); - d_constReads[index] = temp; + Assert(d_equalityEngine->getRepresentative(store) == store); + d_infoMap.addIndex(store, node[1]); + + // Synchronize d_constReadsContext with SAT context + Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); + while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) + { + d_constReadsContext->push(); } - else { - temp = (*it).second; + + // Record read in sharing data structure + TNode index = d_equalityEngine->getRepresentative(node[1]); + if (!options::arraysWeakEquivalence() && index.isConst()) + { + CTNodeList* temp; + CNodeNListMap::iterator it = d_constReads.find(index); + if (it == d_constReads.end()) + { + temp = new (true) CTNodeList(d_constReadsContext); + d_constReads[index] = temp; + } + else + { + temp = (*it).second; + } + temp->push_back(node); + d_constReadsList.push_back(node); + } + else + { + d_reads.push_back(node); } - temp->push_back(node); - d_constReadsList.push_back(node); - } - else { - d_reads.push_back(node); - } - checkRowForIndex(node[1], store); - break; - } - case kind::STORE: { - if (d_equalityEngine->hasTerm(node)) - { + checkRowForIndex(node[1], store); break; } - d_equalityEngine->addTerm(node); - - TNode a = d_equalityEngine->getRepresentative(node[0]); + case kind::STORE: + { + TNode a = d_equalityEngine->getRepresentative(node[0]); - if (node.isConst()) { - // Can't use d_mayEqualEqualityEngine to merge node with a because they are both constants, - // so just set the default value manually for node. - Assert(a == node[0]); - d_mayEqualEqualityEngine.addTerm(node); - Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node); - Assert(d_mayEqualEqualityEngine.getRepresentative(a) == a); - DefValMap::iterator it = d_defValues.find(a); - Assert(it != d_defValues.end()); - d_defValues[node] = (*it).second; - } - else { - d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true); - Assert(d_mayEqualEqualityEngine.consistent()); - } + if (node.isConst()) + { + // Can't use d_mayEqualEqualityEngine to merge node with a because they + // are both constants, so just set the default value manually for node. + Assert(a == node[0]); + d_mayEqualEqualityEngine.addTerm(node); + Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node); + Assert(d_mayEqualEqualityEngine.getRepresentative(a) == a); + DefValMap::iterator it = d_defValues.find(a); + Assert(it != d_defValues.end()); + d_defValues[node] = (*it).second; + } + else + { + d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true); + Assert(d_mayEqualEqualityEngine.consistent()); + } - TNode i = node[1]; - TNode v = node[2]; - NodeManager* nm = NodeManager::currentNM(); - Node ni = nm->mkNode(kind::SELECT, node, i); - if (!d_equalityEngine->hasTerm(ni)) - { - preRegisterTermInternal(ni); - } + TNode i = node[1]; + TNode v = node[2]; + NodeManager* nm = NodeManager::currentNM(); + Node ni = nm->mkNode(kind::SELECT, node, i); + if (!d_equalityEngine->hasTerm(ni)) + { + preRegisterTermInternal(ni); + } - // Apply RIntro1 Rule - d_equalityEngine->assertEquality( - ni.eqNode(v), true, d_true, theory::eq::MERGED_THROUGH_ROW1); + // Apply RIntro1 Rule + d_equalityEngine->assertEquality( + ni.eqNode(v), true, d_true, theory::eq::MERGED_THROUGH_ROW1); - d_infoMap.addStore(node, node); - d_infoMap.addInStore(a, node); - d_infoMap.setModelRep(node, node); + d_infoMap.addStore(node, node); + d_infoMap.addInStore(a, node); + d_infoMap.setModelRep(node, node); - //Add-Store for Weak Equivalence - if (options::arraysWeakEquivalence()) { - Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a)); - Assert(weakEquivGetRep(node) == node); - d_infoMap.setWeakEquivPointer(node, node[0]); - d_infoMap.setWeakEquivIndex(node, node[1]); + // Add-Store for Weak Equivalence + if (options::arraysWeakEquivalence()) + { + Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a)); + Assert(weakEquivGetRep(node) == node); + d_infoMap.setWeakEquivPointer(node, node[0]); + d_infoMap.setWeakEquivIndex(node, node[1]); #ifdef CVC4_ASSERTIONS checkWeakEquiv(false); #endif @@ -761,33 +777,18 @@ void TheoryArrays::preRegisterTermInternal(TNode node) break; } case kind::STORE_ALL: { - if (d_equalityEngine->hasTerm(node)) - { - break; - } ArrayStoreAll storeAll = node.getConst(); Node defaultValue = storeAll.getValue(); if (!defaultValue.isConst()) { throw LogicException("Array theory solver does not yet support non-constant default values for arrays"); } d_infoMap.setConstArr(node, node); - d_mayEqualEqualityEngine.addTerm(node); Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node); - d_equalityEngine->addTerm(node); d_defValues[node] = defaultValue; break; } default: - // Variables etc - if (node.getType().isArray()) { - // The may equal needs the node - d_mayEqualEqualityEngine.addTerm(node); - d_equalityEngine->addTerm(node); - } - else { - d_equalityEngine->addTerm(node); - } - + // Variables etc, already processed above break; } // Invariant: preregistered terms are exactly the terms in the equality engine