Ensure that expand definitions is called on all non-variable expressi… (#1070)

* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.

* Add comments concerning expandDefinitions

* Expand comment, move to .h

16 files changed, 112 insertions, 35 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f360ae2fd..b2f7d6ccc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2277,8 +2277,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
     if(!childrenPushed) {
       Kind k = n.getKind();
 
-      // Apart from apply, we can short circuit leaves
-      if(k != kind::APPLY && n.getNumChildren() == 0) {
+      // we can short circuit (variable) leaves
+      if(n.isVar()) {
         SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
         if(i != d_smt.d_definedFunctions->end()) {
           // replacement must be closed
@@ -2372,15 +2372,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
         node = t->expandDefinition(req, n);
       }
 
-      // there should be children here, otherwise we short-circuited a result-push/continue, above
-      if (node.getNumChildren() == 0) {
-        Debug("expand") << "Unexpectedly no children..." << node << endl;
-      }
-      // This invariant holds at the moment but it is concievable that a new theory
-      // might introduce a kind which can have children before definition expansion but doesn't
-      // afterwards.  If this happens, remove this assertion.
-      Assert(node.getNumChildren() > 0);
-
       // the partial functions can fall through, in which case we still
       // consider their children
       worklist.push(make_triple(Node(n), node, true));            // Original and rewritten result
@@ -2394,22 +2385,24 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
       // Reconstruct the node from it's (now rewritten) children on the stack
 
       Debug("expand") << "cons : " << node << endl;
-      //cout << "cons : " << node << endl;
-      NodeBuilder<> nb(node.getKind());
-      if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        Debug("expand") << "op   : " << node.getOperator() << endl;
-        //cout << "op   : " << node.getOperator() << endl;
-        nb << node.getOperator();
-      }
-      for(size_t i = 0; i < node.getNumChildren(); ++i) {
-        Assert(!result.empty());
-        Node expanded = result.top();
-        result.pop();
-        //cout << "exchld : " << expanded << endl;
-        Debug("expand") << "exchld : " << expanded << endl;
-        nb << expanded;
+      if(node.getNumChildren()>0) {
+        //cout << "cons : " << node << endl;
+        NodeBuilder<> nb(node.getKind());
+        if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+          Debug("expand") << "op   : " << node.getOperator() << endl;
+          //cout << "op   : " << node.getOperator() << endl;
+          nb << node.getOperator();
+        }
+        for(size_t i = 0; i < node.getNumChildren(); ++i) {
+          Assert(!result.empty());
+          Node expanded = result.top();
+          result.pop();
+          //cout << "exchld : " << expanded << endl;
+          Debug("expand") << "exchld : " << expanded << endl;
+          nb << expanded;
+        }
+        node = nb;
       }
-      node = nb;
       cache[n] = n == node ? Node::null() : node;           // Only cache once all subterms are expanded
       result.push(node);
     }
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();
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 73102a6e2..1a72944ff 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -424,6 +424,12 @@ public:
    * used, definitions should only be used when rewrites are not
    * possible, for example in handling under-specified operations
    * using partially defined functions.
+   *
+   * TODO (github issue #1076): 
+   * some theories like sets use expandDefinition as a "context
+   * independent preRegisterTerm".  This is required for cases where
+   * a theory wants to be notified about a term before preprocessing
+   * and simplification but doesn't necessarily want to rewrite it.
    */
   virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
     // by default, do nothing
diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc b/test/regress/regress0/fmf/quant_real_univ.cvc
index c3cefd767..c3dbb2cd6 100644
--- a/test/regress/regress0/fmf/quant_real_univ.cvc
+++ b/test/regress/regress0/fmf/quant_real_univ.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat

 OPTION "fmf-bound";

+OPTION "sets-ext";

 Atom : TYPE;

 REAL_UNIVERSE : SET OF [REAL];

 ATOM_UNIVERSE : SET OF [Atom];

diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc
index e36c6a647..297898a81 100644
--- a/test/regress/regress0/rels/joinImg_0.cvc
+++ b/test/regress/regress0/rels/joinImg_0.cvc
@@ -1,5 +1,6 @@
 % EXPECT: unsat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc
index 602c4fe3f..4e69394bd 100644
--- a/test/regress/regress0/rels/joinImg_0_1.cvc
+++ b/test/regress/regress0/rels/joinImg_0_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc
index 47e57c1fb..81f208fc4 100644
--- a/test/regress/regress0/rels/joinImg_1.cvc
+++ b/test/regress/regress0/rels/joinImg_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: unsat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc
index a7927f7e2..003770a1b 100644
--- a/test/regress/regress0/rels/joinImg_1_1.cvc
+++ b/test/regress/regress0/rels/joinImg_1_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc
index bbf57629b..a4acfe6c6 100644
--- a/test/regress/regress0/rels/joinImg_2.cvc
+++ b/test/regress/regress0/rels/joinImg_2.cvc
@@ -1,5 +1,6 @@
 % EXPECT: unsat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc
index b38bfab06..03f88be37 100644
--- a/test/regress/regress0/rels/joinImg_2_1.cvc
+++ b/test/regress/regress0/rels/joinImg_2_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
@@ -21,4 +22,4 @@ ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
 ASSERT x = {(f, g), (b, c), (d, e), (c, e)};
 ASSERT (NOT(a = b)) OR (NOT(a = f));
 
-CHECKSAT;
\ No newline at end of file
+CHECKSAT;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index c8e416a42..de2170768 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -86,7 +86,9 @@ TESTS =	\
 	sets-poly-nonint.smt2 \
 	int-real-univ.smt2 \
 	int-real-univ-unsat.smt2 \
-	sets-tuple-poly.cvc
+	sets-tuple-poly.cvc \
+	arjun-set-univ.cvc \
+	univ-set-uf-elim.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/arjun-set-univ.cvc b/test/regress/regress0/sets/arjun-set-univ.cvc
new file mode 100644
index 000000000..3c35a62a5
--- /dev/null
+++ b/test/regress/regress0/sets/arjun-set-univ.cvc
@@ -0,0 +1,8 @@
+% EXPECT: Extended set operators are not supported in default mode, try --sets-ext.
+% EXIT: 1
+OPTION "produce-models" true;
+x,y,z : SET OF BOOLEAN;
+ASSERT x = {TRUE};
+ASSERT y = {FALSE};
+CHECKSAT z = ~ y;
+COUNTERMODEL;
diff --git a/test/regress/regress0/sets/univ-set-uf-elim.smt2 b/test/regress/regress0/sets/univ-set-uf-elim.smt2
new file mode 100644
index 000000000..a22f2a44f
--- /dev/null
+++ b/test/regress/regress0/sets/univ-set-uf-elim.smt2
@@ -0,0 +1,16 @@
+; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
+; EXIT: 1
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun f ((Set Bool)) Int)
+(declare-fun s () (Set Bool))
+
+(assert (member true s))
+(assert (member false s))
+(assert (= a (f (as univset (Set Bool)))))
+
+(assert (= (f (as emptyset (Set Bool))) 1))
+(assert (= (f (singleton true)) 2))
+(assert (= (f (singleton false)) 3))
+(assert (= (f (union (singleton true) (singleton false))) 4))
+(check-sat)