Merge pull request #47 from kbansal/sets

Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are:

SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset*
API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET

(those marked with [*] have changed or been added, others are as earlier)

In the set-logic string use FS to enable sets.

A not-so-well-tested perl command for translating old benchmarks:
  perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '

19 files changed, 150 insertions, 65 deletions

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 7fb36bb3a..4d2b8570f 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -180,7 +180,7 @@ public:
 
   CDOhash_map(Context* context,
          CDHashMap<Key, Data, HashFcn>* map,
-	 const Key& key,
+         const Key& key,
          const Data& data,
          bool atLevelZero = false,
          bool allocatedInCMM = false) :
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index cda696a03..8173c7269 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -144,9 +144,9 @@ public:
   /** Is the DecisionEngine in a state where it has solved everything? */
   bool isDone() {
     Trace("decision") << "DecisionEngine::isDone() returning "
-		      << (d_result != SAT_VALUE_UNKNOWN)
-		      << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false")
-		      << std::endl;
+                      << (d_result != SAT_VALUE_UNKNOWN)
+                      << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false")
+                      << std::endl;
     return (d_result != SAT_VALUE_UNKNOWN);
   }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8590229a2..457c9c82f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1115,7 +1115,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
     { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); }
 
   | EMPTYSET_TOK
-    { expr = MK_CONST( ::CVC4::EmptySet()); }
+    { expr = MK_CONST( ::CVC4::EmptySet(Type())); }
 
     // NOTE: Theory constants go here
   ;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 5baa0b16f..0c4b1258f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -149,9 +149,10 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::UNION, "union");
     addOperator(kind::INTERSECTION, "intersection");
     addOperator(kind::SETMINUS, "setminus");
-    addOperator(kind::SUBSET, "subseteq");
-    addOperator(kind::MEMBER, "in");
-    addOperator(kind::SET_SINGLETON, "setenum");
+    addOperator(kind::SUBSET, "subset");
+    addOperator(kind::MEMBER, "member");
+    addOperator(kind::SINGLETON, "singleton");
+    addOperator(kind::INSERT, "insert");
     break;
 
   case THEORY_DATATYPES:
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 15101b0e4..270e0dba0 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -418,7 +418,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::SUBSET:
   case kind::MEMBER:
   case kind::SET_TYPE:
-  case kind::SET_SINGLETON: out << smtKindString(k) << " "; break;
+  case kind::SINGLETON: out << smtKindString(k) << " "; break;
 
    // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
@@ -618,10 +618,11 @@ static string smtKindString(Kind k) throw() {
   case kind::UNION: return "union";
   case kind::INTERSECTION: return "intersection";
   case kind::SETMINUS: return "setminus";
-  case kind::SUBSET: return "subseteq";
-  case kind::MEMBER: return "in";
+  case kind::SUBSET: return "subset";
+  case kind::MEMBER: return "member";
   case kind::SET_TYPE: return "Set";
-  case kind::SET_SINGLETON: return "setenum";
+  case kind::SINGLETON: return "singleton";
+  case kind::INSERT: return "insert";
   default:
     ; /* fall through */
   }
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 78f4996b8..bc2f1286b 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -129,7 +129,7 @@ std::string LogicInfo::getLogicString() const {
         ++seen;
       }
       if(d_theories[THEORY_SETS]) {
-        ss << "_SETS";
+        ss << "FS";
         ++seen;
       }
 
@@ -272,9 +272,9 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         arithNonLinear();
         p += 4;
       }
