fix uses of getMetaKind() from outside the expr package. (they now use isConst(...

also some base infrastructure for the new ::isConst().

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c70fed88929a63046ebcec55b1780d506879b2c9..f88914fd269f84f33200b7b6f609e37fa27037a4 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -114,9 +114,9 @@ namespace expr {
 static Node exportConstant(TNode n, NodeManager* to);
 
 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
-  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+  if(n.isConst()) {
     return exportConstant(n, NodeManager::fromExprManager(to));
-  } else if(n.getMetaKind() == kind::metakind::VARIABLE) {
+  } else if(n.isVar()) {
     Expr from_e(from, new Node(n));
     Expr& to_e = vmap.d_typeMap[from_e];
     if(! to_e.isNull()) {
@@ -522,7 +522,7 @@ ${getConst_implementations}
 namespace expr {
 
 static Node exportConstant(TNode n, NodeManager* to) {
-  Assert(n.getMetaKind() == kind::metakind::CONSTANT);
+  Assert(n.isConst());
   switch(n.getKind()) {
 ${exportConstant_cases}
 

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 8b21814dc6e51c27d325d540b53e92647fe85a8f..28a47d84d5db08021590b374c70c2cd29c21a47a 100755 (executable)
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -62,6 +62,9 @@ mkConst_instantiations=
 mkConst_implementations=
 exportConstant_cases=
 
+typerules=
+construles=
+
 seen_theory=false
 seen_theory_builtin=false
 
@@ -139,6 +142,16 @@ function typerule {
 "
 }
 
+function construle {
+  # isconst OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  construles="${construles}
+  case kind::$1:
+    return $2::computeIsConst(nodeManager, n);
+"
+}
+
 function sort {
   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
@@ -262,6 +275,7 @@ for var in \
     exportConstant_cases \
     typechecker_includes \
     typerules \
+    construles \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done

diff --git a/src/expr/mkkind b/src/expr/mkkind
index 89e77754fbb92201f932c40f1f51d7bd506979e6..88c28d4b9c4e1105b84518d234c3da0f50462348 100755 (executable)
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -142,6 +142,12 @@ function typerule {
   check_theory_seen
 }
 
+function construle {
+  # construle OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function rewriter {
   # properties prop*
   lineno=${BASH_LINENO[0]}

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 654a1f94f44c7152f138944338304dadfddd4c29..5608d297220465477de034c45e826164c418a6dd 100755 (executable)
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -117,6 +117,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/expr/node.h b/src/expr/node.h
index b0fda33543d613df40c8a250589f73a33a8ca8f7..cada443a1d6cc062f63504c175fa5db55246cf92 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -442,10 +442,7 @@ public:
    * Returns true if this node represents a constant
    * @return true if const
    */
-  inline bool isConst() const {
-    assertTNodeNotExpired();
-    return getMetaKind() == kind::metakind::CONSTANT;
-  }
+  inline bool isConst() const;
 
   /**
    * Returns true if this node represents a constant
@@ -917,6 +914,7 @@ inline std::ostream& operator<<(std::ostream& out,
 
 #include "expr/attribute.h"
 #include "expr/node_manager.h"
+#include "expr/type_checker.h"
 
 namespace CVC4 {
 
@@ -1263,6 +1261,36 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
   return NodeManager::currentNM()->getType(*this, check);
 }
 
+/** Is this node constant? (and has that been computed yet?) */
+struct IsConstTag { };
+struct IsConstComputedTag { };
+typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
+typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
+
+template <bool ref_count>
+inline bool
+NodeTemplate<ref_count>::isConst() const {
+  assertTNodeNotExpired();
+  if(isNull()) {
+    return false;
+  }
+  switch(getMetaKind()) {
+  case kind::metakind::CONSTANT:
+    return true;
+  case kind::metakind::VARIABLE:
+    return false;
+  default:
+    if(getAttribute(IsConstComputedAttr())) {
+      return getAttribute(IsConstAttr());
+    } else {
+      bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
+      return bval;
+    }
+  }
+}
+
 template <bool ref_count>
 inline Node
 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 501a0f4fdb769bf3ddc7138e46512a973673978e..ce6a91483988210a54c2fa50054095acc9cbbfa4 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -54,8 +54,8 @@ class TypeChecker;
 // Definition of an attribute for the variable name.
 // TODO: hide this attribute behind a NodeManager interface.
 namespace attr {
-  struct VarNameTag {};
-  struct SortArityTag {};
+  struct VarNameTag { };
+  struct SortArityTag { };
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
@@ -230,8 +230,8 @@ class NodeManager {
   };/* struct NodeManager::NVStorage<N> */
 
   // attribute tags
-  struct TypeTag {};
-  struct TypeCheckedTag;
+  struct TypeTag { };
+  struct TypeCheckedTag { };
 
   // NodeManager's attributes.  These aren't exposed outside of this
   // class; use the getters.

diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index 0c80934692dc936db46c75cf34adb1ea68d05dad..f198e33cacf455490c642df920865e65c80b2622 100644 (file)
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -18,11 +18,12 @@
 
 #include "cvc4_private.h"
 
+// ordering dependence
+#include "expr/node.h"
+
 #ifndef __CVC4__EXPR__TYPE_CHECKER_H
 #define __CVC4__EXPR__TYPE_CHECKER_H
 
-#include "expr/node.h"
-
 namespace CVC4 {
 namespace expr {
 
@@ -32,6 +33,9 @@ public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check = false)
     throw (TypeCheckingExceptionPrivate, AssertionException);
 
+  static bool computeIsConst(NodeManager* nodeManager, TNode n)
+    throw (AssertionException);
+
 };/* class TypeChecker */
 
 }/* CVC4::expr namespace */

diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 2791376b51da1309e715eb752310a44eed110b59..9359a6ab87fbe57f9306aa1c92221f1632c40c36 100644 (file)
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -62,5 +62,22 @@ ${typerules}
 
 }/* TypeChecker::computeType */
 
+bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
+  throw (AssertionException) {
+
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+
+  switch(n.getKind()) {
+${construles}
+
+#line 74 "${template}"
+
+  default:;
+  }
+
+  return false;
+
+}/* TypeChecker::computeIsConst */
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 664ea58fcae0d81c69828c15fb12ea7e4914bda4..5647692077097ed325e2137ee48dd2334af41555 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -81,7 +81,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
   }
 
   // variables
-  if(n.getMetaKind() == kind::metakind::VARIABLE) {
+  if(n.isVar()) {
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
       out << s;
@@ -102,7 +102,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
   }
 
   // constants
-  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+  if(n.isConst()) {
     switch(n.getKind()) {
     case kind::BITVECTOR_TYPE:
       out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")";

diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index 81183182d568f0d59a48eedefd2faf75cdad4b64..580bec63c4ec796ed5dd4fbde5c214b9e3548d6b 100644 (file)
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -53,12 +53,12 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
   // the count beyond the threshold already, we've done the same
   // for all subexpressions, so it isn't useful to traverse and
   // increment again (they'll be dagified anyway).
-  return current.getMetaKind() == kind::metakind::VARIABLE ||
-         current.getMetaKind() == kind::metakind::CONSTANT ||
+  return current.isVar() ||
+         current.isConst() ||
          ( ( current.getKind() == kind::NOT ||
              current.getKind() == kind::UMINUS ) &&
-           ( current[0].getMetaKind() == kind::metakind::VARIABLE ||
-             current[0].getMetaKind() == kind::metakind::CONSTANT ) ) ||
+           ( current[0].isVar() ||
+             current[0].isConst() ) ) ||
          current.getKind() == kind::SORT_TYPE ||
          d_nodeCount[current] > d_threshold;
 }

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 892de551c51eb00cfa3bb4b6db043c2042c80920..dcb37d3d9b75e57cc66e4e1a29e26057143a4e6c 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -80,7 +80,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   }
 
   // variable
-  if(n.getMetaKind() == kind::metakind::VARIABLE) {
+  if(n.isVar()) {
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
       out << s;
@@ -102,7 +102,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   }
 
   // constant
-  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+  if(n.isConst()) {
     switch(n.getKind()) {
     case kind::TYPE_CONSTANT:
       switch(n.getConst<TypeConstant>()) {

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index b498f1e40f94a86c5742fb0c954f89acf9f2b0e5..c5345c5a72bb403ba52a171694e716a984433292 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -150,7 +150,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
   }
 
   if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL &&
-      n.getMetaKind() != kind::metakind::VARIABLE ) {
+      !n.isVar() ) {
     // If we were called with something other than a theory atom (or
     // Boolean variable), we get a SatLiteral that is definitionally
     // equal to it.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 272bfe04ebbc00eb8996bfc6f9aa08bc3849dd06..6b7ca8d2fa8e6a16cce242e0833cc4fc66ebc468 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1743,7 +1743,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
                      ( d_definedFunctions->find(n.getOperator()) !=
                        d_definedFunctions->end() ) &&
                      n.getNumChildren() == 0 ) ||
-                   n.getMetaKind() == kind::metakind::VARIABLE ), e,
+                   n.isVar() ), e,
                  "expected variable or defined-function application "
                  "in addToAssignment(),\ngot %s", e.toString().c_str() );
   if(!options::produceAssignments()) {
@@ -1809,7 +1809,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException)
       Assert((*i).getNumChildren() == 0);
       v.push_back((*i).getOperator().toString());
     } else {
-      Assert((*i).getMetaKind() == kind::metakind::VARIABLE);
+      Assert((*i).isVar());
       v.push_back((*i).toString());
     }
     v.push_back(resultNode.toString());

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index d7a6c0443a59e7ca88b92c620292feeb34a47e07..6b38daccedecee1001f369e035a528bc088d4423 100644 (file)
--- 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 a478f3cfb7f94b10c076aa96b07c1f1a44ad380d..46b0264eac20d514b4d6973a9949e07f9f09ae32 100644 (file)
--- 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 b054f9804b9ab5bb567d83697f85dce69e98930d..33fc42cea484f419ca71c48cc81414f77023e249 100644 (file)
--- 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 d55860c41021966a3a4e1b1d7a213c2a9cd7e616..6b7efa1eecb29b59b13be67f7c8bafdea8832414 100644 (file)
--- 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 5add52d1f8148e52384dfb7cf3fe97146d0c9cbe..47f3e31dbc8cdfaf434be60cfbbed48df3e613e3 100644 (file)
--- 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 63b44f7cae52bcede179083976ddfa4138ea369f..1018289ab967c548da298266f3fe7a3794b31365 100644 (file)
--- 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 b6dcc6662dfb3be7c973b928d15e3366df09fa0d..2bb4857a3dcb0fde281c2a6aba63074387c1634a 100644 (file)
--- 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 896133e464d4e7f707601d910e146971cbdb01fc..39e5bc59990ef98db6cbca535d7dea79278a11ba 100644 (file)
--- 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 73b88986bfbbcb255837210c2a131b06ebc3553e..73fc6706dc8398dc2c8b3e9fd5f6516c0d77e933 100755 (executable)
--- 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 ffdc1d4c695eaf137ac95fb1e44e0f9c93a96cae..0d00b616c8e25ac6880d400771a9ee03ba63a0e5 100755 (executable)
--- 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 3607d52323383cddc82c058300b87f80946bc6df..60ff05d35b525decb09513a57ca9552f13086bb0 100755 (executable)
--- 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 feedc0c31f77aff054656435bce775ed7f661dda..882a3034a1f2e2b126e5d17311008e5f65ad6247 100644 (file)
--- 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 5d7317cbc660396ccf3e1660c5e45935673c91ed..fd616948c19a5563e51f469970d295460f9a0a91 100644 (file)
--- 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 9c1c4c89ed09d0a80ee56cb457bb9779e17776a0..7461f347764858b59f912a841bf7eaa45b9447ad 100644 (file)
--- 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 77daa5f5369e8e19b279ba0193e6ad0fab952ccf..79e4f6a36b830db77d3a7b5c79bf321e93b2f333 100644 (file)
--- 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 f3a9db3943e1e8af0cb1d3bb1723699471e0e161..397f7cff7c80d8f9f9d28911a1469ef86cad8074 100644 (file)
--- 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 26678f21db292af77018b555758f364a7328cf9a..6298ff1ca45b006c4905f8d90bac455aa20a41ed 100644 (file)
--- 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;

diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp
index 862f1e5fc3d60ec464a78453e12c49c1bc759efb..e21aadf0582467e0b67fb86bda6c57c669d871f9 100644 (file)
--- a/src/util/boolean_simplification.cpp
+++ b/src/util/boolean_simplification.cpp
@@ -37,7 +37,7 @@ BooleanSimplification::push_back_associative_commute_recursive
       }
     }else{
       if(negateNode){
-        if(child.getMetaKind() == kind::metakind::CONSTANT) {
+        if(child.isConst()) {
           if((k == kind::AND && child.getConst<bool>()) ||
              (k == kind::OR && !child.getConst<bool>())) {
             buffer.clear();
@@ -48,7 +48,7 @@ BooleanSimplification::push_back_associative_commute_recursive
           buffer.push_back(negate(child));
         }
       }else{
-        if(child.getMetaKind() == kind::metakind::CONSTANT) {
+        if(child.isConst()) {
           if((k == kind::OR && child.getConst<bool>()) ||
              (k == kind::AND && !child.getConst<bool>())) {
             buffer.clear();

diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index b3dffa47505a4bb6d40677d69a2d3c44ce145290..a5a6462319e7a69ea29c7a5c208b91ed144ceb7b 100644 (file)
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -187,7 +187,7 @@ public:
       base = base[0];
       polarity = !polarity;
     }
-    if(n.getMetaKind() == kind::metakind::CONSTANT) {
+    if(n.isConst()) {
       return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
     }
     if(polarity){