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 3dc19d39b1bf2f640f3c2ac5e39b1c0fcefdd07c..28953ab054d88b4cad34a9ad531c6db67871f35e 100644 (file)
--- 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<ArrayStoreAll>();
     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