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().

4 files changed, 14 insertions, 18 deletions

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);
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index a478f3cfb..46b0264ea 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -135,7 +135,7 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
   case IMPLIES:
     // == 3-FINITE VALUE SET : Collect information ==
     if(n[1].getKind() == EQUAL &&
-       n[1][0].getMetaKind() == metakind::VARIABLE &&
+       n[1][0].isVar() &&
        defTrue.find(n) != defTrue.end()){
       Node eqTo = n[1][1];
       Node rewriteEqTo = Rewriter::rewrite(eqTo);
@@ -166,12 +166,12 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
       break;
     }
     Node var, c1, c2;
-    if(n[0][0].getMetaKind() == metakind::VARIABLE &&
-       n[0][1].getMetaKind() == metakind::CONSTANT) {
+    if(n[0][0].isVar() &&
+       n[0][1].isConst()) {
       var = n[0][0];
       c1 = n[0][1];
-    } else if(n[0][1].getMetaKind() == metakind::VARIABLE &&
-              n[0][0].getMetaKind() == metakind::CONSTANT) {
+    } else if(n[0][1].isVar() &&
+              n[0][0].isConst()) {
       var = n[0][1];
       c1 = n[0][0];
     } else {
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index b054f9804..33fc42cea 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -49,7 +49,7 @@ namespace arith {
  *
  * variable := n
  *   where
- *     n.getMetaKind() == metakind::VARIABLE or is foreign
+ *     n.isVar() or is foreign
  *     n.getType() \in {Integer, Real}
  *
  * constant := n
@@ -244,7 +244,7 @@ public:
   }
 
   bool isMetaKindVariable() const {
-    return getNode().getMetaKind() == kind::metakind::VARIABLE;
+    return getNode().isVar();
   }
 
   bool operator<(const Variable& v) const {
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d55860c41..6b7efa1ee 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -741,7 +741,7 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
   case kind::LT:
   case kind::GEQ:
   case kind::GT:
-    if (in[0].getMetaKind() == kind::metakind::VARIABLE) {
+    if (in[0].isVar()) {
       d_learner.addBound(in);
     }
     break;