8 files changed, 312 insertions, 85 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 27014a3bf..b6275ba24 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -86,25 +86,50 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     return rewriteUMinus(t, true);
   }else if(t.getKind() == kind::DIVISION){
     return RewriteResponse(REWRITE_DONE, t); // wait until t[1] is rewritten
+  }else if(t.getKind() == kind::DIVISION_TOTAL){
+    if(t[1].getKind()== kind::CONST_RATIONAL &&
+       t[1].getConst<Rational>().isZero()){
+      return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+    }else{
+      return RewriteResponse(REWRITE_DONE, t); // wait until t[1] is rewritten
+    }
   }else if(t.getKind() == kind::PLUS){
     return preRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return preRewriteMult(t);
   }else if(t.getKind() == kind::INTS_DIVISION){
     Rational intOne(1);
-    if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){
+    if(t[1].getKind()== kind::CONST_RATIONAL &&
+       t[1].getConst<Rational>().isOne()){
       return RewriteResponse(REWRITE_AGAIN, t[0]);
     }else{
       return RewriteResponse(REWRITE_DONE, t);
     }
+  }else if(t.getKind() == kind::INTS_DIVISION_TOTAL){
+    if(t[1].getKind()== kind::CONST_RATIONAL){
+      Rational intOne(1), intZero(0);
+      if(t[1].getConst<Rational>().isOne()){
+        return RewriteResponse(REWRITE_AGAIN, t[0]);
+      } else if(t[1].getConst<Rational>().isZero()){
+        return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+      }
+    }
+    return RewriteResponse(REWRITE_DONE, t);
   }else if(t.getKind() == kind::INTS_MODULUS){
     Rational intOne(1);
-    if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){
-      Rational intZero(0);
-      return RewriteResponse(REWRITE_AGAIN, mkRationalNode(intZero));
+    if(t[1].getKind()== kind::CONST_RATIONAL &&
+       t[1].getConst<Rational>().isOne()){
+      return RewriteResponse(REWRITE_AGAIN, mkRationalNode(0));
     }else{
       return RewriteResponse(REWRITE_DONE, t);
     }
+  }else if(t.getKind() == kind::INTS_MODULUS_TOTAL){
+    if(t[1].getKind()== kind::CONST_RATIONAL){
+      if(t[1].getConst<Rational>().isOne() || t[1].getConst<Rational>().isZero()){
+        return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+      }
+    }
+    return RewriteResponse(REWRITE_DONE, t);
   }else{
     Unreachable();
   }
@@ -118,16 +143,24 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     return rewriteMinus(t, false);
   }else if(t.getKind() == kind::UMINUS){
     return rewriteUMinus(t, false);
-  }else if(t.getKind() == kind::DIVISION){
-    return rewriteDivByConstant(t, false);
+  }else if(t.getKind() == kind::DIVISION ||
+           t.getKind() == kind::DIVISION_TOTAL){
+    return rewriteDiv(t, false);
   }else if(t.getKind() == kind::PLUS){
     return postRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return postRewriteMult(t);
-  }else if(t.getKind() == kind::INTS_DIVISION){
-    return RewriteResponse(REWRITE_DONE, t);
-  }else if(t.getKind() == kind::INTS_MODULUS){
+  }else if(t.getKind() == kind::INTS_DIVISION ||
+           t.getKind() == kind::INTS_MODULUS){
     return RewriteResponse(REWRITE_DONE, t);
+  }else if(t.getKind() == kind::INTS_DIVISION_TOTAL ||
+           t.getKind() == kind::INTS_MODULUS_TOTAL){
+    if(t[1].getKind() == kind::CONST_RATIONAL &&
+       t[1].getConst<Rational>().isZero()){
+      return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+    }else{
+      return RewriteResponse(REWRITE_DONE, t);
+    }
   }else{
     Unreachable();
   }
@@ -272,27 +305,35 @@ Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
   return diff;
 }
 
-RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){
-  Assert(t.getKind()== kind::DIVISION);
+RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){
+  Assert(t.getKind()== kind::DIVISION || t.getKind() == kind::DIVISION_TOTAL);
 
   Node left = t[0];
   Node right = t[1];
-  Assert(right.getKind()== kind::CONST_RATIONAL);
-
-
-  const Rational& den = right.getConst<Rational>();
-
-  Assert(den != Rational(0));
+  if(right.getKind() == kind::CONST_RATIONAL){
+    const Rational& den = right.getConst<Rational>();
+
+    if(den.isZero()){
+      if(t.getKind() == kind::DIVISION_TOTAL){
+        return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+      }else{
+        return RewriteResponse(REWRITE_DONE, t);
+      }
+    }
+    Assert(den != Rational(0));
 
-  Rational div = den.inverse();
+    Rational div = den.inverse();
 
-  Node result = mkRationalNode(div);
+    Node result = mkRationalNode(div);
 
-  Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result);
-  if(pre){
-    return RewriteResponse(REWRITE_DONE, mult);
+    Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result);
+    if(pre){
+      return RewriteResponse(REWRITE_DONE, mult);
+    }else{
+      return RewriteResponse(REWRITE_AGAIN, mult);
+    }
   }else{
-    return RewriteResponse(REWRITE_AGAIN, mult);
+    return RewriteResponse(REWRITE_DONE, t);
   }
 }
 
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 00d816e57..986ff369d 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -49,7 +49,7 @@ private:
   static RewriteResponse rewriteConstant(TNode t);
   static RewriteResponse rewriteMinus(TNode t, bool pre);
   static RewriteResponse rewriteUMinus(TNode t, bool pre);
-  static RewriteResponse rewriteDivByConstant(TNode t, bool pre);
+  static RewriteResponse rewriteDiv(TNode t, bool pre);
 
   static RewriteResponse preRewritePlus(TNode t);
   static RewriteResponse postRewritePlus(TNode t);
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index a724124bd..0be7d31a5 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -18,9 +18,12 @@ 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 "real division"
-operator INTS_DIVISION 2 "ints division"
-operator INTS_MODULUS 2 "ints modulus"
+operator DIVISION 2 "real division (user symbol)"
+operator DIVISION_TOTAL 2 "real division with interpreted division by 0 (internal symbol)"
+operator INTS_DIVISION 2 "ints division (user symbol)"
+operator INTS_DIVISION_TOTAL 2 "ints division with interpreted division by 0 (internal symbol)"
+operator INTS_MODULUS 2 "ints modulus (user symbol)"
+operator INTS_MODULUS_TOTAL 2 "ints modulus with interpreted division by 0 (internal symbol)"
 operator POW 2 "arithmetic power"
 
 sort REAL_TYPE \
@@ -87,4 +90,8 @@ typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule
 
+typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
+
 endtheory
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index de5f801f0..9bd0a3b6c 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -30,6 +30,9 @@ bool Variable::isDivMember(Node n){
   case kind::DIVISION:
   case kind::INTS_DIVISION:
   case kind::INTS_MODULUS:
+  case kind::DIVISION_TOTAL:
+  case kind::INTS_DIVISION_TOTAL:
+  case kind::INTS_MODULUS_TOTAL:
     return Polynomial::isMember(n[0]) && Polynomial::isMember(n[1]);
   default:
     return false;
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 31f8e138e..d4f867099 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -230,11 +230,20 @@ public:
   // TODO: check if it's a theory leaf also
   static bool isMember(Node n) {
     Kind k = n.getKind();
-    if (k == kind::CONST_RATIONAL) return false;
-    if (isRelationOperator(k)) return false;
-    if (Theory::isLeafOf(n, theory::THEORY_ARITH)) return true;
-    if (k == kind::INTS_DIVISION || k == kind::INTS_MODULUS || k == kind::DIVISION) return isDivMember(n);
-    return false;
+    switch(k){
+    case kind::CONST_RATIONAL:
+      return false;
+    case kind::INTS_DIVISION:
+    case kind::INTS_MODULUS:
+    case kind::DIVISION:
+    case kind::INTS_DIVISION_TOTAL:
+    case kind::INTS_MODULUS_TOTAL:
+    case kind::DIVISION_TOTAL:
+      return isDivMember(n);
+    default:
+      return (!isRelationOperator(k)) &&
+        (Theory::isLeafOf(n, theory::THEORY_ARITH));
+    }
   }
 
   static bool isDivMember(Node n);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 5bd4c166d..3ea8b9550 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -84,10 +84,64 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
   d_statistics()
-{}
+{
+  // if(!logicInfo.isLinear()){ // If non-linear
+  //   NodeManager* currNM = NodeManager::currentNM();
+  //   if(logicInfo.areRealsUsed()){ // If reals are enabled, create this symbol
+  //     TypeNode realType = currNM->realType();
+  //     TypeNode realToRealFunctionType = currNM->mkFunctionType(realType, realType);
+  //     d_realDivideBy0Func = currNM->mkSkolem("/by0_$$", realToRealFunctionType);
+  //   }
+  //   if(logicInfo.areIntegersUsed()){  // If integers are enabled, create these symbols
+  //     TypeNode intType = currNM->integerType();
+  //     TypeNode intToIntFunctionType = currNM->mkFunctionType(intType, intType);
+  //     d_intDivideBy0Func = currNM->mkSkolem("divby0_$$", intToIntFunctionType);
+  //     d_intModulusBy0Func = currNM->mkSkolem("modby0_$$", intToIntFunctionType);
+  //   }
+  // }
+}
 
 TheoryArith::~TheoryArith(){}
 
+Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
+  NodeManager* currNM = NodeManager::currentNM();
+  TypeNode functionType = currNM->mkFunctionType(dom, range);
+  return currNM->mkSkolem(name, functionType);
+}
+
+Node TheoryArith::getRealDivideBy0Func(){
+  Assert(!getLogicInfo().isLinear());
+  Assert(getLogicInfo().areRealsUsed());
+
+  if(d_realDivideBy0Func.isNull()){
+    TypeNode realType = NodeManager::currentNM()->realType();
+    d_realDivideBy0Func = skolemFunction("/by0_$$", realType, realType);
+  }
+  return d_realDivideBy0Func;
+}
+
+Node TheoryArith::getIntDivideBy0Func(){
+  Assert(!getLogicInfo().isLinear());
+  Assert(getLogicInfo().areIntegersUsed());
+
+  if(d_intDivideBy0Func.isNull()){
+    TypeNode intType = NodeManager::currentNM()->integerType();
+    d_intDivideBy0Func = skolemFunction("divby0_$$", intType, intType);
+  }
+  return d_intDivideBy0Func;
+}
+
+Node TheoryArith::getIntModulusBy0Func(){
+  Assert(!getLogicInfo().isLinear());
+  Assert(getLogicInfo().areIntegersUsed());
+
+  if(d_intModulusBy0Func.isNull()){
+    TypeNode intType = NodeManager::currentNM()->integerType();
+    d_intModulusBy0Func = skolemFunction("modby0_$$", intType, intType);
+  }
+  return d_intModulusBy0Func;
+}
+
 TheoryArith::Statistics::Statistics():
   d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
   d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
