diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-27 13:57:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-27 13:57:17 -0500 |
commit | a6cc1d8ebff497392533bbb16782bda6351648df (patch) | |
tree | 221f27e8b528d317fa75b2af8084cc4ad520c739 /src/theory/quantifiers/sygus/cegis.h | |
parent | 23f51f715f625a1275a7cb14a3a96e85e1290a89 (diff) |
Infrastructure for using active enumerators in sygus modules (#2547)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.h')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index c7392b378..7387bd468 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -104,6 +104,8 @@ class Cegis : public SygusModule /** substitution entailed by d_refinement_lemma_unit */ std::vector<Node> d_rl_eval_hds; std::vector<Node> d_rl_vals; + /** all variables appearing in refinement lemmas */ + std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_vars; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); /** add refinement lemma conjunct @@ -150,10 +152,14 @@ class Cegis : public SygusModule * Given a candidate solution ms for candidates vs, this function adds lemmas * 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. */ - void getRefinementEvalLemmas(const std::vector<Node>& vs, + bool getRefinementEvalLemmas(const std::vector<Node>& vs, const std::vector<Node>& ms, - std::vector<Node>& lems); + std::vector<Node>& lems, + bool doGen); /** sampler object for the option cegisSample() * * This samples points of the type of the inner variables of the synthesis |