diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 4867fc402..621b5153f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -26,23 +26,19 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusUnif::SygusUnif() - : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false) -{ -} +SygusUnif::SygusUnif() : d_tds(nullptr), d_enableMinimality(false) {} SygusUnif::~SygusUnif() {} void SygusUnif::initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector<Node>& enums, std::map<Node, std::vector<Node>>& strategy_lemmas) { - d_qe = qe; - d_tds = qe->getTermDatabaseSygus(); + d_tds = tds; d_candidates.push_back(f); // initialize the strategy - d_strategy[f].initialize(qe, f, enums); + d_strategy[f].initialize(tds, f, enums); } Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms) |