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, 4 insertions, 2 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index f8e361081..8bb849496 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -833,12 +833,14 @@ public:
   void addTriggerPredicate(TNode predicate);
 
   /**
-   * Returns true if the two are currently in the database and equal.
+   * Returns true if the two terms are equal. Requires both terms to
+   * be in the database.
    */
   bool areEqual(TNode t1, TNode t2) const;
 
   /**
-   * Check whether the two term are dis-equal.
+   * Check whether the two term are dis-equal. Requires both terms to
+   * be in the database.
    */
   bool areDisequal(TNode t1, TNode t2, bool ensureProof) const;