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, 7 insertions, 0 deletions

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