sets: "insert" operator

new™! support for (insert (X (Set X)) (Set X) :right-associative)
from the finte sets theory prosoal.

e.g., (insert 1 2 3 4 (singleton 5))

5 files changed, 42 insertions, 0 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3f1e59e6d..0c4b1258f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -152,6 +152,7 @@ void Smt2::addTheory(Theory theory) {
     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 3c0f4ebc5..bc2cb1ec9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -613,6 +613,7 @@ static string smtKindString(Kind k) throw() {
   case kind::MEMBER: return "member";
   case kind::SET_TYPE: return "Set";
   case kind::SINGLETON: return "singleton";
+  case kind::INSERT: return "insert";
   default:
     ; /* fall through */
   }
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 06d3be5a0..39e7883c6 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -41,6 +41,7 @@ operator SETMINUS      2  "set subtraction"
 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
@@ -49,10 +50,12 @@ typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
 typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
 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 SINGLETON     ::CVC4::theory::sets::SingletonTypeRule
+construle INSERT        ::CVC4::theory::sets::InsertTypeRule
 
 endtheory
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index ce469cc0c..8716d1065 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -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_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 2267ee22a..fa1183e07 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -130,6 +130,34 @@ struct EmptySetTypeRule {
   }
 };/* 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 {
   inline static Cardinality computeCardinality(TypeNode type) {