diff options
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()); } |