This is a coarse grained proof rule for showing that two terms are equivalent up to polynomial normalization. It will be used as a hard coded case in proof reconstruction with DSL granularity.
theory/arith/arith_ite_utils.h
theory/arith/arith_msum.cpp
theory/arith/arith_msum.h
+ theory/arith/arith_poly_norm.cpp
+ theory/arith/arith_poly_norm.h
theory/arith/arith_preprocess.cpp
theory/arith/arith_preprocess.h
theory/arith/arith_rewriter.cpp
case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
+ case PfRule::ARITH_POLY_NORM: return "ARITH_POLY_NORM";
case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";
case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG";
case PfRule::ARITH_TRANS_EXP_POSITIVITY:
// ---------------------
// Conclusion: arith::OperatorElim::getAxiomFor(t)
ARITH_OP_ELIM_AXIOM,
+ // ======== Arithmetic polynomial normalization
+ // Children: none
+ // Arguments: ((= t s))
+ // ---------------------
+ // Conclusion: (= t s)
+ // where arith::PolyNorm::isArithPolyNorm(t, s) = true
+ ARITH_POLY_NORM,
//======== Multiplication sign inference
// Children: none
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Arithmetic utility for polynomial normalization
+ */
+
+#include "theory/arith/arith_poly_norm.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+
+void PolyNorm::addMonomial(TNode x, const Rational& c, bool isNeg)
+{
+ Assert(c.sgn() != 0);
+ std::unordered_map<Node, Rational>::iterator it = d_polyNorm.find(x);
+ if (it == d_polyNorm.end())
+ {
+ d_polyNorm[x] = isNeg ? -c : c;
+ return;
+ }
+ Rational res(it->second + (isNeg ? -c : c));
+ if (res.sgn() == 0)
+ {
+ // cancels
+ d_polyNorm.erase(it);
+ }
+ else
+ {
+ d_polyNorm[x] = res;
+ }
+}
+
+void PolyNorm::multiplyMonomial(TNode x, const Rational& c)
+{
+ Assert(c.sgn() != 0);
+ if (x.isNull())
+ {
+ // multiply by constant
+ for (std::pair<const Node, Rational>& m : d_polyNorm)
+ {
+ // c1*x*c2 = (c1*c2)*x
+ m.second *= c;
+ }
+ }
+ else
+ {
+ std::unordered_map<Node, Rational> ptmp = d_polyNorm;
+ d_polyNorm.clear();
+ for (const std::pair<const Node, Rational>& m : ptmp)
+ {
+ // c1*x1*c2*x2 = (c1*c2)*(x1*x2)
+ Node newM = multMonoVar(m.first, x);
+ d_polyNorm[newM] = m.second * c;
+ }
+ }
+}
+
+void PolyNorm::add(const PolyNorm& p)
+{
+ for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
+ {
+ addMonomial(m.first, m.second);
+ }
+}
+
+void PolyNorm::subtract(const PolyNorm& p)
+{
+ for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
+ {
+ addMonomial(m.first, m.second, true);
+ }
+}
+
+void PolyNorm::multiply(const PolyNorm& p)
+{
+ if (p.d_polyNorm.size() == 1)
+ {
+ for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
+ {
+ multiplyMonomial(m.first, m.second);
+ }
+ }
+ else
+ {
+ // If multiplying by sum, must distribute; if multiplying by zero, clear.
+ // First, remember the current state and clear.
+ std::unordered_map<Node, Rational> ptmp = d_polyNorm;
+ d_polyNorm.clear();
+ for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
+ {
+ PolyNorm pbase;
+ pbase.d_polyNorm = ptmp;
+ pbase.multiplyMonomial(m.first, m.second);
+ // add this to current
+ add(pbase);
+ }
+ }
+}
+
+void PolyNorm::clear() { d_polyNorm.clear(); }
+
+bool PolyNorm::empty() const { return d_polyNorm.empty(); }
+
+bool PolyNorm::isEqual(const PolyNorm& p) const
+{
+ if (d_polyNorm.size() != p.d_polyNorm.size())
+ {
+ return false;
+ }
+ std::unordered_map<Node, Rational>::const_iterator it;
+ for (const std::pair<const Node, Rational>& m : d_polyNorm)
+ {
+ Assert(m.second.sgn() != 0);
+ it = p.d_polyNorm.find(m.first);
+ if (it == p.d_polyNorm.end() || m.second != it->second)
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+Node PolyNorm::multMonoVar(TNode m1, TNode m2)
+{
+ std::vector<TNode> vars = getMonoVars(m1);
+ std::vector<TNode> vars2 = getMonoVars(m2);
+ vars.insert(vars.end(), vars2.begin(), vars2.end());
+ if (vars.empty())
+ {
+ // constants
+ return Node::null();
+ }
+ else if (vars.size() == 1)
+ {
+ return vars[0];
+ }
+ // use default sorting
+ std::sort(vars.begin(), vars.end());
+ return NodeManager::currentNM()->mkNode(NONLINEAR_MULT, vars);
+}
+
+std::vector<TNode> PolyNorm::getMonoVars(TNode m)
+{
+ std::vector<TNode> vars;
+ // m is null if this is the empty variable (for constant monomials)
+ if (!m.isNull())
+ {
+ Kind k = m.getKind();
+ Assert(k != CONST_RATIONAL);
+ if (k == MULT || k == NONLINEAR_MULT)
+ {
+ vars.insert(vars.end(), m.begin(), m.end());
+ }
+ else
+ {
+ vars.push_back(m);
+ }
+ }
+ return vars;
+}
+
+PolyNorm PolyNorm::mkPolyNorm(TNode n)
+{
+ Assert(n.getType().isReal());
+ Rational one(1);
+ Node null;
+ std::unordered_map<TNode, PolyNorm> visited;
+ std::unordered_map<TNode, PolyNorm>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ it = visited.find(cur);
+ Kind k = cur.getKind();
+ if (it == visited.end())
+ {
+ if (k == CONST_RATIONAL)
+ {
+ Rational r = cur.getConst<Rational>();
+ if (r.sgn() == 0)
+ {
+ // zero is not an entry
+ visited[cur] = PolyNorm();
+ }
+ else
+ {
+ visited[cur].addMonomial(null, r);
+ }
+ }
+ else if (k == PLUS || k == MINUS || k == UMINUS || k == MULT
+ || k == NONLINEAR_MULT)
+ {
+ visited[cur] = PolyNorm();
+ for (const Node& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ else
+ {
+ // it is a leaf
+ visited[cur].addMonomial(cur, one);
+ visit.pop_back();
+ }
+ continue;
+ }
+ visit.pop_back();
+ if (it->second.empty())
+ {
+ PolyNorm& ret = visited[cur];
+ switch (k)
+ {
+ case PLUS:
+ case MINUS:
+ case UMINUS:
+ case MULT:
+ case NONLINEAR_MULT:
+ for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
+ {
+ it = visited.find(cur[i]);
+ Assert(it != visited.end());
+ if ((k == MINUS && i == 1) || k == UMINUS)
+ {
+ ret.subtract(it->second);
+ }
+ else if (i > 0 && (k == MULT || k == NONLINEAR_MULT))
+ {
+ ret.multiply(it->second);
+ }
+ else
+ {
+ ret.add(it->second);
+ }
+ }
+ break;
+ case CONST_RATIONAL: break;
+ default: Unhandled() << "Unhandled polynomial operation " << cur; break;
+ }
+ }
+ } while (!visit.empty());
+ Assert(visited.find(n) != visited.end());
+ return visited[n];
+}
+
+bool PolyNorm::isArithPolyNorm(TNode a, TNode b)
+{
+ PolyNorm pa = PolyNorm::mkPolyNorm(a);
+ PolyNorm pb = PolyNorm::mkPolyNorm(b);
+ return pa.isEqual(pb);
+}
+
+} // namespace arith
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Arithmetic utility for polynomial normalization
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__ARITH__POLY_NORM_H
+#define CVC5__THEORY__ARITH__POLY_NORM_H
+
+#include <unordered_map>
+
+#include "expr/node.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+
+/**
+ * A utility class for polynomial normalization. This is used by the proof
+ * rule PfRule::ARITH_POLY_NORM.
+ */
+class PolyNorm
+{
+ public:
+ /**
+ * Add the monomial x*c to this polynomial.
+ * If x is null, then x*c is treated as c.
+ */
+ void addMonomial(TNode x, const Rational& c, bool isNeg = false);
+ /**
+ * Multiply this polynomial by the monomial x*c, where c is a CONST_RATIONAL.
+ * If x is null, then x*c is treated as c.
+ */
+ void multiplyMonomial(TNode x, const Rational& c);
+ /** Add polynomial p to this one. */
+ void add(const PolyNorm& p);
+ /** Subtract polynomial p from this one. */
+ void subtract(const PolyNorm& p);
+ /** Multiply this polynomial by p */
+ void multiply(const PolyNorm& p);
+ /** Clear this polynomial */
+ void clear();
+ /** Return true if this polynomial is empty */
+ bool empty() const;
+ /** Is this polynomial equal to polynomial p? */
+ bool isEqual(const PolyNorm& p) const;
+ /**
+ * Make polynomial from real term n. This method normalizes applications
+ * of operators PLUS, MINUS, UMINUS, MULT, and NONLINEAR_MULT only.
+ */
+ static PolyNorm mkPolyNorm(TNode n);
+ /** Do a and b normalize to the same polynomial? */
+ static bool isArithPolyNorm(TNode a, TNode b);
+
+ private:
+ /**
+ * Given two terms that are variables in monomials, return the
+ * variable for the monomial when they are multiplied.
+ */
+ static Node multMonoVar(TNode m1, TNode m2);
+ /** Get the list of variables whose product is m */
+ static std::vector<TNode> getMonoVars(TNode m);
+ /** The data, mapping monomial variables to coefficients */
+ std::unordered_map<Node, Rational> d_polyNorm;
+};
+
+} // namespace arith
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__ARITH__POLY_NORM_H */
#include <set>
#include "expr/skolem_manager.h"
+#include "theory/arith/arith_poly_norm.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/constraint.h"
#include "theory/arith/normal_form.h"
pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this);
pc->registerChecker(PfRule::ARITH_MULT_POS, this);
pc->registerChecker(PfRule::ARITH_MULT_NEG, this);
+ pc->registerChecker(PfRule::ARITH_POLY_NORM, this);
}
Node ArithProofRuleChecker::checkInternal(PfRule id,
Assert(args.size() == 1);
return OperatorElim::getAxiomFor(args[0]);
}
+ case PfRule::ARITH_POLY_NORM:
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ if (args[0].getKind() != kind::EQUAL)
+ {
+ return Node::null();
+ }
+ if (!PolyNorm::isArithPolyNorm(args[0][0], args[0][1]))
+ {
+ return Node::null();
+ }
+ return args[0];
+ }
default: return Node::null();
}
}
cvc5_add_unit_test_white(theory_strings_word_white theory)
cvc5_add_unit_test_white(theory_white theory)
cvc5_add_unit_test_white(type_enumerator_white theory)
+cvc5_add_unit_test_white(arith_poly_white theory)
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for arithmetic polynomial normalization.
+ */
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "test_smt.h"
+#include "theory/arith/arith_poly_norm.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+
+using namespace theory;
+using namespace theory::arith;
+using namespace kind;
+
+namespace test {
+
+class TestTheoryWhiteArithPolyNorm : public TestSmt
+{
+ protected:
+ void SetUp() override { TestSmt::SetUp(); }
+};
+
+TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int)
+{
+ TypeNode intType = d_nodeManager->integerType();
+ Node zero = d_nodeManager->mkConst(Rational(0));
+ Node one = d_nodeManager->mkConst(Rational(1));
+ Node two = d_nodeManager->mkConst(Rational(2));
+ Node x = d_nodeManager->mkVar("x", intType);
+ Node y = d_nodeManager->mkVar("y", intType);
+ Node z = d_nodeManager->mkVar("z", intType);
+ Node w = d_nodeManager->mkVar("w", intType);
+
+ Node t1, t2;
+
+ t1 = zero;
+ t2 = one;
+ ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(PLUS, x, y);
+ t2 = d_nodeManager->mkNode(PLUS, y, d_nodeManager->mkNode(MULT, one, x));
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t2 = d_nodeManager->mkNode(PLUS, x, x, y);
+ ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(PLUS, x, d_nodeManager->mkNode(MULT, y, zero));
+ t2 = x;
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(MULT, y, d_nodeManager->mkNode(PLUS, one, one));
+ t2 = d_nodeManager->mkNode(PLUS, y, y);
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(MULT,
+ d_nodeManager->mkNode(PLUS, one, zero),
+ d_nodeManager->mkNode(PLUS, x, y));
+ t2 = d_nodeManager->mkNode(PLUS, x, y);
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(PLUS, {x, y, z, w, y});
+ t2 = d_nodeManager->mkNode(PLUS, {w, y, y, z, x});
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(MINUS, t1, t2);
+ t2 = zero;
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(UMINUS, d_nodeManager->mkNode(PLUS, x, y));
+ t2 = d_nodeManager->mkNode(MINUS, zero, d_nodeManager->mkNode(PLUS, y, x));
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, x), y);
+ t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, y), x);
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(PLUS, y, z));
+ t2 = d_nodeManager->mkNode(PLUS,
+ d_nodeManager->mkNode(MULT, x, y),
+ d_nodeManager->mkNode(MULT, z, x));
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+}
+
+TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_real)
+{
+ TypeNode realType = d_nodeManager->realType();
+ Node zero = d_nodeManager->mkConst(Rational(0));
+ Node one = d_nodeManager->mkConst(Rational(1));
+ Node half = d_nodeManager->mkConst(Rational(1) / Rational(2));
+ Node two = d_nodeManager->mkConst(Rational(2));
+ Node x = d_nodeManager->mkVar("x", realType);
+ Node y = d_nodeManager->mkVar("y", realType);
+
+ Node t1, t2;
+
+ t1 = d_nodeManager->mkNode(PLUS, x, y, y);
+ t2 = d_nodeManager->mkNode(PLUS, y, x, y);
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = one;
+ t2 = d_nodeManager->mkNode(MULT, two, half);
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+
+ t1 = d_nodeManager->mkNode(PLUS, y, x);
+ t2 = d_nodeManager->mkNode(
+ MULT,
+ d_nodeManager->mkNode(PLUS,
+ d_nodeManager->mkNode(MULT, half, x),
+ d_nodeManager->mkNode(MULT, half, y)),
+ two);
+ ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
+}
+
+} // namespace test
+} // namespace cvc5
projects / cvc5.git / commitdiff