diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 2c21257b9..bebb91fa3 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -185,13 +185,11 @@ class Cegis : public SygusModule * to lems based on evaluating the conjecture, instantiated for ms, on lemmas * for previous refinements (d_refinement_lemmas). * - * Returns true if any such lemma exists. If doGen is false, then the - * lemmas are not generated or added to lems. + * Returns true if any such lemma exists. */ bool getRefinementEvalLemmas(const std::vector<Node>& vs, const std::vector<Node>& ms, - std::vector<Node>& lems, - bool doGen); + std::vector<Node>& lems); /** Check refinement evaluation lemmas * * This method is similar to above, but does not perform any generalization |