From: Andrew Reynolds Date: Fri, 19 Jun 2020 20:18:24 +0000 (-0500) Subject: (proof-new) Split operator elimination from arithmetic (#4581) X-Git-Tag: cvc5-1.0.0~3194 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e0633c091c37b79f9e3a2517cf95113c788db083;p=cvc5.git (proof-new) Split operator elimination from arithmetic (#4581) This class will be undergoing further refactoring for the sake of proofs. This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d16164562..6850ef450 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -316,6 +316,8 @@ libcvc4_add_sources( theory/arith/nl/transcendental_solver.h theory/arith/normal_form.cpp theory/arith/normal_form.h + theory/arith/operator_elim.cpp + theory/arith/operator_elim.h theory/arith/partial_model.cpp theory/arith/partial_model.h theory/arith/simplex.cpp diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp new file mode 100644 index 000000000..593fbd584 --- /dev/null +++ b/src/theory/arith/operator_elim.cpp @@ -0,0 +1,508 @@ +/********************* */ +/*! \file operator_elim.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Andrew Reynolds, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of operator elimination for arithmetic + **/ + +#include "theory/arith/operator_elim.h" + +#include "expr/skolem_manager.h" +#include "options/arith_options.h" +#include "smt/logic_exception.h" +#include "theory/arith/arith_utilities.h" +#include "theory/rewriter.h" +#include "theory/theory.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arith { + +OperatorElim::OperatorElim(const LogicInfo& info) : d_info(info) {} + +void OperatorElim::checkNonLinearLogic(Node term) +{ + if (d_info.isLinear()) + { + Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term + << std::endl; + std::stringstream serr; + serr << "A non-linear fact was asserted to arithmetic in a linear logic." + << std::endl; + serr << "The fact in question: " << term << std::endl; + throw LogicException(serr.str()); + } +} + +Node OperatorElim::eliminateOperatorsRec(Node n) +{ + Trace("arith-elim") << "Begin elim: " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + Node cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (Theory::theoryOf(cur) != THEORY_ARITH) + { + visited[cur] = cur; + } + else if (it == visited.end()) + { + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + Node retElim = eliminateOperators(ret); + if (retElim != ret) + { + // recursively eliminate operators in result, since some eliminations + // are defined in terms of other non-standard operators. + ret = eliminateOperatorsRec(retElim); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +Node OperatorElim::eliminateOperators(Node node) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + + Kind k = node.getKind(); + switch (k) + { + case TANGENT: + case COSECANT: + case SECANT: + case COTANGENT: + { + // these are eliminated by rewriting + return Rewriter::rewrite(node); + break; + } + case TO_INTEGER: + case IS_INTEGER: + { + Node toIntSkolem; + std::map::const_iterator it = d_to_int_skolem.find(node[0]); + if (it == d_to_int_skolem.end()) + { + // node[0] - 1 < toIntSkolem <= node[0] + // -1 < toIntSkolem - node[0] <= 0 + // 0 <= node[0] - toIntSkolem < 1 + Node v = nm->mkBoundVar(nm->integerType()); + Node one = mkRationalNode(1); + Node zero = mkRationalNode(0); + Node diff = nm->mkNode(MINUS, node[0], v); + Node lem = mkInRange(diff, zero, one); + toIntSkolem = sm->mkSkolem( + v, lem, "toInt", "a conversion of a Real term to its Integer part"); + toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem); + d_to_int_skolem[node[0]] = toIntSkolem; + } + else + { + toIntSkolem = (*it).second; + } + if (k == IS_INTEGER) + { + return nm->mkNode(EQUAL, node[0], toIntSkolem); + } + Assert(k == TO_INTEGER); + return toIntSkolem; + } + + case INTS_DIVISION_TOTAL: + case INTS_MODULUS_TOTAL: + { + Node den = Rewriter::rewrite(node[1]); + Node num = Rewriter::rewrite(node[0]); + Node intVar; + Node rw = nm->mkNode(k, num, den); + std::map::const_iterator it = d_int_div_skolem.find(rw); + if (it == d_int_div_skolem.end()) + { + Node v = nm->mkBoundVar(nm->integerType()); + Node lem; + Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num); + if (den.isConst()) + { + const Rational& rat = den.getConst(); + if (num.isConst() || rat == 0) + { + // just rewrite + return Rewriter::rewrite(node); + } + if (rat > 0) + { + lem = nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode(MULT, + den, + nm->mkNode(PLUS, v, nm->mkConst(Rational(1)))))); + } + else + { + lem = nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode(PLUS, v, nm->mkConst(Rational(-1)))))); + } + } + else + { + checkNonLinearLogic(node); + lem = nm->mkNode( + AND, + nm->mkNode( + IMPLIES, + nm->mkNode(GT, den, nm->mkConst(Rational(0))), + nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))), + nm->mkNode( + IMPLIES, + nm->mkNode(LT, den, nm->mkConst(Rational(0))), + nm->mkNode( + AND, + leqNum, + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode( + PLUS, v, nm->mkConst(Rational(-1)))))))); + } + intVar = sm->mkSkolem( + v, lem, "linearIntDiv", "the result of an intdiv-by-k term"); + intVar = SkolemManager::getWitnessForm(intVar); + d_int_div_skolem[rw] = intVar; + } + else + { + intVar = (*it).second; + } + if (k == INTS_MODULUS_TOTAL) + { + Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar)); + return nn; + } + else + { + return intVar; + } + break; + } + case DIVISION_TOTAL: + { + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + if (den.isConst()) + { + // No need to eliminate here, can eliminate via rewriting later. + // Moreover, rewriting may change the type of this node from real to + // int, which impacts certain issues with subtyping. + return node; + } + checkNonLinearLogic(node); + Node var; + Node rw = nm->mkNode(k, num, den); + std::map::const_iterator it = d_div_skolem.find(rw); + if (it == d_div_skolem.end()) + { + Node v = nm->mkBoundVar(nm->realType()); + Node lem = nm->mkNode(IMPLIES, + den.eqNode(nm->mkConst(Rational(0))).negate(), + nm->mkNode(MULT, den, v).eqNode(num)); + var = sm->mkSkolem( + v, lem, "nonlinearDiv", "the result of a non-linear div term"); + var = SkolemManager::getWitnessForm(var); + d_div_skolem[rw] = var; + } + else + { + var = (*it).second; + } + return var; + break; + } + case DIVISION: + { + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + Node ret = nm->mkNode(DIVISION_TOTAL, num, den); + if (!den.isConst() || den.getConst().sgn() == 0) + { + checkNonLinearLogic(node); + Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); + ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret); + } + return ret; + break; + } + + case INTS_DIVISION: + { + // partial function: integer div + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + Node ret = nm->mkNode(INTS_DIVISION_TOTAL, num, den); + if (!den.isConst() || den.getConst().sgn() == 0) + { + checkNonLinearLogic(node); + Node intDivByZeroNum = + getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); + ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret); + } + return ret; + break; + } + + case INTS_MODULUS: + { + // partial function: mod + Node num = Rewriter::rewrite(node[0]); + Node den = Rewriter::rewrite(node[1]); + Node ret = nm->mkNode(INTS_MODULUS_TOTAL, num, den); + if (!den.isConst() || den.getConst().sgn() == 0) + { + checkNonLinearLogic(node); + Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); + ret = nm->mkNode(ITE, denEq0, modZeroNum, ret); + } + return ret; + break; + } + + case ABS: + { + return nm->mkNode(ITE, + nm->mkNode(LT, node[0], nm->mkConst(Rational(0))), + nm->mkNode(UMINUS, node[0]), + node[0]); + break; + } + case SQRT: + case ARCSINE: + case ARCCOSINE: + case ARCTANGENT: + case ARCCOSECANT: + case ARCSECANT: + case ARCCOTANGENT: + { + checkNonLinearLogic(node); + // eliminate inverse functions here + std::map::const_iterator it = + d_nlin_inverse_skolem.find(node); + if (it == d_nlin_inverse_skolem.end()) + { + Node var = nm->mkBoundVar(nm->realType()); + Node lem; + if (k == SQRT) + { + Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT); + Node uf = skolemApp.eqNode(var); + Node nonNeg = + nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf); + + // sqrt(x) reduces to: + // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x)) + // + // Uf(x) makes sure that the reduction still behaves like a function, + // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be + // satisfiable. On the original formula, this would require that we + // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid + // model. + lem = nm->mkNode(ITE, + nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))), + nonNeg, + uf); + } + else + { + Node pi = mkPi(); + + // range of the skolem + Node rlem; + if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT) + { + Node half = nm->mkConst(Rational(1) / Rational(2)); + Node pi2 = nm->mkNode(MULT, half, pi); + Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2); + // -pi/2 < var <= pi/2 + rlem = nm->mkNode( + AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2)); + } + else + { + // 0 <= var < pi + rlem = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConst(Rational(0)), var), + nm->mkNode(LT, var, pi)); + } + + Kind rk = k == ARCSINE + ? SINE + : (k == ARCCOSINE + ? COSINE + : (k == ARCTANGENT + ? TANGENT + : (k == ARCCOSECANT + ? COSECANT + : (k == ARCSECANT ? SECANT + : COTANGENT)))); + Node invTerm = nm->mkNode(rk, var); + lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0])); + } + Assert(!lem.isNull()); + Node ret = sm->mkSkolem( + var, + lem, + "tfk", + "Skolem to eliminate a non-standard transcendental function"); + ret = SkolemManager::getWitnessForm(ret); + d_nlin_inverse_skolem[node] = ret; + return ret; + } + return (*it).second; + break; + } + + default: break; + } + return node; +} + +Node OperatorElim::getArithSkolem(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; + switch (asi) + { + case ArithSkolemId::DIV_BY_ZERO: + tn = nm->realType(); + name = std::string("divByZero"); + desc = std::string("partial real division"); + break; + case ArithSkolemId::INT_DIV_BY_ZERO: + tn = nm->integerType(); + name = std::string("intDivByZero"); + desc = std::string("partial int division"); + break; + case ArithSkolemId::MOD_BY_ZERO: + tn = nm->integerType(); + name = std::string("modZero"); + desc = std::string("partial modulus"); + break; + case ArithSkolemId::SQRT: + tn = nm->realType(); + name = std::string("sqrtUf"); + desc = std::string("partial sqrt"); + break; + default: Unhandled(); + } + + 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); + } + d_arith_skolem[asi] = skolem; + return skolem; + } + return it->second; +} + +Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi) +{ + Node skolem = getArithSkolem(asi); + if (!options::arithNoPartialFun()) + { + skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n); + } + return skolem; +} + +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h new file mode 100644 index 000000000..2cdf9bc49 --- /dev/null +++ b/src/theory/arith/operator_elim.h @@ -0,0 +1,123 @@ +/********************* */ +/*! \file operator_elim.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Operator elimination for arithmetic + **/ + +#pragma once + +#include + +#include "expr/node.h" +#include "theory/logic_info.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class OperatorElim +{ + public: + OperatorElim(const LogicInfo& info); + ~OperatorElim() {} + /** + * Eliminate operators in term n. If n has top symbol that is not a core + * one (including division, int division, mod, to_int, is_int, syntactic sugar + * transcendental functions), then we replace it by a form that eliminates + * that operator. This may involve the introduction of witness terms. + * + * One exception to the above rule is that we may leave certain applications + * like (/ 4 1) unchanged, since replacing this by 4 changes its type from + * real to int. This is important for some subtyping issues during + * expandDefinition. Moreover, applications like this can be eliminated + * trivially later by rewriting. + * + * This method is called both during expandDefinition and during ppRewrite. + * + * @param n The node to eliminate operators from. + * @return The (single step) eliminated form of n. + */ + Node eliminateOperators(Node n); + /** + * Recursively ensure that n has no non-standard operators. This applies + * the above method on all subterms of n. + * + * @param n The node to eliminate operators from. + * @return The eliminated form of n. + */ + Node eliminateOperatorsRec(Node n); + + private: + /** Logic info of the owner of this class */ + const LogicInfo& d_info; + + /** + * Maps for Skolems for to-integer, real/integer div-by-k, and inverse + * non-linear operators that are introduced during ppRewriteTerms. + */ + std::map d_to_int_skolem; + std::map d_div_skolem; + std::map d_int_div_skolem; + std::map d_nlin_inverse_skolem; + + /** Arithmetic skolem identifier */ + enum class ArithSkolemId + { + /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */ + DIV_BY_ZERO, + /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */ + INT_DIV_BY_ZERO, + /* an uninterpreted function f s.t. f(x) = x mod 0 */ + MOD_BY_ZERO, + /* an uninterpreted function f s.t. f(x) = sqrt(x) */ + SQRT, + }; + + /** + * 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. + */ + 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. + */ + Node getArithSkolem(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 getArithSkolemApp(Node n, ArithSkolemId asi); + + /** + * Called when a non-linear term n is given to this class. Throw an exception + * if the logic is linear. + */ + void checkNonLinearLogic(Node term); +}; + +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ed0adc59e..7b7f5a411 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -156,10 +156,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_solveIntMaybeHelp(0u), d_solveIntAttempts(0u), d_statistics(), - d_to_int_skolem(u), - d_div_skolem(u), - d_int_div_skolem(u), - d_nlin_inverse_skolem(u) + d_opElim(logicInfo) { if( options::nlExt() ){ d_nonlinearExtension = new nl::NonlinearExtension( @@ -1088,427 +1085,16 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may // introduce non-standard arithmetic terms appearing in grammars. // call eliminate operators - Node nn = eliminateOperators(n); + Node nn = d_opElim.eliminateOperators(n); if (nn != n) { // since elimination may introduce new operators to eliminate, we must // recursively eliminate result - return eliminateOperatorsRec(nn); + return d_opElim.eliminateOperatorsRec(nn); } return n; } -void TheoryArithPrivate::checkNonLinearLogic(Node term) -{ - if (getLogicInfo().isLinear()) - { - Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term - << std::endl; - std::stringstream serr; - serr << "A non-linear fact was asserted to arithmetic in a linear logic." - << std::endl; - serr << "The fact in question: " << term << endl; - throw LogicException(serr.str()); - } -} - -Node TheoryArithPrivate::eliminateOperatorsRec(Node n) -{ - Trace("arith-elim") << "Begin elim: " << n << std::endl; - NodeManager* nm = NodeManager::currentNM(); - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - Node cur; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - if (Theory::theoryOf(cur) != THEORY_ARITH) - { - visited[cur] = cur; - } - else if (it == visited.end()) - { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - else if (it->second.isNull()) - { - Node ret = cur; - bool childChanged = false; - std::vector children; - if (cur.getMetaKind() == metakind::PARAMETERIZED) - { - children.push_back(cur.getOperator()); - } - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); - } - if (childChanged) - { - ret = nm->mkNode(cur.getKind(), children); - } - Node retElim = eliminateOperators(ret); - if (retElim != ret) - { - // recursively eliminate operators in result, since some eliminations - // are defined in terms of other non-standard operators. - ret = eliminateOperatorsRec(retElim); - } - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - -Node TheoryArithPrivate::eliminateOperators(Node node) -{ - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - - Kind k = node.getKind(); - switch (k) - { - case kind::TANGENT: - case kind::COSECANT: - case kind::SECANT: - case kind::COTANGENT: - { - // these are eliminated by rewriting - return Rewriter::rewrite(node); - break; - } - case kind::TO_INTEGER: - case kind::IS_INTEGER: - { - Node toIntSkolem; - NodeMap::const_iterator it = d_to_int_skolem.find(node[0]); - if (it == d_to_int_skolem.end()) - { - // node[0] - 1 < toIntSkolem <= node[0] - // -1 < toIntSkolem - node[0] <= 0 - // 0 <= node[0] - toIntSkolem < 1 - Node v = nm->mkBoundVar(nm->integerType()); - Node one = mkRationalNode(1); - Node zero = mkRationalNode(0); - Node diff = nm->mkNode(kind::MINUS, node[0], v); - Node lem = mkInRange(diff, zero, one); - toIntSkolem = sm->mkSkolem( - v, lem, "toInt", "a conversion of a Real term to its Integer part"); - toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem); - d_to_int_skolem[node[0]] = toIntSkolem; - } - else - { - toIntSkolem = (*it).second; - } - if (k == kind::IS_INTEGER) - { - return nm->mkNode(kind::EQUAL, node[0], toIntSkolem); - } - Assert(k == kind::TO_INTEGER); - return toIntSkolem; - } - - case kind::INTS_DIVISION_TOTAL: - case kind::INTS_MODULUS_TOTAL: - { - Node den = Rewriter::rewrite(node[1]); - Node num = Rewriter::rewrite(node[0]); - Node intVar; - Node rw = nm->mkNode(k, num, den); - NodeMap::const_iterator it = d_int_div_skolem.find(rw); - if (it == d_int_div_skolem.end()) - { - Node v = nm->mkBoundVar(nm->integerType()); - Node lem; - Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num); - if (den.isConst()) - { - const Rational& rat = den.getConst(); - if (num.isConst() || rat == 0) - { - // just rewrite - return Rewriter::rewrite(node); - } - if (rat > 0) - { - lem = nm->mkNode( - AND, - leqNum, - nm->mkNode( - LT, - num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, v, nm->mkConst(Rational(1)))))); - } - else - { - lem = nm->mkNode( - AND, - leqNum, - nm->mkNode( - LT, - num, - nm->mkNode( - MULT, - den, - nm->mkNode(PLUS, v, nm->mkConst(Rational(-1)))))); - } - } - else - { - checkNonLinearLogic(node); - lem = nm->mkNode( - AND, - nm->mkNode( - IMPLIES, - nm->mkNode(GT, den, nm->mkConst(Rational(0))), - nm->mkNode( - AND, - leqNum, - nm->mkNode( - LT, - num, - nm->mkNode( - MULT, - den, - nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))), - nm->mkNode( - IMPLIES, - nm->mkNode(LT, den, nm->mkConst(Rational(0))), - nm->mkNode( - AND, - leqNum, - nm->mkNode( - LT, - num, - nm->mkNode( - MULT, - den, - nm->mkNode( - PLUS, v, nm->mkConst(Rational(-1)))))))); - } - intVar = sm->mkSkolem( - v, lem, "linearIntDiv", "the result of an intdiv-by-k term"); - intVar = SkolemManager::getWitnessForm(intVar); - d_int_div_skolem[rw] = intVar; - } - else - { - intVar = (*it).second; - } - if (k == kind::INTS_MODULUS_TOTAL) - { - Node nn = - nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar)); - return nn; - } - else - { - return intVar; - } - break; - } - case kind::DIVISION_TOTAL: - { - Node num = Rewriter::rewrite(node[0]); - Node den = Rewriter::rewrite(node[1]); - if (den.isConst()) - { - // No need to eliminate here, can eliminate via rewriting later. - // Moreover, rewriting may change the type of this node from real to - // int, which impacts certain issues with subtyping. - return node; - } - checkNonLinearLogic(node); - Node var; - Node rw = nm->mkNode(k, num, den); - NodeMap::const_iterator it = d_div_skolem.find(rw); - if (it == d_div_skolem.end()) - { - Node v = nm->mkBoundVar(nm->realType()); - Node lem = nm->mkNode(IMPLIES, - den.eqNode(nm->mkConst(Rational(0))).negate(), - nm->mkNode(MULT, den, v).eqNode(num)); - var = sm->mkSkolem( - v, lem, "nonlinearDiv", "the result of a non-linear div term"); - var = SkolemManager::getWitnessForm(var); - d_div_skolem[rw] = var; - } - else - { - var = (*it).second; - } - return var; - break; - } - case kind::DIVISION: - { - Node num = Rewriter::rewrite(node[0]); - Node den = Rewriter::rewrite(node[1]); - Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den); - if (!den.isConst() || den.getConst().sgn() == 0) - { - checkNonLinearLogic(node); - Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO); - Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret); - } - return ret; - break; - } - - case kind::INTS_DIVISION: - { - // partial function: integer div - Node num = Rewriter::rewrite(node[0]); - Node den = Rewriter::rewrite(node[1]); - Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); - if (!den.isConst() || den.getConst().sgn() == 0) - { - checkNonLinearLogic(node); - Node intDivByZeroNum = - getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO); - Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret); - } - return ret; - break; - } - - case kind::INTS_MODULUS: - { - // partial function: mod - Node num = Rewriter::rewrite(node[0]); - Node den = Rewriter::rewrite(node[1]); - Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); - if (!den.isConst() || den.getConst().sgn() == 0) - { - checkNonLinearLogic(node); - Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO); - Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret); - } - return ret; - break; - } - - case kind::ABS: - { - return nm->mkNode(kind::ITE, - nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), - nm->mkNode(kind::UMINUS, node[0]), - node[0]); - break; - } - case kind::SQRT: - case kind::ARCSINE: - case kind::ARCCOSINE: - case kind::ARCTANGENT: - case kind::ARCCOSECANT: - case kind::ARCSECANT: - case kind::ARCCOTANGENT: - { - checkNonLinearLogic(node); - // eliminate inverse functions here - NodeMap::const_iterator it = d_nlin_inverse_skolem.find(node); - if (it == d_nlin_inverse_skolem.end()) - { - Node var = nm->mkBoundVar(nm->realType()); - Node lem; - if (k == kind::SQRT) - { - Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT); - Node uf = skolemApp.eqNode(var); - Node nonNeg = nm->mkNode( - kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf); - - // sqrt(x) reduces to: - // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x)) - // - // Uf(x) makes sure that the reduction still behaves like a function, - // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be - // satisfiable. On the original formula, this would require that we - // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid - // model. - lem = nm->mkNode( - kind::ITE, - nm->mkNode(kind::GEQ, node[0], nm->mkConst(Rational(0))), - nonNeg, - uf); - } - else - { - Node pi = mkPi(); - - // range of the skolem - Node rlem; - if (k == kind::ARCSINE || k == ARCTANGENT || k == ARCCOSECANT) - { - Node half = nm->mkConst(Rational(1) / Rational(2)); - Node pi2 = nm->mkNode(kind::MULT, half, pi); - Node npi2 = nm->mkNode(kind::MULT, nm->mkConst(Rational(-1)), pi2); - // -pi/2 < var <= pi/2 - rlem = nm->mkNode( - AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2)); - } - else - { - // 0 <= var < pi - rlem = nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkConst(Rational(0)), var), - nm->mkNode(LT, var, pi)); - } - - Kind rk = k == kind::ARCSINE - ? kind::SINE - : (k == kind::ARCCOSINE - ? kind::COSINE - : (k == kind::ARCTANGENT - ? kind::TANGENT - : (k == kind::ARCCOSECANT - ? kind::COSECANT - : (k == kind::ARCSECANT - ? kind::SECANT - : kind::COTANGENT)))); - Node invTerm = nm->mkNode(rk, var); - lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0])); - } - Assert(!lem.isNull()); - Node ret = sm->mkSkolem( - var, - lem, - "tfk", - "Skolem to eliminate a non-standard transcendental function"); - ret = SkolemManager::getWitnessForm(ret); - d_nlin_inverse_skolem[node] = ret; - return ret; - } - return (*it).second; - break; - } - - default: break; - } - return node; -} - Node TheoryArithPrivate::ppRewrite(TNode atom) { Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; @@ -5218,155 +4804,16 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ Node TheoryArithPrivate::expandDefinition(Node node) { // call eliminate operators - Node nn = eliminateOperators(node); + Node nn = d_opElim.eliminateOperators(node); if (nn != node) { // since elimination may introduce new operators to eliminate, we must // recursively eliminate result - return eliminateOperatorsRec(nn); + return d_opElim.eliminateOperatorsRec(nn); } return node; } -Node TheoryArithPrivate::getArithSkolem(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; - switch (asi) - { - case ArithSkolemId::DIV_BY_ZERO: - tn = nm->realType(); - name = std::string("divByZero"); - desc = std::string("partial real division"); - break; - case ArithSkolemId::INT_DIV_BY_ZERO: - tn = nm->integerType(); - name = std::string("intDivByZero"); - desc = std::string("partial int division"); - break; - case ArithSkolemId::MOD_BY_ZERO: - tn = nm->integerType(); - name = std::string("modZero"); - desc = std::string("partial modulus"); - break; - case ArithSkolemId::SQRT: - tn = nm->realType(); - name = std::string("sqrtUf"); - desc = std::string("partial sqrt"); - break; - default: Unhandled(); - } - - 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); - } - d_arith_skolem[asi] = skolem; - return skolem; - } - return it->second; -} - -Node TheoryArithPrivate::getArithSkolemApp(Node n, ArithSkolemId asi) -{ - Node skolem = getArithSkolem(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); -// Assert(Polynomial::isMember(t)); -// Polynomial p = Polynomial::parsePolynomial(t); -// if(p.containsConstant()){ -// Constant c = p.getHead().getConstant(); -// if(p.isConstant()){ -// InferBoundsResult res(t, param.findLowerBound()); -// res.setBound((DeltaRational)c.getValue(), mkBoolNode(true)); -// return res; -// }else{ -// Polynomial tail = p.getTail(); -// InferBoundsResult res = inferBound(tail.getNode(), param); -// if(res.foundBound()){ -// DeltaRational newBound = res.getValue() + c.getValue(); -// if(tail.isIntegral()){ -// Integer asInt = (param.findLowerBound()) ? newBound.ceiling() : -// newBound.floor(); newBound = DeltaRational(asInt); -// } -// res.setBound(newBound, res.getExplanation()); -// } -// return res; -// } -// }else if(param.findLowerBound()){ -// InferBoundsParameters find_ub = param; -// find_ub.setFindUpperBound(); -// if(param.useThreshold()){ -// find_ub.setThreshold(- param.getThreshold() ); -// } -// Polynomial negP = -p; -// InferBoundsResult res = inferBound(negP.getNode(), find_ub); -// res.setFindLowerBound(); -// if(res.foundBound()){ -// res.setTerm(p.getNode()); -// res.setBound(-res.getValue(), res.getExplanation()); -// } -// return res; -// }else{ -// Assert(param.findUpperBound()); -// // does not contain a constant -// switch(param.getEffort()){ -// case InferBoundsParameters::Lookup: -// return inferUpperBoundLookup(t, param); -// case InferBoundsParameters::Simplex: -// return inferUpperBoundSimplex(t, param); -// case InferBoundsParameters::LookupAndSimplexOnFailure: -// case InferBoundsParameters::TryBoth: -// { -// InferBoundsResult lookup = inferUpperBoundLookup(t, param); -// if(lookup.foundBound()){ -// if(param.getEffort() == -// InferBoundsParameters::LookupAndSimplexOnFailure || -// lookup.boundIsOptimal()){ -// return lookup; -// } -// } -// InferBoundsResult simplex = inferUpperBoundSimplex(t, param); -// if(lookup.foundBound() && simplex.foundBound()){ -// return (lookup.getValue() <= simplex.getValue()) ? lookup : -// simplex; -// }else if(lookup.foundBound()){ -// return lookup; -// }else{ -// return simplex; -// } -// } -// default: -// Unreachable(); -// return InferBoundsResult(); -// } -// } -// } - std::pair TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ using namespace inferbounds; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 8252326bf..867029e3c 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -35,15 +35,12 @@ #include "smt/logic_exception.h" #include "smt_util/boolean_simplification.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" #include "theory/arith/attempt_solution_simplex.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" -#include "theory/arith/constraint.h" -#include "theory/arith/delta_rational.h" #include "theory/arith/delta_rational.h" #include "theory/arith/dio_solver.h" #include "theory/arith/dual_simplex.h" @@ -51,9 +48,8 @@ #include "theory/arith/infer_bounds.h" #include "theory/arith/linear_equality.h" #include "theory/arith/matrix.h" -#include "theory/arith/matrix.h" #include "theory/arith/normal_form.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/operator_elim.h" #include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" #include "theory/arith/soi_simplex.h" @@ -421,40 +417,13 @@ private: // handle linear /, div, mod, and also is_int, to_int Node ppRewriteTerms(TNode atom); - /** - * Called when a non-linear term n is given to this class. Throw an exception - * if the logic is linear. - */ - void checkNonLinearLogic(Node term); - /** - * Eliminate operators in term n. If n has top symbol that is not a core - * one (including division, int division, mod, to_int, is_int, syntactic sugar - * transcendental functions), then we replace it by a form that eliminates - * that operator. This may involve the introduction of witness terms. - * - * One exception to the above rule is that we may leave certain applications - * like (/ 4 1) unchanged, since replacing this by 4 changes its type from - * real to int. This is important for some subtyping issues during - * expandDefinition. Moreover, applications like this can be eliminated - * trivially later by rewriting. - * - * This method is called both during expandDefinition and during ppRewrite. - * - * @param n The node to eliminate operators from. - * @return The (single step) eliminated form of n. - */ - Node eliminateOperators(Node n); - /** - * Recursively ensure that n has no non-standard operators. This applies - * the above method on all subterms of n. - * - * @param n The node to eliminate operators from. - * @return The eliminated form of n. - */ - Node eliminateOperatorsRec(Node n); - public: - TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryArithPrivate(TheoryArith& containing, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); ~TheoryArithPrivate(); TheoryRewriter* getTheoryRewriter() { return &d_rewriter; } @@ -862,60 +831,10 @@ private: Statistics d_statistics; - enum class ArithSkolemId - { - /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */ - DIV_BY_ZERO, - /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */ - INT_DIV_BY_ZERO, - /* an uninterpreted function f s.t. f(x) = x mod 0 */ - MOD_BY_ZERO, - /* an uninterpreted function f s.t. f(x) = sqrt(x) */ - SQRT, - }; - - /** - * 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. - */ - 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. - */ - Node getArithSkolem(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 getArithSkolemApp(Node n, ArithSkolemId asi); - - /** - * Maps for Skolems for to-integer, real/integer div-by-k, and inverse - * non-linear operators that are introduced during ppRewriteTerms. - */ - typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; - NodeMap d_to_int_skolem; - NodeMap d_div_skolem; - NodeMap d_int_div_skolem; - NodeMap d_nlin_inverse_skolem; - /** The theory rewriter for this theory. */ ArithRewriter d_rewriter; + /** The operator elimination utility */ + OperatorElim d_opElim; };/* class TheoryArithPrivate */ }/* CVC4::theory::arith namespace */