Added the division symbol to the parser, and minimal support for it in TheoryArith...

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index dde5d26eb111b41944e363e93bd3e38f1819a55f..07dd3de5b8b849045a2df36fdf7fedcb63911f5d 100644 (file)
--- 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 a20d187bd144ebefeed4cd15ecb953d21b08a0fa..13ee9183f34ec7cb582ed1dd1ff554b3bd207220 100644 (file)
--- 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 a2a8b1b4b32f9e74c0c65c1ab0236ea3606d9d7d..5d94d20a9e5065cdf52c71649a456ac52add05be 100644 (file)
--- 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 fafa33a682a468992c151e588c3e550df3c545c1..99f7258da07d8194b1cd510c252f4ebc8717e0fb 100644 (file)
--- 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 e3347df642cdfd96a8f53c3f3d8ea155b3c0f682..4ac03c9040c2cdfb5c6d099b66166686b883a95f 100644 (file)
--- 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 390cb60aaac0a604785e14fd7f2afaea43a4f4fb..66883161ebad61bd579506079cadd2706253336b 100644 (file)
--- 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 ecdebd720a728ab1f1663b1c298ccff7de4097f7..7bfa535a84121c8b8ce152a6ee18e6944b956fd7 100644 (file)
--- 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 b559da56269668c9a0bcb37c8008796fa2d6ce95..c8b93e8b4ccb7d0fd83e44a4b9d8317f403a6625 100644 (file)
--- 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);
       }

diff --git a/test/regress/regress0/ite.smt2 b/test/regress/regress0/ite.smt2
index 0e171666f6d786636cfc10f06e839d41c7611a3d..99f170ff426c16014e53418cb474ddccb309c45a 100644 (file)
--- a/test/regress/regress0/ite.smt2
+++ b/test/regress/regress0/ite.smt2
@@ -1,6 +1,7 @@
-(set-logic QF_LRA)
+(set-logic QF_UF)
 (set-info :status unsat)
-(declare-fun x () Real)
-(declare-fun y () Real)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
 (assert (not (= x (ite true x y))))
 (check-sat)