From 3daaecd22fe5f6147cb08e5a4e08177b33a2daa2 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 3 Aug 2012 20:39:25 +0000
Subject: fix uses of getMetaKind() from outside the expr package.  (they now
 use isConst() and isVar() as appropriate)

also some base infrastructure for the new ::isConst().
---
 src/theory/arith/arith_rewriter.cpp | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

(limited to 'src/theory/arith/arith_rewriter.cpp')

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index d7a6c0443..6b38dacce 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -30,23 +30,19 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-bool isVariable(TNode t){
-  return t.getMetaKind() == kind::metakind::VARIABLE;
-}
-
 bool ArithRewriter::isAtom(TNode n) {
   return arith::isRelationOperator(n.getKind());
 }
 
 RewriteResponse ArithRewriter::rewriteConstant(TNode t){
-  Assert(t.getMetaKind() == kind::metakind::CONSTANT);
+  Assert(t.isConst());
   Assert(t.getKind() == kind::CONST_RATIONAL);
 
   return RewriteResponse(REWRITE_DONE, t);
 }
 
 RewriteResponse ArithRewriter::rewriteVariable(TNode t){
-  Assert(isVariable(t));
+  Assert(t.isVar());
 
   return RewriteResponse(REWRITE_DONE, t);
 }
@@ -82,9 +78,9 @@ RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){
 }
 
 RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
-  if(t.getMetaKind() == kind::metakind::CONSTANT){
+  if(t.isConst()){
     return rewriteConstant(t);
-  }else if(isVariable(t)){
+  }else if(t.isVar()){
     return rewriteVariable(t);
   }else if(t.getKind() == kind::MINUS){
     return rewriteMinus(t, true);
@@ -116,9 +112,9 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   }
 }
 RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
-  if(t.getMetaKind() == kind::metakind::CONSTANT){
+  if(t.isConst()){
     return rewriteConstant(t);
-  }else if(isVariable(t)){
+  }else if(t.isVar()){
     return rewriteVariable(t);
   }else if(t.getKind() == kind::MINUS){
     return rewriteMinus(t, false);
-- 
cgit v1.2.3