From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 29 Jun 2014 22:44:40 +0000 (-0400)
Subject: sets: "insert" operator
X-Git-Tag: cvc5-1.0.0~6712^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4d031742d969c689d38c0756a5026a434ef89b3;p=cvc5.git

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 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) {
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index ccedc7596..9536dfac1 100644
--- 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
index 000000000..3a7b18179
--- /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)