Searched refs:mk_full_seq (Results 1 – 10 of 10) sorted by relevance
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
| H A D | api_seq.cpp | 250 MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq);
|
| /dports/math/z3/z3-z3-4.8.13/src/api/ |
| H A D | api_seq.cpp | 318 MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq);
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | seq_rewriter.cpp | 3048 auto dotstar = [&]() { return expr_ref(re().mk_full_seq(r->get_sort()), m()); }; in mk_antimirov_deriv_rec()
3266 auto dotstar = [&]() { return expr_ref(re().mk_full_seq(d->get_sort()), m()); }; in mk_antimirov_deriv_negate()
4107 expr_ref full(re().mk_full_seq(rs), m()), prefix(m()), suffix(m()); in rewrite_contains_pattern()
4465 auto mk_full = [&]() { return re().mk_full_seq(a->get_sort()); }; in mk_re_union()
4535 result = re().mk_full_seq(a->get_sort()); in mk_re_complement()
4746 result = re().mk_full_seq(a->get_sort()); in mk_re_star()
4761 result = re().mk_full_seq(a->get_sort()); in mk_re_star()
4792 result = re().mk_full_seq(b1->get_sort()); in mk_re_star()
5350 expr* all = re().mk_full_seq(re().mk_re(b->get_sort())); in reduce_contains()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | seq_rewriter.cpp | 3243 expr_ref full(re().mk_full_seq(rs), m()), prefix(m()), suffix(m()); in rewrite_contains_pattern()
3593 auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); }; in mk_re_union()
3662 result = re().mk_full_seq(m().get_sort(a)); in mk_re_complement()
3860 result = re().mk_full_seq(m().get_sort(a)); in mk_re_star()
3899 result = re().mk_full_seq(m().get_sort(b1)); in mk_re_star()
4408 expr* all = re().mk_full_seq(re().mk_re(m().get_sort(b))); in reduce_contains()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | seq_regex.cpp | 196 expr_ref dotstar(re().mk_full_seq(s_to_re->get_sort()), m); in get_overapprox_regex()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | seq_regex.cpp | 195 expr_ref dotstar(re().mk_full_seq(m.get_sort(s_to_re)), m); in get_overapprox_regex()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | seq_decl_plugin.h | 529 app* mk_full_seq(sort* s);
|
| H A D | seq_decl_plugin.cpp | 1384 app* seq_util::rex::mk_full_seq(sort* s) { in mk_full_seq() function in seq_util::rex
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | seq_decl_plugin.h | 521 app* mk_full_seq(sort* s);
|
| H A D | seq_decl_plugin.cpp | 1035 app* seq_util::rex::mk_full_seq(sort* s) { in mk_full_seq() function in seq_util::rex
|