From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 14 Jan 2022 15:36:17 +0000 (-0800)
Subject: Add RAN support in UMINUS rewriter (#7933)
X-Git-Tag: cvc5-1.0.0~548
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=554d96c4c74118ad4078eb12eccd537434baca41;p=cvc5.git

Add RAN support in UMINUS rewriter (#7933)

This adds rewriting for UMINUS of real algebraic numbers
---

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<RealAlgebraicNumber>();
+    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>(), 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