diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_grammar_cons.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 16f4672b0..39f95527f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -35,6 +35,7 @@ public: CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p); ~CegGrammarConstructor() {} /** process + * * This converts node q based on its deep embedding * (Section 4 of Reynolds et al CAV 2015). * The syntactic restrictions are associated with @@ -48,8 +49,17 @@ public: * for some t if !templates[i].isNull(). */ Node process(Node q, - std::map<Node, Node>& templates, - std::map<Node, Node>& templates_arg); + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg); + /** + * Same as above, but we have already determined that the set of first-order + * datatype variables that will quantify the deep embedding conjecture are + * the vector ebvl. + */ + Node process(Node q, + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg, + const std::vector<Node>& ebvl); /** is the syntax restricted? */ bool isSyntaxRestricted() { return d_is_syntax_restricted; } /** does the syntax allow ITE expressions? */ |