summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/theory_engine.cpp8
-rw-r--r--src/theory/uf/Makefile.am4
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.cpp14
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.h3
-rw-r--r--src/theory/uf/symmetry_breaker.cpp616
-rw-r--r--src/theory/uf/symmetry_breaker.h160
-rw-r--r--src/theory/uf/theory_uf.cpp20
-rw-r--r--src/theory/uf/theory_uf.h9
8 files changed, 830 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index fa885590b..4237e0992 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -286,6 +286,12 @@ Node TheoryEngine::getValue(TNode node) {
}/* TheoryEngine::getValue(TNode node) */
bool TheoryEngine::presolve() {
+ // NOTE that we don't look at d_theoryIsActive[] here. First of
+ // all, we haven't done any pre-registration yet, so we don't know
+ // which theories are active. Second, let's give each theory a shot
+ // at doing something with the input formula, even if it wouldn't
+ // otherwise be active.
+
d_theoryOut.d_conflictNode = Node::null();
d_theoryOut.d_propagatedLiterals.clear();
@@ -295,7 +301,7 @@ bool TheoryEngine::presolve() {
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \
+ if (theory::TheoryTraits<THEORY>::hasPresolve) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \
if(!d_theoryOut.d_conflictNode.get().isNull()) { \
return true; \
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback