Add RAN support in UMINUS rewriter (#7933)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 14 Jan 2022 15:36:17 +0000 (07:36 -0800)
committerGitHub <noreply@github.com>
Fri, 14 Jan 2022 15:36:17 +0000 (09:36 -0600)
This adds rewriting for UMINUS of real algebraic numbers

src/theory/arith/arith_rewriter.cpp
test/unit/theory/theory_arith_rewriter_black.cpp

index 9ccb6407f3c8bba1d467f42f92d58cb29fa7a3ae..1c955582099e356082b5aec092cf5a29e1aa6a4f 100644 (file)
@@ -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)
index ab3895cbbd054bbae711aef186757948d12507e3..a836cf8bda9fedab11d3edaf826bd91fee5d902a 100644 (file)
@@ -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