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.

8 files changed, 80 insertions, 15 deletions

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index dde5d26eb..07dd3de5b 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -284,10 +284,11 @@ builtinOp[CVC4::Kind& kind]
   | STAR_TOK     { $kind = CVC4::kind::MULT; }
   | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
+  | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
   // Bit-vectors
   | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
-  | BVAND_TOK    { $kind = CVC4::kind::BITVECTOR_AND;    } 
-  | BVOR_TOK     { $kind = CVC4::kind::BITVECTOR_OR;     }   
+  | BVAND_TOK    { $kind = CVC4::kind::BITVECTOR_AND;    }
+  | BVOR_TOK     { $kind = CVC4::kind::BITVECTOR_OR;     }
   | BVXOR_TOK    { $kind = CVC4::kind::BITVECTOR_XOR;    }
   | BVNOT_TOK    { $kind = CVC4::kind::BITVECTOR_NOT;    }
   | BVNAND_TOK   { $kind = CVC4::kind::BITVECTOR_NAND;   }
@@ -300,7 +301,7 @@ builtinOp[CVC4::Kind& kind]
   | BVNEG_TOK    { $kind = CVC4::kind::BITVECTOR_NEG;    }
   | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV;   }
   | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM;   }
-  | BVSDIV_TOK   { $kind = CVC4::kind::BITVECTOR_SDIV;   } 
+  | BVSDIV_TOK   { $kind = CVC4::kind::BITVECTOR_SDIV;   }
   | BVSREM_TOK   { $kind = CVC4::kind::BITVECTOR_SREM;   }
   | BVSMOD_TOK   { $kind = CVC4::kind::BITVECTOR_SMOD;   }
   | BVSHL_TOK    { $kind = CVC4::kind::BITVECTOR_SHL;    }
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a20d187bd..13ee9183f 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -253,7 +253,7 @@ Node ArithRewriter::rewritePlus(TNode t){
   if(pnfs.size() == 1){
     Node p_1 = *(pnfs.begin());
     if(p_1[0].getConst<Rational>() == d_constants->d_ONE){
-      if(accumulator == 0){  // 0 + (* 1 var) |-> var
+      if(accumulator == d_constants->d_ZERO){  // 0 + (* 1 var) |-> var
         Node var = p_1[1];
         return var;
       }
@@ -386,6 +386,26 @@ Node ArithRewriter::rewriteMult(TNode t){
   }
 }
 
+Node ArithRewriter::rewriteConstantDiv(TNode t){
+  Assert(t.getKind()== kind::DIVISION);
+
+  Node reLeft = rewrite(t[0]);
+  Node reRight = rewrite(t[1]);
+  Assert(reLeft.getKind()== kind::CONST_RATIONAL);
+  Assert(reRight.getKind()== kind::CONST_RATIONAL);
+
+  Rational num = reLeft.getConst<Rational>();
+  Rational den = reRight.getConst<Rational>();
+
+  Assert(den != d_constants->d_ZERO);
+
+  Rational div = num / den;
+
+  Node result = mkRationalNode(div);
+
+  return result;
+}
+
 Node ArithRewriter::rewriteTerm(TNode t){
   if(t.getMetaKind() == kind::metakind::CONSTANT){
     return coerceToRationalNode(t);
@@ -395,6 +415,8 @@ Node ArithRewriter::rewriteTerm(TNode t){
     return rewriteMult(t);
   }else if(t.getKind() == kind::PLUS){
     return rewritePlus(t);
+  }else if(t.getKind() == kind::DIVISION){
+    return rewriteConstantDiv(t);
   }else{
     Unreachable();
     return Node::null();
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index a2a8b1b4b..5d94d20a9 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -82,6 +82,9 @@ private:
 
   Node multPnfByNonZero(TNode pnf, Rational& q);
 
+  Node rewriteConstantDiv(TNode t);
+
+
 public:
   ArithRewriter(ArithConstants* ac) :
     d_constants(ac)
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index fafa33a68..99f7258da 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -10,6 +10,7 @@ operator PLUS 2: "arithmetic addition"
 operator MULT 2: "arithmetic multiplication"
 operator MINUS 2 "arithmetic binary subtraction operator"
 operator UMINUS 1 "arithmetic unary negation"
+operator DIVISION 2 "arithmetic division"
 
 constant CONST_RATIONAL \
     ::CVC4::Rational \
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index e3347df64..4ac03c904 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -12,12 +12,14 @@ using namespace CVC4::theory::arith::partial_model;
 void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
+  Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
+
   d_UpperBoundMap[x] = r;
 }
 
 void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
+  Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
   d_LowerBoundMap[x] = r;
 }
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 390cb60aa..66883161e 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -31,15 +31,20 @@ using namespace CVC4::theory::arith;
 
 TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   Theory(c, out),
+  d_preprocessed(c),
   d_constants(NodeManager::currentNM()),
   d_partialModel(c),
   d_diseq(c),
-  d_preprocessed(c),
   d_rewriter(&d_constants)
 {
   uint64_t ass_id = partial_model::Assignment::getId();
-  Debug("arithsetup") << "Assignment: " << ass_id
-                      << std::endl;
+  Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
+}
+TheoryArith::~TheoryArith(){
+  for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
+    Node var = *i;
+    Debug("arithgc") << var << endl;
+  }
 }
 
 
@@ -87,13 +92,14 @@ Node TheoryArith::rewrite(TNode n){
   return result;
 }
 
+
 void TheoryArith::registerTerm(TNode tn){
   Debug("arith") << "registerTerm(" << tn << ")" << endl;
 
   if(tn.getKind() == kind::BUILTIN) return;
 
   if(tn.getMetaKind() == metakind::VARIABLE){
-    d_partialModel.setAssignment(tn,d_constants.d_ZERO_DELTA);
+    setupVariable(tn);
   }
 
   //TODO is an atom
@@ -115,7 +121,9 @@ void TheoryArith::registerTerm(TNode tn){
           //TODO
           TypeNode real_type = NodeManager::currentNM()->realType();
           slack = NodeManager::currentNM()->mkVar(real_type);
-          d_partialModel.setAssignment(slack,d_constants.d_ZERO_DELTA);
+
+          setupVariable(slack);
+
           left.setAttribute(Slack(), slack);
           makeBasic(slack);
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ecdebd720..7bfa535a8 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -28,26 +28,40 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
 
+#include <vector>
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
 class TheoryArith : public Theory {
 private:
-  ArithConstants d_constants;
-  ArithPartialModel d_partialModel;
+  /* Chopping block begins */
 
-  context::CDList<Node> d_diseq;
   context::CDList<Node> d_preprocessed;
   //TODO This is currently needed to save preprocessed nodes that may not
   //currently have an outisde reference. Get rid of when preprocessing is occuring
   //correctly.
 
+  std::vector<Node> d_variables;
+  //TODO get rid of this.  Currently forces every variable and skolem constant that
+  // can hit the tableau to stay alive forever!
+  //This needs to come before d_partialModel and d_tableau in the file
+
+
+  /* Chopping block ends */
+  ArithConstants d_constants;
+  ArithPartialModel d_partialModel;
+
+  context::CDList<Node> d_diseq;
   Tableau d_tableau;
   ArithRewriter d_rewriter;
 
+
+
 public:
   TheoryArith(context::Context* c, OutputChannel& out);
+  ~TheoryArith();
 
   Node rewrite(TNode n);
 
@@ -74,6 +88,13 @@ private:
 
   //TODO get rid of this!
   Node simulatePreprocessing(TNode n);
+  void setupVariable(TNode x){
+    Assert(x.getMetaKind() == kind::metakind::VARIABLE);
+    d_partialModel.setAssignment(x,d_constants.d_ZERO_DELTA);
+    d_variables.push_back(Node(x));
+
+    Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
+  };
 
 };
 
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);
       }