From: Gereon Kremer Date: Fri, 25 Feb 2022 21:22:36 +0000 (+0100) Subject: Add utilities to rewrite atoms for the arithmetic rewriter (#8014) X-Git-Tag: cvc5-1.0.0~371 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c8319a7ffe36f407f2b541bbd0a99f31b7add81;p=cvc5.git Add utilities to rewrite atoms for the arithmetic rewriter (#8014) This PR adds utilities to rewrite atoms in the arithmetic rewriter. They retain compatibility with the current normal_form utility, but make the process more transparent so that changing the normal form in the future should be simpler. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index dba712aed..ac8b64293 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -503,6 +503,8 @@ libcvc5_add_sources( theory/arith/rewriter/node_utils.cpp theory/arith/rewriter/node_utils.h theory/arith/rewriter/ordering.h + theory/arith/rewriter/rewrite_atom.cpp + theory/arith/rewriter/rewrite_atom.h theory/arith/rewrites.cpp theory/arith/rewrites.h theory/arith/simplex.cpp diff --git a/src/theory/arith/rewriter/addition.cpp b/src/theory/arith/rewriter/addition.cpp index c9758fa1c..16e288920 100644 --- a/src/theory/arith/rewriter/addition.cpp +++ b/src/theory/arith/rewriter/addition.cpp @@ -262,4 +262,4 @@ Node distributeMultiplication(const std::vector& factors) } // namespace rewriter } // namespace arith } // namespace theory -} // namespace cvc5 \ No newline at end of file +} // namespace cvc5 diff --git a/src/theory/arith/rewriter/rewrite_atom.cpp b/src/theory/arith/rewriter/rewrite_atom.cpp new file mode 100644 index 000000000..e627186f2 --- /dev/null +++ b/src/theory/arith/rewriter/rewrite_atom.cpp @@ -0,0 +1,340 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Utilities for rewriting atoms in the arithmetic rewriter. + */ + +#include "theory/arith/rewriter/rewrite_atom.h" + +#include "base/check.h" +#include "theory/arith/rewriter/node_utils.h" + +namespace cvc5 { +namespace theory { +namespace arith { +namespace rewriter { + +namespace { + +/** + * Evaluate the given relation based on values l and r. Expects that the + * relational operators `operator<(L,R)`, `operator==(L,R)`, etc are defined. + */ +template +bool evaluateRelation(Kind rel, const L& l, const R& r) +{ + switch (rel) + { + case Kind::LT: return l < r; + case Kind::LEQ: return l <= r; + case Kind::EQUAL: return l == r; + case Kind::DISTINCT: return l != r; + case Kind::GEQ: return l >= r; + case Kind::GT: return l > r; + default: Unreachable(); return false; + } +} + +auto getLTermIt(Sum& sum) +{ + auto ltermit = sum.begin(); + if (ltermit->first.isConst()) + { + ++ltermit; + } + return ltermit; +} + +auto& getLTerm(Sum& sum) +{ + Assert(getLTermIt(sum) != sum.end()); + return *getLTermIt(sum); +} + +/** + * Normalize the sum, making the leading coefficient to be one or minus one. + */ +void normalizeLCoeffAbsOne(Sum& sum) +{ + if (sum.empty()) return; + if (sum.size() == 1) + { + auto& front = *sum.begin(); + // Trivial if there is only one summand + front.second = Integer(sgn(front.second) > 0 ? 1 : -1); + return; + } + // LCoeff is first coefficient of non-constant monomial + RealAlgebraicNumber lcoeff = getLTerm(sum).second; + ; + if (sgn(lcoeff) < 0) + { + lcoeff = -lcoeff; + } + if (isOne(lcoeff)) return; + for (auto& s : sum) + { + s.second = s.second / lcoeff; + } +} + +/** + * Normalize the sum, making all coefficients integral and their gcd one. + * If followLCoeffSign is true, the leading coefficient is made positive, + * possibly negating all other coefficients. If this is the case return true to + * indicate that the relational operator needs to be negated. + * Otherwise return false. + */ +bool normalizeGCDLCM(Sum& sum, bool followLCoeffSign = false) +{ + if (sum.empty()) return false; + Integer denLCM(1); + Integer numGCD; + auto it = sum.begin(); + if (!it->first.isConst()) + { + Rational r = it->second.toRational(); + denLCM = r.getDenominator(); + numGCD = r.getNumerator().abs(); + } + ++it; + for (; it != sum.end(); ++it) + { + if (it->first.isConst()) continue; + Assert(it->second.isRational()); + Rational r = it->second.toRational(); + denLCM = denLCM.lcm(r.getDenominator()); + if (numGCD.isZero()) + numGCD = r.getNumerator().abs(); + else + numGCD = numGCD.gcd(r.getNumerator().abs()); + } + if (numGCD.isZero()) return false; + Rational mult(denLCM, numGCD); + + bool negate = false; + if (followLCoeffSign) + { + if (sgn(getLTerm(sum).second) < 0) + { + negate = true; + mult = -mult; + } + } + + for (auto& s : sum) + { + s.second *= mult; + } + return negate; +} + +std::pair removeMinAbsCoeff(Sum& sum) +{ + auto minit = getLTermIt(sum); + for (auto it = minit; it != sum.end(); ++it) + { + if (it->first.isConst()) continue; + if (it->second.toRational().absCmp(minit->second.toRational()) < 0) + { + minit = it; + } + } + if (minit == sum.end()) + { + return std::make_pair(mkConst(Integer(1)), Integer(0)); + } + Assert(minit != sum.end()); + auto res = *minit; + sum.erase(minit); + return res; +} + +RealAlgebraicNumber removeConstant(Sum& sum) +{ + RealAlgebraicNumber res; + if (!sum.empty()) + { + auto constantit = sum.begin(); + if (constantit->first.isConst()) + { + Assert(constantit->first.getConst().isOne()); + res = constantit->second; + sum.erase(constantit); + } + } + return res; +} + +std::pair removeLTerm(Sum& sum) +{ + auto it = getLTermIt(sum); + if (it == sum.end()) + { + return std::make_pair(mkConst(Integer(1)), Integer(0)); + } + Assert(it != sum.end()); + auto res = *it; + sum.erase(it); + return res; +} + +} // namespace + +std::optional tryEvaluateRelation(Kind rel, TNode left, TNode right) +{ + if (left.isConst()) + { + const Rational& l = left.getConst(); + if (right.isConst()) + { + const Rational& r = right.getConst(); + return evaluateRelation(rel, l, r); + } + else if (right.getKind() == Kind::REAL_ALGEBRAIC_NUMBER) + { + const RealAlgebraicNumber& r = + right.getOperator().getConst(); + return evaluateRelation(rel, l, r); + } + } + else if (left.getKind() == Kind::REAL_ALGEBRAIC_NUMBER) + { + const RealAlgebraicNumber& l = + left.getOperator().getConst(); + if (right.isConst()) + { + const Rational& r = right.getConst(); + return evaluateRelation(rel, l, r); + } + else if (right.getKind() == Kind::REAL_ALGEBRAIC_NUMBER) + { + const RealAlgebraicNumber& r = + right.getOperator().getConst(); + return evaluateRelation(rel, l, r); + } + } + return {}; +} + +std::optional tryEvaluateRelationReflexive(TNode atom) +{ + if (atom.getNumChildren() == 2 && atom[0] == atom[1]) + { + switch (atom.getKind()) + { + case Kind::LT: return false; + case Kind::LEQ: return true; + case Kind::EQUAL: return true; + case Kind::DISTINCT: return false; + case Kind::GEQ: return true; + case Kind::GT: return false; + default:; + } + } + return {}; +} + +Node buildRelation(Kind kind, Node left, Node right, bool negate) +{ + if (auto response = tryEvaluateRelation(kind, left, right); response) + { + return mkConst(*response != negate); + } + if (negate) + { + return NodeManager::currentNM()->mkNode(kind, left, right).notNode(); + } + return NodeManager::currentNM()->mkNode(kind, left, right); +} + +Node buildIntegerEquality(Sum&& sum) +{ + normalizeGCDLCM(sum); + + const auto& constant = *sum.begin(); + if (constant.first.isConst()) + { + Assert(constant.second.isRational()); + if (!constant.second.toRational().isIntegral()) + { + return mkConst(false); + } + } + + auto minabscoeff = removeMinAbsCoeff(sum); + if (sgn(minabscoeff.second) < 0) + { + // move minabscoeff goes to the right and switch lhs and rhs + minabscoeff.second = -minabscoeff.second; + } + else + { + // move the sum to the right + for (auto& s : sum) s.second = -s.second; + } + Node left = mkMultTerm(minabscoeff.second, minabscoeff.first); + + return buildRelation(Kind::EQUAL, left, collectSum(sum)); +} + +Node buildRealEquality(Sum&& sum) +{ + auto lterm = removeLTerm(sum); + if (isZero(lterm.second)) + { + return buildRelation(Kind::EQUAL, mkConst(Integer(0)), collectSum(sum)); + } + RealAlgebraicNumber lcoeff = -lterm.second; + for (auto& s : sum) + { + s.second = s.second / lcoeff; + } + return buildRelation(Kind::EQUAL, lterm.first, collectSum(sum)); +} + +Node buildIntegerInequality(Sum&& sum, Kind k) +{ + bool negate = normalizeGCDLCM(sum, true); + + if (negate) + { + k = (k == Kind::GEQ) ? Kind::GT : Kind::GEQ; + } + + RealAlgebraicNumber constant = removeConstant(sum); + Assert(constant.isRational()); + Rational rhs = -constant.toRational(); + + if (rhs.isIntegral() && k == Kind::GT) + { + rhs += 1; + } + else + { + rhs = rhs.ceiling(); + } + auto* nm = NodeManager::currentNM(); + return buildRelation(Kind::GEQ, collectSum(sum), nm->mkConstInt(rhs), negate); +} + +Node buildRealInequality(Sum&& sum, Kind k) +{ + normalizeLCoeffAbsOne(sum); + Node rhs = mkConst(-removeConstant(sum)); + return buildRelation(k, collectSum(sum), rhs); +} + +} // namespace rewriter +} // namespace arith +} // namespace theory +} // namespace cvc5 \ No newline at end of file diff --git a/src/theory/arith/rewriter/rewrite_atom.h b/src/theory/arith/rewriter/rewrite_atom.h new file mode 100644 index 000000000..2648228bd --- /dev/null +++ b/src/theory/arith/rewriter/rewrite_atom.h @@ -0,0 +1,95 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Utilities for rewriting atoms in the arithmetic rewriter. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__ARITH__REWRITER__REWRITE_ATOM_H +#define CVC5__THEORY__ARITH__REWRITER__REWRITE_ATOM_H + +#include + +#include "expr/node.h" +#include "theory/arith/rewriter/addition.h" + +namespace cvc5 { +namespace theory { +namespace arith { +namespace rewriter { + +/** + * Tries to evaluate the given relation. Returns std::nullopt if either left + * or right is not a value (constant or a real algebraic number). + * Assumes rel to be a relational operator, i.e. one of <,<=,=,!=,>=,>. + */ +std::optional tryEvaluateRelation(Kind rel, TNode left, TNode right); + +/** + * Tries to evaluate a reflexive relation. Returns std::nullopt if the atom + * is either not a relational operator or not reflexive (i.e. the two terms are + * not identical). + * Assumes atom to be a relational operator, i.e. one of <,<=,=,!=,>=,>. + */ +std::optional tryEvaluateRelationReflexive(TNode atom); + +/** + * Build a node `(kind left right)`. If negate is true, it returns the negation + * of this as `(not (kind left right))`. Before doing so, try to evaluate it to + * true or false using the tryEvaluateRelation method. + */ +Node buildRelation(Kind kind, Node left, Node right, bool negate = false); + +/** + * Build an integer equality from the given sum. The result is equivalent to the + * sum being equal to zero. We first normalize the non-constant coefficients to + * integers (using GCD and LCM). If the coefficient is non-integral after that, + * the result is false. We then put the term with minimal absolute coefficient + * to the left side of the equality and make its coefficient positive. + * The sum is taken as rvalue as it is modified in the process. + */ +Node buildIntegerEquality(Sum&& sum); + +/** + * Build a real equality from the given sum. The result is equivalent to the sum + * being equal to zero. We first extract the leading term and normalize its + * coefficient to be plus or minus one. The result is the (normalized) leading + * term being equal to the rest of the sum. + * The sum is taken as rvalue as it is modified in the process. + */ +Node buildRealEquality(Sum&& sum); + +/** + * Build an integer inequality from the given sum. The result is equivalent to + * `(k sum 0)`. We first normalize the non-constant coefficients to integers + * (using GCD and LCM), tighten the inequality if possible and turn it into a + * weak inequality. The result is the resulting sum compared with the constant + * where the overall inequalit is possibly negated. + * The sum is taken as rvalue as it is modified in the process. + */ +Node buildIntegerInequality(Sum&& sum, Kind k); + +/** + * Build a real inequality from the given sum. The result is equivalent to + * `(k sum 0)`. We normalize the leading coefficient to be one or minus one. + * The result is the resulting sum compared with the constant. + * The sum is taken as rvalue as it is modified in the process. + */ +Node buildRealInequality(Sum&& sum, Kind k); + +} // namespace rewriter +} // namespace arith +} // namespace theory +} // namespace cvc5 + +#endif