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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a1a6dcefc..890f04aad 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -516,6 +516,10 @@ Node QuantifiersEngine::getNextDecisionRequest(){ return Node::null(); } +quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() { + return getTermDatabase()->getTermDatabaseSygus(); +} + void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); |