From b3470b5e0b7a664443b9f835db5dd86fb1487866 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 8 Nov 2012 21:25:27 +0000 Subject: Improved support for division by zero. This adds the *_TOTAL kinds and uninterpreted functions for division by 0. --- src/theory/arith/arith_rewriter.cpp | 87 +++++++--- src/theory/arith/arith_rewriter.h | 2 +- src/theory/arith/kinds | 13 +- src/theory/arith/normal_form.cpp | 3 + src/theory/arith/normal_form.h | 19 ++- src/theory/arith/theory_arith.cpp | 251 +++++++++++++++++++++++------ src/theory/arith/theory_arith.h | 19 ++- src/theory/arith/theory_arith_type_rules.h | 3 +- 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().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() == intOne){ + if(t[1].getKind()== kind::CONST_RATIONAL && + t[1].getConst().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().isOne()){ + return RewriteResponse(REWRITE_AGAIN, t[0]); + } else if(t[1].getConst().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() == intOne){ - Rational intZero(0); - return RewriteResponse(REWRITE_AGAIN, mkRationalNode(intZero)); + if(t[1].getKind()== kind::CONST_RATIONAL && + t[1].getConst().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().isOne() || t[1].getConst().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().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(); - - Assert(den != Rational(0)); + if(right.getKind() == kind::CONST_RATIONAL){ + const Rational& den = right.getConst(); + + 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 */ -- cgit v1.2.3