summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 78609914f..bdb2795b4 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -39,6 +39,7 @@ class QuantifiersEngine;
namespace quantifiers {
class TermDb;
+ class TermDbSygus;
}
class QuantifiersModule {
@@ -290,6 +291,8 @@ public:
quantifiers::FirstOrderModel* getModel() { return d_model; }
/** get term database */
quantifiers::TermDb* getTermDatabase() { return d_term_db; }
+ /** get term database sygus */
+ quantifiers::TermDbSygus* getTermDatabaseSygus();
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback