diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-20 20:00:22 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 18:11:56 -0400 |
| commit | 1a41e26473ff12108eb6700da3d386ffa9e731bd (patch) | |
| tree | 0bd5e31740d2c3a7c89a0a7e663b734b98982e79 /src/theory/arrays | |
| parent | 75ec455661ecc88a8b9f77f7b913c227b7f3e728 (diff) | |
Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, and arith.
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/kinds | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index a731d3677..0bc973de9 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -26,20 +26,20 @@ enumerator ARRAY_TYPE \ "theory/arrays/type_enumerator.h" # select a i is a[i] -operator SELECT 2 "array select" +operator SELECT 2 "array select; first parameter is an array term, second is the selection index" # store a i e is a[i] <= e -operator STORE 3 "array store" +operator STORE 3 "array store; first parameter is an array term, second is the store index, third is the term to store at the index" # storeall t e is \all i in indexType(t) <= e constant STORE_ALL \ ::CVC4::ArrayStoreAll \ ::CVC4::ArrayStoreAllHashFunction \ "util/array_store_all.h" \ - "array store-all" + "array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)" # used internally by array theory -operator ARR_TABLE_FUN 4 "array table function (internal symbol)" +operator ARR_TABLE_FUN 4 "array table function (internal-only symbol)" typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule |