From: Morgan Deters Date: Fri, 1 Aug 2014 19:08:06 +0000 (-0400) Subject: Some fixes to symmetry breaker (resolves bug 576). X-Git-Tag: cvc5-1.0.0~6509^2~39 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6e615d3f8c080970ce9b3927f99c98e6eb0d3002;p=cvc5.git Some fixes to symmetry breaker (resolves bug 576). --- diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index f60f15c92..bd85b735d 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -177,7 +177,8 @@ SymmetryBreaker::SymmetryBreaker(context::Context* context) : d_terms(), d_template(), d_normalizationCache(), - d_termEqs() { + d_termEqs(), + d_termEqsOnly() { } class SBGuard { @@ -207,10 +208,10 @@ void SymmetryBreaker::rerunAssertionsIfNecessary() { Node SymmetryBreaker::norm(TNode phi) { Node n = Rewriter::rewrite(phi); - return normInternal(n); + return normInternal(n, 0); } -Node SymmetryBreaker::normInternal(TNode n) { +Node SymmetryBreaker::normInternal(TNode n, size_t level) { Node& result = d_normalizationCache[n]; if(!result.isNull()) { return result; @@ -225,7 +226,46 @@ Node SymmetryBreaker::normInternal(TNode n) { return result = NodeManager::currentNM()->mkNode(k, kids); } - case kind::AND: + case kind::AND: { + // commutative+associative N-ary operator handling + vector kids; + kids.reserve(n.getNumChildren()); + queue work; + work.push(n); + Debug("ufsymm:norm") << "UFSYMM processing " << n << endl; + do { + TNode m = work.front(); + work.pop(); + for(TNode::iterator i = m.begin(); i != m.end(); ++i) { + if((*i).getKind() == k) { + work.push(*i); + } else { + if( (*i).getKind() == kind::OR ) { + kids.push_back(normInternal(*i, level)); + } else if((*i).getKind() == kind::IFF || + (*i).getKind() == kind::EQUAL) { + kids.push_back(normInternal(*i, level)); + if((*i)[0].isVar() || + (*i)[1].isVar()) { + d_termEqs[(*i)[0]].insert((*i)[1]); + d_termEqs[(*i)[1]].insert((*i)[0]); + if(level == 0) { + d_termEqsOnly[(*i)[0]].insert((*i)[1]); + d_termEqsOnly[(*i)[1]].insert((*i)[0]); + Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl; + } + } + } else { + kids.push_back(*i); + } + } + } + } while(!work.empty()); + Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl; + sort(kids.begin(), kids.end()); + return result = NodeManager::currentNM()->mkNode(k, kids); + } + case kind::OR: { // commutative+associative N-ary operator handling vector kids; @@ -233,6 +273,9 @@ Node SymmetryBreaker::normInternal(TNode n) { queue work; work.push(n); Debug("ufsymm:norm") << "UFSYMM processing " << n << endl; + TNode matchingTerm = TNode::null(); + vector matchingTermEquals; + bool first = true, matchedVar = false; do { TNode m = work.front(); work.pop(); @@ -240,24 +283,76 @@ Node SymmetryBreaker::normInternal(TNode n) { if((*i).getKind() == k) { work.push(*i); } else { - if( (*i).getKind() == kind::AND || - (*i).getKind() == kind::OR ) { - kids.push_back(normInternal(*i)); + if( (*i).getKind() == kind::AND ) { + first = false; + matchingTerm = TNode::null(); + kids.push_back(normInternal(*i, level + 1)); } else if((*i).getKind() == kind::IFF || (*i).getKind() == kind::EQUAL) { - kids.push_back(normInternal(*i)); + kids.push_back(normInternal(*i, level + 1)); if((*i)[0].isVar() || (*i)[1].isVar()) { d_termEqs[(*i)[0]].insert((*i)[1]); d_termEqs[(*i)[1]].insert((*i)[0]); - Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl; + if(level == 0) { + if(first) { + matchingTerm = *i; + } else if(!matchingTerm.isNull()) { + if(matchedVar) { + if(matchingTerm == (*i)[0]) { + matchingTermEquals.push_back((*i)[1]); + } else if(matchingTerm == (*i)[1]) { + matchingTermEquals.push_back((*i)[0]); + } else { + matchingTerm = TNode::null(); + } + } else if((*i)[0] == matchingTerm[0]) { + matchingTermEquals.push_back(matchingTerm[1]); + matchingTermEquals.push_back((*i)[1]); + matchingTerm = matchingTerm[0]; + matchedVar = true; + } else if((*i)[1] == matchingTerm[0]) { + matchingTermEquals.push_back(matchingTerm[1]); + matchingTermEquals.push_back((*i)[0]); + matchingTerm = matchingTerm[0]; + matchedVar = true; + } else if((*i)[0] == matchingTerm[1]) { + matchingTermEquals.push_back(matchingTerm[0]); + matchingTermEquals.push_back((*i)[1]); + matchingTerm = matchingTerm[1]; + matchedVar = true; + } else if((*i)[1] == matchingTerm[1]) { + matchingTermEquals.push_back(matchingTerm[0]); + matchingTermEquals.push_back((*i)[0]); + matchingTerm = matchingTerm[1]; + matchedVar = true; + } else { + matchingTerm = TNode::null(); + } + } + } + } else { + matchingTerm = TNode::null(); } + first = false; } else { + first = false; + matchingTerm = TNode::null(); kids.push_back(*i); } } } } while(!work.empty()); + if(!matchingTerm.isNull()) { + if(Debug.isOn("ufsymm:eq")) { + Debug("ufsymm:eq") << "UFSYMM here we can conclude that " << matchingTerm << " is one of {"; + for(vector::const_iterator i = matchingTermEquals.begin(); i != matchingTermEquals.end(); ++i) { + Debug("ufsymm:eq") << " " << *i; + } + Debug("ufsymm:eq") << " }" << endl; + } + d_termEqsOnly[matchingTerm].insert(matchingTermEquals.begin(), matchingTermEquals.end()); + } Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl; sort(kids.begin(), kids.end()); return result = NodeManager::currentNM()->mkNode(k, kids); @@ -269,7 +364,11 @@ Node SymmetryBreaker::normInternal(TNode n) { n[1].isVar()) { d_termEqs[n[0]].insert(n[1]); d_termEqs[n[1]].insert(n[0]); - Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; + if(level == 0) { + d_termEqsOnly[n[0]].insert(n[1]); + d_termEqsOnly[n[1]].insert(n[0]); + Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; + } } /* intentional fall-through! */ case kind::XOR: @@ -353,6 +452,7 @@ void SymmetryBreaker::clear() { d_template.reset(); d_normalizationCache.clear(); d_termEqs.clear(); + d_termEqsOnly.clear(); } void SymmetryBreaker::apply(std::vector& newClauses) { @@ -589,29 +689,41 @@ void SymmetryBreaker::selectTerms(const Permutation& p) { set terms; for(Permutation::iterator i = p.begin(); i != p.end(); ++i) { const TermEq& teq = d_termEqs[*i]; + for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) { + Debug("ufsymm") << "selectTerms: insert in terms " << *j << std::endl; + } terms.insert(teq.begin(), teq.end()); } for(set::iterator i = terms.begin(); i != terms.end(); ++i) { - const TermEq& teq = d_termEqs[*i]; - if(isSubset(teq, p)) { - d_terms.insert(d_terms.end(), *i); - } else { - if(Debug.isOn("ufsymm")) { - Debug("ufsymm") << "UFSYMM selectTerms() threw away candidate: " << *i << endl; - Debug("ufsymm:eq") << "UFSYMM selectTerms() #teq == " << teq.size() << " #p == " << p.size() << endl; - TermEq::iterator j; - for(j = teq.begin(); j != teq.end(); ++j) { - Debug("ufsymm:eq") << "UFSYMM -- teq " << *j << " in " << p << " ?" << endl; - if(p.find(*j) == p.end()) { - Debug("ufsymm") << "UFSYMM -- because its teq " << *j - << " isn't in " << p << endl; - break; - } else { - Debug("ufsymm:eq") << "UFSYMM -- yep" << endl; + if(d_termEqsOnly.find(*i) != d_termEqsOnly.end()) { + const TermEq& teq = d_termEqsOnly[*i]; + if(isSubset(teq, p)) { + Debug("ufsymm") << "selectTerms: teq = {"; + for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) { + Debug("ufsymm") << " " << *j << std::endl; + } + Debug("ufsymm") << " } is subset of p " << p << std::endl; + d_terms.insert(d_terms.end(), *i); + } else { + if(Debug.isOn("ufsymm")) { + Debug("ufsymm") << "UFSYMM selectTerms() threw away candidate: " << *i << endl; + Debug("ufsymm:eq") << "UFSYMM selectTerms() #teq == " << teq.size() << " #p == " << p.size() << endl; + TermEq::iterator j; + for(j = teq.begin(); j != teq.end(); ++j) { + Debug("ufsymm:eq") << "UFSYMM -- teq " << *j << " in " << p << " ?" << endl; + if(p.find(*j) == p.end()) { + Debug("ufsymm") << "UFSYMM -- because its teq " << *j + << " isn't in " << p << endl; + break; + } else { + Debug("ufsymm:eq") << "UFSYMM -- yep" << endl; + } } + Assert(j != teq.end(), "failed to find a difference between p and teq ?!"); } - Assert(j != teq.end(), "failed to find a difference between p and teq ?!"); } + } else { + Debug("ufsymm") << "selectTerms: don't have data for " << *i << " so can't conclude anything" << endl; } } if(Debug.isOn("ufsymm")) { diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 8cc2ef6a7..d07ef64e0 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -114,6 +114,7 @@ private: Template d_template; std::hash_map d_normalizationCache; TermEqs d_termEqs; + TermEqs d_termEqsOnly; void clear(); void rerunAssertionsIfNecessary(); @@ -123,7 +124,7 @@ private: void selectTerms(const Permutation& p); Terms::iterator selectMostPromisingTerm(Terms& terms); void insertUsedIn(Term term, const Permutation& p, std::set& cts); - Node normInternal(TNode phi); + Node normInternal(TNode phi, size_t level); Node norm(TNode n); // === STATISTICS === diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index cc691f8d2..55a588362 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -160,7 +160,9 @@ BUG_TESTS = \ bug543.smt2 \ bug544.smt2 \ bug548a.smt2 \ - bug567.smt2 + bug567.smt2 \ + bug576.smt2 \ + bug576a.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug576.smt2 b/test/regress/regress0/bug576.smt2 new file mode 100644 index 000000000..c9ca241d7 --- /dev/null +++ b/test/regress/regress0/bug576.smt2 @@ -0,0 +1,27 @@ +(set-logic QF_UF) +(set-info :status sat) +(declare-sort var 0) +(declare-sort reg 0) +(declare-fun var5_1 () var) +(declare-fun b_1 () var) +(declare-fun a_1 () var) +(declare-fun r0 () reg) +(declare-fun r1 () reg) +(declare-fun r2 () reg) +(declare-fun r3 () reg) +(assert (not (= r0 r1))) +(assert (not (= r0 r2))) +(assert (not (= r0 r3))) +(assert (not (= r1 r2))) +(assert (not (= r1 r3))) +(assert (not (= r2 r3))) +(declare-fun assign (var) reg) +(assert (or (= (assign var5_1) r0) (= (assign var5_1) r1) (= (assign var5_1) r2) (= (assign var5_1) r3) )) +(assert (or (= (assign b_1) r1) )) +(assert (or (= (assign a_1) r0) )) +(assert (not (= (assign b_1) (assign a_1)))) +(assert (= (assign var5_1) r0)) +(assert (= (assign b_1) r1)) +(assert (= (assign a_1) r0)) +(check-sat) +(exit) diff --git a/test/regress/regress0/bug576a.smt2 b/test/regress/regress0/bug576a.smt2 new file mode 100644 index 000000000..00487a183 --- /dev/null +++ b/test/regress/regress0/bug576a.smt2 @@ -0,0 +1,48 @@ +(set-logic QF_UF) +(set-info :status sat) +(declare-sort var 0) +(declare-sort reg 0) +(declare-fun a1_1 () var) +(declare-fun a2_1 () var) +(declare-fun c_3 () var) +(declare-fun c_4 () var) +(declare-fun b_3 () var) +(declare-fun r0 () reg) +(declare-fun r1 () reg) +(declare-fun r2 () reg) +(declare-fun r3 () reg) +(declare-fun r4 () reg) +(declare-fun r6 () reg) +(assert (not (= r0 r1))) +(assert (not (= r0 r2))) +(assert (not (= r0 r3))) +(assert (not (= r0 r4))) +(assert (not (= r0 r6))) +(assert (not (= r1 r2))) +(assert (not (= r1 r3))) +(assert (not (= r1 r4))) +(assert (not (= r1 r6))) +(assert (not (= r2 r3))) +(assert (not (= r2 r4))) +(assert (not (= r2 r6))) +(assert (not (= r3 r4))) +(assert (not (= r3 r6))) +(assert (not (= r4 r6))) +(declare-fun assign (var) reg) +(assert (or (= (assign a1_1) r0) (= (assign a1_1) r1) (= (assign a1_1) r2) (= (assign a1_1) r3) (= (assign a1_1) r4) (= (assign a1_1) r6) )) +(assert (or (= (assign a2_1) r0) (= (assign a2_1) r1) (= (assign a2_1) r2) (= (assign a2_1) r3) (= (assign a2_1) r4) (= (assign a2_1) r6) )) +(assert (or (= (assign c_3) r0) (= (assign c_3) r1) (= (assign c_3) r2) (= (assign c_3) r3) (= (assign c_3) r4) (= (assign c_3) r6) )) +(assert (or (= (assign c_4) r0) (= (assign c_4) r1) (= (assign c_4) r2) (= (assign c_4) r3) (= (assign c_4) r4) (= (assign c_4) r6) )) +(assert (or (= (assign b_3) r0) (= (assign b_3) r1) (= (assign b_3) r2) (= (assign b_3) r3) (= (assign b_3) r4) (= (assign b_3) r6) )) +(assert (not (= (assign a1_1) (assign c_4)))) +(assert (not (= (assign a2_1) (assign c_3)))) +(assert (not (= (assign a2_1) (assign b_3)))) +(assert (not (= (assign c_3) (assign b_3)))) +(assert (not (= (assign c_4) (assign b_3)))) +(assert (= (assign a1_1) r0)) +(assert (= (assign a2_1) r2)) +(assert (= (assign c_3) r1)) +(assert (= (assign c_4) r1)) +(assert (= (assign b_3) r0)) +(check-sat) +(exit)