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

17 files changed, 60 insertions, 48 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;
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 5add52d1f..47f3e31db 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -280,11 +280,11 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
     {
       d_ppFacts.push_back(in);
       d_ppEqualityEngine.assertEquality(in, true, in);
-      if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+      if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+      if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
         outSubstitutions.addSubstitution(in[1], in[0]);
         return PP_ASSERT_STATUS_SOLVED;
       }
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 63b44f7ca..1018289ab 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -366,7 +366,7 @@ bool CircuitPropagator::propagate() {
     Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl;
 
     // Is this an atom
-    bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.getMetaKind() == kind::metakind::VARIABLE;
+    bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar();
 
     // If an atom, add to the list for simplification
     if (atom) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b6dcc6662..2bb4857a3 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -154,12 +154,12 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
   switch(in.getKind()) {
   case kind::EQUAL:
 
-    if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+    if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
       ++(d_statistics.d_solveSubstitutions);
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+    if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
       ++(d_statistics.d_solveSubstitutions);
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 896133e46..39e5bc599 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -425,8 +425,8 @@ Node RewriteRule<MultDistribConst>::apply(TNode node) {
 template<> inline
 bool RewriteRule<SolveEq>::applies(TNode node) {
   if (node.getKind() != kind::EQUAL ||
-      (node[0].getMetaKind() == kind::metakind::VARIABLE && !node[1].hasSubterm(node[0])) ||
-      (node[1].getMetaKind() == kind::metakind::VARIABLE && !node[0].hasSubterm(node[1]))) {
+      (node[0].isVar() && !node[1].hasSubterm(node[0])) ||
+      (node[1].isVar() && !node[0].hasSubterm(node[1]))) {
     return false;
   }
   return true;
diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator
index 73b88986b..73fc6706d 100755
--- a/src/theory/mkinstantiator
+++ b/src/theory/mkinstantiator
@@ -143,6 +143,12 @@ function typerule {
   check_theory_seen
 }
 
+function construle {
+  # construle OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function rewriter {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index ffdc1d4c6..0d00b616c 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -118,6 +118,12 @@ function typerule {
   check_theory_seen
 }
 
+function construle {
+  # construle OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function rewriter {
   # rewriter class header
   class="$1"
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 3607d5232..60ff05d35 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -232,6 +232,12 @@ function typerule {
   check_theory_seen
 }
 
+function construle {
+  # construle OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function instantiator {
   # instantiator class header
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index feedc0c31..882a3034a 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -157,16 +157,14 @@ void TheoryModel::toStream( std::ostream& out ){
 Node TheoryModel::getValue( TNode n ){
   Debug("model") << "TheoryModel::getValue " << n << std::endl;
 
-  kind::MetaKind metakind = n.getMetaKind();
-
   //// special case: prop engine handles boolean vars
-  //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) {
+  //if(n.isVar() && n.getType().isBoolean()) {
   //  Debug("model") << "-> Propositional variable." << std::endl;
   //  return d_te->getPropEngine()->getValue( n );
   //}
 
   // special case: value of a constant == itself
-  if(metakind == kind::metakind::CONSTANT) {
+  if(n.isConst()) {
     Debug("model") << "-> Constant." << std::endl;
     return n;
   }
@@ -174,7 +172,7 @@ Node TheoryModel::getValue( TNode n ){
   Node nn;
   if( n.getNumChildren()>0 ){
     std::vector< Node > children;
-    if( metakind == kind::metakind::PARAMETERIZED ){
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
       Debug("model-debug") << "get operator: " << n.getOperator() << std::endl;
       children.push_back( n.getOperator() );
     }
@@ -194,7 +192,7 @@ Node TheoryModel::getValue( TNode n ){
   nn = Rewriter::rewrite( nn );
 
   // special case: value of a constant == itself
-  if(metakind == kind::metakind::CONSTANT) {
+  if(n.isConst()) {
     Debug("model") << "-> Theory-interpreted term." << std::endl;
     return nn;
   }else{
@@ -444,7 +442,7 @@ void TheoryEngineModelBuilder::buildModel( Model* m ){
     while( !eqc_i.isFinished() ){
       Node n = *eqc_i;
       //check if this is constant, if so, we will use it as representative
-      if( n.getMetaKind()==kind::metakind::CONSTANT ){
+      if( n.isConst() ){
         const_rep = n;
       }
       //theory-specific information needed
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 5d7317cbc..fd616948c 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -168,7 +168,7 @@ void FirstOrderModel::toStream(std::ostream& out){
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ){
       //do not print things that have interpretations in model
-      if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){
+      if( !(*eqc_i).isConst() && !hasInterpretedValue( *eqc_i ) ){
         out << "(" << (*eqc_i) << " " << rep << ")" << std::endl;
       }
       ++eqc_i;
diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp
index 9c1c4c89e..7461f3477 100644
--- a/src/theory/quantifiers/rep_set_iterator.cpp
+++ b/src/theory/quantifiers/rep_set_iterator.cpp
@@ -380,7 +380,7 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
         //if not set already, rewrite and consult model for interpretation
         if( !setVal ){
           val = Rewriter::rewrite( val );
-          if( val.getMetaKind()!=kind::metakind::CONSTANT ){
+          if( !val.isConst() ){
             //FIXME: we cannot do this until we trust all theories collectModelInfo!
             //val = d_model->getInterpretedValue( val );
             //val = d_model->getRepresentative( val );
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 77daa5f53..79e4f6a36 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -66,7 +66,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
   switch(mode) {
   case THEORY_OF_TYPE_BASED:
     // Constants, variables, 0-ary constructors
-    if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
+    if (node.isVar() || node.isConst()) {
       return theoryOf(node.getType());
     }
     // Equality is owned by the theory that owns the domain
@@ -78,7 +78,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
     break;
   case THEORY_OF_TERM_BASED:
     // Variables
-    if (node.getMetaKind() == kind::metakind::VARIABLE) {
+    if (node.isVar()) {
       if (theoryOf(node.getType()) != theory::THEORY_BOOL) {
         // We treat the varibables as uninterpreted
         return s_uninterpretedSortOwner;
@@ -88,7 +88,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
       }
     }
     // Constants
-    if (node.getMetaKind() == kind::metakind::CONSTANT) {
+    if (node.isConst()) {
       // Constants go to the theory of the type
       return theoryOf(node.getType());
     }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index f3a9db394..397f7cff7 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -583,15 +583,15 @@ public:
    */
   virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
     if (in.getKind() == kind::EQUAL) {
-      if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+      if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+      if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
         outSubstitutions.addSubstitution(in[1], in[0]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) {
+      if (in[0].isConst() && in[1].isConst()) {
         if (in[0] != in[1]) {
           return PP_ASSERT_STATUS_CONFLICT;
         }
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 26678f21d..6298ff1ca 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -81,13 +81,13 @@ bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) {
   }
 
   if(t.getNumChildren() == 0) {
-    if(t.getMetaKind() == kind::metakind::CONSTANT) {
-      Assert(n.getMetaKind() == kind::metakind::CONSTANT);
+    if(t.isConst()) {
+      Assert(n.isConst());
       Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl;
       return false;
     }
-    Assert(t.getMetaKind() == kind::metakind::VARIABLE &&
-           n.getMetaKind() == kind::metakind::VARIABLE);
+    Assert(t.isVar() &&
+           n.isVar());
     t = find(t);
     n = find(n);
     Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl;
@@ -218,8 +218,8 @@ Node SymmetryBreaker::normInternal(TNode n) {
           } else if((*i).getKind() == kind::IFF ||
                     (*i).getKind() == kind::EQUAL) {
             kids.push_back(normInternal(*i));
-            if((*i)[0].getMetaKind() == kind::metakind::VARIABLE ||
-               (*i)[1].getMetaKind() == kind::metakind::VARIABLE) {
+            if((*i)[0].isVar() ||
+               (*i)[1].isVar()) {
               d_termEqs[(*i)[0]].insert((*i)[1]);
               d_termEqs[(*i)[1]].insert((*i)[0]);
               Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl;
@@ -237,8 +237,8 @@ Node SymmetryBreaker::normInternal(TNode n) {
 
   case kind::IFF:
   case kind::EQUAL:
-    if(n[0].getMetaKind() == kind::metakind::VARIABLE ||
-       n[1].getMetaKind() == kind::metakind::VARIABLE) {
+    if(n[0].isVar() ||
+       n[1].isVar()) {
       d_termEqs[n[0]].insert(n[1]);
       d_termEqs[n[1]].insert(n[0]);
       Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;