@@ -777,7 +831,7 @@ void TheoryArith::setupVariable(const Variable& x){
 
 
   if(x.isDivLike()){
-    interpretDivLike(x);
+    setupDivLike(x);
   }
 
 }
@@ -815,68 +869,163 @@ void TheoryArith::setupVariableList(const VarList& vl){
    * See the comment in setupPolynomail for more.
    */
 }
-void TheoryArith::interpretDivLike(const Variable& v){
+
+void TheoryArith::cautiousSetupPolynomial(const Polynomial& p){
+  if(p.containsConstant()){
+    if(!p.isConstant()){
+      Polynomial noConstant = p.getTail();
+      if(!isSetup(noConstant.getNode())){
+        setupPolynomial(noConstant);
+      }
+    }
+  }else if(!isSetup(p.getNode())){
+    setupPolynomial(p);
+  }
+}
+
+void TheoryArith::setupDivLike(const Variable& v){
   Assert(v.isDivLike());
   Node vnode = v.getNode();
   Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion
   Polynomial m = Polynomial::parsePolynomial(vnode[0]);
   Polynomial n = Polynomial::parsePolynomial(vnode[1]);
 
+  cautiousSetupPolynomial(m);
+  cautiousSetupPolynomial(n);
+
+  Node lem;
+  switch(vnode.getKind()){
+  case DIVISION:
+  case INTS_DIVISION:
+  case INTS_MODULUS:
+    lem = definingIteForDivLike(vnode);
+    break;
+  case DIVISION_TOTAL:
+    lem = axiomIteForTotalDivision(vnode);
+    break;
+  case INTS_DIVISION_TOTAL:
+  case INTS_MODULUS_TOTAL:
+    lem = axiomIteForTotalIntDivision(vnode);
+    break;
+  default:
+    /* intentionally blank */
+    break;
+  }
+
+  if(!lem.isNull()){
+    Debug("arith::div") << lem << endl;
+    d_out->lemma(lem);
+  }
+}
+
+Node TheoryArith::definingIteForDivLike(Node divLike){
+  Kind k = divLike.getKind();
+  Assert(k == DIVISION || k == INTS_DIVISION || k == INTS_MODULUS);
+  // (for all ((n Real) (d Real))
+  //  (=
+  //   (DIVISION n d)
+  //   (ite (= d 0)
+  //    (APPLY [div_0_skolem_function] n)
+  //    (DIVISION_TOTAL x y))))
+
+  Polynomial n = Polynomial::parsePolynomial(divLike[0]);
+  Polynomial d = Polynomial::parsePolynomial(divLike[1]);
+
   NodeManager* currNM = NodeManager::currentNM();
-  Node nNeq0 = currNM->mkNode(EQUAL, n.getNode(), mkRationalNode(0)).notNode();
-  if(vnode.getKind() == INTS_DIVISION || vnode.getKind() == INTS_MODULUS){
-    // (for all ((m Int) (n Int))
-    //   (=> (distinct n 0)
-    //       (let ((q (div m n)) (r (mod m n)))
-    //         (and (= m (+ (* n q) r))
-    //              (<= 0 r (- (abs n) 1))))))
-
-    // Updated for div 0 functions
-    // (for all ((m Int) (n Int))
-    //   (let ((q (div m n)) (r (mod m n)))
-    //     (ite (= n 0)
-    //          (and (= q (div_0_func m)) (= r (mod_0_func m)))
-    //          (and (= m (+ (* n q) r))
-    //               (<= 0 r (- (abs n) 1)))))))
-
-    Node q = (vnode.getKind() == INTS_DIVISION) ? vnode : currNM->mkNode(INTS_DIVISION, m.getNode(), n.getNode());
-    Node r = (vnode.getKind() == INTS_MODULUS) ? vnode : currNM->mkNode(INTS_MODULUS, m.getNode(), n.getNode());
-
-
-    Polynomial rp = Polynomial::parsePolynomial(r);
-    Polynomial qp = Polynomial::parsePolynomial(q);
-
-    Node abs_n;
-    Node zero = mkRationalNode(0);
-
-    if(n.isConstant()){
-      abs_n = n.getHead().getConstant().abs().getNode();
-    }else{
-      abs_n = mkIntSkolem("abs_$$");
-      Node absCnd = n.makeAbsCondition(Variable(abs_n));
-      d_out->lemma(absCnd);
-    }
+  Node dEq0 = currNM->mkNode(EQUAL, d.getNode(), mkRationalNode(0));
 
-    Node eq = Comparison::mkComparison(EQUAL, m, n * qp + rp).getNode();
-    Node leq0 = currNM->mkNode(LEQ,  zero, r);
-    Node leq1 = currNM->mkNode(LT, r, abs_n);
+  Kind kTotal = (k == DIVISION) ? DIVISION_TOTAL :
+    (k == INTS_DIVISION) ? INTS_DIVISION_TOTAL : INTS_MODULUS_TOTAL;
 
-    Node andE = currNM->mkNode(AND, eq, leq0, leq1);
-    Node nNeq0ImpliesandE = currNM->mkNode(IMPLIES, nNeq0, andE);
+  Node by0Func = (k == DIVISION) ?  getRealDivideBy0Func():
+    (k == INTS_DIVISION) ? getIntDivideBy0Func() : getIntModulusBy0Func();
+
+
+  Debug("arith::div") << divLike << endl;
+  Debug("arith::div") << by0Func << endl;
+
+  Node divTotal = currNM->mkNode(kTotal, n.getNode(), d.getNode());
+  Node divZero = currNM->mkNode(APPLY_UF, by0Func, n.getNode());
+
+  Node defining = divLike.eqNode(dEq0.iteNode( divZero, divTotal));
+
+  return defining;
+}
+
+Node TheoryArith::axiomIteForTotalDivision(Node div_tot){
+  Assert(div_tot.getKind() == DIVISION_TOTAL);
+
+  // Inverse of multiplication axiom:
+  //   (for all ((n Real) (d Real))
+  //    (ite (= d 0)
+  //     (= (DIVISION_TOTAL n d) 0)
+  //     (= (* d (DIVISION_TOTAL n d)) n)))
 
-    d_out->lemma(nNeq0ImpliesandE);
-  }else{
-    // DIVISION (/ q r)
-    // (=> (distinct 0 n) (= m (* d n)))
-    Assert(vnode.getKind() == DIVISION);
-    Node d = mkRealSkolem("division_$$");
-    Node eq = Comparison::mkComparison(EQUAL, m, n * Polynomial::parsePolynomial(d)).getNode();
-    Node nNeq0ImpliesEq = currNM->mkNode(IMPLIES, nNeq0, eq);
-    d_out->lemma(nNeq0ImpliesEq);
-  }
 
+  Polynomial n = Polynomial::parsePolynomial(div_tot[0]);
+  Polynomial d = Polynomial::parsePolynomial(div_tot[1]);
+  Polynomial div_tot_p = Polynomial::parsePolynomial(div_tot);
+
+  Comparison invEq = Comparison::mkComparison(EQUAL, n, d * div_tot_p);
+  Comparison zeroEq = Comparison::mkComparison(EQUAL, div_tot_p, Polynomial::mkZero());
+  Node dEq0 = (d.getNode()).eqNode(mkRationalNode(0));
+  Node ite = dEq0.iteNode(zeroEq.getNode(), invEq.getNode()); 
+
+  return ite;
 }
 
+Node TheoryArith::axiomIteForTotalIntDivision(Node int_div_like){
+  Kind k = int_div_like.getKind();
+  Assert(k == INTS_DIVISION_TOTAL || k == INTS_MODULUS_TOTAL);
+
+  // (for all ((m Int) (n Int))
+  //   (=> (distinct n 0)
+  //       (let ((q (div m n)) (r (mod m n)))
+  //         (and (= m (+ (* n q) r))
+  //              (<= 0 r (- (abs n) 1))))))
+
+  // Updated for div 0 functions
+  // (for all ((m Int) (n Int))
+  //   (let ((q (div m n)) (r (mod m n)))
+  //     (ite (= n 0)
+  //          (and (= q (div_0_func m)) (= r (mod_0_func m)))
+  //          (and (= m (+ (* n q) r))
+  //               (<= 0 r (- (abs n) 1)))))))
+
+  Polynomial n = Polynomial::parsePolynomial(int_div_like[0]);
+  Polynomial d = Polynomial::parsePolynomial(int_div_like[1]);
+
+  NodeManager* currNM = NodeManager::currentNM();
+  Node zero = mkRationalNode(0);
+
+  Node q = (k == INTS_DIVISION_TOTAL) ? int_div_like : currNM->mkNode(INTS_DIVISION_TOTAL, n.getNode(), d.getNode());
+  Node r = (k == INTS_MODULUS_TOTAL) ? int_div_like : currNM->mkNode(INTS_MODULUS_TOTAL, n.getNode(), d.getNode());
+
+  Node dEq0 = (d.getNode()).eqNode(zero);
+  Node qEq0 = q.eqNode(zero);
+  Node rEq0 = r.eqNode(zero);
+
+  Polynomial rp = Polynomial::parsePolynomial(r);
+  Polynomial qp = Polynomial::parsePolynomial(q);
+
+  Node abs_d = (n.isConstant()) ? 
+    d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
+
+  Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode();
+  Node leq0 = currNM->mkNode(LEQ, zero, r);
+  Node leq1 = currNM->mkNode(LT, r, abs_d);
+
+  Node andE = currNM->mkNode(AND, eq, leq0, leq1);
+    
+  Node defDivMode = dEq0.iteNode(qEq0.andNode(rEq0), andE);
+    
+  Node lem = abs_d.getMetaKind () == metakind::VARIABLE ?
+    defDivMode.andNode(d.makeAbsCondition(Variable(abs_d))) : defDivMode;
+
+  return lem;
+}
+
+
 void TheoryArith::setupPolynomial(const Polynomial& poly) {
   Assert(!poly.containsConstant());
   TNode polyNode = poly.getNode();
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index fd664e04a..da4a80208 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -107,13 +107,15 @@ private:
     d_setupNodes.insert(n);
   }
 
-  void interpretDivLike(const Variable& x);
+  void setupDivLike(const Variable& x);
 
   void setupVariable(const Variable& x);
   void setupVariableList(const VarList& vl);
   void setupPolynomial(const Polynomial& poly);
   void setupAtom(TNode atom);
 
+  void cautiousSetupPolynomial(const Polynomial& p);
+
   class SetupLiteralCallBack : public TNodeCallBack {
   private:
     TheoryArith* d_arith;
@@ -305,6 +307,21 @@ private:
   /** TODO : get rid of this. */ 
   DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed);
 
+  /** Uninterpretted function symbol for use when interpreting
+   * division by zero.
+   */
+  Node d_realDivideBy0Func;
+  Node d_intDivideBy0Func;
+  Node d_intModulusBy0Func;
+  Node getRealDivideBy0Func();
+  Node getIntDivideBy0Func();
+  Node getIntModulusBy0Func();
+
+  Node definingIteForDivLike(Node divLike);
+  Node axiomIteForTotalDivision(Node div_tot);
+  Node axiomIteForTotalIntDivision(Node int_div_like);
+
+
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   virtual ~TheoryArith();
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 5d5d4d5a0..30b5e279a 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -62,7 +62,8 @@ public:
         }
       }
     }
-    bool isDivision = n.getKind() == kind::DIVISION;
+    Kind k = n.getKind();
+    bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
     return (isInteger && !isDivision ? integerType : realType);
   }
 };/* class ArithOperatorTypeRule */