-      if(!strncmp(p, "_SETS", 5)) {
+      if(!strncmp(p, "FS", 2)) {
         enableTheory(THEORY_SETS);
-        p += 5;
+        p += 2;
       }
     }
   }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9f25b0825..2c309899d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -74,7 +74,7 @@ unsigned TermDb::getNumGroundTerms( Node f ) {
 Node TermDb::getOperator( Node n ) {
   //return n.getOperator();
   Kind k = n.getKind();
-  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON ){
+  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
     Node op = n.getOperator();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 77a4efff5..0d8f2c06d 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -330,7 +330,7 @@ bool Trigger::isAtomicTrigger( Node n ){
 bool Trigger::isAtomicTriggerKind( Kind k ) {
   return k==APPLY_UF || k==SELECT || k==STORE ||
          k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
-         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON;
+         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON;
 }
 
 bool Trigger::isSimpleTrigger( Node n ){
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
index bc5b6b9e0..93307d227 100644
--- a/src/theory/sets/expr_patterns.h
+++ b/src/theory/sets/expr_patterns.h
@@ -44,8 +44,8 @@ static Node MEMBER(TNode a, TNode b) {
   return NodeManager::currentNM()->mkNode(kind::MEMBER, a, b);
 }
 
-static Node SET_SINGLETON(TNode a) {
-  return NodeManager::currentNM()->mkNode(kind::SET_SINGLETON, a);
+static Node SINGLETON(TNode a) {
+  return NodeManager::currentNM()->mkNode(kind::SINGLETON, a);
 }
 
 static Node EQUAL(TNode a, TNode b) {
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 12f114fc0..39e7883c6 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -19,10 +19,10 @@ constant EMPTYSET \
     ::CVC4::EmptySet \
     ::CVC4::EmptySetHashFunction \
     "util/emptyset.h" \
-    "empty set"
+    "the empty set constant; payload is an instance of the CVC4::EmptySet class"
 
 # the type
-operator SET_TYPE 1 "set type"
+operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
 cardinality SET_TYPE \
     "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
     "theory/sets/theory_sets_type_rules.h"
@@ -38,21 +38,24 @@ enumerator SET_TYPE \
 operator UNION         2  "set union"
 operator INTERSECTION  2  "set intersection"
 operator SETMINUS      2  "set subtraction"
-operator SUBSET        2  "subset"
-operator MEMBER        2  "set membership"
-operator SET_SINGLETON 1  "singleton set"
+operator SUBSET        2  "subset predicate; first parameter a subset of second"
+operator MEMBER        2  "set membership predicate; first parameter a member of second"
+operator SINGLETON     1  "the set of the single element given as a parameter"
+operator INSERT        2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
 
 typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule SETMINUS       ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
 typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
-typerule SET_SINGLETON  ::CVC4::theory::sets::SetSingletonTypeRule
+typerule SINGLETON      ::CVC4::theory::sets::SingletonTypeRule
 typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
+typerule INSERT         ::CVC4::theory::sets::InsertTypeRule
 
 construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle SETMINUS      ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+construle SINGLETON     ::CVC4::theory::sets::SingletonTypeRule
+construle INSERT        ::CVC4::theory::sets::InsertTypeRule
 
 endtheory
diff --git a/src/theory/sets/options b/src/theory/sets/options
index dc6c6e907..1c95e78e4 100644
--- a/src/theory/sets/options
+++ b/src/theory/sets/options
@@ -8,7 +8,7 @@ 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
+option setsEagerLemmas --sets-eager-lemmas bool :default true
+ add lemmas even at regular effort
 
 endmodule
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index c230b9ac5..5d5e1f9ee 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,10 +34,6 @@ TheorySets::~TheorySets() {
   delete d_internal;
 }
 
-void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_internal->setMasterEqualityEngine(eq);
-}
-
 void TheorySets::addSharedTerm(TNode n) {
   d_internal->addSharedTerm(n);
 }
@@ -50,8 +46,8 @@ void TheorySets::collectModelInfo(TheoryModel* m, bool fullModel) {
   d_internal->collectModelInfo(m, fullModel);
 }
 
-void TheorySets::propagate(Effort e) {
-  d_internal->propagate(e);
+void TheorySets::computeCareGraph() {
+  d_internal->computeCareGraph();
 }
 
 Node TheorySets::explain(TNode node) {
@@ -59,7 +55,15 @@ Node TheorySets::explain(TNode node) {
 }
 
 void TheorySets::preRegisterTerm(TNode node) {
-  return d_internal->preRegisterTerm(node);
+  d_internal->preRegisterTerm(node);
+}
+
+void TheorySets::propagate(Effort e) {
+  d_internal->propagate(e);
+}
+
+void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_internal->setMasterEqualityEngine(eq);
 }
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 6ff41d5f5..84d91de72 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -48,14 +48,14 @@ public:
 
   ~TheorySets();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-  
   void addSharedTerm(TNode);
 
   void check(Effort);
 
   void collectModelInfo(TheoryModel*, bool fullModel);
 
+  void computeCareGraph();
+
   Node explain(TNode);
 
   std::string identify() const { return "THEORY_SETS"; }
@@ -64,6 +64,8 @@ public:
 
   void propagate(Effort);
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
 };/* class TheorySets */
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f768bd62d..be2b48f81 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -97,7 +97,7 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
   }
 
-  if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+  if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
     d_external.d_out->lemma(getLemma());
     return;
   }
@@ -225,7 +225,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
     if(S.getKind() == kind::UNION ||
        S.getKind() == kind::INTERSECTION ||
        S.getKind() == kind::SETMINUS ||
-       S.getKind() == kind::SET_SINGLETON) {
+       S.getKind() == kind::SINGLETON) {
       doSettermPropagation(x, S);
       if(d_conflict) return;
     }// propagation: children
@@ -276,7 +276,7 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
     left_literal  =       MEMBER(x, S[0])   ;
     right_literal = NOT(  MEMBER(x, S[1])  );
     break;
-  case kind::SET_SINGLETON: {
+  case kind::SINGLETON: {
     Node atom = MEMBER(x, S);
     if(holds(atom, true)) {
       learnLiteral(EQUAL(x, S[0]), true, atom);
@@ -408,6 +408,42 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 }/*TheorySetsPrivate::learnLiteral(...)*/
 
 
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+
+void TheorySetsPrivate::addSharedTerm(TNode n) {
+  Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+  d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
+}
+
+
+void TheorySetsPrivate::computeCareGraph() {
+  Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
+  for (unsigned i = 0; i < d_external.d_sharedTerms.size(); ++ i) {
+    TNode a = d_external.d_sharedTerms[i];
+    TypeNode aType = a.getType();
+    for (unsigned j = i + 1; j < d_external.d_sharedTerms.size(); ++ j) {
+      TNode b = d_external.d_sharedTerms[j];
+      if (b.getType() != aType) {
+        // We don't care about the terms of different types
+        continue;
+      }
+      switch (d_external.d_valuation.getEqualityStatus(a, b)) {
+      case EQUALITY_TRUE_AND_PROPAGATED:
+      case EQUALITY_FALSE_AND_PROPAGATED:
+        // If we know about it, we should have propagated it, so we can skip
+        break;
+      default:
+        // Let's split on it
+        d_external.addCarePair(a, b);
+        break;
+      }
+    }
+  }
+}
+
+
 /******************** Model generation ********************/
 /******************** Model generation ********************/
 /******************** Model generation ********************/
@@ -535,9 +571,9 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con
     return nm->mkConst(EmptySet(nm->toType(setType)));
   } else {
     Elements::iterator it = elements.begin();
-    Node cur = SET_SINGLETON(*it);
+    Node cur = SINGLETON(*it);
     while( ++it != elements.end() ) {
-      cur = nm->mkNode(kind::UNION, cur, SET_SINGLETON(*it));
+      cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
     }
     return cur;
   }
@@ -886,11 +922,6 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
 
-void TheorySetsPrivate::addSharedTerm(TNode n) {
-  Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
-}
-
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
   if (a.getKind() == kind::CONST_BOOLEAN) {
@@ -948,7 +979,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
     // d_equalityEngine.addTerm(node);
   }
-  if(node.getKind() == kind::SET_SINGLETON) {
+  if(node.getKind() == kind::SINGLETON) {
     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
     learnLiteral(MEMBER(node[0], node), true, true_node);
     //intentional fallthrough
@@ -1125,7 +1156,7 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
   if(S.getKind() == kind::UNION ||
      S.getKind() == kind::INTERSECTION ||
      S.getKind() == kind::SETMINUS ||
-     S.getKind() == kind::SET_SINGLETON) {
+     S.getKind() == kind::SINGLETON) {
     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
   }// propagation: children
 
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 90dec7c0b..e5d7beb2c 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -56,6 +56,8 @@ public:
 
   void collectModelInfo(TheoryModel*, bool fullModel);
 
+  void computeCareGraph();
+
   Node explain(TNode);
 
   void preRegisterTerm(TNode node);
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 7b02c1bfb..8716d1065 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -32,11 +32,11 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
     return false;
   }
 
-  if(setTerm.getKind() == kind::SET_SINGLETON) {
+  if(setTerm.getKind() == kind::SINGLETON) {
     return elementTerm == setTerm[0];
   }
 
-  Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SET_SINGLETON,
+  Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SINGLETON,
          "kind was %d, term: %s", setTerm.getKind(), setTerm.toString().c_str());
 
   return elementTerm == setTerm[1][0] || checkConstantMembership(elementTerm, setTerm[0]);
@@ -44,7 +44,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
   // switch(setTerm.getKind()) {
   // case kind::EMPTYSET:
   //   return false;
-  // case kind::SET_SINGLETON:
+  // case kind::SINGLETON:
   //   return elementTerm == setTerm[0];
   // case kind::UNION:
   //   return checkConstantMembership(elementTerm, setTerm[0]) ||
@@ -195,7 +195,7 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
       case kind::EMPTYSET:
         /* assign emptyset, which is default */
         break;
-      case kind::SET_SINGLETON:
+      case kind::SINGLETON:
         Assert(setterm[0].isConst());
         cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node);
         break;
@@ -220,10 +220,10 @@ Node elementsToNormalConstant(Elements elements,
   } else {
 
     Elements::iterator it = elements.begin();
-    Node cur = nm->mkNode(kind::SET_SINGLETON, *it);
+    Node cur = nm->mkNode(kind::SINGLETON, *it);
     while( ++it != elements.end() ) {
       cur = nm->mkNode(kind::UNION, cur,
-                       nm->mkNode(kind::SET_SINGLETON, *it));
+                       nm->mkNode(kind::SINGLETON, *it));
     }
     return cur;
   }
@@ -239,6 +239,15 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
     return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
   // Further optimization, if constants but differing ones
 
+  if(node.getKind() == kind::INSERT) {
+    Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]);
+    size_t setNodeIndex =  node.getNumChildren()-1;
+    for(size_t i = 1; i < setNodeIndex; ++i) {
+      insertedElements = nm->mkNode(kind::UNION, insertedElements, nm->mkNode(kind::SINGLETON, node[i]));
+    }
+    return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::UNION, insertedElements, node[setNodeIndex]));
+  }//kind::INSERT
+
   if(node.getType().isSet() && node.isConst()) {
     //rewrite set to normal form
     SettermElementsMap setTermElementsMap;   // cache
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 2f4cc6a2f..97fbfe94f 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -76,7 +76,7 @@ public:
     Assert(d_index == 0 || d_index == 1);
 
     if(d_index == 1) {
-      n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+      n = d_nm->mkNode(kind::SINGLETON, *(*(d_constituentVec[0])));
     }
 
     // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 3b2acd956..fa1183e07 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -105,20 +105,20 @@ struct MemberTypeRule {
     }
     return nodeManager->booleanType();
   }
