From fe72120c20dc211c7fdf02af7ff1a89527366a47 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 28 Sep 2016 12:03:08 -0400 Subject: [PATCH] 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). --- src/theory/sets/theory_sets_private.cpp | 49 +++++++++++++++++-- src/theory/sets/theory_sets_private.h | 2 +- test/regress/regress0/sets/Makefile.am | 3 +- .../regress0/sets/card-vc6-minimized.smt2 | 15 ++++++ 4 files changed, 62 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress0/sets/card-vc6-minimized.smt2 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& 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 leaves1, std::set 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 get_leaves(Node vertex1, Node vertex2); std::set get_leaves(Node vertex1, Node vertex2, Node vertex3); std::set non_empty(std::set vertices); - void print_graph(); + void print_graph(bool printmodel=false); context::CDQueue < std::pair > d_graphMergesPending; context::CDList 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) -- 2.30.2