diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 358b50536..7500abb78 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -64,7 +64,7 @@ class Cegis : public SygusModule Node lem, std::vector<Node>& lems) override; - private: + protected: /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */ std::vector<Node> d_base_vars; /** @@ -94,6 +94,17 @@ class Cegis : public SygusModule bool sampleAddRefinementLemma(const std::vector<Node>& candidates, const std::vector<Node>& vals, std::vector<Node>& lems); + + /** evaluates candidate values on current refinement lemmas + * + * Returns true if refinement lemmas are added after evaluation, false + * otherwise. + * + * Also eagerly unfolds evaluation functions in a heuristic manner, which is + * useful e.g. for boolean connectives + */ + bool addEvalLemmas(const std::vector<Node>& candidates, + const std::vector<Node>& candidate_values); //-----------------------------------end refinement lemmas /** Get refinement evaluation lemmas |