diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ce096b127..735477821 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -59,8 +59,14 @@ class CegisUnifEnumManager void initialize(const std::vector<Node>& es, const std::map<Node, Node>& e_to_cond, const std::map<Node, std::vector<Node>>& strategy_lemmas); - /** get the current set of conditional enumerators for strategy point e */ - void getCondEnumeratorsForStrategyPt(Node e, std::vector<Node>& ces) const; + /** get the current set of enumerators for strategy point e + * + * Index 0 adds the set of return value enumerators to es, index 1 adds the + * set of condition enumerators to es. + */ + void getEnumeratorsForStrategyPt(Node e, + std::vector<Node>& es, + unsigned index) const; /** register evaluation point for candidate * * This notifies this class that eis is a set of heads of evaluation points |