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 | |
parent | 3daaecd22fe5f6147cb08e5a4e08177b33a2daa2 (diff) |
ArrayStoreAll infrastructure
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/kinds | 8 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 1 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 7 |
3 files changed, 16 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 diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 39945e081..57baa82cd 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -270,6 +270,7 @@ constant UNINTERPRETED_CONSTANT \ ::CVC4::UninterpretedConstantHashStrategy \ "util/uninterpreted_constant.h" \ "The kind of nodes representing uninterpreted constants" +typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule enumerator SORT_TYPE \ ::CVC4::theory::builtin::UninterpretedSortEnumerator \ "theory/builtin/type_enumerator.h" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 9b0611ed8..d443b8452 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -130,6 +130,13 @@ public: } };/* class TupleTypeRule */ +class UninterpretedConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + return TypeNode::fromType(n.getConst<UninterpretedConstant>().getType()); + } +};/* class UninterpretedConstantTypeRule */ + class StringConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { |