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

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 525b129cf..a30867ee1 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -122,6 +122,10 @@ std::string LogicInfo::getLogicString() const {
         }
         ++seen;
       }
+      if(d_theories[THEORY_SETS]) {
+        ss << "_SETS";
+        ++seen;
+      }
 
       if(seen != d_sharingTheories) {
         Unhandled("can't extract a logic string from LogicInfo; at least one "
@@ -256,6 +260,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         arithNonLinear();
         p += 4;
       }
+      if(!strncmp(p, "_SETS", 5)) {
+        enableTheory(THEORY_SETS);
+        p += 5;
+      }
     }
   }
   if(*p != '\0') {