Added the division symbol to the parser, and minimal support for it in TheoryArith. Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.

1 files changed, 9 insertions, 2 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index b559da562..c8b93e8b4 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -221,8 +221,15 @@ public:
       if(lhs.getKind() == kind::VARIABLE) {
         // FIXME: we don't yet have a Type-to-Theory map.  When we do,
         // look up the type of the LHS and return that Theory (?)
-        return &d_uf;
-        //Unimplemented();
+
+        //The following JUST hacks around this lack of a table
+        TypeNode type_of_n = lhs.getType();
+        if(type_of_n.isReal()){
+          return &d_arith;
+        }else{
+          return &d_uf;
+          //Unimplemented();
+        }
       } else {
         return theoryOf(lhs);
       }