incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also make theoryOf(= t1 t2) return theoryOf(t1.getType()), rather than theoryOf(t1), as the latter gives different results for (= (geq x1 x2) (leq x2 x1)) and (= a (leq x2 x1)), which is strange and causes problems. should discuss at tuesday meeting. resolves bug 187.

1 files changed, 21 insertions, 22 deletions

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 570fa74a4..7f0e7d2db 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -96,7 +96,7 @@ public:
 
   RewriteResponse preRewrite(TNode n, bool topLevel) {
     if(s_expected.empty()) {
-      cout << std::endl
+      cout << std::endl << Expr::setdepth(-1)
            << "didn't expect anything more, but got" << std::endl
            << "     PRE  " << topLevel << " " << identify() << " " << n << std::endl;
     }
@@ -109,7 +109,7 @@ public:
        expected.d_theory != this ||
        expected.d_node != n ||
        expected.d_topLevel != topLevel) {
-      cout << std::endl
+      cout << std::endl << Expr::setdepth(-1)
            << "HAVE PRE  " << topLevel << " " << identify() << " " << n << std::endl
            << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
     }
@@ -124,7 +124,7 @@ public:
 
   RewriteResponse postRewrite(TNode n, bool topLevel) {
     if(s_expected.empty()) {
-      cout << std::endl
+      cout << std::endl << Expr::setdepth(-1)
            << "didn't expect anything more, but got" << std::endl
            << "     POST " << topLevel << " " << identify() << " " << n << std::endl;
     }
@@ -137,7 +137,7 @@ public:
        expected.d_theory != this ||
        expected.d_node != n ||
        expected.d_topLevel != topLevel) {
-      cout << std::endl
+      cout << std::endl << Expr::setdepth(-1)
            << "HAVE POST " << topLevel << " " << identify() << " " << n << std::endl
            << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
     }
@@ -208,7 +208,7 @@ public:
     d_theoryEngine->d_theoryOfTable.
       registerTheory(reinterpret_cast<theory::bv::TheoryBV*>(d_bv));
 
-    Debug.on("theory-rewrite");
+    //Debug.on("theory-rewrite");
   }
 
   void tearDown() {
@@ -294,56 +294,55 @@ public:
     // We WOULD expect that the commented-out calls were made, except
     // for the cache
     FakeTheory::expect(PRE, d_bool, n, true);
-    FakeTheory::expect(PRE, d_uf, f1eqf2, true);
-    FakeTheory::expect(PRE, d_uf, f1, false);
+    FakeTheory::expect(PRE, d_arith, f1eqf2, true);
+    FakeTheory::expect(PRE, d_uf, f1, true);
     FakeTheory::expect(PRE, d_builtin, f, true);
     FakeTheory::expect(POST, d_builtin, f, true);
     FakeTheory::expect(PRE, d_arith, one, true);
     FakeTheory::expect(POST, d_arith, one, true);
-    FakeTheory::expect(POST, d_uf, f1, false);
-    FakeTheory::expect(PRE, d_uf, f2, false);
+    FakeTheory::expect(POST, d_uf, f1, true);
+    FakeTheory::expect(PRE, d_uf, f2, true);
     //FakeTheory::expect(PRE, d_builtin, f, true);
     //FakeTheory::expect(POST, d_builtin, f, true);
     FakeTheory::expect(PRE, d_arith, two, true);
     FakeTheory::expect(POST, d_arith, two, true);
-    FakeTheory::expect(POST, d_uf, f2, false);
-    FakeTheory::expect(POST, d_uf, f1eqf2, true);
+    FakeTheory::expect(POST, d_uf, f2, true);
+    FakeTheory::expect(POST, d_arith, f1eqf2, true);
     FakeTheory::expect(PRE, d_bool, or1, false);
     FakeTheory::expect(PRE, d_bool, and1, false);
-    FakeTheory::expect(PRE, d_uf, ffxeqgy, true);
-    FakeTheory::expect(PRE, d_uf, ffx, false);
+    FakeTheory::expect(PRE, d_arith, ffxeqgy, true);
+    FakeTheory::expect(PRE, d_uf, ffx, true);
     FakeTheory::expect(PRE, d_uf, fx, false);
     //FakeTheory::expect(PRE, d_builtin, f, true);
     //FakeTheory::expect(POST, d_builtin, f, true);
     FakeTheory::expect(PRE, d_arith, x, true);
     FakeTheory::expect(POST, d_arith, x, true);
     FakeTheory::expect(POST, d_uf, fx, false);
-    FakeTheory::expect(POST, d_uf, ffx, false);
-    FakeTheory::expect(PRE, d_uf, gy, false);
+    FakeTheory::expect(POST, d_uf, ffx, true);
+    FakeTheory::expect(PRE, d_uf, gy, true);
     FakeTheory::expect(PRE, d_builtin, g, true);
     FakeTheory::expect(POST, d_builtin, g, true);
     FakeTheory::expect(PRE, d_arith, y, true);
     FakeTheory::expect(POST, d_arith, y, true);
-    FakeTheory::expect(POST, d_uf, gy, false);
-    FakeTheory::expect(POST, d_uf, ffxeqgy, true);
+    FakeTheory::expect(POST, d_uf, gy, true);
+    FakeTheory::expect(POST, d_arith, ffxeqgy, true);
     FakeTheory::expect(PRE, d_uf, z1eqz2, true);
     FakeTheory::expect(PRE, d_uf, z1, false);
     FakeTheory::expect(POST, d_uf, z1, false);
     FakeTheory::expect(PRE, d_uf, z2, false);
     FakeTheory::expect(POST, d_uf, z2, false);
     FakeTheory::expect(POST, d_uf, z1eqz2, true);
-    // tricky one: ffx is in cache but for a non-topLevel !
-    FakeTheory::expect(PRE, d_uf, ffx, true);
+    //FakeTheory::expect(PRE, d_uf, ffx, true);
     //FakeTheory::expect(PRE, d_uf, fx, false);
     //FakeTheory::expect(POST, d_uf, fx, false);
-    FakeTheory::expect(POST, d_uf, ffx, true);
+    //FakeTheory::expect(POST, d_uf, ffx, true);
     FakeTheory::expect(POST, d_bool, and1, false);
-    FakeTheory::expect(PRE, d_uf, ffxeqf1, true);
+    FakeTheory::expect(PRE, d_arith, ffxeqf1, true);
     //FakeTheory::expect(PRE, d_uf, ffx, false);
     //FakeTheory::expect(POST, d_uf, ffx, false);
     //FakeTheory::expect(PRE, d_uf, f1, false);
     //FakeTheory::expect(POST, d_uf, f1, false);
-    FakeTheory::expect(POST, d_uf, ffxeqf1, true);
+    FakeTheory::expect(POST, d_arith, ffxeqf1, true);
     FakeTheory::expect(POST, d_bool, or1, false);
     FakeTheory::expect(POST, d_bool, n, true);
     nOut = d_theoryEngine->rewrite(n);