From: Andrew Reynolds Date: Fri, 29 Oct 2021 16:36:26 +0000 (-0500) Subject: Add PfRule ARITH_POLY_NORM (#7501) X-Git-Tag: cvc5-1.0.0~932 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f12af39c6ac5f19913b9e9996eb9453eb7b30034;p=cvc5.git Add PfRule ARITH_POLY_NORM (#7501) 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. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 201ab6eb2..d87d51559 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -379,6 +379,8 @@ libcvc5_add_sources( 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 diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index d4e763fe6..c82928dc5 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -171,6 +171,7 @@ const char* toString(PfRule id) 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: diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 25bbf3d34..d9e92fa92 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1153,6 +1153,13 @@ enum class PfRule : uint32_t // --------------------- // 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 diff --git a/src/theory/arith/arith_poly_norm.cpp b/src/theory/arith/arith_poly_norm.cpp new file mode 100644 index 000000000..81cd3646a --- /dev/null +++ b/src/theory/arith/arith_poly_norm.cpp @@ -0,0 +1,268 @@ +/****************************************************************************** + * 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::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& m : d_polyNorm) + { + // c1*x*c2 = (c1*c2)*x + m.second *= c; + } + } + else + { + std::unordered_map ptmp = d_polyNorm; + d_polyNorm.clear(); + for (const std::pair& 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& m : p.d_polyNorm) + { + addMonomial(m.first, m.second); + } +} + +void PolyNorm::subtract(const PolyNorm& p) +{ + for (const std::pair& 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& 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 ptmp = d_polyNorm; + d_polyNorm.clear(); + for (const std::pair& 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::const_iterator it; + for (const std::pair& 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 vars = getMonoVars(m1); + std::vector 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 PolyNorm::getMonoVars(TNode m) +{ + std::vector 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 visited; + std::unordered_map::iterator it; + std::vector 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(); + 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 diff --git a/src/theory/arith/arith_poly_norm.h b/src/theory/arith/arith_poly_norm.h new file mode 100644 index 000000000..9c3cbcf95 --- /dev/null +++ b/src/theory/arith/arith_poly_norm.h @@ -0,0 +1,83 @@ +/****************************************************************************** + * 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 + +#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 getMonoVars(TNode m); + /** The data, mapping monomial variables to coefficients */ + std::unordered_map d_polyNorm; +}; + +} // namespace arith +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__ARITH__POLY_NORM_H */ diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 58de8e391..171cdf182 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -19,6 +19,7 @@ #include #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" @@ -38,6 +39,7 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc) 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, @@ -343,6 +345,20 @@ 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(); } } diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 2af747fd5..15c5e8570 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -42,3 +42,4 @@ cvc5_add_unit_test_white(theory_strings_utils_white theory) 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) diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp new file mode 100644 index 000000000..3e0bb6c17 --- /dev/null +++ b/test/unit/theory/arith_poly_white.cpp @@ -0,0 +1,132 @@ +/****************************************************************************** + * 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 +#include +#include + +#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