From: Andrew Reynolds Date: Tue, 27 Feb 2018 21:15:07 +0000 (-0600) Subject: Option to not use partial function semantics for arithmetic div by zero (#1620) X-Git-Tag: cvc5-1.0.0~5267 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f5447f5ca07688ff7e6da7973d7f97d17678427;p=cvc5.git Option to not use partial function semantics for arithmetic div by zero (#1620) --- diff --git a/src/options/arith_options b/src/options/arith_options index e6f7fd6d0..722af1fa1 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -155,6 +155,8 @@ option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2 option maxReplayTree --max-replay-tree int :default 512 threshold for attempting to replay a tree +option arithNoPartialFun --arith-no-partial-fun bool :default false + do not use partial function semantics for arithmetic (not SMT LIB compliant) option pbRewrites --pb-rewrites bool :default false apply pseudo boolean rewrites diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index da17dd2f5..a990e008c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4902,18 +4902,9 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den); if (!den.isConst() || den.getConst().sgn() == 0) { - // partial function: division - if (d_divByZero.isNull()) - { - d_divByZero = - nm->mkSkolem("divByZero", - nm->mkFunctionType(nm->realType(), nm->realType()), - "partial real division", - NodeManager::SKOLEM_EXACT_NAME); - logicRequest.widenLogic(THEORY_UF); - } + Node divByZeroNum = + getArithSkolemApp(logicRequest, num, arith_skolem_div_by_zero); Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num); ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret); } return ret; @@ -4927,17 +4918,9 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); if (!den.isConst() || den.getConst().sgn() == 0) { - if (d_intDivByZero.isNull()) - { - d_intDivByZero = nm->mkSkolem( - "intDivByZero", - nm->mkFunctionType(nm->integerType(), nm->integerType()), - "partial integer division", - NodeManager::SKOLEM_EXACT_NAME); - logicRequest.widenLogic(THEORY_UF); - } + Node intDivByZeroNum = + getArithSkolemApp(logicRequest, num, arith_skolem_int_div_by_zero); Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num); ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret); } return ret; @@ -4951,17 +4934,9 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); if (!den.isConst() || den.getConst().sgn() == 0) { - if (d_modZero.isNull()) - { - d_modZero = nm->mkSkolem( - "modZero", - nm->mkFunctionType(nm->integerType(), nm->integerType()), - "partial modulus", - NodeManager::SKOLEM_EXACT_NAME); - logicRequest.widenLogic(THEORY_UF); - } + Node modZeroNum = + getArithSkolemApp(logicRequest, num, arith_skolem_mod_by_zero); Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num); ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret); } return ret; @@ -5062,8 +5037,68 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Unreachable(); } +Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest, + ArithSkolemId asi) +{ + std::map::iterator it = d_arith_skolem.find(asi); + if (it == d_arith_skolem.end()) + { + NodeManager* nm = NodeManager::currentNM(); + + TypeNode tn; + std::string name; + std::string desc; + if (asi == arith_skolem_div_by_zero) + { + tn = nm->realType(); + name = std::string("divByZero"); + desc = std::string("partial real division"); + } + else if (asi == arith_skolem_int_div_by_zero) + { + tn = nm->integerType(); + name = std::string("intDivByZero"); + desc = std::string("partial int division"); + } + else if (asi == arith_skolem_mod_by_zero) + { + tn = nm->integerType(); + name = std::string("modZero"); + desc = std::string("partial modulus"); + } + Node skolem; + if (options::arithNoPartialFun()) + { + // partial function: division + skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME); + } + else + { + // partial function: division + skolem = nm->mkSkolem(name, + nm->mkFunctionType(tn, tn), + desc, + NodeManager::SKOLEM_EXACT_NAME); + logicRequest.widenLogic(THEORY_UF); + } + d_arith_skolem[asi] = skolem; + return skolem; + } + return it->second; +} +Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest, + Node n, + ArithSkolemId asi) +{ + Node skolem = getArithSkolem(logicRequest, asi); + if (!options::arithNoPartialFun()) + { + skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n); + } + return skolem; +} // InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const InferBoundsParameters& param){ // Node t = Rewriter::rewrite(term); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 23712016d..af0012304 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -829,25 +829,43 @@ private: Statistics d_statistics; + enum ArithSkolemId + { + arith_skolem_div_by_zero, + arith_skolem_int_div_by_zero, + arith_skolem_mod_by_zero, + }; /** - * Function symbol used to implement uninterpreted division-by-zero - * semantics. Needed to deal with partial division function ("/"). + * Function symbols used to implement: + * (1) Uninterpreted division-by-zero semantics. Needed to deal with partial + * division function ("/"), + * (2) Uninterpreted int-division-by-zero semantics. Needed to deal with + * partial function "div", + * (3) Uninterpreted mod-zero semantics. Needed to deal with partial + * function "mod". + * + * If the option arithNoPartialFun() is enabled, then the range of this map + * stores Skolem constants instead of Skolem functions, meaning that the + * function-ness of e.g. division by zero is ignored. */ - Node d_divByZero; - - /** - * Function symbol used to implement uninterpreted - * int-division-by-zero semantics. Needed to deal with partial - * function "div". + std::map d_arith_skolem; + /** get arithmetic skolem + * + * Returns the Skolem in the above map for the given id, creating it if it + * does not already exist. If a Skolem function is created, the logic is + * widened to include UF. */ - Node d_intDivByZero; - - /** - * Function symbol used to implement uninterpreted mod-zero - * semantics. Needed to deal with partial function "mod". + Node getArithSkolem(LogicRequest& logicRequest, ArithSkolemId asi); + /** get arithmetic skolem application + * + * By default, this returns the term f( n ), where f is the Skolem function + * for the identifier asi. + * + * If the option arithNoPartialFun is enabled, this returns f, where f is + * the Skolem constant for the identifier asi. */ - Node d_modZero; + Node getArithSkolemApp(LogicRequest& logicRequest, Node n, ArithSkolemId asi); /** * Maps for Skolems for to-integer, real/integer div-by-k, and inverse