diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-03 07:54:27 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-03 07:54:27 -0500 |
commit | 53e1523de04c8643186244d9fc3c329ff158a057 (patch) | |
tree | 122b85b66cba8b45a892f02147229121adf58630 /src/theory/quantifiers/sygus/cegis.h | |
parent | f45c0f10a01023b7653c8c36ffe37f70e4e56baa (diff) |
Make CegisUnif default to Cegis when no unif used (#1836)
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 |