summaryrefslogtreecommitdiff
path: root/src/theory/theory.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r--src/theory/theory.cpp6
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());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback