Fix the merge of kbansal/card branch (2039eab).

A bug was introduced in the cleanup process as preparation for the merge
(theory_sets_private.cpp, lines 2502-2508 in this commit).

4 files changed, 62 insertions, 7 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index ec6bb7fcd..6fb90fea3 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -853,6 +853,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
 
   //processCard2 begin
   if(Debug.isOn("sets-card")) {
+    print_graph(true);
     for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
       Node n = nm->mkNode(kind::CARD, *it);
       Debug("sets-card") << "[sets-card] " << n << " = ";
@@ -1040,7 +1041,7 @@ Node mkAnd(const std::vector<TNode>& conjunctions) {
     if (t.getKind() == kind::AND) {
       for(TNode::iterator child_it = t.begin();
           child_it != t.end(); ++child_it) {
-        Assert((*child_it).getKind() != kind::AND);
+        // Assert((*child_it).getKind() != kind::AND);
         all.insert(*child_it);
       }
     }
@@ -1436,7 +1437,11 @@ Node TheorySetsPrivate::explain(TNode literal)
     Unhandled();
   }
 
-  return mkAnd(assumptions);
+  if(assumptions.size()) {
+    return mkAnd(assumptions);
+  } else {
+    return d_trueNode;
+  }
 }
 
 bool TheorySetsPrivate::lemma(Node n, SetsLemmaTag t)
@@ -2333,7 +2338,8 @@ void TheorySetsPrivate::merge_nodes(std::set<TNode> leaves1, std::set<TNode> lea
 
 }
 
-void  TheorySetsPrivate::print_graph() {
+void  TheorySetsPrivate::print_graph(bool printmodel) {
+  NodeManager* nm = NodeManager::currentNM();
   std::string tag = "sets-graph";
   if(Trace.isOn("sets-graph")) {
     Trace(tag) << "[sets-graph] Graph : " << std::endl;
@@ -2358,13 +2364,38 @@ void  TheorySetsPrivate::print_graph() {
     oss << "digraph G { ";
     for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
       TNode v = *it;
+
+      std::ostringstream v_oss;
+      v_oss << v;
+      if(printmodel)
+      {
+        Node n = nm->mkNode(kind::CARD, v);
+        if((Rewriter::rewrite(n)).isConst()) {
+          v_oss << " " << (Rewriter::rewrite(n));
+        } else {
+          v_oss << " " << d_external.d_valuation.getModelValue(n);
+        }
+      }
+      
       if(d_E.find(v) != d_E.end()) {
         BOOST_FOREACH(TNode w, d_E[v].get()) {
+
+          std::ostringstream w_oss;
+          w_oss << w;
+          if(printmodel) {
+            Node n = nm->mkNode(kind::CARD, w);
+            if((Rewriter::rewrite(n)).isConst()) {
+              w_oss << " " << (Rewriter::rewrite(n));
+            } else {
+              w_oss << " " << d_external.d_valuation.getModelValue(n);
+            }
+          }
+          
           //oss << v.getId() << " -> " << w.getId() << "; ";
-          oss << "\"" << v << "\" -> \"" << w << "\"; ";
+          oss << "\"" << v_oss.str() << "\" -> \"" << w_oss.str() << "\"; ";
         }
       } else {
-        oss << "\"" << v << "\";";
+        oss << "\"" << v_oss.str() << "\";";
       }
     }
     oss << "}";
@@ -2468,6 +2499,14 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) {
 
   NodeManager* nm = NodeManager::currentNM();
 
+  if(options::setsGuessEmpty() == 0) {
+    Trace("sets-guess-empty") << "[sets-guess-empty] Generating lemmas before introduce." << std::endl;
+    guessLeavesEmptyLemmas();
+    if(d_newLemmaGenerated) {
+      return;
+    }
+  }
+
   // Introduce
   for(CDNodeSet::const_iterator it = d_cardTerms.begin();
       it != d_cardTerms.end(); ++it) {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 71a6d9b2d..049e95786 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -280,7 +280,7 @@ private:
   std::set<TNode> get_leaves(Node vertex1, Node vertex2);
   std::set<TNode> get_leaves(Node vertex1, Node vertex2, Node vertex3);
   std::set<TNode> non_empty(std::set<TNode> vertices);
-  void print_graph();
+  void print_graph(bool printmodel=false);
   context::CDQueue < std::pair<TNode, TNode> > d_graphMergesPending;
   context::CDList<Node> d_allSetEqualitiesSoFar;
   Node eqSoFar();
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 558d170d7..2f36cc188 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -64,7 +64,8 @@ TESTS =	\
 	union-1b.smt2 \
 	union-2.smt2 \
 	dt-simp-mem.smt2 \
-	card3-ground.smt2
+	card3-ground.smt2 \
+	card-vc6-minimized.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/card-vc6-minimized.smt2 b/test/regress/regress0/sets/card-vc6-minimized.smt2
new file mode 100644
index 000000000..d7f4bdf1e
--- /dev/null
+++ b/test/regress/regress0/sets/card-vc6-minimized.smt2
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+(set-logic QF_UFLIAFS)
+(declare-fun x () Int)
+(declare-fun c () (Set Int))
+(declare-fun alloc0 () (Set Int))
+(declare-fun alloc1 () (Set Int))
+(declare-fun alloc2 () (Set Int))
+(assert
+(and (member x c)
+      (<= (card (setminus alloc1 alloc0)) 1)
+      (<= (card (setminus alloc2 alloc1))
+          (card (setminus c (singleton x))))
+      (> (card (setminus alloc2 alloc0)) (card c))
+))
+(check-sat)