diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-10 15:57:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-10 15:57:54 -0500 |
commit | f29ced85757a85b6bd72b741d6ac7ff45ba29619 (patch) | |
tree | f8f8f9f7c816de60b65c6f7b179f69a87af2fe93 /src/theory/quantifiers/sygus/cegis_unif.h | |
parent | 44b167728ce08c9f1cc7dd5df6e4503f159daff4 (diff) |
Static learn redundant operators in CegisUnif (#1899)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.h')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ed38c9268..dd98b20ba 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -54,7 +54,8 @@ class CegisUnifEnumManager * Each candidate c in cs should be such that we are using a * synthesis-by-unification approach for c. */ - void initialize(const std::vector<Node>& cs); + void initialize(const std::vector<Node>& cs, + const std::map<Node, std::vector<Node>>& strategy_lemmas); /** register evaluation point for candidate * * This notifies this class that eis is a set of heads of evaluation points @@ -100,6 +101,10 @@ class CegisUnifEnumManager std::vector<Node> d_enums; /** the set of evaluation points of this type */ std::vector<Node> d_eval_points; + /** symmetry breaking lemma template for this type */ + Node d_sbt_lemma; + /** argument (to be instantiated) of symmetry breaking lemma template */ + Node d_sbt_arg; }; /** map types to the above info */ std::map<TypeNode, TypeInfo> d_ce_info; |