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

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3f1e59e6d0065fdada435b7cd911c839b61c597c..0c4b1258f794bc1198f5f6db2f3893d34def8a12 100644 (file)
--- 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 3c0f4ebc5ee627e9c0c70008c7bc86f02851ce1c..bc2cb1ec9e5d5f76339c427a9c1b9c1cde14df08 100644 (file)
--- 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 06d3be5a0e175ca7d61570630bb76e914518d593..39e7883c6ddf367dfa64270efc6246710317cd02 100644 (file)
--- 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 ce469cc0c9faac96ea0c399bb6f7acef3987c258..8716d10656220804571bf638e633e9882787f09d 100644 (file)
--- 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 2267ee22a035b5dd53a5d7bba6620d7f1dffc2e9..fa1183e074b1cf6b41a7c4a03596582524decb33 100644 (file)
--- 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) {

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index ccedc7596557788edd6bc175fe4621dd5db8af5c..9536dfac1d5a748321a7ad896d68d17690cd00a7 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -44,6 +44,7 @@ TESTS =       \
        error1.smt2 \
        error2.smt2 \
        eqtest.smt2 \
+       insert.smt2 \
        fuzz14418.smt2 \
        fuzz15201.smt2 \
        fuzz31811.smt2 \

diff --git a/test/regress/regress0/sets/insert.smt2 b/test/regress/regress0/sets/insert.smt2
new file mode 100644 (file)
index 0000000..3a7b181
--- /dev/null
+++ b/test/regress/regress0/sets/insert.smt2
@@ -0,0 +1,7 @@
+(set-option :produce-models true)
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun X () (Set Int))
+(assert (= X (insert 1 2 (singleton 3))))
+(check-sat)
+;(get-model)