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

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");