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

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 2359d5d86..e8d53e539 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -620,6 +620,9 @@ public:
    * check() or propagate() method called.  A Theory may empty its
    * assertFact() queue using get().  A Theory can raise conflicts,
    * add lemmas, and propagate literals during presolve().
+   *
+   * NOTE: The presolve property must be added to the kinds file for
+   * the theory.
    */
   virtual void presolve() { }