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

35 files changed, 2135 insertions, 10 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index f20fabf6b..86067d3ef 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -20,7 +20,7 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv arrays datatypes strings quantifiers rewriterules idl
+THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers rewriterules idl
 
 lib_LTLIBRARIES = libcvc4.la
 
@@ -220,6 +220,13 @@ libcvc4_la_SOURCES = \
 	theory/datatypes/theory_datatypes.h \
 	theory/datatypes/datatypes_rewriter.h \
 	theory/datatypes/theory_datatypes.cpp \
+	theory/sets/theory_sets.h \
+	theory/sets/theory_sets.cpp \
+	theory/sets/theory_sets_private.h \
+	theory/sets/theory_sets_private.cpp \
+	theory/sets/theory_sets_rewriter.h \
+	theory/sets/theory_sets_rewriter.cpp \
+	theory/sets/theory_sets_type_rules.h \
 	theory/strings/theory_strings.h \
 	theory/strings/theory_strings.cpp \
 	theory/strings/theory_strings_rewriter.h \
@@ -453,6 +460,7 @@ EXTRA_DIST = \
 	theory/idl/kinds \
 	theory/builtin/kinds \
 	theory/datatypes/kinds \
+	theory/sets/kinds \
 	theory/strings/kinds \
 	theory/arrays/kinds \
 	theory/quantifiers/kinds \
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index e2ffac49b..881c3f629 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -57,6 +57,10 @@ public:
     return super::size();
   }
 
+  bool empty() const {
+    return super::empty();
+  }
+
   bool insert(const V& v) {
     return super::insert_safe(v, true);
   }
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5fe7b34c1..41f69e587 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -540,6 +540,11 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 }
 
+SetType ExprManager::mkSetType(Type elementType) const {
+  NodeManagerScope nms(d_nodeManager);
+  return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
+}
+
 DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
   // Not worth a special implementation; this doesn't need to be fast
   // code anyway.
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 3f0ec2f9c..f5e01d545 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -376,6 +376,9 @@ public:
   /** Make the type of arrays with the given parameterization. */
   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 
+  /** Make the type of set with the given parameterization. */
+  SetType mkSetType(Type elementType) const;
+
   /** Make a type representing the given datatype. */
   DatatypeType mkDatatypeType(const Datatype& datatype);
 
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");
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 672fc6aae..d0fe77aae 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -292,6 +292,12 @@ bool Type::isArray() const {
   return d_typeNode->isArray();
 }
 
+/** Is this a Set type? */
+bool Type::isSet() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSet();
+}
+
 /** Is this a sort kind */
 bool Type::isSort() const {
   NodeManagerScope nms(d_nodeManager);
@@ -480,6 +486,11 @@ ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) :
   CheckArgument(isNull() || isArray(), this);
 }
 
+SetType::SetType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  CheckArgument(isNull() || isSet(), this);
+}
+
 SortType::SortType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   CheckArgument(isNull() || isSort(), this);
@@ -517,6 +528,10 @@ Type ArrayType::getConstituentType() const {
   return makeType(d_typeNode->getArrayConstituentType());
 }
 
+Type SetType::getElementType() const {
+  return makeType(d_typeNode->getSetElementType());
+}
+
 DatatypeType ConstructorType::getRangeType() const {
   return DatatypeType(makeType(d_typeNode->getConstructorRangeType()));
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 3c772d461..b4761e1d6 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -49,6 +49,7 @@ class RealType;
 class StringType;
 class BitVectorType;
 class ArrayType;
+class SetType;
 class DatatypeType;
 class ConstructorType;
 class SelectorType;
@@ -301,6 +302,12 @@ public:
   bool isArray() const;
 
   /**
+   * Is this a Set type?
+   * @return true if the type is a Set type
+   */
+  bool isSet() const;
+
+ /**
    * Is this a datatype type?
    * @return true if the type is a datatype type
    */
@@ -489,6 +496,20 @@ public:
 };/* class ArrayType */
 
 /**
+ * Class encapsulating an set type.
+ */
+class CVC4_PUBLIC SetType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SetType(const Type& type = Type()) throw(IllegalArgumentException);
+
+  /** Get the index type */
+  Type getElementType() const;
+};/* class SetType */
+
+/**
  * Class encapsulating a user-defined sort.
  */
 class CVC4_PUBLIC SortType : public Type {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index c823190bf..a49ae31bf 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -466,6 +466,9 @@ public:
   /** Is this an array type? */
   bool isArray() const;
 
+  /** Is this a Set type? */
+  bool isSet() const;
+
   /** Get the index type (for array types) */
   TypeNode getArrayIndexType() const;
 
@@ -475,6 +478,9 @@ public:
   /** Get the return type (for constructor types) */
   TypeNode getConstructorRangeType() const;
 
+  /** Get the element type (for set types) */
+  TypeNode getSetElementType() const;
+
   /**
    * Is this a function type?  Function-like things (e.g. datatype
    * selectors) that aren't actually functions are NOT considered
@@ -867,6 +873,15 @@ inline TypeNode TypeNode::getConstructorRangeType() const {
   return (*this)[getNumChildren()-1];
 }
 
+inline bool TypeNode::isSet() const {
+  return getKind() == kind::SET_TYPE;
+}
+
+inline TypeNode TypeNode::getSetElementType() const {
+  Assert(isSet());
+  return (*this)[0];
+}
+
 inline bool TypeNode::isFunction() const {
   return getKind() == kind::FUNCTION_TYPE;
 }
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 5b0894680..8780922c9 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -40,7 +40,9 @@ OPTIONS_FILES_SRCS = \
 	../parser/options.cpp \
 	../parser/options.h \
 	../theory/idl/options.cpp \
-	../theory/idl/options.h
+	../theory/idl/options.h \
+	../theory/sets/options.cpp \
+	../theory/sets/options.h
 
 OPTIONS_FILES = \
 	$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
@@ -101,7 +103,9 @@ nodist_liboptions_la_SOURCES = \
 	../parser/options.cpp \
 	../parser/options.h \
 	../theory/idl/options.cpp \
-	../theory/idl/options.h
+	../theory/idl/options.h \
+	../theory/sets/options.cpp \
+	../theory/sets/options.h
 
 BUILT_SOURCES = \
 	exprs-builts \
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f97f4a8ae..6974c62af 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -833,6 +833,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
                              MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
         v.insert(v.end(), f.begin(), f.end());
         expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+      } else if(f.getKind() == CVC4::kind::EMPTYSET) {
+        Debug("parser") << "Empty set encountered: " << f << " "
+                          << f2 << " " << type <<  std::endl;
+        // TODO: what is f2 about, should we add some assertions?
+        expr = MK_CONST( ::CVC4::EmptySet(type) );
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1028,6 +1033,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | str[s,false]
     { expr = MK_CONST( ::CVC4::String(s) ); }
 
+  | EMPTYSET_TOK
+    { expr = MK_CONST( ::CVC4::EmptySet()); }
+
     // NOTE: Theory constants go here
   ;
 
@@ -1298,6 +1306,12 @@ builtinOp[CVC4::Kind& kind]
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
+  | SETUNION_TOK  { $kind = CVC4::kind::UNION; }
+  | SETINT_TOK    { $kind = CVC4::kind::INTERSECTION; }
+  | SETMINUS_TOK  { $kind = CVC4::kind::SETMINUS; }
+  | SETSUB_TOK    { $kind = CVC4::kind::SUBSET; }
+  | SETIN_TOK     { $kind = CVC4::kind::IN; }
+  | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; }
 
   // NOTE: Theory operators go here
   ;
@@ -1407,6 +1421,11 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
           PARSER_STATE->parseError("Illegal array type.");
         }
         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
+      } else if(name == "Set") {
+        if(args.size() != 1) {
+          PARSER_STATE->parseError("Illegal set type.");
+        }
+        t = EXPR_MANAGER->mkSetType( args[0] );
       } else if(check == CHECK_DECLARED ||
                 PARSER_STATE->isDeclared(name, SYM_SORT)) {
         t = PARSER_STATE->getSort(name, args);
@@ -1688,6 +1707,14 @@ REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
 RERANGE_TOK : 're.range';
 
+SETUNION_TOK: 'union';
+SETINT_TOK: 'intersection';
+SETMINUS_TOK: 'setminus';
+SETSUB_TOK: 'subseteq';
+SETIN_TOK: 'in';
+SETSINGLETON_TOK: 'setenum';
+EMPTYSET_TOK: 'emptyset';
+
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
  * and ends with | and does not otherwise contain |.
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5dc3043af..fcb352ea7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -203,6 +203,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
+    case kind::EMPTYSET:
+      out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
+      break;
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -343,7 +347,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     stillNeedToPrintParams = false;
     break;
 
-    // datatypes
+    // sets
+  case kind::UNION:
+  case kind::INTERSECTION:
+  case kind::SETMINUS:
+  case kind::SUBSET:
+  case kind::IN:
+  case kind::SET_TYPE:
+  case kind::SET_SINGLETON: out << smtKindString(k) << " "; break;
+
+   // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
       out << "as ";
       toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
@@ -528,6 +541,14 @@ static string smtKindString(Kind k) throw() {
   case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
   case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
+
+  case kind::UNION: return "union";
+  case kind::INTERSECTION: return "intersection";
+  case kind::SETMINUS: return "setminus";
+  case kind::SUBSET: return "subseteq";
+  case kind::IN: return "in";
+  case kind::SET_TYPE: return "Set";
+  case kind::SET_SINGLETON: return "setenum";
   default:
     ; /* fall through */
   }
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 1f97c02ca..0a2a96603 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -75,8 +75,6 @@ public:
   }
 
   ~Info() {
-    //FIXME!
-    //indices->deleteSelf();
     indices->deleteSelf();
     stores->deleteSelf();
     in_stores->deleteSelf();
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 525b129cf..a30867ee1 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -122,6 +122,10 @@ std::string LogicInfo::getLogicString() const {
         }
         ++seen;
       }
