Searched refs:expr_pattern_match (Results 1 – 8 of 8) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/ast/pattern/ |
| H A D | expr_pattern_match.cpp | 40 expr_pattern_match::expr_pattern_match(ast_manager & manager): in expr_pattern_match() function in expr_pattern_match
44 expr_pattern_match::~expr_pattern_match() { in ~expr_pattern_match()
100 expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result) { in instantiate()
117 expr_pattern_match::compile(expr* q) in compile()
217 expr_pattern_match::match(expr* a, unsigned init, subst& s) in match()
366 expr_pattern_match::match_decl(func_decl const * pat, func_decl const * d) const { in match_decl()
395 expr_pattern_match::is_var(func_decl* d) { in is_var()
401 expr_pattern_match::initialize(char const * spec_string) { in initialize()
419 unsigned expr_pattern_match::initialize(quantifier* q) { in initialize()
428 void expr_pattern_match::display(std::ostream& out) const { in display()
[all …]
|
| H A D | expr_pattern_match.h | 25 class expr_pattern_match {
118 expr_pattern_match(ast_manager & manager);
119 ~expr_pattern_match();
|
| H A D | pattern_inference.h | 192 expr_pattern_match m_database;
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/pattern/ |
| H A D | expr_pattern_match.cpp | 40 expr_pattern_match::expr_pattern_match(ast_manager & manager): in expr_pattern_match() function in expr_pattern_match
44 expr_pattern_match::~expr_pattern_match() { in ~expr_pattern_match()
100 expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result) { in instantiate()
117 expr_pattern_match::compile(expr* q) in compile()
217 expr_pattern_match::match(expr* a, unsigned init, subst& s) in match()
366 expr_pattern_match::match_decl(func_decl const * pat, func_decl const * d) const { in match_decl()
395 expr_pattern_match::is_var(func_decl* d) { in is_var()
401 expr_pattern_match::initialize(char const * spec_string) { in initialize()
419 unsigned expr_pattern_match::initialize(quantifier* q) { in initialize()
428 void expr_pattern_match::display(std::ostream& out) const { in display()
[all …]
|
| H A D | expr_pattern_match.h | 25 class expr_pattern_match {
118 expr_pattern_match(ast_manager & manager);
119 ~expr_pattern_match();
|
| H A D | pattern_inference.h | 192 expr_pattern_match m_database;
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/ |
| H A D | special_relations_tactic.h | 30 expr_pattern_match m_pm;
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/core/ |
| H A D | special_relations_tactic.h | 30 expr_pattern_match m_pm;
|