4 files changed, 52 insertions, 7 deletions

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 4992f654f..263d61934 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -74,6 +74,10 @@ void TheorySets::preRegisterTerm(TNode node) {
   d_internal->preRegisterTerm(node);
 }
 
+Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) {
+  return d_internal->expandDefinition(logicRequest, n);
+}
+
 Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   return d_internal->ppAssert( in, outSubstitutions );
 }
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index bbc6ae0c4..3ecd404bb 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -66,6 +66,8 @@ public:
 
   void preRegisterTerm(TNode node);
 
+  Node expandDefinition(LogicRequest &logicRequest, Node n);
+
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
   void presolve();
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index a2a56e137..3013711eb 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -604,13 +604,8 @@ void TheorySetsPrivate::fullEffortCheck(){
           }else if( n.getKind()==kind::EMPTYSET ){
             d_eqc_emptyset[tnn] = eqc;
           }else if( n.getKind()==kind::UNIVERSE_SET ){
-            if( options::setsExt() ){
-              d_eqc_univset[tnn] = eqc;
-            }else{
-              std::stringstream ss;
-              ss << "Symbols complement and universe set are not supported in default mode, try --sets-ext." << std::endl;
-              throw LogicException(ss.str());
-            }
+            Assert( options::setsExt() );
+            d_eqc_univset[tnn] = eqc;
           }else{
             Node r1 = d_equalityEngine.getRepresentative( n[0] );
             Node r2 = d_equalityEngine.getRepresentative( n[1] );
@@ -2155,8 +2150,20 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
   }
 }
 
+Node TheorySetsPrivate::expandDefinition(LogicRequest &logicRequest, Node n) {
+  Debug("sets-proc") << "expandDefinition : " << n << std::endl;
+  if( n.getKind()==kind::UNIVERSE_SET || n.getKind()==kind::COMPLEMENT || n.getKind()==kind::JOIN_IMAGE ){
+    if( !options::setsExt() ){
+      std::stringstream ss;
+      ss << "Extended set operators are not supported in default mode, try --sets-ext.";
+      throw LogicException(ss.str());
+    }
+  }
+  return n;
+}
 
 Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+  Debug("sets-proc") << "ppAssert : " << in << std::endl;
   Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
   
   //TODO: allow variable elimination for sets when setsExt = true
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 7bc17c927..175e82bb8 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -188,6 +188,38 @@ public:
 
   void preRegisterTerm(TNode node);
 
+  /** expandDefinition
+   * If the sets-ext option is not set and we have an extended operator, 
+   * we throw an exception. This function is a no-op otherwise.
+   *
+   * This is related to github issue #1076
+   * TheorySets uses expandDefinition as an entry point to see if the input
+   * contains extended operators.
+   *
+   * We need to be notified when a universe set occurs in our input,
+   * before preprocessing and simplification takes place. Otherwise the models
+   * may be inaccurate when setsExt is false, here is an example:
+   *
+   * x,y : (Set Int)
+   * x = (as univset (Set Int));
+   * 0 in y;
+   * check-sat;
+   *
+   * If setsExt is enabled, the model value of (as univset (Set Int)) is always accurate.
+   *
+   * If setsExt is not enabled, the following can happen for the above example:
+   * x = (as univset (Set Int)) is made into a model substitution during 
+   * simplification. This means (as univset (Set Int)) is not a term in any assertion, 
+   * and hence we do not throw an exception, nor do we infer that 0 is a member of 
+   * (as univset (Set Int)). We instead report a model where x = {}. The correct behavior 
+   * is to throw an exception that says universe set is not supported when setsExt disabled.
+   * Hence we check for the existence of universe set before simplification here.
+   *
+   * Another option to fix this is to make TheoryModel::getValue more general
+   * so that it makes theory-specific calls to evaluate interpreted symbols.
+   */
+  Node expandDefinition(LogicRequest &logicRequest, Node n);
+
   Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   
   void presolve();