+      if(d_theories[THEORY_SETS]) {
+        ss << "_SETS";
+        ++seen;
+      }
 
       if(seen != d_sharingTheories) {
         Unhandled("can't extract a logic string from LogicInfo; at least one "
@@ -256,6 +260,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         arithNonLinear();
         p += 4;
       }
+      if(!strncmp(p, "_SETS", 5)) {
+        enableTheory(THEORY_SETS);
+        p += 5;
+      }
     }
   }
   if(*p != '\0') {
diff --git a/src/theory/sets/.gitignore b/src/theory/sets/.gitignore
new file mode 100644
index 000000000..4c83ffd6f
--- /dev/null
+++ b/src/theory/sets/.gitignore
@@ -0,0 +1 @@
+README.WHATS-NEXT
diff --git a/src/theory/sets/Makefile b/src/theory/sets/Makefile
new file mode 100644
index 000000000..68a2c5cb6
--- /dev/null
+++ b/src/theory/sets/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/sets
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/sets/Makefile.am b/src/theory/sets/Makefile.am
new file mode 100644
index 000000000..00678628f
--- /dev/null
+++ b/src/theory/sets/Makefile.am
@@ -0,0 +1,20 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libsets.la
+
+libsets_la_SOURCES = \
+	theory_sets.h \
+	theory_sets.cpp \
+	theory_sets_private.h \
+	theory_sets_private.cpp \
+	theory_sets_rewriter.h \
+	theory_sets_rewriter.cpp \
+	theory_sets_type_rules.h \
+	theory_set_type_enumerator.h
+
+EXTRA_DIST = \
+	kinds \
+	options_handlers.h
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
new file mode 100644
index 000000000..089549457
--- /dev/null
+++ b/src/theory/sets/expr_patterns.h
@@ -0,0 +1,51 @@
+/*********************                                                        */
+/*! \file expr_patterns.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Expr patterns.
+ **
+ ** Expr patterns.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace expr {
+namespace pattern {
+
+static Node AND(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::AND, a, b);
+}
+
+static Node OR(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::OR, a, b);
+}
+
+static Node OR(TNode a, TNode b, TNode c) {
+  return NodeManager::currentNM()->mkNode(kind::OR, a, b, c);
+}
+
+static Node IN(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::IN, a, b);
+}
+
+static Node EQUAL(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
+}
+
+static Node NOT(TNode a) {
+  return NodeManager::currentNM()->mkNode(kind::NOT, a);
+}
+
+}/* CVC4::expr::pattern namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
new file mode 100644
index 000000000..bae0c5f1d
--- /dev/null
+++ b/src/theory/sets/kinds
@@ -0,0 +1,55 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h"
+typechecker "theory/sets/theory_sets_type_rules.h"
+rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h"
+
+properties check propagate #presolve postsolve
+
+# Theory content goes here.
+
+# constants...
+constant EMPTYSET \
+    ::CVC4::EmptySet \
+    ::CVC4::EmptySetHashFunction \
+    "util/emptyset.h" \
+    "empty set"
+
+# types...
+operator SET_TYPE 1 "set type"   # the type
+cardinality SET_TYPE \
+    "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
+    "theory/sets/theory_sets_type_rules.h"
+well-founded SET_TYPE \
+    "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
+    "theory/sets/theory_sets_type_rules.h"
+enumerator SET_TYPE \
+    "::CVC4::theory::sets::SetEnumerator" \
+    "theory/sets/theory_sets_type_enumerator.h"
+
+# operators...
+operator UNION 2 "set union"
+operator INTERSECTION 2 "set intersection"
+operator SETMINUS 2 "set subtraction"
+operator SUBSET 2 "subset"
+operator IN 2 "set membership"
+
+operator SET_SINGLETON 1 "singleton set"
+
+typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
+typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
+typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
+typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
+typerule IN ::CVC4::theory::sets::SetInTypeRule
+typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
+
+construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule
+construle UNION ::CVC4::theory::sets::SetConstTypeRule
+
+endtheory
diff --git a/src/theory/sets/options b/src/theory/sets/options
new file mode 100644
index 000000000..dc6c6e907
--- /dev/null
+++ b/src/theory/sets/options
@@ -0,0 +1,14 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module SETS "theory/sets/options.h" Sets
+
+option setsPropagate --sets-propagate bool :default true
+ determines whether to propagate learnt facts to Theory Engine / SAT solver
+
+option setsEagerLemmas --sets-eager-lemmas bool :default false
+ if true, will add lemmas even if not at FULL_EFFORT
+
+endmodule
diff --git a/src/theory/sets/options_handlers.h b/src/theory/sets/options_handlers.h
new file mode 100644
index 000000000..ff535945e
--- /dev/null
+++ b/src/theory/sets/options_handlers.h
@@ -0,0 +1,14 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h
new file mode 100644
index 000000000..ea435d9b7
--- /dev/null
+++ b/src/theory/sets/term_info.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file term_info.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Term info.
+ **
+ ** Term info.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+
+typedef context::CDList<TNode> CDTNodeList;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+class TheorySetsTermInfo {
+public:
+  CDTNodeList* elementsInThisSet;
+  CDTNodeList* elementsNotInThisSet;
+  CDTNodeList* parents;
+
+  TheorySetsTermInfo(context::Context* c)
+  {
+    elementsInThisSet = new(true)CDTNodeList(c);
+    elementsNotInThisSet = new(true)CDTNodeList(c);
+    parents = new(true)CDTNodeList(c);
+  }
+
+  void addToElementList(TNode n, bool polarity) {
+    if(polarity) elementsInThisSet -> push_back(n);
+    else elementsNotInThisSet -> push_back(n);
+  }
+
+  ~TheorySetsTermInfo() {
+    elementsInThisSet -> deleteSelf();
+    elementsNotInThisSet -> deleteSelf();
+    parents -> deleteSelf();
+  }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
new file mode 100644
index 000000000..91195e67e
--- /dev/null
+++ b/src/theory/sets/theory_sets.cpp
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file theory_sets.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory.
+ **
+ ** Sets theory.
+ **/
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+TheorySets::TheorySets(context::Context* c,
+                       context::UserContext* u,
+                       OutputChannel& out,
+                       Valuation valuation,
+                       const LogicInfo& logicInfo) :
+  Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
+  d_internal(new TheorySetsPrivate(*this, c, u)) {
+}
+
+TheorySets::~TheorySets() {
+  delete d_internal;
+}
+
+void TheorySets::check(Effort e) {
+  d_internal->check(e);
+}
+
+void TheorySets::propagate(Effort e) {
+  d_internal->propagate(e);
+}
+
+Node TheorySets::explain(TNode node) {
+  return d_internal->explain(node);
+}
+
+void TheorySets::preRegisterTerm(TNode node) {
+  return d_internal->preRegisterTerm(node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
new file mode 100644
index 000000000..c95229f05
--- /dev/null
+++ b/src/theory/sets/theory_sets.h
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file theory_sets.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory.
+ **
+ ** Sets theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_H
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+class TheorySets : public Theory {
+private:
+  friend class TheorySetsPrivate;
+  TheorySetsPrivate* d_internal;
+public:
+
+  /**
+   * Constructs a new instance of TheorySets w.r.t. the provided
+   * contexts.
+   */
+  TheorySets(context::Context* c,
+               context::UserContext* u,
+               OutputChannel& out,
+               Valuation valuation,
+               const LogicInfo& logicInfo);
+
+  ~TheorySets();
+
+  void check(Effort);
+
+  void propagate(Effort);
+
+  Node explain(TNode);
+
+  std::string identify() const { return "THEORY_SETS"; }
+
+  void preRegisterTerm(TNode node);
+
+};/* class TheorySets */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_H */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
new file mode 100644
index 000000000..8fd490554
--- /dev/null
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -0,0 +1,871 @@
+/*********************                                                        */
+/*! \file theory_sets_private.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Sets theory implementation.
+ **/
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+#include "theory/sets/options.h"
+#include "theory/sets/expr_patterns.h" // ONLY included here
+
+#include "util/result.h"
+
+using namespace std;
+using namespace CVC4::expr::pattern;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+const char* element_of_str = " \u2208 ";
+
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+
+void TheorySetsPrivate::check(Theory::Effort level) {
+
+  CodeTimer checkCodeTimer(d_statistics.d_checkTime);
+
+  while(!d_external.done() && !d_conflict) {
+    // Get all the assertions
+    Assertion assertion = d_external.get();
+    TNode fact = assertion.assertion;
+
+    Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
+                  << fact << std::endl;
+
+    bool polarity = fact.getKind() != kind::NOT;
+    TNode atom = polarity ? fact : fact[0];
+
+    // Solve each
+    switch(atom.getKind()) {
+    case kind::EQUAL:
+      Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+                    << "be equal to " << atom[1] << std::endl;
+      assertEquality(fact, fact, /* learnt = */ false);
+      break;
+
+    case kind::IN:
+      Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+                    << "be in " << atom[1] << std::endl;
+      assertMemebership(fact, fact, /* learnt = */ false);
+      break;
+
+    default:
+      Unhandled(fact.getKind());
+    }
+    finishPropagation();
+
+    Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
+
+    if(d_conflict && !d_equalityEngine.consistent()) return;
+    Assert(!d_conflict);
+    Assert(d_equalityEngine.consistent());
+  }
+
+  Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
+
+  if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+    d_external.d_out->lemma(getLemma());
+  }
+
+  return;
+}/* TheorySetsPrivate::check() */
+
+
+void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
+{
+  Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
+                    << ", " << reason
+                    << ", " << learnt << std::endl;
+
+  bool polarity = fact.getKind() != kind::NOT;
+  TNode atom = polarity ? fact : fact[0];
+
+  // fact already holds
+  if( holds(atom, polarity) ) {
+    Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
+    return;
+  }
+
+  // assert fact & check for conflict
+  if(learnt) {
+    registerReason(reason, /*save=*/ true);
+  }
+  d_equalityEngine.assertEquality(atom, polarity, reason);
+
+  if(!d_equalityEngine.consistent()) {
+    Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
+    d_conflict = true;
+    return;
+  }
+
+  if(!polarity && atom[0].getType().isSet()) {
+    addToPending(atom);
+  }
+
+}/* TheorySetsPrivate::assertEquality() */
+
+
+void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
+{
+  Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
+                       << ", " << reason
+                       << ", " << learnt << std::endl;
+
+  bool polarity = fact.getKind() == kind::NOT ? false : true;
+  TNode atom = polarity ? fact : fact[0];
+
+  // fact already holds
+  if( holds(atom, polarity) ) {
+    Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
+    return;
+  }
+
+  // assert fact & check for conflict
+  if(learnt) {
+    registerReason(reason, true);
+  }
+  d_equalityEngine.assertPredicate(atom, polarity, reason);
+
+  if(!d_equalityEngine.consistent()) {
+    Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
+    d_conflict = true;
+    return;
+  }
+
+  // update term info data structures
+  d_termInfoManager->notifyMembership(fact);
+
+  // propagation
+  TNode x = d_equalityEngine.getRepresentative(atom[0]);
+  eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
+                        &d_equalityEngine);
+  TNode S = (*j);
+  Node cur_atom = IN(x, S);
+
+  /**
+   * It is sufficient to do emptyset propagation outside the loop as
+   * constant term is guaranteed to be class representative.
+   */
+  if(polarity && S.getKind() == kind::EMPTYSET) {
+    Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
+                       << std::endl;
+    learnLiteral(cur_atom, false, cur_atom);
+    Assert(d_conflict);
+    return;
+  }
+
+  for(; !j.isFinished(); ++j) {
+    TNode S = (*j);
+    Node cur_atom = IN(x, S);
+
+    // propagation : children
+    Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
+                       << x << element_of_str << S << std::endl;
+    if(S.getKind() == kind::UNION ||
+       S.getKind() == kind::INTERSECTION ||
+       S.getKind() == kind::SETMINUS ||
+       S.getKind() == kind::SET_SINGLETON) {
+      doSettermPropagation(x, S);
+      if(d_conflict) return;
+    }// propagation: children
+
+
+    // propagation : parents
+    Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
+                       << x << element_of_str << S << std::endl;
+    const CDTNodeList* parentList = d_termInfoManager->getParents(S);
+    for(typeof(parentList->begin()) k = parentList->begin();
+        k != parentList->end(); ++k) {
+      doSettermPropagation(x, *k);
+      if(d_conflict) return;
+    }// propagation : parents
+
+
+  }//j loop
+
+}/* TheorySetsPrivate::assertMemebership() */
+
+
+void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
+{
+  Debug("sets-prop") << "[sets-prop] doSettermPropagation("
+                     << x << ", " << S << std::endl;
+
+  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
+
+  Node literal, left_literal, right_literal;
+
+  // axiom: literal <=> left_literal AND right_literal
+  switch(S.getKind()) {
+  case kind::INTERSECTION:
+    literal       =       IN(x, S)      ;
+    left_literal  =       IN(x, S[0])   ;
+    right_literal =       IN(x, S[1])   ;
+    break;
+  case kind::UNION:
+    literal       = NOT(  IN(x, S)     );
+    left_literal  = NOT(  IN(x, S[0])  );
+    right_literal = NOT(  IN(x, S[1])  );
+    break;
+  case kind::SETMINUS:
+    literal       =       IN(x, S)      ;
+    left_literal  =       IN(x, S[0])   ;
+    right_literal = NOT(  IN(x, S[1])  );
+    break;
+  case kind::SET_SINGLETON: {
+    Node atom = IN(x, S);
+    if(holds(atom, true)) {
+      learnLiteral(EQUAL(x, S[0]), true, atom);
+    } else if(holds(atom, false)) {
+      learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
+    }
+    return;
+  }
+  default:
+    Unhandled();
+  }
+
+  Debug("sets-prop-details")
+    << "[sets-prop-details]   " << literal << " IFF " << left_literal
+    << " AND " << right_literal << std::endl;
+
+  Debug("sets-prop-details")
+    << "[sets-prop-details]   "
+    << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
+    << " IFF "
+    << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
+    << " AND "
+    << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
+    << std::endl;
+
+  Assert( present( IN(x, S)    ) ||
+          present( IN(x, S[0]) ) ||
+          present( IN(x, S[1]) ) );
+
+  if( holds(literal) ) {
+    // 1a. literal => left_literal
+    Debug("sets-prop") << "[sets-prop]  ... via case 1a. ..." << std::endl;
+    learnLiteral(left_literal, literal);
+    if(d_conflict) return;
+
+    // 1b. literal => right_literal
+    Debug("sets-prop") << "[sets-prop]  ... via case 1b. ..." << std::endl;
+    learnLiteral(right_literal, literal);
+    if(d_conflict) return;
+
+    // subsumption requirement met, exit
+    return;
+  }
+  else if( holds(literal.negate() ) ) {
+    // 4. neg(literal), left_literal => neg(right_literal)
+    if( holds(left_literal) ) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 4. ..." << std::endl;
+      learnLiteral(right_literal.negate(), AND( literal.negate(),
+                                                left_literal) );
+      if(d_conflict) return;
+    }
+
+    // 5. neg(literal), right_literal => neg(left_literal)
+    if( holds(right_literal) ) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 5. ..." << std::endl;
+      learnLiteral(left_literal.negate(), AND( literal.negate(),
+                                               right_literal) );
+      if(d_conflict) return;
+    }
+  }
+  else {
+    // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
+    if(holds(left_literal.negate())) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 2. ..." << std::endl;
+      learnLiteral(literal.negate(), left_literal.negate());
+      if(d_conflict) return;
+    }
+    else if(holds(right_literal.negate())) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 3. ..." << std::endl;
+      learnLiteral(literal.negate(), right_literal.negate());
+      if(d_conflict) return;
+    }
+
+    // 6. the axiom itself:
+    else if(holds(left_literal) && holds(right_literal)) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 6. ..." << std::endl;
+      learnLiteral(literal, AND(left_literal, right_literal) );
+      if(d_conflict) return;
+    }
+  }
+
+  // check fulfilling rule
+  Node n;
+  switch(S.getKind()) {
+  case kind::UNION:
+    if( holds(IN(x, S)) &&
+        !present( IN(x, S[0]) ) )
+      addToPending( IN(x, S[0]) );
+    break;
+  case kind::SETMINUS: // intentional fallthrough
+  case kind::INTERSECTION:
+    if( holds(IN(x, S[0])) &&
+        !present( IN(x, S[1]) ))
+      addToPending( IN(x, S[1]) );
+    break;
+  default:
+    Assert(false, "MembershipEngine::doSettermPropagation");
+  }
+}
+
+
+void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
+  Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
+                      << ", " << polarity << ")" << std::endl;
+
+  if( holds(atom, polarity) ) {
+    Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
+    return;
+  }
+
+  if( holds(atom, !polarity) ) {
+    Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
+
+    registerReason(reason, /*save=*/ true);
+
+    if(atom.getKind() == kind::EQUAL) {
+      d_equalityEngine.assertEquality(atom, polarity, reason);
+    } else {
+      d_equalityEngine.assertPredicate(atom, polarity, reason);
+    }
+    Assert(d_conflict);       // should be marked due to equality engine
+    return;
+  }
+
+  Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IN);
+
+  Node learnt_literal = polarity ? Node(atom) : NOT(atom);
+  d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
+}
+
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+  Assert(conjunctions.size() > 0);
+
+  std::set<TNode> all;
+
+  for (unsigned i = 0; i < conjunctions.size(); ++i) {
+    TNode t = conjunctions[i];
+
+    if (t.getKind() == kind::AND) {
+      for(TNode::iterator child_it = t.begin();
+          child_it != t.end(); ++child_it) {
+        Assert((*child_it).getKind() != kind::AND);
+        all.insert(*child_it);
+      }
+    }
+    else {
+      all.insert(t);
+    }
+
+  }
+
+  Assert(all.size() > 0);
+
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}/* mkAnd() */
+
+
+TheorySetsPrivate::Statistics::Statistics() :
+  d_checkTime("theory::sets::time") {
+  StatisticsRegistry::registerStat(&d_checkTime);
+}
+
+
+TheorySetsPrivate::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_checkTime);
+}
+
+
+bool TheorySetsPrivate::present(TNode atom) {
+  return holds(atom) || holds(atom.notNode());
+}
+
+
+bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
+  Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
+
+  Node atomModEq = NodeManager::currentNM()->mkNode
+    (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
+     d_equalityEngine.getRepresentative(atom[1]) );
+
+  d_equalityEngine.addTerm(atomModEq);
+
+  return d_equalityEngine.areEqual(atomModEq, polarity_atom);
+}
+
+
+void TheorySetsPrivate::registerReason(TNode reason, bool save)
+{
+  if(save) d_nodeSaver.insert(reason);
+
+  if(reason.getKind() == kind::AND) {
+    Assert(reason.getNumChildren() == 2);
+    registerReason(reason[0], false);
+    registerReason(reason[1], false);
+  } else if(reason.getKind() == kind::NOT) {
+    registerReason(reason[0], false);
+  } else if(reason.getKind() == kind::IN) {
+    d_equalityEngine.addTerm(reason);
+    Assert(present(reason));
+  } else if(reason.getKind() == kind::EQUAL) {
+    d_equalityEngine.addTerm(reason);
+    Assert(present(reason));
+  } else if(reason.getKind() == kind::CONST_BOOLEAN) {
+    // That's OK, already in EqEngine
+  } else {
+    Unhandled();
+  }
+}
+
+void TheorySetsPrivate::finishPropagation()
+{
+  while(!d_conflict && !d_settermPropagationQueue.empty()) {
+    std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
+    d_settermPropagationQueue.pop();
+    doSettermPropagation(np.first, np.second);
+  }
+  while(!d_conflict && !d_propagationQueue.empty()) {
+    std::pair<Node,Node> np = d_propagationQueue.front();
+    d_propagationQueue.pop();
+    TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
+    if(atom.getKind() == kind::IN) {
+      assertMemebership(np.first, np.second, /* learnt = */ true);
+    } else {
+      assertEquality(np.first, np.second, /* learnt = */ true);
+    }
+  }
+}
+
+void TheorySetsPrivate::addToPending(Node n) {
+  if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
+    if(n.getKind() == kind::IN) {
+      d_pending.push(n);
+    } else {
+      Assert(n.getKind() == kind::EQUAL);
+      d_pendingDisequal.push(n);
+    }
+    d_pendingEverInserted.insert(n);
+  }
+}
+
+bool TheorySetsPrivate::isComplete() {
+  while(!d_pending.empty() && present(d_pending.front()))
+    d_pending.pop();
+  return d_pending.empty() && d_pendingDisequal.empty();
+}
+
+Node TheorySetsPrivate::getLemma() {
+  Assert(!d_pending.empty() || !d_pendingDisequal.empty());
+
+  Node lemma;
+
+  if(!d_pending.empty()) {
+    Node n = d_pending.front();
+    d_pending.pop();
+
+    Assert(!present(n));
+    Assert(n.getKind() == kind::IN);
+
+    lemma = OR(n, NOT(n));
+  } else {
+    Node n = d_pendingDisequal.front();
+    d_pendingDisequal.pop();
+
+    Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
+    Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
+    Node l1 = IN(x, n[0]), l2 = IN(x, n[1]);
+
+    // d_equalityEngine.addTerm(x);
+    // d_equalityEngine.addTerm(l1);
+    // d_equalityEngine.addTerm(l2);
+    // d_terms.insert(x);
+
+    lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
+  }
+
+  Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl;
+
+  return  lemma;
+}
+
+
+TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
+                                     context::Context* c,
+                                     context::UserContext* u):
+  d_external(external),
+  d_notify(*this),
+  d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
+  d_conflict(c),
+  d_termInfoManager(NULL),
+  d_propagationQueue(c),
+  d_settermPropagationQueue(c),
+  d_nodeSaver(c),
+  d_pending(u),
+  d_pendingDisequal(u),
+  d_pendingEverInserted(u)
+{
+  d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
+
+  d_equalityEngine.addFunctionKind(kind::UNION);
+  d_equalityEngine.addFunctionKind(kind::INTERSECTION);
+  d_equalityEngine.addFunctionKind(kind::SETMINUS);
+
+  d_equalityEngine.addFunctionKind(kind::IN);
+  d_equalityEngine.addFunctionKind(kind::SUBSET);
+}/* TheorySetsPrivate::TheorySetsPrivate() */
+
+TheorySetsPrivate::~TheorySetsPrivate()
+{
+  delete d_termInfoManager;
+}
+
+
+
+void TheorySetsPrivate::propagate(Theory::Effort e)
+{
+  return;
+}
+
+bool TheorySetsPrivate::propagate(TNode literal) {
+  Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
+
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+    return false;
+  }
+
+  // Propagate out
+  bool ok = d_external.d_out->propagate(literal);
+  if (!ok) {
+    d_conflict = true;
+  }
+
+  return ok;
+}/* TheorySetsPropagate::propagate(TNode) */
+
+
+void TheorySetsPrivate::conflict(TNode a, TNode b)
+{
+  if (a.getKind() == kind::CONST_BOOLEAN) {
+    d_conflictNode = explain(a.iffNode(b));
+  } else {
+    d_conflictNode = explain(a.eqNode(b));
+  }
+  d_external.d_out->conflict(d_conflictNode);
+  Debug("sets") << "[sets] conflict: " << a << " iff " << b
+                << ", explaination " << d_conflictNode << std::endl;
+  d_conflict = true;
+}
+
+Node TheorySetsPrivate::explain(TNode literal)
+{
+  Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
+                << std::endl;
+
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
+  std::vector<TNode> assumptions;
+
+  if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+  } else if(atom.getKind() == kind::IN) {
+    if( !d_equalityEngine.hasTerm(atom)) {
+      d_equalityEngine.addTerm(atom);
+    }
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+  } else {
+    Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
+                  << polarity << "); kind" << atom.getKind() << std::endl;
+    Unhandled();
+  }
+
+  return mkAnd(assumptions);
+}
+
+void TheorySetsPrivate::preRegisterTerm(TNode node)
+{
+  Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
+                << std::endl;
+
+  switch(node.getKind()) {
+  case kind::EQUAL:
+    // TODO: what's the point of this
+    d_equalityEngine.addTriggerEquality(node);
+    break;
+  case kind::IN:
+    // TODO: what's the point of this
+    d_equalityEngine.addTriggerPredicate(node);
+    break;
+  default:
+    d_termInfoManager->addTerm(node);
+    d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
+    // d_equalityEngine.addTerm(node);
+  }
+  if(node.getKind() == kind::SET_SINGLETON) {
+    Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
+    learnLiteral(IN(node[0], node), true, true_node);
+    //intentional fallthrough
+  }
+}
+
+
+
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality << " value = " << value << std::endl;
+  if (value) {
+    return d_theory.propagate(equality);
+  } else {
+    // We use only literal triggers so taking not is safe
+    return d_theory.propagate(equality.notNode());
+  }
+}
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate << " value = " << value << std::endl;
+  if (value) {
+    return d_theory.propagate(predicate);
+  } else {
+    return d_theory.propagate(predicate.notNode());
+  }
+}
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
+  if(value) {
+    d_theory.d_termInfoManager->mergeTerms(t1, t2);
+  }
+  return true;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+  d_theory.conflict(t1, t2);
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
+}
+
+
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+
+void TheorySetsPrivate::TermInfoManager::mergeLists
+(CDTNodeList* la, const CDTNodeList* lb) const {
+  // straight from theory/arrays/array_info.cpp
+  std::set<TNode> temp;
+  CDTNodeList::const_iterator it;
+  for(it = la->begin() ; it != la->end(); it++ ) {
+    temp.insert((*it));
+  }
+
+  for(it = lb->begin() ; it!= lb->end(); it++ ) {
+    if(temp.count(*it) == 0) {
+      la->push_back(*it);
+    }
+  }
+}
+
+TheorySetsPrivate::TermInfoManager::TermInfoManager
+(TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
+  d_theory(theory),
+  d_context(satContext),
+  d_eqEngine(eq),
+  d_terms(satContext),
+  d_info()
+{ }
+
+TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
+  for( typeof(d_info.begin()) it = d_info.begin();
+       it != d_info.end(); ++it) {
+    delete (*it).second;
+  }
+}
+
+void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
+  bool polarity = fact.getKind() != kind::NOT;
+  TNode atom = polarity ? fact : fact[0];
+
+  TNode x = d_eqEngine->getRepresentative(atom[0]);
+  TNode S = d_eqEngine->getRepresentative(atom[1]);
+
+  Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
+                         << " in " << S << " " << polarity << std::endl;
+
+  d_info[S]->addToElementList(x, polarity);
+}
+
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
+  return d_info[x]->parents;
+}
+
+void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
+  unsigned numChild = n.getNumChildren();
+
+  if(!d_terms.contains(n)) {
+    d_terms.insert(n);
+    d_info[n] = new TheorySetsTermInfo(d_context);
+  }
+
+  if(n.getKind() == kind::UNION ||
+     n.getKind() == kind::INTERSECTION ||
+     n.getKind() == kind::SETMINUS ||
+     n.getKind() == kind::SET_SINGLETON) {
+
+    for(unsigned i = 0; i < numChild; ++i) {
+      if(d_terms.contains(n[i])) {
+        Debug("sets-parent") << "Adding " << n << " to parent list of "
+                             << n[i] << std::endl;
+        d_info[n[i]]->parents->push_back(n);
+      }
+    }
+
+  }
+}
+
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(CDTNodeList* l, TNode S, bool polarity)
+{
+  for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
+    Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
+                       << IN(*i, d_eqEngine->getRepresentative(S))
+                       << std::endl;
+
+    d_eqEngine->addTerm(IN(d_eqEngine->getRepresentative(*i),
+                           d_eqEngine->getRepresentative(S)));
+
+    for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
+        !j.isFinished(); ++j) {
+
+      TNode x = (*i);
+      TNode S = (*j);
+      Node cur_atom = IN(x, S);
+
+      // propagation : empty set
+      if(polarity && S.getKind() == kind::EMPTYSET) {
+        Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
+                           << std::endl;
+        d_theory.learnLiteral(cur_atom, false, cur_atom);
+        return;
+      }// propagation: empty set
+
+      // propagation : children
+      if(S.getKind() == kind::UNION ||
+         S.getKind() == kind::INTERSECTION ||
+         S.getKind() == kind::SETMINUS ||
+         S.getKind() == kind::SET_SINGLETON) {
+        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
+      }// propagation: children
+
+      // propagation : parents
+      const CDTNodeList* parentList = getParents(S);
+      for(typeof(parentList->begin()) k = parentList->begin();
+          k != parentList->end(); ++k) {
+        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
+      }// propagation : parents
+
+
+    }//j loop
+
+  }
+
+}
+
+void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
+  // merge b into a
+
+  if(!a.getType().isSet()) return;
+
+  Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
+                         << ", b = " << b << std::endl;
+  Debug("sets-terminfo") << "[sets-terminfo] reps"
+                         << ", a: " << d_eqEngine->getRepresentative(a)
+                         << ", b: " << d_eqEngine->getRepresentative(b)
+                         << std::endl;
+
+  typeof(d_info.begin()) ita = d_info.find(a);
+  typeof(d_info.begin()) itb = d_info.find(b);
+
+  Assert(ita != d_info.end());
+  Assert(itb != d_info.end());
+
+  pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
+  pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
+  pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
+  pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
+
+  mergeLists((*ita).second->elementsInThisSet,
+             (*itb).second->elementsInThisSet);
+
+  mergeLists((*ita).second->elementsNotInThisSet,
+             (*itb).second->elementsNotInThisSet);
+}
+
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
new file mode 100644
index 000000000..f1a8c0a46
--- /dev/null
+++ b/src/theory/sets/theory_sets_private.h
@@ -0,0 +1,166 @@
+/*********************                                                        */
+/*! \file theory_sets_private.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Sets theory implementation.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/sets/term_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/** Internal classes, forward declared here */
+class TheorySetsTermInfoManager;
+class TheorySets;
+
+class TheorySetsPrivate {
+public:
+
+  /**
+   * Constructs a new instance of TheorySetsPrivate w.r.t. the provided
+   * contexts.
+   */
+  TheorySetsPrivate(TheorySets& external,
+                    context::Context* c,
+                    context::UserContext* u);
+
+  ~TheorySetsPrivate();
+
+  void check(Theory::Effort);
+
+  void propagate(Theory::Effort);
+
+  Node explain(TNode);
+
+  std::string identify() const { return "THEORY_SETS_PRIVATE"; }
+
+  void preRegisterTerm(TNode node);
+
+private:
+  TheorySets& d_external;
+
+  class Statistics {
+  public:
+    TimerStat d_checkTime;
+
+    Statistics();
+    ~Statistics();
+  } d_statistics;
+
+  /** Functions to handle callbacks from equality engine */
+  class NotifyClass : public eq::EqualityEngineNotify {
+    TheorySetsPrivate& d_theory;
+
+  public:
+    NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+    void eqNotifyNewClass(TNode t);
+    void eqNotifyPreMerge(TNode t1, TNode t2);
+    void eqNotifyPostMerge(TNode t1, TNode t2);
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+  } d_notify;
+
+  /** Equality engine */
+  eq::EqualityEngine d_equalityEngine;
+
+  context::CDO<bool> d_conflict;
+  Node d_conflictNode;
+
+  /** Proagate out to output channel */
+  bool propagate(TNode);
+
+  /** generate and send out conflict node */
+  void conflict(TNode, TNode);
+
+  class TermInfoManager {
+    TheorySetsPrivate& d_theory;
+    context::Context* d_context;
+    eq::EqualityEngine* d_eqEngine;
+
+    CDNodeSet d_terms;
+    std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info;
+
+    void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const;
+    void pushToSettermPropagationQueue(CDTNodeList* l, TNode S, bool polarity);
+  public:
+    TermInfoManager(TheorySetsPrivate&,
+                    context::Context* satContext,
+                    eq::EqualityEngine*);
+    ~TermInfoManager();
+    void notifyMembership(TNode fact);
+    const CDTNodeList* getParents(TNode x);
+    void addTerm(TNode n);
+    void mergeTerms(TNode a, TNode b);
+  };
+  TermInfoManager* d_termInfoManager;
+
+  /** Assertions and helper functions */
+  bool present(TNode atom);
+  bool holds(TNode lit) {
+    bool polarity = lit.getKind() == kind::NOT ? false : true;
+    TNode atom = polarity ? lit : lit[0];
+    return holds(atom, polarity);
+  }
+  bool holds(TNode atom, bool polarity);
+
+  void assertEquality(TNode fact, TNode reason, bool learnt);
+  void assertMemebership(TNode fact, TNode reason, bool learnt);
+
+  /** Propagation / learning and helper functions. */
+  context::CDQueue< std::pair<Node, Node> > d_propagationQueue;
+  context::CDQueue< std::pair<TNode, TNode> > d_settermPropagationQueue;
+
+  void doSettermPropagation(TNode x, TNode S);
+  void registerReason(TNode reason, bool save);
+  void learnLiteral(TNode atom, bool polarity, Node reason);
+  void learnLiteral(TNode lit, Node reason) {
+    if(lit.getKind() == kind::NOT) {
+      learnLiteral(lit[0], false, reason);
+    } else {
+      learnLiteral(lit, true, reason);
+    }
+  }
+  void finishPropagation();
+
+  // for any nodes we need to save, because others use TNode
+  context::CDHashSet <Node, NodeHashFunction> d_nodeSaver;
+
+  /** Lemmas and helper functions */
+  context::CDQueue <TNode> d_pending;
+  context::CDQueue <TNode> d_pendingDisequal;
+  context::CDHashSet <Node, NodeHashFunction> d_pendingEverInserted;
+
+  void addToPending(Node n);
+  bool isComplete();
+  Node getLemma();
+};/* class TheorySetsPrivate */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
new file mode 100644
index 000000000..11a2e9297
--- /dev/null
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -0,0 +1,110 @@
+#include "theory/sets/theory_sets_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+bool checkConstantMembership(TNode elementTerm, TNode setTerm)
+{
+  switch(setTerm.getKind()) {
+  case kind::EMPTYSET:
+    return false;
+  case kind::SET_SINGLETON:
+    return elementTerm == setTerm[0];
+  case kind::UNION:
+    return checkConstantMembership(elementTerm, setTerm[0]) ||
+      checkConstantMembership(elementTerm, setTerm[1]);
+  case kind::INTERSECTION:
+    return checkConstantMembership(elementTerm, setTerm[0]) &&
+      checkConstantMembership(elementTerm, setTerm[1]);
+  case kind::SETMINUS:
+    return checkConstantMembership(elementTerm, setTerm[0]) &&
+      !checkConstantMembership(elementTerm, setTerm[1]);
+  default:
+    Unhandled();
+  }
+}
+
+// static
+RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
+  NodeManager* nm = NodeManager::currentNM();
+
+  switch(node.getKind()) {
+
+  case kind::IN: {
+    if(!node[0].isConst() || !node[1].isConst())
+      break;
+
+    // both are constants
+    bool isMember = checkConstantMembership(node[0], node[1]);
+    return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
+  }
+
+  case kind::SUBSET: {
+    // rewrite (A subset-or-equal B) as (A union B = B)
+    TNode A = node[0];
+    TNode B = node[1];
+    return RewriteResponse(REWRITE_AGAIN,
+                           nm->mkNode(kind::EQUAL,
+                                      nm->mkNode(kind::UNION, A, B),
+                                      B) );
+  }//kind::SUBSET
+
+  case kind::EQUAL:
+  case kind::IFF: {
+    //rewrite: t = t with true (t term)
+    //rewrite: c = c' with c different from c' false (c, c' constants)
+    //otherwise: sort them
+    if(node[0] == node[1]) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl;
+      return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+    }
+    else if (node[0].isConst() && node[1].isConst()) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl;
+      return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
+    }
+    else if (node[0] > node[1]) {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+    break;
+  }
+
+  case kind::UNION:
+  case kind::INTERSECTION: {
+    if(node[0] == node[1]) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
+      return RewriteResponse(REWRITE_DONE, node[0]);
+    } else if (node[0] > node[1]) {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+    break;
+  }
+
+  default:
+    break;
+
+  }//switch(node.getKind())
+
+  // This default implementation
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+// static
+RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
+  NodeManager* nm = NodeManager::currentNM();
+
+  // do nothing
+  if(node.getKind() == kind::EQUAL && node[0] == node[1])
+    return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+  // Further optimization, if constants but differing ones
+
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
new file mode 100644
index 000000000..f01d198cf
--- /dev/null
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -0,0 +1,77 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsRewriter {
+public:
+
+  /**
+   * Rewrite a node into the normal form for the theory of sets.
+   * Called in post-order (really reverse-topological order) when
+   * traversing the expression DAG during rewriting.  This is the
+   * main function of the rewriter, and because of the ordering,
+   * it can assume its children are all rewritten already.
+   *
+   * This function can return one of three rewrite response codes
+   * along with the rewritten node:
+   *
+   *   REWRITE_DONE indicates that no more rewriting is needed.
+   *   REWRITE_AGAIN means that the top-level expression should be
+   *     rewritten again, but that its children are in final form.
+   *   REWRITE_AGAIN_FULL means that the entire returned expression
+   *     should be rewritten again (top-down with preRewrite(), then
+   *     bottom-up with postRewrite()).
+   *
+   * Even if this function returns REWRITE_DONE, if the returned
+   * expression belongs to a different theory, it will be fully
+   * rewritten by that theory's rewriter.
+   */
+  static RewriteResponse postRewrite(TNode node);
+
+  /**
+   * Rewrite a node into the normal form for the theory of sets
+   * in pre-order (really topological order)---meaning that the
+   * children may not be in the normal form.  This is an optimization
+   * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
+   * in arithmetic rewrites to 0 without the need to look at the big
+   * nasty expression).  Since it's only an optimization, the
+   * implementation here can do nothing.
+   */
+  static RewriteResponse preRewrite(TNode node);
+
+  /**
+   * Rewrite an equality, in case special handling is required.
+   */
+  static Node rewriteEquality(TNode equality) {
+    // often this will suffice
+    return postRewrite(equality).node;
+  }
+
+  /**
+   * Initialize the rewriter.
+   */
+  static inline void init() {
+    // nothing to do
+  }
+
+  /**
+   * Shut down the rewriter.
+   */
+  static inline void shutdown() {
+    // nothing to do
+  }
+
+};/* class TheorySetsRewriter */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
new file mode 100644
index 000000000..2f4cc6a2f
--- /dev/null
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -0,0 +1,161 @@
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
+  unsigned d_index;
+  TypeNode d_constituentType;
+  NodeManager* d_nm;
+  std::vector<bool> d_indexVec;
+  std::vector<TypeEnumerator*> d_constituentVec;
+  bool d_finished;
+  Node d_setConst;
+
+public:
+
+  SetEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase<SetEnumerator>(type),
+    d_index(0),
+    d_constituentType(type.getSetElementType()),
+    d_nm(NodeManager::currentNM()),
+    d_indexVec(),
+    d_constituentVec(),
+    d_finished(false),
+    d_setConst()
+  {
+    // d_indexVec.push_back(false);
+    // d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+    d_setConst = d_nm->mkConst(EmptySet(type.toType()));
+  }
+
+  // An set enumerator could be large, and generally you don't want to
+  // go around copying these things; but a copy ctor is presently required
+  // by the TypeEnumerator framework.
+  SetEnumerator(const SetEnumerator& ae) throw() :
+    TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
+    d_constituentType(ae.d_constituentType),
+    d_nm(ae.d_nm),
+    d_indexVec(ae.d_indexVec),
+    d_constituentVec(),// copied below
+    d_finished(ae.d_finished),
+    d_setConst(ae.d_setConst)
+  {
+    for(std::vector<TypeEnumerator*>::const_iterator i =
+          ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
+        i != i_end;
+        ++i) {
+      d_constituentVec.push_back(new TypeEnumerator(**i));
+    }
+  }
+
+  ~SetEnumerator() {
+    while (!d_constituentVec.empty()) {
+      delete d_constituentVec.back();
+      d_constituentVec.pop_back();
+    }
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    if (d_finished) {
+      throw NoMoreValuesException(getType());
+    }
+    Node n = d_setConst;
+
+    // For now only support only sets of size 1
+    Assert(d_index == 0 || d_index == 1);
+
+    if(d_index == 1) {
+      n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+    }
+
+    // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
+    //   n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
+    // }
+    Trace("set-type-enum") << "operator * prerewrite: " << n << std::endl;
+    n = Rewriter::rewrite(n);
+    Trace("set-type-enum") << "operator * returning: " << n << std::endl;
+    return n;
+  }
+
+  SetEnumerator& operator++() throw() {
+    Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl;
+
+    if (d_finished) {
+      Trace("set-type-enum") << "operator++ finished!" << std::endl;
+      return *this;
+    }
+
+    // increment by one, at the same time deleting all elements that
+    // cannot be incremented any further (note: we are keeping a set
+    // -- no repetitions -- thus some trickery to know what to pop and
+    // what not to.)
+    if(d_index > 0) {
+      Assert(d_index == d_constituentVec.size());
+
+      Node last_pre_increment;
+      last_pre_increment = *(*d_constituentVec.back());
+
+      ++(*d_constituentVec.back());
+
+      if (d_constituentVec.back()->isFinished()) {
+        delete d_constituentVec.back();
+        d_constituentVec.pop_back();
+
+        while(!d_constituentVec.empty()) {
+          Node cur_pre_increment = *(*d_constituentVec.back());
+          ++(*d_constituentVec.back());
+          Node cur_post_increment = *(*d_constituentVec.back());
+          if(last_pre_increment == cur_post_increment) {
+            delete d_constituentVec.back();
+            d_constituentVec.pop_back();
+            last_pre_increment = cur_pre_increment;
+          } else {
+            break;
+          }
+        }
+      }
+    }
+
+    if (d_constituentVec.empty()) {
+      ++d_index;
+      d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+    }
+
+    while (d_constituentVec.size() < d_index) {
+      TypeEnumerator *d_newEnumerator = new TypeEnumerator(*d_constituentVec.back());
+      ++(*d_newEnumerator);
+      if( (*d_newEnumerator).isFinished() ) {
+        Trace("set-type-enum") << "operator++ finished!" << std::endl;
+        d_finished = true;
+        return *this;
+      }
+      d_constituentVec.push_back(d_newEnumerator);
+    }
+
+    Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl;
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl;
+    return d_finished;
+  }
+
+};/* class SetEnumerator */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
new file mode 100644
index 000000000..026c90ca4
--- /dev/null
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -0,0 +1,176 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetsTypeRule {
+public:
+
+  /**
+   * Compute the type for (and optionally typecheck) a term belonging
+   * to the theory of sets.
+   *
+   * @param check if true, the node's type should be checked as well
+   * as computed.
+   */
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+                                     bool check)
+    throw (TypeCheckingExceptionPrivate) {
+
+    // TODO: implement me!
+    Unimplemented();
+
+  }
+
+};/* class SetsTypeRule */
+
+// TODO: Union, Intersection and Setminus should be combined to one check
+struct SetUnionTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::UNION);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set union operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set union operating on sets of different types");
+      }
+    }
+    return setType;
+  }
+};/* struct SetUnionTypeRule */
+
+struct SetIntersectionTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::INTERSECTION);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set intersection operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set intersection operating on sets of different types");
+      }
+    }
+    return setType;
+  }
+};/* struct SetIntersectionTypeRule */
+
+struct SetSetminusTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SETMINUS);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set setminus operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set setminus operating on sets of different types");
+      }
+    }
+    return setType;
+  }
+};/* struct SetSetminusTypeRule */
+
+struct SetSubsetTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SUBSET);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct SetSubsetTypeRule */
+
+struct SetInTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::IN);
+    TypeNode setType = n[1].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
+      }
+      TypeNode elementType = n[0].getType(check);
+      if(elementType != setType.getSetElementType()) {
+        throw TypeCheckingExceptionPrivate(n, "set in operating on sets of different types");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct SetInTypeRule */
+
+struct SetSingletonTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SET_SINGLETON);
+    return nodeManager->mkSetType(n[0].getType(check));
+  }
+};/* struct SetInTypeRule */
+
+struct SetConstTypeRule {
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    switch(n.getKind()) {
+    case kind::SET_SINGLETON:
+      return n[0].isConst();
+    case kind::UNION:
+      return n[0].isConst() && n[1].isConst();
+    default:
+      Unhandled();
+    }
+  }
+};
+
+struct EmptySetTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+
+    Assert(n.getKind() == kind::EMPTYSET);
+    EmptySet emptySet = n.getConst<EmptySet>();
+    Type setType = emptySet.getType();
+    return TypeNode::fromType(setType);
+  }
+};
+
+
+struct SetsProperties {
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::SET_TYPE);
+    Cardinality elementCard = type[0].getCardinality();
+    return elementCard;
+  }
+
+  inline static bool isWellFounded(TypeNode type) {
+    return type[0].isWellFounded();
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.isSet());
+    return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
+  }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 2359d5d86..e8d53e539 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -620,6 +620,9 @@ public:
    * check() or propagate() method called.  A Theory may empty its
    * assertFact() queue using get().  A Theory can raise conflicts,
    * add lemmas, and propagate literals during presolve().
