From 554d96c4c74118ad4078eb12eccd537434baca41 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 14 Jan 2022 07:36:17 -0800 Subject: [PATCH] Add RAN support in UMINUS rewriter (#7933) This adds rewriting for UMINUS of real algebraic numbers --- src/theory/arith/arith_rewriter.cpp | 7 +++++++ test/unit/theory/theory_arith_rewriter_black.cpp | 14 ++++++++++++++ 2 files changed, 21 insertions(+) diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 9ccb6407f..1c9555820 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -279,6 +279,13 @@ RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ return RewriteResponse(REWRITE_DONE, nm->mkConstRealOrInt(t[0].getType(), neg)); } + if (t[0].getKind() == Kind::REAL_ALGEBRAIC_NUMBER) + { + const RealAlgebraicNumber& r = + t[0].getOperator().getConst(); + NodeManager* nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, nm->mkRealAlgebraicNumber(-r)); + } Node noUminus = makeUnaryMinusNode(t[0]); if(pre) diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp index ab3895cbb..a836cf8bd 100644 --- a/test/unit/theory/theory_arith_rewriter_black.cpp +++ b/test/unit/theory/theory_arith_rewriter_black.cpp @@ -55,6 +55,20 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber) EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL); EXPECT_EQ(n.getConst(), Rational(0)); } + { + RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1); + RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2); + Node m = d_nodeManager->mkRealAlgebraicNumber(msqrt2); + Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2); + Node mm = d_nodeManager->mkNode(Kind::UMINUS, m); + Node mn = d_nodeManager->mkNode(Kind::UMINUS, n); + mm = d_slvEngine->getRewriter()->rewrite(mm); + mn = d_slvEngine->getRewriter()->rewrite(mn); + EXPECT_EQ(-msqrt2, sqrt2); + EXPECT_EQ(-sqrt2, msqrt2); + EXPECT_EQ(mm, n); + EXPECT_EQ(mn, m); + } } } // namespace test -- 2.30.2