Refactor post rewriter for addition (#7931)

This makes the post rewriter for addition aware of real algebraic numbers. Also, it tries a bit harder to avoid the normal_form utilities if only constants are present.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index d865eebe99a172f4bb96ee30fedc800769afc495..3a355839de29966f1a6c14553c5342d234175472 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -513,28 +513,68 @@ RewriteResponse ArithRewriter::preRewritePlus(TNode t){
 
 RewriteResponse ArithRewriter::postRewritePlus(TNode t){
   Assert(t.getKind() == kind::PLUS);
+  Assert(t.getNumChildren() > 1);
 
+  Rational rational;
+  RealAlgebraicNumber ran;
   std::vector<Monomial> monomials;
   std::vector<Polynomial> polynomials;
 
-  for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){
-    TNode curr = *i;
-    if(Monomial::isMember(curr)){
-      monomials.push_back(Monomial::parseMonomial(curr));
-    }else{
-      polynomials.push_back(Polynomial::parsePolynomial(curr));
+  for (const auto& child : t)
+  {
+    if (child.isConst())
+    {
+      if (child.getConst<Rational>().isZero())
+      {
+        continue;
+      }
+      rational += child.getConst<Rational>();
+    }
+    else if (child.getKind() == Kind::REAL_ALGEBRAIC_NUMBER)
+    {
+      ran += child.getOperator().getConst<RealAlgebraicNumber>();
+    }
+    else if (Monomial::isMember(child))
+    {
+      monomials.emplace_back(Monomial::parseMonomial(child));
+    }
+    else
+    {
+      polynomials.emplace_back(Polynomial::parsePolynomial(child));
     }
   }
 
   if(!monomials.empty()){
     Monomial::sort(monomials);
     Monomial::combineAdjacentMonomials(monomials);
-    polynomials.push_back(Polynomial::mkPolynomial(monomials));
+    polynomials.emplace_back(Polynomial::mkPolynomial(monomials));
+  }
+  if (!rational.isZero())
+  {
+    polynomials.emplace_back(
+        Polynomial::mkPolynomial(Constant::mkConstant(rational)));
   }
 
-  Polynomial res = Polynomial::sumPolynomials(polynomials);
+  Polynomial poly = Polynomial::sumPolynomials(polynomials);
 
-  return RewriteResponse(REWRITE_DONE, res.getNode());
+  if (isZero(ran))
+  {
+    return RewriteResponse(REWRITE_DONE, poly.getNode());
+  }
+  if (poly.containsConstant())
+  {
+    ran += RealAlgebraicNumber(poly.getHead().getConstant().getValue());
+    poly = poly.getTail();
+  }
+
+  auto* nm = NodeManager::currentNM();
+  if (poly.isConstant())
+  {
+    return RewriteResponse(REWRITE_DONE, nm->mkRealAlgebraicNumber(ran));
+  }
+  return RewriteResponse(
+      REWRITE_DONE,
+      nm->mkNode(Kind::PLUS, nm->mkRealAlgebraicNumber(ran), poly.getNode()));
 }
 
 RewriteResponse ArithRewriter::postRewriteMult(TNode t){

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 9a0a3e26d7fa685000685383b0619045a1e34b2b..82e191d83a5d456a876298101bd55097c76b4d5c 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -23,6 +23,7 @@ cvc5_add_unit_test_white(strings_rewriter_white theory)
 cvc5_add_unit_test_white(theory_arith_pow2_white theory)
 cvc5_add_unit_test_white(theory_arith_white theory)
 cvc5_add_unit_test_white(theory_arith_cad_white theory)
+cvc5_add_unit_test_black(theory_arith_rewriter_black theory)
 cvc5_add_unit_test_white(theory_bags_normal_form_white theory)
 cvc5_add_unit_test_white(theory_bags_rewriter_white theory)
 cvc5_add_unit_test_white(theory_bags_type_rules_white theory)

diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp
new file mode 100644 (file)
index 0000000..99766e9
--- /dev/null
+++ b/test/unit/theory/theory_arith_rewriter_black.cpp
@@ -0,0 +1,52 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of rewriter for arithmetic.
+ */
+
+#include "test_smt.h"
+#include "util/rational.h"
+#include "util/real_algebraic_number.h"
+
+namespace cvc5 {
+
+using namespace kind;
+using namespace context;
+using namespace theory;
+
+namespace test {
+
+class TestTheoryArithRewriterBlack : public TestSmt
+{
+};
+
+TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber)
+{
+  Trace.on("arith-rewriter");
+  {
+    RealAlgebraicNumber two({-8, 0, 0, 1}, 1, 3);
+    Node n = d_nodeManager->mkRealAlgebraicNumber(two);
+    EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL);
+    EXPECT_EQ(n.getConst<Rational>(), Rational(2));
+  }
+  {
+    RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 3);
+    Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
+    n = d_nodeManager->mkNode(Kind::MINUS, n, n);
+    n = d_slvEngine->getRewriter()->rewrite(n);
+    EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL);
+    EXPECT_EQ(n.getConst<Rational>(), Rational(0));
+  }
+}
+
+}  // namespace test
+}  // namespace cvc5