Use TypeNode/Node in ArrayStoreAll (#4728)

This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.

4 files changed, 11 insertions, 11 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 49f93286e..37443c070 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -808,7 +808,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
       break;
     }
     ArrayStoreAll storeAll = node.getConst<ArrayStoreAll>();
-    Node defaultValue = Node::fromExpr(storeAll.getExpr());
+    Node defaultValue = storeAll.getValue();
     if (!defaultValue.isConst()) {
       throw LogicException("Array theory solver does not yet support non-constant default values for arrays");
     }
@@ -1230,7 +1230,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
       }
 
       // Build the STORE_ALL term with the default value
-      rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr()));
+      rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep));
       /*
     }
     else {
@@ -1904,7 +1904,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
   TNode constArr = d_infoMap.getConstArr(a);
   if (!constArr.isNull()) {
     ArrayStoreAll storeAll = constArr.getConst<ArrayStoreAll>();
-    Node defValue = Node::fromExpr(storeAll.getExpr());
+    Node defValue = storeAll.getValue();
     Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
     if (!d_equalityEngine.hasTerm(selConst)) {
       preRegisterTermInternal(selConst);
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index e81b7d7c0..e8f03c1d0 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -93,7 +93,7 @@ class TheoryArraysRewriter : public TheoryRewriter
     }
     Assert(store.getKind() == kind::STORE_ALL);
     ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
-    Node defaultValue = Node::fromExpr(storeAll.getExpr());
+    Node defaultValue = storeAll.getValue();
     NodeManager* nm = NodeManager::currentNM();
 
     // Check if we are writing to default value - if so the store
@@ -214,7 +214,7 @@ class TheoryArraysRewriter : public TheoryRewriter
       std::sort(newIndices.begin(), newIndices.end());
     }
 
-    n = nm->mkConst(ArrayStoreAll(node.getType().toType(), maxValue.toExpr()));
+    n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
     std::vector<Node>::iterator itNew = newIndices.begin(), it_end = newIndices.end();
     while (itNew != it_end || !indices.empty()) {
       if (itNew != it_end && (indices.empty() || (*itNew) < indices.back())) {
@@ -267,7 +267,7 @@ class TheoryArraysRewriter : public TheoryRewriter
         if (store.getKind() == kind::STORE_ALL) {
           // select(store_all(v),i) = v
           ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
-          n = Node::fromExpr(storeAll.getExpr());
+          n = storeAll.getValue();
           Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
           Assert(n.isConst());
           return RewriteResponse(REWRITE_DONE, n);
@@ -432,7 +432,7 @@ class TheoryArraysRewriter : public TheoryRewriter
         if (store.getKind() == kind::STORE_ALL) {
           // select(store_all(v),i) = v
           ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
-          n = Node::fromExpr(storeAll.getExpr());
+          n = storeAll.getValue();
           Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
           Assert(n.isConst());
           return RewriteResponse(REWRITE_DONE, n);
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index e5681d50f..56c51d9bf 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -69,8 +69,7 @@ struct ArrayStoreTypeRule {
     else {
       Assert(n.getKind() == kind::STORE_ALL);
       ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
-      ArrayType arrayType = storeAll.getType();
-      return TypeNode::fromType(arrayType);
+      return storeAll.getType();
     }
   }
 
@@ -106,7 +105,7 @@ struct ArrayStoreTypeRule {
     }
     Assert(store.getKind() == kind::STORE_ALL);
     ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
-    Node defaultValue = Node::fromExpr(storeAll.getExpr());
+    Node defaultValue = storeAll.getValue();
     if (value == defaultValue) {
       return false;
     }
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 3da793617..5894501b2 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -53,7 +53,8 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
   {
     d_indexVec.push_back(*d_index);
     d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
-    d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
+    d_arrayConst =
+        d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back()))));
     Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl;
   }