merge from symmetry branch

1 files changed, 20 insertions, 0 deletions

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);
+  }
 }