diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-29 14:40:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-29 19:40:53 +0000 |
| commit | 96ac1d2a5d1f25eaa1b0b265bb21d1a8b3c3d872 (patch) | |
| tree | 173382d78c1f917b49922aa0aabc206a497d364d /src/theory/quantifiers/sygus/sygus_unif.h | |
| parent | 52c7724a940aee682d550da077d7124a078ac077 (diff) | |
Eliminate the use of quantifiers engine in sygus solver (#6232)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index a8a82b2cf..ca5eb0a73 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -23,9 +23,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class TermDbSygus; @@ -67,7 +64,7 @@ class SygusUnif * the respective function-to-synthesize. */ virtual void initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector<Node>& enums, std::map<Node, std::vector<Node>>& strategy_lemmas); @@ -92,10 +89,8 @@ class SygusUnif std::vector<Node>& lemmas) = 0; protected: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; - /** sygus term database of d_qe */ - quantifiers::TermDbSygus* d_tds; + /** Pointer to the term database sygus */ + TermDbSygus* d_tds; //-----------------------debug printing /** print ind indentations on trace c */ |