diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-09 14:47:53 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 07:25:13 -0500 |
commit | 50c26544c83a71e87efa487e4af063b1b5647c0f (patch) | |
tree | 82d4f3b2632a2cf06aff70550f37f80dc80d9543 /src/expr/node_manager.h | |
parent | 53b8499f48a00dc876d56c76fbc79aafe5803529 (diff) |
add new theory (sets)
Specification (smt2) -- as per this commit, subject to change
- Parameterized sort Set, e.g. (Set Int)
- Empty set constant (typed), use with "as" to specify the type, e.g.
(as emptyset (Set Int))
- Create a singleton set
(setenum X (Set X)) : creates singleton set
- Functions/operators
(union (Set X) (Set X) (Set X))
(intersection (Set X) (Set X) (Set X))
(setminus (Set X) (Set X) (Set X))
- Predicates
(in X (Set X) Bool) : membership
(subseteq (Set X) (Set X) Bool) : set containment
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index caf8f5ad4..b4d20b514 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -751,6 +751,9 @@ public: /** Make the type of arrays with the given parameterization */ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + /** Make the type of arrays with the given parameterization */ + inline TypeNode mkSetType(TypeNode elementType); + /** Make a type representing a constructor with the given parameterization */ TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range); @@ -1058,6 +1061,16 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } +inline TypeNode NodeManager::mkSetType(TypeNode elementType) { + CheckArgument(!elementType.isNull(), elementType, + "unexpected NULL element type"); + // TODO: Confirm meaning of isFunctionLike(). --K + CheckArgument(!elementType.isFunctionLike(), elementType, + "cannot store function-like types in sets"); + Debug("sets") << "making sets type " << elementType << std::endl; + return mkTypeNode(kind::SET_TYPE, elementType); +} + inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { CheckArgument(!domain.isFunctionLike(), domain, "cannot create higher-order function types"); |