diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 13:29:28 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 13:29:28 +0100 |
commit | 97e30c1089e42b668a914472b986f2d986190fc6 (patch) | |
tree | c2072c1db332ba61268f23fd67959d134a2f2373 /src/theory/quantifiers_engine.h | |
parent | 03541f4faeb820539ac25f06f1e64adc7aedca6f (diff) |
Refactor sygus_util to TermDb. Initial work on solution reconstruction into syntax for single inv properties.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 3 |
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 */ |