diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
commit | 25e9c72dd689d3b621b901220794c652a3ba589a (patch) | |
tree | 58b14dd3818f3e7a8ca3311a0457716e7753a95e /src/theory/uf | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 14 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 3 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 616 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 160 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 20 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 9 |
7 files changed, 823 insertions, 3 deletions
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 8527924da..fc0f32927 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -15,7 +15,9 @@ libuf_la_SOURCES = \ theory_uf_type_rules.h \ theory_uf_rewriter.h \ equality_engine.h \ - equality_engine_impl.h + equality_engine_impl.h \ + symmetry_breaker.h \ + symmetry_breaker.cpp libuf_la_LIBADD = \ @builddir@/tim/libuftim.la \ diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index e15467bff..01bab53ac 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -20,6 +20,7 @@ #include "theory/valuation.h" #include "expr/kind.h" #include "util/congruence_closure.h" +#include "theory/uf/symmetry_breaker.h" #include <map> @@ -559,6 +560,15 @@ void TheoryUFMorgan::presolve() { TimerStat::CodeTimer codeTimer(d_presolveTimer); Debug("uf") << "uf: begin presolve()" << endl; + if(Options::current()->ufSymmetryBreaker) { + vector<Node> newClauses; + d_symb.apply(newClauses); + for(vector<Node>::const_iterator i = newClauses.begin(); + i != newClauses.end(); + ++i) { + d_out->lemma(*i); + } + } Debug("uf") << "uf: end presolve()" << endl; } @@ -699,6 +709,10 @@ void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) { } } } + + if(Options::current()->ufSymmetryBreaker) { + d_symb.assertFormula(n); + } } /* diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index c2feef349..e801f383e 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -31,6 +31,7 @@ #include "theory/theory.h" #include "theory/uf/theory_uf.h" #include "theory/uf/morgan/union_find.h" +#include "theory/uf/symmetry_breaker.h" #include "context/context.h" #include "context/context_mm.h" @@ -66,6 +67,8 @@ private: */ context::CDList<Node> d_assertions; + SymmetryBreaker d_symb; + /** * Our channel connected to the congruence closure module. */ diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp new file mode 100644 index 000000000..1c2e8cd0d --- /dev/null +++ b/src/theory/uf/symmetry_breaker.cpp @@ -0,0 +1,616 @@ +/********************* */ +/*! \file symmetry_breaker.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of algorithm suggested by Deharbe, Fontaine, + ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011 + ** + ** Implementation of algorithm suggested by Deharbe, Fontaine, Merz, + ** and Paleo, "Exploiting symmetry in SMT problems," CADE 2011. + ** + ** From the paper: + ** + ** <pre> + ** P := guess_permutations(phi) + ** foreach {c_0, ..., c_n} \in P do + ** if invariant_by_permutations(phi, {c_0, ..., c_n}) then + ** T := select_terms(phi, {c_0, ..., c_n}) + ** cts := \empty + ** while T != \empty && |cts| <= n do + ** t := select_most_promising_term(T, phi) + ** T := T \ {t} + ** cts := cts \cup used_in(t, {c_0, ..., c_n}) + ** let c \in {c_0, ..., c_n} \ cts + ** cts := cts \cup {c} + ** if cts != {c_0, ..., c_n} then + ** phi := phi /\ ( \vee_{c_i \in cts} t = c_i ) + ** end + ** end + ** end + ** end + ** return phi + ** </pre> + **/ + +#include "theory/uf/symmetry_breaker.h" +#include "theory/rewriter.h" +#include "util/hash.h" + +#include <iterator> +#include <queue> + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace uf { + +SymmetryBreaker::Template::Template() : + d_template(), + d_sets(), + d_reps() { +} + +TNode SymmetryBreaker::Template::find(TNode n) { + hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); + if(i == d_reps.end()) { + return n; + } else { + return d_reps[n] = find((*i).second); + } +} + +bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) { + IndentedScope scope(Debug("ufsymm:match")); + + Debug("ufsymm:match") << "UFSYMM matching " << t << endl + << "UFSYMM to " << n << endl; + + if(t.getKind() != n.getKind() || t.getNumChildren() != n.getNumChildren()) { + Debug("ufsymm:match") << "UFSYMM BAD MATCH on kind, #children" << endl; + return false; + } + + if(t.getNumChildren() == 0) { + if(t.getMetaKind() == kind::metakind::CONSTANT) { + Assert(n.getMetaKind() == kind::metakind::CONSTANT); + Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl; + return false; + } + Assert(t.getMetaKind() == kind::metakind::VARIABLE && + n.getMetaKind() == kind::metakind::VARIABLE); + t = find(t); + n = find(n); + Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl; + Debug("ufsymm:match") << "UFSYMM sets: " << t << " =>"; + if(d_sets.find(t) != d_sets.end()) { + for(set<TNode>::iterator i = d_sets[t].begin(); i != d_sets[t].end(); ++i) { + Debug("ufsymm:match") << " " << *i; + } + } + Debug("ufsymm:match") << endl; + if(t != n) { + Debug("ufsymm:match") << "UFSYMM sets: " << n << " =>"; + if(d_sets.find(n) != d_sets.end()) { + for(set<TNode>::iterator i = d_sets[n].begin(); i != d_sets[n].end(); ++i) { + Debug("ufsymm:match") << " " << *i; + } + } + Debug("ufsymm:match") << endl; + + if(d_sets.find(t) == d_sets.end()) { + Debug("ufsymm:match") << "UFSYMM inserting " << t << " in with " << n << endl; + d_reps[t] = n; + d_sets[n].insert(t); + } else { + if(d_sets.find(n) != d_sets.end()) { + Debug("ufsymm:match") << "UFSYMM merging " << n << " and " << t << " in with " << n << endl; + d_sets[n].insert(d_sets[t].begin(), d_sets[t].end()); + d_sets[n].insert(t); + d_reps[t] = n; + d_sets.erase(t); + } else { + Debug("ufsymm:match") << "UFSYMM inserting " << n << " in with " << t << endl; + d_sets[t].insert(n); + d_reps[n] = t; + } + } + } + return true; + } + + if(t.getMetaKind() == kind::metakind::PARAMETERIZED) { + if(t.getOperator() != n.getOperator()) { + Debug("ufsymm:match") << "UFSYMM BAD MATCH on operators: " << t.getOperator() << " != " << n.getOperator() << endl; + return false; + } + } + TNode::iterator ti = t.begin(); + TNode::iterator ni = n.begin(); + while(ti != t.end()) { + if(*ti != *ni) { // nothing to do if equal + if(!matchRecursive(*ti, *ni)) { + Debug("ufsymm:match") << "UFSYMM BAD MATCH, withdrawing.." << endl; + return false; + } + } + ++ti; + ++ni; + } + + return true; +} + +bool SymmetryBreaker::Template::match(TNode n) { + // try to "match" n and d_template + if(d_template.isNull()) { + Debug("ufsymm") << "UFSYMM setting template " << n << endl; + d_template = n; + return true; + } else { + return matchRecursive(d_template, n); + } +} + +void SymmetryBreaker::Template::reset() { + d_template = Node::null(); + d_sets.clear(); + d_reps.clear(); +} + +SymmetryBreaker::SymmetryBreaker() : + d_phi(), + d_phiSet(), + d_permutations(), + d_terms(), + d_template(), + d_normalizationCache(), + d_termEqs() { +} + +Node SymmetryBreaker::norm(TNode phi) { + Node n = Rewriter::rewrite(phi); + return normInternal(n); +} + +Node SymmetryBreaker::normInternal(TNode n) { + Node& result = d_normalizationCache[n]; + if(!result.isNull()) { + return result; + } + + switch(Kind k = n.getKind()) { + + case kind::DISTINCT: { + // commutative N-ary operator handling + vector<TNode> kids(n.begin(), n.end()); + sort(kids.begin(), kids.end()); + return result = NodeManager::currentNM()->mkNode(k, kids); + } + + case kind::AND: + case kind::OR: { + // 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::AND || + (*i).getKind() == kind::OR ) { + kids.push_back(normInternal(*i)); + } else if((*i).getKind() == kind::IFF || + (*i).getKind() == kind::EQUAL) { + kids.push_back(normInternal(*i)); + if((*i)[0].getMetaKind() == kind::metakind::VARIABLE || + (*i)[1].getMetaKind() == kind::metakind::VARIABLE) { + d_termEqs[(*i)[0]].insert((*i)[1]); + d_termEqs[(*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::IFF: + case kind::EQUAL: + if(n[0].getMetaKind() == kind::metakind::VARIABLE || + n[1].getMetaKind() == kind::metakind::VARIABLE) { + d_termEqs[n[0]].insert(n[1]); + d_termEqs[n[1]].insert(n[0]); + Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; + } + /* intentional fall-through! */ + case kind::XOR: + // commutative binary operator handling + return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n); + + default: + // Normally T-rewriting is enough; only special cases (like + // Boolean-layer stuff) has to go above. + return n; + } +} + +void SymmetryBreaker::assertFormula(TNode phi) { + // use d_phi, put into d_permutations + Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl; + d_phi.push_back(phi); + if(phi.getKind() == kind::OR) { + Template t; + Node::iterator i = phi.begin(); + t.match(*i++); + while(i != phi.end()) { + if(!t.match(*i++)) { + break; + } + } + hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); + for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + i != ps.end(); + ++i) { + Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; + set<TNode>& p = (*i).second; + for(set<TNode>::iterator j = p.begin(); + j != p.end(); + ++j) { + Debug("ufsymm") << " " << *j; + } + Debug("ufsymm") << endl; + p.insert((*i).first); + Permutations::iterator pi = d_permutations.find(p); + if(pi == d_permutations.end()) { + d_permutations.insert(p); + } + } + } + if(!d_template.match(phi)) { + // we hit a bad match, extract the partitions and reset the template + hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); + Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; + for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + i != ps.end(); + ++i) { + Debug("ufsymm") << "UFSYMM partition: " << (*i).first; + set<TNode>& p = (*i).second; + if(Debug.isOn("ufsymm")) { + for(set<TNode>::iterator j = p.begin(); + j != p.end(); + ++j) { + Debug("ufsymm") << " " << *j; + } + } + Debug("ufsymm") << endl; + p.insert((*i).first); + d_permutations.insert(p); + } + d_template.reset(); + bool good CVC4_UNUSED = d_template.match(phi); + Assert(good); + } +} + +void SymmetryBreaker::clear() { + d_phi.clear(); + d_phiSet.clear(); + d_permutations.clear(); + d_terms.clear(); + d_template.reset(); + d_normalizationCache.clear(); + d_termEqs.clear(); +} + +void SymmetryBreaker::apply(std::vector<Node>& newClauses) { + guessPermutations(); + Debug("ufsymm") << "UFSYMM =====================================================" << endl + << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl; + if(!d_permutations.empty()) { + { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer); + // normalize d_phi + + for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { + Node n = *i; + *i = norm(n); + d_phiSet.insert(*i); + Debug("ufsymm:norm") << "UFSYMM init-norm-rewrite " << n << endl + << "UFSYMM to " << *i << endl; + } + } + + for(Permutations::iterator i = d_permutations.begin(); + i != d_permutations.end(); + ++i) { + ++d_permutationSetsConsidered; + const Permutation& p = *i; + Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; + size_t n = p.size() - 1; + if(invariantByPermutations(p)) { + ++d_permutationSetsInvariant; + selectTerms(p); + set<Node> cts; + while(!d_terms.empty() && cts.size() <= n) { + Debug("ufsymm") << "UFSYMM ==== top of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl; + Terms::iterator ti = selectMostPromisingTerm(d_terms); + Node t = *ti; + Debug("ufsymm") << "UFSYMM promising term is " << t << endl; + d_terms.erase(ti); + insertUsedIn(t, p, cts); + if(Debug.isOn("ufsymm")) { + if(cts.empty()) { + Debug("ufsymm") << "UFSYMM cts is empty" << endl; + } else { + for(set<Node>::iterator ctsi = cts.begin(); ctsi != cts.end(); ++ctsi) { + Debug("ufsymm") << "UFSYMM cts: " << *ctsi << endl; + } + } + } + TNode c; + Debug("ufsymm") << "UFSYMM looking for c \\in " << p << " \\ cts" << endl; + set<TNode>::const_iterator i; + for(i = p.begin(); i != p.end(); ++i) { + if(cts.find(*i) == cts.end()) { + if(c.isNull()) { + c = *i; + Debug("ufsymm") << "UFSYMM found first: " << c << endl; + } else { + Debug("ufsymm") << "UFSYMM found second: " << *i << endl; + break; + } + } + } + if(c.isNull()) { + Debug("ufsymm") << "UFSYMM can't find a c, restart outer loop" << endl; + break; + } + Debug("ufsymm") << "UFSYMM inserting into cts: " << c << endl; + cts.insert(c); + // This tests cts != p: if "i == p.end()", we got all the way + // through p without seeing two elements not in cts (on the + // second one, we break from the above loop). We know we + // found at least one (and subsequently added it to cts). So + // now cts == p. + Debug("ufsymm") << "UFSYMM p == " << p << endl; + if(i != p.end() || p.size() != cts.size()) { + Debug("ufsymm") << "UFSYMM cts != p" << endl; + NodeBuilder<> disj(kind::OR); + for(set<Node>::const_iterator i = cts.begin(); + i != cts.end(); + ++i) { + if(t != *i) { + disj << NodeManager::currentNM()->mkNode(kind::EQUAL, t, *i); + } + } + Node d; + if(disj.getNumChildren() > 1) { + d = disj; + ++d_clauses; + } else { + d = disj[0]; + disj.clear(); + ++d_units; + } + if(Debug.isOn("ufsymm")) { + Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl; + } else { + Debug("ufsymm:clauses") << "UFSYMM symmetry-breaking clause: " << d << endl; + } + newClauses.push_back(d); + } else { + Debug("ufsymm") << "UFSYMM cts == p" << endl; + } + Debug("ufsymm") << "UFSYMM ==== end of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl; + } + } + } + } + + clear(); +} + +void SymmetryBreaker::guessPermutations() { + // use d_phi, put into d_permutations + Debug("ufsymm") << "UFSYMM guessPermutations()" << endl; +} + +bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { + TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer); + + // use d_phi + Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl; + + Assert(p.size() > 1); + + // check P_swap + vector<Node> subs; + vector<Node> repls; + Permutation::iterator i = p.begin(); + TNode p0 = *i++; + TNode p1 = *i; + subs.push_back(p0); + subs.push_back(p1); + repls.push_back(p1); + repls.push_back(p0); + for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { + Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + Node n = norm(s); + if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { + Debug("ufsymm") << "UFSYMM P_swap is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << *i << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" << endl; + return false; + } else if(Debug.isOn("ufsymm:p")) { + if(*i == s) { + Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << *i << endl; + } else { + Debug("ufsymm:p") << "UFSYMM P_swap passes: " << *i << endl + << "UFSYMM rewrites: " << s << endl + << "UFSYMM norms: " << n << endl; + } + } + } + Debug("ufsymm") << "UFSYMM P_swap is an inv perm op for " << p << endl; + + // check P_circ, unless size == 2 in which case P_circ == P_swap + if(p.size() > 2) { + subs.clear(); + repls.clear(); + bool first = true; + for(Permutation::const_iterator i = p.begin(); i != p.end(); ++i) { + subs.push_back(*i); + if(!first) { + repls.push_back(*i); + } else { + first = false; + } + } + repls.push_back(*p.begin()); + Assert(subs.size() == repls.size()); + for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { + Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + Node n = norm(s); + if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { + Debug("ufsymm") << "UFSYMM P_circ is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << *i << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" << endl; + return false; + } else if(Debug.isOn("ufsymm:p")) { + if(*i == s) { + Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << *i << endl; + } else { + Debug("ufsymm:p") << "UFSYMM P_circ passes: " << *i << endl + << "UFSYMM rewrites: " << s << endl + << "UFSYMM norms: " << n << endl; + } + } + } + Debug("ufsymm") << "UFSYMM P_circ is an inv perm op for " << p << endl; + } else { + Debug("ufsymm") << "UFSYMM no need to check P_circ, since P_circ == P_swap for perm sets of size 2" << endl; + } + + return true; +} + +// debug-assertion-only function +template <class T1, class T2> +static bool isSubset(const T1& s, const T2& t) { + if(s.size() > t.size()) { + //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t " + // << "because size(s) > size(t)" << endl; + return false; + } + for(typename T1::const_iterator si = s.begin(); si != s.end(); ++si) { + if(t.find(*si) == t.end()) { + //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t " + // << "because s element \"" << *si << "\" not in t" << endl; + return false; + } + } + + // At this point, didn't find any elements from s not in t, so + // conclude that s \subseteq t + return true; +} + +void SymmetryBreaker::selectTerms(const Permutation& p) { + TimerStat::CodeTimer codeTimer(d_selectTermsTimer); + + // use d_phi, put into d_terms + Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl; + d_terms.clear(); + set<Node> terms; + for(Permutation::iterator i = p.begin(); i != p.end(); ++i) { + const TermEq& teq = d_termEqs[*i]; + 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; + } + } + Assert(j != teq.end(), "failed to find a difference between p and teq ?!"); + } + } + } + if(Debug.isOn("ufsymm")) { + for(list<Term>::iterator i = d_terms.begin(); i != d_terms.end(); ++i) { + Debug("ufsymm") << "UFSYMM selectTerms() returning: " << *i << endl; + } + } +} + +SymmetryBreaker::Terms::iterator +SymmetryBreaker::selectMostPromisingTerm(Terms& terms) { + // use d_phi + Debug("ufsymm") << "UFSYMM selectMostPromisingTerm()" << endl; + return terms.begin(); +} + +void SymmetryBreaker::insertUsedIn(Term term, const Permutation& p, set<Node>& cts) { + // insert terms from p used in term into cts + //Debug("ufsymm") << "UFSYMM usedIn(): " << term << " , " << p << endl; + if(find(p.begin(), p.end(), term) != p.end()) { + cts.insert(term); + } else { + for(TNode::iterator i = term.begin(); i != term.end(); ++i) { + insertUsedIn(*i, p, cts); + } + } +} + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, const theory::uf::SymmetryBreaker::Permutation& p) { + out << "{"; + set<TNode>::const_iterator i = p.begin(); + while(i != p.end()) { + out << *i; + if(++i != p.end()) { + out << ","; + } + } + out << "}"; + return out; +} + +}/* CVC4 namespace */ diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h new file mode 100644 index 000000000..1b2680cf3 --- /dev/null +++ b/src/theory/uf/symmetry_breaker.h @@ -0,0 +1,160 @@ +/********************* */ +/*! \file symmetry_breaker.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of algorithm suggested by Deharbe, Fontaine, + ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011 + ** + ** Implementation of algorithm suggested by Deharbe, Fontaine, + ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011. + ** + ** From the paper: + ** + ** <pre> + ** P := guess_permutations(phi) + ** foreach {c_0, ..., c_n} \in P do + ** if invariant_by_permutations(phi, {c_0, ..., c_n}) then + ** T := select_terms(phi, {c_0, ..., c_n}) + ** cts := \empty + ** while T != \empty && |cts| <= n do + ** t := select_most_promising_term(T, phi) + ** T := T \ {t} + ** cts := cts \cup used_in(t, {c_0, ..., c_n}) + ** let c \in {c_0, ..., c_n} \ cts + ** cts := cts \cup {c} + ** if cts != {c_0, ..., c_n} then + ** phi := phi /\ ( \vee_{c_i \in cts} t = c_i ) + ** end + ** end + ** end + ** end + ** return phi + ** </pre> + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__SYMMETRY_BREAKER_H +#define __CVC4__THEORY__UF__SYMMETRY_BREAKER_H + +#include <iostream> +#include <list> +#include <vector> + +#include "expr/node.h" +#include "expr/node_builder.h" +#include "util/stats.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class SymmetryBreaker { + + class Template { + Node d_template; + NodeBuilder<> d_assertions; + std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; + std::hash_map<TNode, TNode, TNodeHashFunction> d_reps; + + TNode find(TNode n); + bool matchRecursive(TNode t, TNode n); + + public: + Template(); + bool match(TNode n); + std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } + Node assertions() { + switch(d_assertions.getNumChildren()) { + case 0: return Node::null(); + case 1: return d_assertions[0]; + default: return Node(d_assertions); + } + } + void reset(); + };/* class SymmetryBreaker::Template */ + +public: + + typedef std::set<TNode> Permutation; + typedef std::set<Permutation> Permutations; + typedef TNode Term; + typedef std::list<Term> Terms; + typedef std::set<Term> TermEq; + typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs; + +private: + + std::vector<Node> d_phi; + std::set<TNode> d_phiSet; + Permutations d_permutations; + Terms d_terms; + Template d_template; + std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache; + TermEqs d_termEqs; + + void clear(); + + void guessPermutations(); + bool invariantByPermutations(const Permutation& p); + 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 norm(TNode n); + + // === STATISTICS === + /** number of new clauses that come from the SymmetryBreaker */ + KEEP_STATISTIC(IntStat, + d_clauses, + "theory::uf::symmetry_breaker::clauses", 0); + /** number of new clauses that come from the SymmetryBreaker */ + KEEP_STATISTIC(IntStat, + d_units, + "theory::uf::symmetry_breaker::units", 0); + /** number of potential permutation sets we found */ + KEEP_STATISTIC(IntStat, + d_permutationSetsConsidered, + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0); + /** number of invariant permutation sets we found */ + KEEP_STATISTIC(IntStat, + d_permutationSetsInvariant, + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0); + /** time spent in invariantByPermutations() */ + KEEP_STATISTIC(TimerStat, + d_invariantByPermutationsTimer, + "theory::uf::symmetry_breaker::timers::invariantByPermutations"); + /** time spent in selectTerms() */ + KEEP_STATISTIC(TimerStat, + d_selectTermsTimer, + "theory::uf::symmetry_breaker::timers::selectTerms"); + /** time spent in initial round of normalization */ + KEEP_STATISTIC(TimerStat, + d_initNormalizationTimer, + "theory::uf::symmetry_breaker::timers::initNormalization"); + +public: + + SymmetryBreaker(); + void assertFormula(TNode phi); + void apply(std::vector<Node>& newClauses); + +};/* class SymmetryBreaker */ + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBreaker::Permutation& p); + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__SYMMETRY_BREAKER_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9903acc57..0776ecf0d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -227,6 +227,22 @@ void TheoryUF::explain(TNode literal) { d_out->explanation(mkAnd(assumptions)); } +void TheoryUF::presolve() { + // TimerStat::CodeTimer codeTimer(d_presolveTimer); + + Debug("uf") << "uf: begin presolve()" << endl; + if(Options::current()->ufSymmetryBreaker) { + vector<Node> newClauses; + d_symb.apply(newClauses); + for(vector<Node>::const_iterator i = newClauses.begin(); + i != newClauses.end(); + ++i) { + d_out->lemma(*i); + } + } + Debug("uf") << "uf: end presolve()" << endl; +} + void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) { //TimerStat::CodeTimer codeTimer(d_staticLearningTimer); @@ -334,4 +350,8 @@ void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) { } } } + + if(Options::current()->ufSymmetryBreaker) { + d_symb.assertFormula(n); + } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index eaab96f27..d78504dc8 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -27,6 +27,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/symmetry_breaker.h" #include "context/cdo.h" #include "context/cdset.h" @@ -87,6 +88,9 @@ private: /** True node for predicates = false */ Node d_false; + /** Symmetry analyzer */ + SymmetryBreaker d_symb; + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ @@ -113,12 +117,13 @@ public: void preRegisterTerm(TNode term); void explain(TNode n); + void staticLearning(TNode in, NodeBuilder<>& learned); + void presolve(); + std::string identify() const { return "THEORY_UF"; } - void staticLearning(TNode in, NodeBuilder<>& learned); - };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |