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/theory_engine.cpp b/src/theory/theory_engine.cpp
index 47ba50aad..63024e5d5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -671,6 +671,7 @@ bool TheoryEngine::presolve() {
 void TheoryEngine::postsolve() {
   // Reset the interrupt flag
   d_interrupted = false;
+  bool CVC4_UNUSED wasInConflict = d_inConflict;
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -680,7 +681,7 @@ void TheoryEngine::postsolve() {
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
       theoryOf(THEORY)->postsolve(); \
-      Assert(! d_inConflict, "conflict raised during postsolve()"); \
+      Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
     }
 
     // Postsolve for each theory using the statement above
@@ -961,7 +962,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
       bool value;
       if (d_propEngine->hasValue(assertion, value)) {
         if (!value) {
-          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << endl;
+          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
           d_inConflict = true;
         } else {
           return;
@@ -1011,6 +1012,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
       // Check for propositional conflicts
       bool value;
       if (d_propEngine->hasValue(assertion, value) && !value) {
+          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" << endl;
         d_inConflict = true;
       }
     }