From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 9 Jul 2014 18:33:31 +0000 (-0400)
Subject: sets cvc printer
X-Git-Tag: cvc5-1.0.0~6701^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3c76399db741d8d616a75242345710dc1c1b81c;p=cvc5.git

sets cvc printer
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2548c22ab..41e87b809 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -162,6 +162,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << n.getConst<Datatype>().getName();
       break;
 
+    case kind::EMPTYSET: {
+      out << "{} :: " << n.getConst<EmptySet>().getType();
+      return;
+      break;
+    }
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and print something reasonable
@@ -696,6 +702,58 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       return;
       break;
 
+    // SETS
+    case kind::SET_TYPE:
+      out << "SET OF ";
+      toStream(out, n[0], depth, types, false);
+      return;
+      break;
+    case kind::UNION:
+      op << '|';
+      opType = INFIX;
+      break;
+    case kind::INTERSECTION:
+      op << '&';
+      opType = INFIX;
+      break;
+    case kind::SETMINUS:
+      op << '-';
+      opType = INFIX;
+      break;
+    case kind::SUBSET:
+      op << "<=";
+      opType = INFIX;
+      break;
+    case kind::MEMBER:
+      op << "IN";
+      opType = INFIX;
+      break;
+    case kind::SINGLETON:
+      out << "{";
+      toStream(out, n[0], depth, types, false);
+      out << "}";
+      return;
+      break;
+    case kind::INSERT: {
+      if(bracket) {
+	out << '(';
+      }
+      out << '{';
+      size_t i = 0;
+      toStream(out, n[i++], depth, types, false);
+      for(;i+1 < n.getNumChildren(); ++i) {
+        out << ", ";
+        toStream(out, n[i], depth, types, false);
+      }
+      out << "} | ";
+      toStream(out, n[i], depth, types, true);
+      if(bracket) {
+	out << ')';
+      }
+      return;
+      break;
+    }
+
     // Quantifiers
     case kind::FORALL:
       out << "(FORALL";
diff --git a/test/regress/regress0/sets/cvc-sample.smt2 b/test/regress/regress0/sets/cvc-sample.smt2
new file mode 100644
index 000000000..6f8b9f48b
--- /dev/null
+++ b/test/regress/regress0/sets/cvc-sample.smt2
@@ -0,0 +1,53 @@
+OPTION "logic" "ALL_SUPPORTED";
+SetInt : TYPE = SET OF INT;
+PUSH;
+a : SET OF INT;
+b : SET OF INT;
+c : SET OF INT;
+e : INT;
+ASSERT a = {5};
+ASSERT c = (a | b);
+ASSERT NOT(c = (a & b));
+ASSERT c = (a - b);
+ASSERT a <= b;
+ASSERT e IN c;
+ASSERT e IN a;
+ASSERT e IN (a & b);
+CHECKSAT TRUE;
+POP;
+PUSH;
+x : SET OF INT;
+y : SET OF INT;
+z : SET OF INT;
+ASSERT x = y;
+ASSERT NOT((x | z) = (y | z));
+CHECKSAT TRUE;
+POP;
+PUSH;
+x : SET OF INT;
+y : SET OF INT;
+e1 : INT;
+e2 : INT;
+ASSERT x = y;
+ASSERT e1 = e2;
+ASSERT e1 IN x;
+ASSERT NOT(e2 IN y);
+CHECKSAT TRUE;
+POP;
+PUSH;
+x : SET OF INT;
+y : SET OF INT;
+z : SET OF INT;
+e1 : INT;
+e2 : INT;
+ASSERT x = y;
+ASSERT e1 = e2;
+ASSERT e1 IN (x | z);
+ASSERT NOT(e2 IN (y | z));
+CHECKSAT TRUE;
+POP;
+PUSH;
+ASSERT 5 IN ({1, 2, 3, 4} | {5});
+ASSERT 5 IN ({1, 2, 3, 4} | {} :: SET OF INT);
+CHECKSAT TRUE;
+
diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2
index a040b0bec..3bc2da065 100644
--- a/test/regress/regress0/sets/sets-sample.smt2
+++ b/test/regress/regress0/sets/sets-sample.smt2
@@ -3,6 +3,7 @@
 ; EXPECT: unsat
 ; EXPECT: unsat
 ; EXPECT: unsat
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (define-sort SetInt () (Set Int))
 
@@ -59,6 +60,11 @@
 (assert (not (member e2 (union y z))))
 (check-sat)
 (pop 1)
+
+; test all the other kinds for completeness
+(push 1)
+(assert (member 5 (insert 1 2 3 4 (singleton 5))))
+(assert (member 5 (insert 1 2 3 4 (as emptyset (Set Int)))))
+(check-sat)
  
 (exit) 
-(exit)