summaryrefslogtreecommitdiff
path: root/src/theory/theory.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r--src/theory/theory.h8
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b0f5e4e53..35c81239f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -142,7 +142,7 @@ private:
protected:
- /**
+ /**
* A list of shared terms that the theory has.
*/
context::CDList<TNode> d_sharedTerms;
@@ -210,6 +210,9 @@ protected:
*/
static TheoryId s_uninterpretedSortOwner;
+ void printFacts(std::ostream& os) const;
+
+
public:
/**
@@ -218,6 +221,9 @@ public:
static inline TheoryId theoryOf(TypeNode typeNode) {
Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl;
TheoryId id;
+ while (typeNode.isPredicateSubtype()) {
+ typeNode = typeNode.getSubtypeBaseType();
+ }
if (typeNode.getKind() == kind::TYPE_CONSTANT) {
id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
} else {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback