diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 166 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 3 |
2 files changed, 141 insertions, 28 deletions
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<Node> kids; + kids.reserve(n.getNumChildren()); + queue<TNode> 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<Node> kids; @@ -233,6 +273,9 @@ Node SymmetryBreaker::normInternal(TNode n) { queue<TNode> work; work.push(n); Debug("ufsymm:norm") << "UFSYMM processing " << n << endl; + TNode matchingTerm = TNode::null(); + vector<TNode> 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<TNode>::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<Node>& newClauses) { @@ -589,29 +689,41 @@ void SymmetryBreaker::selectTerms(const Permutation& p) { set<Node> 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<Node>::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<Node, Node, NodeHashFunction> 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<Node>& cts); - Node normInternal(TNode phi); + Node normInternal(TNode phi, size_t level); Node norm(TNode n); // === STATISTICS === |