Searched refs:term_irrelevant (Results 1 – 3 of 3) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | sygus_grammar_cons.h | 79 std::unordered_set<Node, NodeHashFunction>& term_irrelevant);
87 std::unordered_set<Node, NodeHashFunction> term_irrelevant; in mkSygusDefaultType() local
89 range, bvl, fun, extra_cons, exclude_cons, term_irrelevant); in mkSygusDefaultType()
160 std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
|
| H A D | sygus_grammar_cons.cpp | 424 std::unordered_set<Node, NodeHashFunction>& term_irrelevant, in mkSygusDefaultGrammar() argument
437 if (term_irrelevant.find(bvl[i]) == term_irrelevant.end()) in mkSygusDefaultGrammar()
934 std::unordered_set<Node, NodeHashFunction>& term_irrelevant) in mkSygusDefaultType() argument
947 term_irrelevant, in mkSygusDefaultType()
|
| H A D | cegis_unif.cpp | 462 std::unordered_set<Node, NodeHashFunction> term_irrelevant; in mkLiteral() local
468 term_irrelevant); in mkLiteral()
|