Some fixes to symmetry breaker (resolves bug 576).

5 files changed, 219 insertions, 29 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 ===
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index cc691f8d2..55a588362 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -160,7 +160,9 @@ BUG_TESTS = \
 	bug543.smt2 \
 	bug544.smt2 \
 	bug548a.smt2 \
-	bug567.smt2
+	bug567.smt2 \
+	bug576.smt2 \
+	bug576a.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug576.smt2 b/test/regress/regress0/bug576.smt2
new file mode 100644
index 000000000..c9ca241d7
--- /dev/null
+++ b/test/regress/regress0/bug576.smt2
@@ -0,0 +1,27 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-sort var 0)
+(declare-sort reg 0)
+(declare-fun var5_1 () var)
+(declare-fun b_1 () var)
+(declare-fun a_1 () var)
+(declare-fun r0 () reg)
+(declare-fun r1 () reg)
+(declare-fun r2 () reg)
+(declare-fun r3 () reg)
+(assert (not (= r0 r1)))
+(assert (not (= r0 r2)))
+(assert (not (= r0 r3)))
+(assert (not (= r1 r2)))
+(assert (not (= r1 r3)))
+(assert (not (= r2 r3)))
+(declare-fun assign (var) reg)
+(assert (or (= (assign var5_1) r0) (= (assign var5_1) r1) (= (assign var5_1) r2) (= (assign var5_1) r3) ))
+(assert (or (= (assign b_1) r1) ))
+(assert (or (= (assign a_1) r0) ))
+(assert (not (= (assign b_1) (assign a_1))))
+(assert (= (assign var5_1) r0))
+(assert (= (assign b_1) r1))
+(assert (= (assign a_1) r0))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bug576a.smt2 b/test/regress/regress0/bug576a.smt2
new file mode 100644
index 000000000..00487a183
--- /dev/null
+++ b/test/regress/regress0/bug576a.smt2
@@ -0,0 +1,48 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-sort var 0)
+(declare-sort reg 0)
+(declare-fun a1_1 () var)
+(declare-fun a2_1 () var)
+(declare-fun c_3 () var)
+(declare-fun c_4 () var)
+(declare-fun b_3 () var)
+(declare-fun r0 () reg)
+(declare-fun r1 () reg)
+(declare-fun r2 () reg)
+(declare-fun r3 () reg)
+(declare-fun r4 () reg)
+(declare-fun r6 () reg)
+(assert (not (= r0 r1)))
+(assert (not (= r0 r2)))
+(assert (not (= r0 r3)))
+(assert (not (= r0 r4)))
+(assert (not (= r0 r6)))
+(assert (not (= r1 r2)))
+(assert (not (= r1 r3)))
+(assert (not (= r1 r4)))
+(assert (not (= r1 r6)))
+(assert (not (= r2 r3)))
+(assert (not (= r2 r4)))
+(assert (not (= r2 r6)))
+(assert (not (= r3 r4)))
+(assert (not (= r3 r6)))
+(assert (not (= r4 r6)))
+(declare-fun assign (var) reg)
+(assert (or (= (assign a1_1) r0) (= (assign a1_1) r1) (= (assign a1_1) r2) (= (assign a1_1) r3) (= (assign a1_1) r4) (= (assign a1_1) r6) ))
+(assert (or (= (assign a2_1) r0) (= (assign a2_1) r1) (= (assign a2_1) r2) (= (assign a2_1) r3) (= (assign a2_1) r4) (= (assign a2_1) r6) ))
+(assert (or (= (assign c_3) r0) (= (assign c_3) r1) (= (assign c_3) r2) (= (assign c_3) r3) (= (assign c_3) r4) (= (assign c_3) r6) ))
+(assert (or (= (assign c_4) r0) (= (assign c_4) r1) (= (assign c_4) r2) (= (assign c_4) r3) (= (assign c_4) r4) (= (assign c_4) r6) ))
+(assert (or (= (assign b_3) r0) (= (assign b_3) r1) (= (assign b_3) r2) (= (assign b_3) r3) (= (assign b_3) r4) (= (assign b_3) r6) ))
+(assert (not (= (assign a1_1) (assign c_4))))
+(assert (not (= (assign a2_1) (assign c_3))))
+(assert (not (= (assign a2_1) (assign b_3))))
+(assert (not (= (assign c_3) (assign b_3))))
+(assert (not (= (assign c_4) (assign b_3))))
+(assert (= (assign a1_1) r0))
+(assert (= (assign a2_1) r2))
+(assert (= (assign c_3) r1))
+(assert (= (assign c_4) r1))
+(assert (= (assign b_3) r0))
+(check-sat)
+(exit)