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.

2 files changed, 33 insertions, 22 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4fae94254..bf501ec37 100644
--- 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 bb9131023..fbe9fba16 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -247,6 +247,13 @@ public:
   }
 
   /**
+   * 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.
    *
    * @returns the theory, or NULL if the TNode is