add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

1 files changed, 22 insertions, 1 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5dc3043af..fcb352ea7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -203,6 +203,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
+    case kind::EMPTYSET:
+      out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
+      break;
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -343,7 +347,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     stillNeedToPrintParams = false;
     break;
 
-    // datatypes
+    // sets
+  case kind::UNION:
+  case kind::INTERSECTION:
+  case kind::SETMINUS:
+  case kind::SUBSET:
+  case kind::IN:
+  case kind::SET_TYPE:
+  case kind::SET_SINGLETON: out << smtKindString(k) << " "; break;
+
+   // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
       out << "as ";
       toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
@@ -528,6 +541,14 @@ static string smtKindString(Kind k) throw() {
   case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
   case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
+
+  case kind::UNION: return "union";
+  case kind::INTERSECTION: return "intersection";
+  case kind::SETMINUS: return "setminus";
+  case kind::SUBSET: return "subseteq";
+  case kind::IN: return "in";
+  case kind::SET_TYPE: return "Set";
+  case kind::SET_SINGLETON: return "setenum";
   default:
     ; /* fall through */
   }