From 593130c35c03da15bfd4bad794246fef0fd09a66 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 3 Feb 2022 02:15:15 -0800 Subject: [PATCH] Add node utils for the arithmetic rewriter (#8012) This PR adds a bunch of small utilities to inspect or create nodes in the arithmetic rewriter. --- src/CMakeLists.txt | 2 + src/theory/arith/rewriter/node_utils.cpp | 111 +++++++++++++++ src/theory/arith/rewriter/node_utils.h | 169 +++++++++++++++++++++++ 3 files changed, 282 insertions(+) create mode 100644 src/theory/arith/rewriter/node_utils.cpp create mode 100644 src/theory/arith/rewriter/node_utils.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 71fe64dfa..226f4632d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -498,6 +498,8 @@ libcvc5_add_sources( theory/arith/pp_rewrite_eq.h theory/arith/proof_checker.cpp theory/arith/proof_checker.h + theory/arith/rewriter/node_utils.cpp + theory/arith/rewriter/node_utils.h theory/arith/rewriter/ordering.h theory/arith/rewrites.cpp theory/arith/rewrites.h diff --git a/src/theory/arith/rewriter/node_utils.cpp b/src/theory/arith/rewriter/node_utils.cpp new file mode 100644 index 000000000..34c3849a0 --- /dev/null +++ b/src/theory/arith/rewriter/node_utils.cpp @@ -0,0 +1,111 @@ +/****************************************************************************** + * 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 nodes in the arithmetic rewriter. + */ + +#include "theory/arith/rewriter/node_utils.h" + +#include "base/check.h" +#include "theory/arith/rewriter/ordering.h" + +namespace cvc5 { +namespace theory { +namespace arith { +namespace rewriter { + +bool isIntegral(TNode n) +{ + std::vector queue = {n}; + while (!queue.empty()) + { + TNode cur = queue.back(); + queue.pop_back(); + + if (cur.isConst()) continue; + switch (cur.getKind()) + { + case Kind::LT: + case Kind::LEQ: + case Kind::EQUAL: + case Kind::DISTINCT: + case Kind::GEQ: + case Kind::GT: + queue.emplace_back(n[0]); + queue.emplace_back(n[1]); + break; + case Kind::ADD: + case Kind::NEG: + case Kind::SUB: + case Kind::MULT: + queue.insert(queue.end(), cur.begin(), cur.end()); + break; + default: + if (!cur.getType().isInteger()) return false; + } + } + return true; +} + +Node mkMultTerm(const Rational& multiplicity, TNode monomial) +{ + if (monomial.isConst()) + { + return mkConst(multiplicity * monomial.getConst()); + } + if (isOne(multiplicity)) + { + return monomial; + } + return NodeManager::currentNM()->mkNode( + Kind::MULT, mkConst(multiplicity), monomial); +} + +Node mkMultTerm(const RealAlgebraicNumber& multiplicity, TNode monomial) +{ + if (multiplicity.isRational()) + { + return mkMultTerm(multiplicity.toRational(), monomial); + } + if (monomial.isConst()) + { + return mkConst(multiplicity * monomial.getConst()); + } + std::vector prod; + prod.emplace_back(mkConst(multiplicity)); + prod.insert(prod.end(), monomial.begin(), monomial.end()); + Assert(prod.size() >= 2); + return NodeManager::currentNM()->mkNode(Kind::NONLINEAR_MULT, prod); +} + +Node mkMultTerm(const RealAlgebraicNumber& multiplicity, + std::vector&& monomial) +{ + if (monomial.empty()) + { + return mkConst(multiplicity); + } + if (multiplicity.isRational()) + { + std::sort(monomial.begin(), monomial.end(), rewriter::LeafNodeComparator()); + return mkMultTerm(multiplicity.toRational(), mkNonlinearMult(monomial)); + } + monomial.emplace_back(mkConst(multiplicity)); + std::sort(monomial.begin(), monomial.end(), rewriter::LeafNodeComparator()); + Assert(monomial.size() >= 2); + return NodeManager::currentNM()->mkNode(Kind::NONLINEAR_MULT, monomial); +} + +} // namespace rewriter +} // namespace arith +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/arith/rewriter/node_utils.h b/src/theory/arith/rewriter/node_utils.h new file mode 100644 index 000000000..f8e030386 --- /dev/null +++ b/src/theory/arith/rewriter/node_utils.h @@ -0,0 +1,169 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Node utilities for the arithmetic rewriter. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__ARITH__REWRITER__NODE_UTILS_H +#define CVC5__THEORY__ARITH__REWRITER__NODE_UTILS_H + +#include "base/check.h" +#include "expr/node.h" +#include "util/integer.h" +#include "util/rational.h" +#include "util/real_algebraic_number.h" + +namespace cvc5 { +namespace theory { +namespace arith { +namespace rewriter { + +/** + * Check whether the node is an arithmetic atom, that is one of LT, LEQ, EQUAL, + * GEQ, GT, IS_INTEGER, DIVISIBLE. + * Note that DISTINCT somehow belongs to this list, but should already be + * eliminated at this point. + */ +inline bool isAtom(TNode n) +{ + switch (n.getKind()) + { + case Kind::LT: + case Kind::LEQ: + case Kind::EQUAL: + case Kind::GEQ: + case Kind::GT: + case Kind::IS_INTEGER: + case Kind::DIVISIBLE: return true; + case Kind::DISTINCT: Unreachable(); return false; + default: return false; + } +} + +/** + * Check whether the given node can be rewritten to an integer node. This + * differs from checking the node type in two major ways: we consider relational + * operators integral if both children are integral in this sense; rational + * constants are always integral, as they are rewritten to integers by simple + * multiplication with their denominator. + */ +bool isIntegral(TNode n); + +/** Check whether the node wraps a real algebraic number. */ +inline bool isRAN(TNode n) +{ + return n.getKind() == Kind::REAL_ALGEBRAIC_NUMBER; +} +/** Retrieve the wrapped a real algebraic number. Asserts isRAN(n) */ +inline const RealAlgebraicNumber& getRAN(TNode n) +{ + Assert(isRAN(n)); + return n.getOperator().getConst(); +} + +/** + * Check whether the parent has a child that is a constant zero. If so, return + * this child. Otherwise, return std::nullopt. Works on any kind of iterable, + * i.e. both a node or a vector of nodes. + */ +template +std::optional getZeroChild(const Iterable& parent) +{ + for (const auto& node : parent) + { + if (node.isConst() && node.template getConst().isZero()) + { + return node; + } + } + return {}; +} + +/** Create a Boolean constant node */ +inline Node mkConst(bool value) +{ + return NodeManager::currentNM()->mkConst(value); +} +/** Create an integer constant node */ +inline Node mkConst(const Integer& value) +{ + return NodeManager::currentNM()->mkConstInt(value); +} +/** Create an integer or rational constant node */ +inline Node mkConst(const Rational& value) +{ + if (value.isIntegral()) + { + return NodeManager::currentNM()->mkConstInt(value); + } + return NodeManager::currentNM()->mkConstReal(value); +} +/** Create a real algebraic number node */ +inline Node mkConst(const RealAlgebraicNumber& value) +{ + return NodeManager::currentNM()->mkRealAlgebraicNumber(value); +} + +/** Make a nonlinear multiplication from the given factors */ +inline Node mkNonlinearMult(const std::vector& factors) +{ + auto* nm = NodeManager::currentNM(); + switch (factors.size()) + { + case 0: return nm->mkConstInt(Rational(1)); + case 1: return factors[0]; + default: return nm->mkNode(Kind::NONLINEAR_MULT, factors); + } +} + +/** + * Create the product of `multiplicity * monomial`. Assumes that the monomial is + * either a product of non-values (neither rational nor real algebraic numbers) + * or a rational constant. + * If the monomial is a constant, return the product of the two numbers. If the + * multiplicity is one, return the monomial. Otherwise return `(MULT + * multiplicity monomial)`. + */ +Node mkMultTerm(const Rational& multiplicity, TNode monomial); + +/** + * Create the product of `multiplicity * monomial`. Assumes that the monomial is + * either a product of non-values (neither rational nor real algebraic numbers) + * or a rational constant. + * If multiplicity is rational, defer to the appropriate overload. If the + * monomial is one, return the product of the two numbers. Otherwise return the + * nonlinear product of the two, i.e. `(NONLINEAR_MULT multiplicity *monomial)`. + */ +Node mkMultTerm(const RealAlgebraicNumber& multiplicity, TNode monomial); + +/** + * Create the product of `multiplicity * monomial`, where the monomial is given + * as the (implicitly multiplied, possibly unsorted) list of children. Assumes + * that monomial is either empty (implicitly one) or a list of non-values + * (neither rational nor real algebraic numbers). If multiplicity is rational, + * sort the monomial, create a nonlinear mult term and defer to the appropriate + * overload. Otherwise return the nonlinear product of the two, i.e. + * `(NONLINEAR_MULT multiplicity *monomial)`. The monomial is taken as rvalue as + * it may be modified in the process. + * + */ +Node mkMultTerm(const RealAlgebraicNumber& multiplicity, + std::vector&& monomial); + +} // namespace rewriter +} // namespace arith +} // namespace theory +} // namespace cvc5 + +#endif -- 2.30.2