From: ajreynol Date: Mon, 15 May 2017 21:43:50 +0000 (-0500) Subject: Cleanup handling of division (possible fix for bugs 803, 804, 805). X-Git-Tag: cvc5-1.0.0~5798 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35f6efbd087dff865709b0a859b782fb03bdf859;p=cvc5.git Cleanup handling of division (possible fix for bugs 803, 804, 805). --- diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index f40e7204a..dfe092aa5 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -83,6 +83,7 @@ namespace arith { namespace attr { struct ToIntegerTag { }; struct LinearIntDivTag { }; + struct LinearDivTag { }; }/* CVC4::theory::arith::attr namespace */ /** @@ -96,6 +97,7 @@ typedef expr::CDAttribute ToIntegerAttr; * used to eliminate them. */ typedef expr::CDAttribute LinearIntDivAttr; +typedef expr::CDAttribute LinearDivAttr; static Node toSumNode(const ArithVariables& vars, const DenseMap& sum); static double fRand(double fMin, double fMax); @@ -235,12 +237,12 @@ static Node getSkolemConstrainedToDivisionTotal( NodeManager* nm = NodeManager::currentNM(); Node total_div_node = nm->mkNode(kind::DIVISION_TOTAL, num, den); Node total_div_skolem; - if(total_div_node.getAttribute(LinearIntDivAttr(), total_div_skolem)) { + if(total_div_node.getAttribute(LinearDivAttr(), total_div_skolem)) { return total_div_skolem; } total_div_skolem = nm->mkSkolem("DivisionTotalSkolem", nm->realType(), "the result of a div term"); - total_div_node.setAttribute(LinearIntDivAttr(), total_div_skolem); + total_div_node.setAttribute(LinearDivAttr(), total_div_skolem); Node zero = mkRationalNode(0); Node lemma = den.eqNode(zero).iteNode( total_div_skolem.eqNode(zero), num.eqNode(mkMult(total_div_skolem, den))); @@ -248,25 +250,6 @@ static Node getSkolemConstrainedToDivisionTotal( return total_div_skolem; } -// Returns a skolem variable that is constrained to equal division(num, den) in -// the current context. May add lemmas to out. -static Node getSkolemConstrainedToDivision( - Node num, Node den, Node div0Func, OutputChannel* out) { - NodeManager* nm = NodeManager::currentNM(); - Node div_node = nm->mkNode(kind::DIVISION, num, den); - Node div_skolem; - if(div_node.getAttribute(LinearIntDivAttr(), div_skolem)) { - return div_skolem; - } - div_skolem = nm->mkSkolem("DivisionSkolem", nm->realType(), - "the result of a div term"); - div_node.setAttribute(LinearIntDivAttr(), div_skolem); - Node div0 = nm->mkNode(APPLY_UF, div0Func, num); - Node total_div = getSkolemConstrainedToDivisionTotal(num, den, out); - out->lemma(mkOnZeroIte(den, div_skolem, div0, total_div)); - return div_skolem; -} - // Integer division axioms: // These concenrate the high level constructs needed to constrain the functions: @@ -374,106 +357,16 @@ static Node getSkolemConstrainedToIntegerDivisionTotal( return total_div_skolem; } total_div_skolem = nm->mkSkolem("linearIntDiv", nm->integerType(), - "the result of an intdiv-by-k term"); + "the result of an intdiv term"); total_div_node.setAttribute(LinearIntDivAttr(), total_div_skolem); out->lemma(mkAxiomForTotalIntDivision(num, den, total_div_skolem)); return total_div_skolem; } -// Returns a skolem variable that is constrained to equal -// integer_division(num, den) in the current context. May add lemmas to out. -static Node getSkolemConstrainedToIntegerDivision( - Node num, Node den, Node div0Func, OutputChannel* out) { - NodeManager* nm = NodeManager::currentNM(); - Node div_node = nm->mkNode(kind::INTS_DIVISION, num, den); - Node div_skolem; - if(div_node.getAttribute(LinearIntDivAttr(), div_skolem)) { - return div_skolem; - } - div_skolem = nm->mkSkolem("IntDivSkolem", nm->integerType(), - "the result of an intdiv-by-k term"); - div_node.setAttribute(LinearIntDivAttr(), div_skolem); - Node div0 = nm->mkNode(APPLY_UF, div0Func, num); - Node total_div = getSkolemConstrainedToIntegerDivisionTotal(num, den, out); - out->lemma(mkOnZeroIte(den, div_skolem, div0, total_div)); - return div_skolem; -} - -// Returns a skolem variable that is constrained to equal -// integer_modulus_total(num, den) in the current context. May add lemmas to -// out. -static Node getSkolemConstrainedToIntegerModulusTotal( - Node num, Node den, OutputChannel* out) { - NodeManager* nm = NodeManager::currentNM(); - Node total_mod_node = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); - Node total_mod_skolem; - if(total_mod_node.getAttribute(LinearIntDivAttr(), total_mod_skolem)) { - return total_mod_skolem; - } - total_mod_skolem = nm->mkSkolem("IntModTotalSkolem", nm->integerType(), - "the result of an intdiv-by-k term"); - total_mod_node.setAttribute(LinearIntDivAttr(), total_mod_skolem); - Node total_div = getSkolemConstrainedToIntegerDivisionTotal(num, den, out); - out->lemma(mkAxiomForTotalIntMod(num, den, total_div, total_mod_skolem)); - return total_mod_skolem; -} - -// Returns a skolem variable that is constrained to equal -// integer_modulus(num, den) in the current context. May add lemmas to out. -static Node getSkolemConstrainedToIntegerModulus( - Node num, Node den, Node mod0Func, OutputChannel* out) { - NodeManager* nm = NodeManager::currentNM(); - Node mod_node = nm->mkNode(kind::INTS_MODULUS, num, den); - Node mod_skolem; - if(mod_node.getAttribute(LinearIntDivAttr(), mod_skolem)) { - return mod_skolem; - } - mod_skolem = nm->mkSkolem("IntModSkolem", nm->integerType(), - "the result of an intdiv-by-k term"); - mod_node.setAttribute(LinearIntDivAttr(), mod_skolem); - Node mod0 = nm->mkNode(APPLY_UF, mod0Func, num); - Node total_mod = getSkolemConstrainedToIntegerModulusTotal(num, den, out); - out->lemma(mkOnZeroIte(den, mod_skolem, mod0, total_mod)); - return mod_skolem; -} - void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_congruenceManager.setMasterEqualityEngine(eq); } -Node TheoryArithPrivate::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 TheoryArithPrivate::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 TheoryArithPrivate::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; -} - TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) throw (){ stringstream ss; ss << "Cannot construct a model for " << n << " as " << endl << msg; @@ -1354,42 +1247,99 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { Assert(k == kind::TO_INTEGER); return toIntSkolem; } + case kind::INTS_DIVISION: case kind::INTS_MODULUS: + case kind::DIVISION: + // these should be removed during expand definitions + Assert( false ); + break; +/*//AJR : This version seems to cause memory corruption, see bugs 803-805 + // The only difference w.r.t the code below is that the integer division skolem is shared between MOD AND DIV terms. + // There may be an issue related to garbage collection on attributes, TODO : revisit this. case kind::INTS_MODULUS_TOTAL: - case kind::INTS_DIVISION: case kind::INTS_DIVISION_TOTAL: { Node den = Rewriter::rewrite(n[1]); if (!options::rewriteDivk() && den.isConst()) { return n; } Node num = Rewriter::rewrite(n[0]); - if (k == kind::INTS_MODULUS) { - return getSkolemConstrainedToIntegerModulus( - num, den, getIntModulusBy0Func(), d_containing.d_out); - } else if (k == kind::INTS_MODULUS_TOTAL) { - return getSkolemConstrainedToIntegerModulusTotal(num, den, - d_containing.d_out); - } else if (k == kind::INTS_DIVISION) { - return getSkolemConstrainedToIntegerDivision( - num, den, getIntDivideBy0Func(), d_containing.d_out); - } - Assert(k == kind::INTS_DIVISION_TOTAL); - return getSkolemConstrainedToIntegerDivisionTotal(num, den, - d_containing.d_out); + if( k == kind::INTS_MODULUS_TOTAL ){ + Node dk = getSkolemConstrainedToIntegerDivisionTotal(num, den, d_containing.d_out); + return node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, dk)); + } else{ + + Assert(k == kind::INTS_DIVISION_TOTAL); + return getSkolemConstrainedToIntegerDivisionTotal(num, den, d_containing.d_out); + } } - case kind::DIVISION: case kind::DIVISION_TOTAL: { Node num = Rewriter::rewrite(n[0]); Node den = Rewriter::rewrite(n[1]); Assert(!den.isConst()); - if (k == kind::DIVISION) { - return getSkolemConstrainedToDivision(num, den, getRealDivideBy0Func(), - d_containing.d_out); - } - Assert(k == kind::DIVISION_TOTAL); return getSkolemConstrainedToDivisionTotal(num, den, d_containing.d_out); } - + */ + + case kind::INTS_DIVISION_TOTAL: + case kind::INTS_MODULUS_TOTAL: { + Node den = Rewriter::rewrite(n[1]); + if(!options::rewriteDivk() && den.isConst()) { + return n; + } + Node num = Rewriter::rewrite(n[0]); + Node intVar; + Node rw = nm->mkNode(k, num, den); + if(!rw.getAttribute(LinearIntDivAttr(), intVar)) { + intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term"); + rw.setAttribute(LinearIntDivAttr(), intVar); + Node lem; + if (den.isConst()) { + const Rational& rat = den.getConst(); + Assert(!num.isConst()); + if(rat != 0) { + if(rat > 0) { + lem = nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), + nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))); + } else { + lem = nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), + nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))); + } + } + }else{ + lem = nm->mkNode(kind::AND, + nm->mkNode(kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::GT, den, nm->mkConst(Rational(0)) ), + nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), + nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1))))))), + nm->mkNode(kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::LT, den, nm->mkConst(Rational(0)) ), + nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), + nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))))); + } + if( !lem.isNull() ){ + d_containing.d_out->lemma(lem); + } + } + if( k==kind::INTS_MODULUS_TOTAL ){ + Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar)); + return node; + }else{ + return intVar; + } + break; + } + case kind::DIVISION_TOTAL: { + Node num = Rewriter::rewrite(n[0]); + Node den = Rewriter::rewrite(n[1]); + Assert(!den.isConst()); + Node var; + Node rw = nm->mkNode(k, num, den); + if(!rw.getAttribute(LinearDivAttr(), var)) { + var = nm->mkSkolem("nonlinearDiv", nm->realType(), "the result of a non-linear div term"); + rw.setAttribute(LinearDivAttr(), var); + d_containing.d_out->lemma(nm->mkNode(kind::IMPLIES, den.eqNode(nm->mkConst(Rational(0))).negate(), nm->mkNode(kind::MULT, den, var).eqNode(num))); + } + return var; + break; + } default: break; } @@ -1630,7 +1580,8 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){ case DIVISION: case INTS_DIVISION: case INTS_MODULUS: - lem = definingIteForDivLike(vnode); + // these should be removed during expand definitions + Assert( false ); break; case DIVISION_TOTAL: lem = axiomIteForTotalDivision(vnode); @@ -1650,40 +1601,6 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){ } } -Node TheoryArithPrivate::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 n d)))) - - Polynomial n = Polynomial::parsePolynomial(divLike[0]); - Polynomial d = Polynomial::parsePolynomial(divLike[1]); - - NodeManager* currNM = NodeManager::currentNM(); - Node dEq0 = currNM->mkNode(EQUAL, d.getNode(), mkRationalNode(0)); - - Kind kTotal = (k == DIVISION) ? DIVISION_TOTAL : - (k == INTS_DIVISION) ? INTS_DIVISION_TOTAL : INTS_MODULUS_TOTAL; - - 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 TheoryArithPrivate::axiomIteForTotalDivision(Node div_tot){ Assert(div_tot.getKind() == DIVISION_TOTAL); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 9d27aac7a..b73877dc1 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -416,17 +416,6 @@ private: DeltaRational getDeltaValue(TNode term) const throw(DeltaRationalException, ModelException); - /** 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); diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index 4e350c9c8..0da1816b0 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -47,7 +47,8 @@ TESTS = \ rewriting-sums.smt2 \ disj-eval.smt2 \ bug698.smt2 \ - real-div-ufnra.smt2 + real-div-ufnra.smt2 \ + div-mod-partial.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/nl/div-mod-partial.smt2 b/test/regress/regress0/nl/div-mod-partial.smt2 new file mode 100644 index 000000000..fa75ee594 --- /dev/null +++ b/test/regress/regress0/nl/div-mod-partial.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: sat +(set-logic QF_UFNIA) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (not (= y 0))) +; should be SAT if the partial functions for div and mod are different +(assert (not (= (- y (* (div y x) x)) (mod y x)))) +(check-sat)