diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-08-03 21:49:20 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-08-03 21:49:20 +0000 |
| commit | 39a66fe81b66498c82d1638c58c3c4ccc8f586db (patch) | |
| tree | 5b423aabea9494abac34dad5bb5846cc7c1496c6 /src/theory/arrays | |
| parent | 3daaecd22fe5f6147cb08e5a4e08177b33a2daa2 (diff) | |
ArrayStoreAll infrastructure
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/kinds | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index eaef3746e..4a8695ec4 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -29,11 +29,19 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" +# storeall t e is \all i in indexType(t) <= e +constant STORE_ALL \ + ::CVC4::ArrayStoreAll \ + ::CVC4::ArrayStoreAllHashStrategy \ + "util/array_store_all.h" \ + "array store-all" + # used internally by array theory operator ARR_TABLE_FUN 4 "array table function" typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule +typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule endtheory |