+   *
+   * NOTE: The presolve property must be added to the kinds file for
+   * the theory.
    */
   virtual void presolve() { }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 47ba50aad..63024e5d5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -671,6 +671,7 @@ bool TheoryEngine::presolve() {
 void TheoryEngine::postsolve() {
   // Reset the interrupt flag
   d_interrupted = false;
+  bool CVC4_UNUSED wasInConflict = d_inConflict;
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -680,7 +681,7 @@ void TheoryEngine::postsolve() {
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
       theoryOf(THEORY)->postsolve(); \
-      Assert(! d_inConflict, "conflict raised during postsolve()"); \
+      Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
     }
 
     // Postsolve for each theory using the statement above
@@ -961,7 +962,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
       bool value;
       if (d_propEngine->hasValue(assertion, value)) {
         if (!value) {
-          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << endl;
+          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
           d_inConflict = true;
         } else {
           return;
@@ -1011,6 +1012,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
       // Check for propositional conflicts
       bool value;
       if (d_propEngine->hasValue(assertion, value) && !value) {
+          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" << endl;
         d_inConflict = true;
       }
     }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index f8e361081..8bb849496 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -833,12 +833,14 @@ public:
   void addTriggerPredicate(TNode predicate);
 
   /**
-   * Returns true if the two are currently in the database and equal.
+   * Returns true if the two terms are equal. Requires both terms to
+   * be in the database.
    */
   bool areEqual(TNode t1, TNode t2) const;
 
   /**
-   * Check whether the two term are dis-equal.
+   * Check whether the two term are dis-equal. Requires both terms to
+   * be in the database.
    */
   bool areDisequal(TNode t1, TNode t2, bool ensureProof) const;
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 1d6ce1a73..0717df907 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -87,6 +87,8 @@ libutil_la_SOURCES = \
 	abstract_value.cpp \
 	array_store_all.h \
 	array_store_all.cpp \
+	emptyset.h \
+	emptyset.cpp \
 	model.h \
 	model.cpp \
 	sort_inference.h \
diff --git a/src/util/emptyset.cpp b/src/util/emptyset.cpp
new file mode 100644
index 000000000..fa1bb8f10
--- /dev/null
+++ b/src/util/emptyset.cpp
@@ -0,0 +1,12 @@
+#include "util/emptyset.h"
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const EmptySet& asa) {
+  return out << "emptyset(" << asa.getType() << ')';
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/emptyset.h b/src/util/emptyset.h
new file mode 100644
index 000000000..aae08e43b
--- /dev/null
+++ b/src/util/emptyset.h
@@ -0,0 +1,65 @@
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace CVC4 {
+  // messy; Expr needs ArrayStoreAll (because it's the payload of a
+  // CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
+  class CVC4_PUBLIC EmptySet;
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+#include <iostream>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC EmptySet {
+
+  const SetType d_type;
+
+public:
+
+  EmptySet() { }		/* Null typed */
+  EmptySet(SetType t):d_type(t) { }
+
+
+  ~EmptySet() throw() {
+  }
+
+  SetType getType() const { return d_type; }
+
+  bool operator==(const EmptySet& asa) const throw() {
+    return d_type == asa.d_type;
+  }
+  bool operator!=(const EmptySet& asa) const throw() {
+    return !(*this == asa);
+  }
+
+  bool operator<(const EmptySet& asa) const throw() {
+    return d_type < asa.d_type;
+  }
+  bool operator<=(const EmptySet& asa) const throw() {
+    return d_type <= asa.d_type;
+  }
+  bool operator>(const EmptySet& asa) const throw() {
+    return !(*this <= asa);
+  }
+  bool operator>=(const EmptySet& asa) const throw() {
+    return !(*this < asa);
+  }
+
+
+};/* class EmptySet */
+
+std::ostream& operator<<(std::ostream& out, const EmptySet& asa) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC EmptySetHashFunction {
+  inline size_t operator()(const EmptySet& asa) const {
+    return TypeHashFunction()(asa.getType());
+  }
+};/* struct EmptysetHashFunction */
+
+
+}