-};/* struct SetInTypeRule */
+};/* struct MemberTypeRule */
 
-struct SetSingletonTypeRule {
+struct SingletonTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::SET_SINGLETON);
+    Assert(n.getKind() == kind::SINGLETON);
     return nodeManager->mkSetType(n[0].getType(check));
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::SET_SINGLETON);
+    Assert(n.getKind() == kind::SINGLETON);
     return n[0].isConst();
   }
-};/* struct SetInTypeRule */
+};/* struct SingletonTypeRule */
 
 struct EmptySetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -128,7 +128,35 @@ struct EmptySetTypeRule {
     Type setType = emptySet.getType();
     return TypeNode::fromType(setType);
   }
-};
+};/* struct EmptySetTypeRule */
+
+struct InsertTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::INSERT);
+    size_t numChildren = n.getNumChildren();
+    Assert( numChildren >= 2 );
+    TypeNode setType = n[numChildren-1].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "inserting into a non-set");
+      }
+      for(size_t i = 0; i < numChildren-1; ++i) {
+        TypeNode elementType = n[i].getType(check);
+        if(elementType != setType.getSetElementType()) {
+          throw TypeCheckingExceptionPrivate
+            (n, "type of element should be same as element type of set being inserted into");
+        }
+      }
+    }
+    return setType;
+  }
+
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    Assert(n.getKind() == kind::INSERT);
+    return n[0].isConst() && n[1].isConst();
+  }
+};/* struct InsertTypeRule */
 
 
 struct SetsProperties {
@@ -146,7 +174,7 @@ struct SetsProperties {
     Assert(type.isSet());
     return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
   }
-};
+};/* struct SetsProperties */
 
 }/* CVC4::theory::sets namespace */
 }/* CVC4::theory namespace */
diff --git a/src/util/emptyset.h b/src/util/emptyset.h
index 2f6c54173..43a868e42 100644
--- a/src/util/emptyset.h
+++ b/src/util/emptyset.h
@@ -35,10 +35,14 @@ class CVC4_PUBLIC EmptySet {
 
   const SetType d_type;
 
+  EmptySet() { }
 public:
 
-  EmptySet() { }		/* Null typed */
-  EmptySet(SetType t):d_type(t) { }
+  /**
+   * Constructs an emptyset of the specified type. Note that the argument
+   * is the type of the set itself, NOT the type of the elements.
+   */
+  EmptySet(SetType setType):d_type(setType) { }
 
 
   ~EmptySet() throw() {