diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-13 19:48:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 21:48:07 -0500 |
commit | 78c0daa482b35b95c90dd058ee4dd8a981e1337f (patch) | |
tree | c45fe72ac96032b0e6f7ea53798443671ad08d86 /src/theory/arrays | |
parent | 84fe644cb1956119b7b35ede06ee93583eae1925 (diff) |
Use TypeNode/Node in ArrayStoreAll (#4728)
This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 5 | ||||
-rw-r--r-- | src/theory/arrays/type_enumerator.h | 3 |
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; } |