diff options
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.h')
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 3313b507b..321880dc0 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -64,15 +64,14 @@ class CandidateRewriteDatabase : public ExprMiner * Serves the same purpose as the above function, but we will be using * sygus to enumerate terms and generate samples. * - * qe : pointer to quantifiers engine. We use the sygus term database of this - * quantifiers engine, and the extended rewriter of the corresponding term + * tds : pointer to sygus term database. We use the extended rewriter of this * database when computing candidate rewrites, * f : a term of some SyGuS datatype type whose values we will be * testing under the free variables in the grammar of f. This is the * "candidate variable" CegConjecture::d_candidates. */ void initializeSygus(const std::vector<Node>& vars, - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, SygusSampler* ss); /** add term @@ -102,8 +101,6 @@ class CandidateRewriteDatabase : public ExprMiner void setExtendedRewriter(ExtendedRewriter* er); private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; /** (required) pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; /** an extended rewriter object */ |