diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-17 14:09:46 -0500 |
|---|---|---|
| committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-17 14:09:46 -0500 |
| commit | 19cf50fcb832b01bb119dc1cfc31884e4e864f06 (patch) | |
| tree | 2c9c0f41307ab5d62df39102571935bd2ea5fff1 /src/theory/quantifiers/sygus/cegis.h | |
| parent | 19ab3936ef46e93a98a142e0c454659ecc1d1e27 (diff) | |
Cegis-specific infrastructure (#1933)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index cbd563e07..e5ee6bc56 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -72,6 +72,23 @@ class Cegis : public SygusModule * formula P( CegConjecture::d_candidates, y ). */ Node d_base_body; + //----------------------------------cegis-implementation-specific + /** do cegis-implementation-specific intialization for this class */ + virtual bool processInitialize(Node n, + const std::vector<Node>& candidates, + std::vector<Node>& lemmas); + /** do cegis-implementation-specific construct candidate + * + * satisfiedRl is whether all refinement lemmas are satisfied under the + * substitution { enums -> enum_values }. + */ + virtual bool processConstructCandidates(const std::vector<Node>& enums, + const std::vector<Node>& enum_values, + const std::vector<Node>& candidates, + std::vector<Node>& candidate_values, + bool satisfiedRl, + std::vector<Node>& lems); + //----------------------------------end cegis-implementation-specific //-----------------------------------refinement lemmas /** refinement lemmas */ |