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, 27 insertions, 0 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f97f4a8ae..6974c62af 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -833,6 +833,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
                              MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
         v.insert(v.end(), f.begin(), f.end());
         expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+      } else if(f.getKind() == CVC4::kind::EMPTYSET) {
+        Debug("parser") << "Empty set encountered: " << f << " "
+                          << f2 << " " << type <<  std::endl;
+        // TODO: what is f2 about, should we add some assertions?
+        expr = MK_CONST( ::CVC4::EmptySet(type) );
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1028,6 +1033,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | str[s,false]
     { expr = MK_CONST( ::CVC4::String(s) ); }
 
+  | EMPTYSET_TOK
+    { expr = MK_CONST( ::CVC4::EmptySet()); }
+
     // NOTE: Theory constants go here
   ;
 
@@ -1298,6 +1306,12 @@ builtinOp[CVC4::Kind& kind]
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
+  | SETUNION_TOK  { $kind = CVC4::kind::UNION; }
+  | SETINT_TOK    { $kind = CVC4::kind::INTERSECTION; }
+  | SETMINUS_TOK  { $kind = CVC4::kind::SETMINUS; }
+  | SETSUB_TOK    { $kind = CVC4::kind::SUBSET; }
+  | SETIN_TOK     { $kind = CVC4::kind::IN; }
+  | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; }
 
   // NOTE: Theory operators go here
   ;
@@ -1407,6 +1421,11 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
           PARSER_STATE->parseError("Illegal array type.");
         }
         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
+      } else if(name == "Set") {
+        if(args.size() != 1) {
+          PARSER_STATE->parseError("Illegal set type.");
+        }
+        t = EXPR_MANAGER->mkSetType( args[0] );
       } else if(check == CHECK_DECLARED ||
                 PARSER_STATE->isDeclared(name, SYM_SORT)) {
         t = PARSER_STATE->getSort(name, args);
@@ -1688,6 +1707,14 @@ REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
 RERANGE_TOK : 're.range';
 
+SETUNION_TOK: 'union';
+SETINT_TOK: 'intersection';
+SETMINUS_TOK: 'setminus';
+SETSUB_TOK: 'subseteq';
+SETIN_TOK: 'in';
+SETSINGLETON_TOK: 'setenum';
+EMPTYSET_TOK: 'emptyset';
+
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
  * and ends with | and does not otherwise contain |.