incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also...

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9136a73c307795aa831ef7d8789e2009223d8905..e9532234867a11827e895db2170d3c78437ca6a0 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -364,6 +364,13 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     case AND:
       nodeLit = handleAnd(node);
       break;
+    case EQUAL:
+      if(node[0].getType().isBoolean() && node[1].getType().isBoolean()) {
+        nodeLit = handleIff(node[0].iffNode(node[1]));
+      } else {
+        nodeLit = convertAtom(node);
+      }
+      break;
     default:
       {
         //TODO make sure this does not contain any boolean substructure

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4fae9425469881d8532b73ef4e045560a0d69a59..bf501ec376c33fca473afeccf37f04711dca0228 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -132,36 +132,40 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
 }
 
 
+Theory* TheoryEngine::theoryOf(TypeNode t) {
+  // FIXME: we don't yet have a Type-to-Theory map.  When we do,
+  // look up the type of the var and return that Theory (?)
+
+  // The following JUST hacks around this lack of a table
+  Kind k = t.getKind();
+  if(k == kind::TYPE_CONSTANT) {
+    switch(TypeConstant tc = t.getConst<TypeConstant>()) {
+    case BOOLEAN_TYPE:
+      return d_theoryOfTable[kind::CONST_BOOLEAN];
+    case INTEGER_TYPE:
+      return d_theoryOfTable[kind::CONST_INTEGER];
+    case REAL_TYPE:
+      return d_theoryOfTable[kind::CONST_RATIONAL];
+    case KIND_TYPE:
+    default:
+      Unhandled(tc);
+    }
+  }
+
+  return d_theoryOfTable[k];
+}
+
+
 Theory* TheoryEngine::theoryOf(TNode n) {
   Kind k = n.getKind();
 
   Assert(k >= 0 && k < kind::LAST_KIND);
 
   if(n.getMetaKind() == kind::metakind::VARIABLE) {
-    // FIXME: we don't yet have a Type-to-Theory map.  When we do,
-    // look up the type of the var and return that Theory (?)
-
-    //The following JUST hacks around this lack of a table
-    TypeNode t = n.getType();
-    Kind k = t.getKind();
-    if(k == kind::TYPE_CONSTANT) {
-      switch(TypeConstant tc = t.getConst<TypeConstant>()) {
-      case BOOLEAN_TYPE:
-        return d_theoryOfTable[kind::CONST_BOOLEAN];
-      case INTEGER_TYPE:
-        return d_theoryOfTable[kind::CONST_INTEGER];
-      case REAL_TYPE:
-        return d_theoryOfTable[kind::CONST_RATIONAL];
-      case KIND_TYPE:
-      default:
-        Unhandled(tc);
-      }
-    }
-
-    return d_theoryOfTable[k];
+    return theoryOf(n.getType());
   } else if(k == kind::EQUAL) {
     // equality is special: use LHS
-    return theoryOf(n[0]);
+    return theoryOf(n[0].getType());
   } else {
     // use our Kind-to-Theory mapping
     return d_theoryOfTable[k];

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bb9131023673cda5daa6aedc2e07aba54339e194..fbe9fba16c6343bc12f2b434964fac73b32254a1 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -246,6 +246,13 @@ public:
     delete d_sharedTermManager;
   }
 
+  /**
+   * Get the theory associated to a given TypeNode.
+   *
+   * @returns the theory owning the type
+   */
+  theory::Theory* theoryOf(TypeNode t);
+
   /**
    * Get the theory associated to a given Node.
    *

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 570fa74a40f539f649c074d5fc0a58675a915360..7f0e7d2db468f4b9188375bd2856182539cf5f4f 100644 (file)
--- 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);