Refactor rewriting of arithmetic leafs (#8177)

Minor refactoring of how we rewrite arithmetic leaf nodes (constants, algebraic numbers and "variables").

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a251d9e08cf92b76df31446d17c9d58670dcde09..38fb0d162905ced381c4d3cc5e6c1f5a4c16ee62 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -248,35 +248,6 @@ bool ArithRewriter::isAtom(TNode n) {
       || k == kind::DIVISIBLE;
 }
 
-RewriteResponse ArithRewriter::rewriteConstant(TNode t){
-  Assert(t.isConst());
-  Assert(t.getKind() == CONST_RATIONAL || t.getKind() == CONST_INTEGER);
-
-  return RewriteResponse(REWRITE_DONE, t);
-}
-
-RewriteResponse ArithRewriter::rewriteRAN(TNode t)
-{
-  Assert(t.getKind() == REAL_ALGEBRAIC_NUMBER);
-
-  const RealAlgebraicNumber& r =
-      t.getOperator().getConst<RealAlgebraicNumber>();
-  if (r.isRational())
-  {
-    return RewriteResponse(
-        REWRITE_DONE, NodeManager::currentNM()->mkConstReal(r.toRational()));
-  }
-
-  return RewriteResponse(REWRITE_DONE, t);
-}
-
-RewriteResponse ArithRewriter::rewriteVariable(TNode t)
-{
-  Assert(t.isVar());
-
-  return RewriteResponse(REWRITE_DONE, t);
-}
-
 RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
 {
   Assert(t.getKind() == kind::NEG);
@@ -319,7 +290,7 @@ RewriteResponse ArithRewriter::rewriteSub(TNode t)
 
 RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   if(t.isConst()){
-    return rewriteConstant(t);
+    return RewriteResponse(REWRITE_DONE, t);
   }else if(t.isVar()){
     return rewriteVariable(t);
   }else{
@@ -366,7 +337,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
 
 RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
   if(t.isConst()){
-    return rewriteConstant(t);
+    return RewriteResponse(REWRITE_DONE, t);
   }else if(t.isVar()){
     return rewriteVariable(t);
   }else{
@@ -458,6 +429,23 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
   }
 }
 
+RewriteResponse ArithRewriter::rewriteRAN(TNode t)
+{
+  Assert(rewriter::isRAN(t));
+  const RealAlgebraicNumber& r = rewriter::getRAN(t);
+  if (r.isRational())
+  {
+    return RewriteResponse(REWRITE_DONE, rewriter::mkConst(r.toRational()));
+  }
+  return RewriteResponse(REWRITE_DONE, t);
+}
+
+RewriteResponse ArithRewriter::rewriteVariable(TNode t)
+{
+  Assert(t.isVar());
+
+  return RewriteResponse(REWRITE_DONE, t);
+}
 
 RewriteResponse ArithRewriter::preRewritePlus(TNode t)
 {

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 7cf9a4f5b29362cc43a7a0a847ade537be7dcea6..c4590ffdc58d241af6c852704ec7840380e2f38f 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -49,8 +49,9 @@ class ArithRewriter : public TheoryRewriter
   static RewriteResponse preRewriteTerm(TNode t);
   static RewriteResponse postRewriteTerm(TNode t);
 
-  static RewriteResponse rewriteConstant(TNode t);
+  /** rewrite real algebraic numbers */
   static RewriteResponse rewriteRAN(TNode t);
+  /** rewrite variables */
   static RewriteResponse rewriteVariable(TNode t);
 
   /** rewrite unary minus */