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, 8 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 382d4cf65..e8518b1f6 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -781,6 +781,14 @@ public:
assertions_iterator facts_end() const {
return d_facts.end();
}
+ /**
+ * Whether facts have been asserted to this theory.
+ *
+ * @return true iff facts have been asserted to this theory.
+ */
+ bool hasFacts() {
+ return !d_facts.empty();
+ }
typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback