--- /dev/null
+/******************************************************************************
+ * 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<TNode> 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<Rational>());
+ }
+ 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<Rational>());
+ }
+ std::vector<Node> 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<Node>&& 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
--- /dev/null
+/******************************************************************************
+ * 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<RealAlgebraicNumber>();
+}
+
+/**
+ * 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 <typename Iterable>
+std::optional<TNode> getZeroChild(const Iterable& parent)
+{
+ for (const auto& node : parent)
+ {
+ if (node.isConst() && node.template getConst<Rational>().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<Node>& 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<Node>&& monomial);
+
+} // namespace rewriter
+} // namespace arith
+} // namespace theory
+} // namespace cvc5
+
+#endif
projects / cvc5.git / commitdiff