diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-03 20:39:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-03 20:39:25 +0000 |
commit | 3daaecd22fe5f6147cb08e5a4e08177b33a2daa2 (patch) | |
tree | 46cb65c3673a5678a7779ff970aea9460233f1f1 /src/theory/theory.cpp | |
parent | e26a44d5f98a9953dffeb07b29a21e7efd501684 (diff) |
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().
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
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()); } |