diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-22 12:26:14 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-22 12:26:14 -0700 |
commit | 258a3f016b0957455ef3838a0b749c4a97fee41e (patch) | |
tree | 7c8648a59659ec94d19bebecdeec01329ba71c41 /src | |
parent | 204d645e97bbacd948b5777b704f7b418577610a (diff) |
Faster isConstarrayConst
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.cpp | 46 |
1 files changed, 25 insertions, 21 deletions
diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 6d16e4020..fe78ee74d 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -98,47 +98,51 @@ bool ArrayStoreTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) TNode index = n[1]; TNode value = n[2]; - // A constant must have only constant children and be in normal form - // If any child is non-const, this is not a constant - if (!store.isConst() || !index.isConst() || !value.isConst()) + unsigned depth = 1; + while (store.getKind() == kind::STORE) { - return false; + // A constant must have only constant children and be in normal form + // If any child is non-const, this is not a constant + if (!index.isConst() || !value.isConst()) + { + return false; + } + + // Normal form for nested stores is just ordering by index + if (!(store[1] < index)) + { + return false; + } + + depth += 1; + store = store[0]; } - // Normal form for nested stores is just ordering by index but also need to - // check that we are not writing to default value - if (store.getKind() == kind::STORE && (!(store[1] < index))) - { + if (store.getKind() != kind::STORE_ALL) { return false; } - unsigned depth = 1; - unsigned valCount = 1; + ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>(); + Node defaultValue = storeAll.getValue(); + + store = n[0]; while (store.getKind() == kind::STORE) { - depth += 1; - if (store[2] == value) + if (value == defaultValue) { - valCount += 1; + return false; } store = store[0]; } - Assert(store.getKind() == kind::STORE_ALL); - ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>(); - Node defaultValue = storeAll.getValue(); - if (value == defaultValue) - { - return false; - } // Get the cardinality of the index type Cardinality indexCard = index.getType().getCardinality(); - if (indexCard.isInfinite()) { return true; } + size_t valCount = 1; // When index sort is finite, we have to check whether there is any value // that is written to more than the default value. If so, it is not in // normal form. |