Fix incremental bug in symmetry breaker.

Thanks to Christoph Sticksel for reporting this.

1 files changed, 36 insertions, 1 deletions

diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index fcb6c3cd5..f5d7f9235 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -52,6 +52,8 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
+using namespace ::CVC4::context;
+
 SymmetryBreaker::Template::Template() :
   d_template(),
   d_sets(),
@@ -165,7 +167,10 @@ void SymmetryBreaker::Template::reset() {
   d_reps.clear();
 }
 
-SymmetryBreaker::SymmetryBreaker() :
+SymmetryBreaker::SymmetryBreaker(context::Context* context) :
+  ContextNotifyObj(context),
+  d_assertionsToRerun(context),
+  d_rerunningAssertions(false),
   d_phi(),
   d_phiSet(),
   d_permutations(),
@@ -175,6 +180,31 @@ SymmetryBreaker::SymmetryBreaker() :
   d_termEqs() {
 }
 
+class SBGuard {
+  bool& d_ref;
+  bool d_old;
+public:
+  SBGuard(bool& b) : d_ref(b), d_old(b) {}
+  ~SBGuard() { Debug("uf") << "reset to " << d_old << std::endl; d_ref = d_old; }
+};/* class SBGuard */
+
+void SymmetryBreaker::rerunAssertionsIfNecessary() {
+  if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) {
+    return;
+  }
+
+  SBGuard g(d_rerunningAssertions);
+  d_rerunningAssertions = true;
+
+  Debug("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl;
+  for(CDList<Node>::const_iterator i = d_assertionsToRerun.begin();
+      i != d_assertionsToRerun.end();
+      ++i) {
+    assertFormula(*i);
+  }
+  Debug("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl;
+}
+
 Node SymmetryBreaker::norm(TNode phi) {
   Node n = Rewriter::rewrite(phi);
   return normInternal(n);
@@ -254,6 +284,10 @@ Node SymmetryBreaker::normInternal(TNode n) {
 }
 
 void SymmetryBreaker::assertFormula(TNode phi) {
+  rerunAssertionsIfNecessary();
+  if(!d_rerunningAssertions) {
+    d_assertionsToRerun.push_back(phi);
+  }
   // use d_phi, put into d_permutations
   Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
   d_phi.push_back(phi);
@@ -322,6 +356,7 @@ void SymmetryBreaker::clear() {
 }
 
 void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
+  rerunAssertionsIfNecessary();
   guessPermutations();
   Debug("ufsymm") << "UFSYMM =====================================================" << endl
                   << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;