/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
H A D | seq_rewriter.cpp | 912 result = str().mk_substr(s, m_autil.mk_int(jv + 1), mk_sub(k, 1)); in mk_seq_rest() 914 result = str().mk_substr(t, one(), mk_sub(str().mk_length(t), 1)); in mk_seq_rest() 950 result = str().mk_substr(s, j, m_autil.mk_add_simplify(k_min_1)); in mk_seq_butlast() 1092 result = str().mk_substr(a, b, c); in extract_pop_suffix() 1121 result = str().mk_substr(t1, t2, c); in extract_push_offset() 1156 result = str().mk_substr(t1, b, t2); in extract_push_length() 1251 result = str().mk_substr(a1, b1, m_autil.mk_add(c1, q)); in mk_seq_extract() 1324 result = str().mk_substr(result, position, c); in mk_seq_extract() 1523 r = str().mk_substr(tmp, y, z); in reduce_by_char() 4223 re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd), in mk_str_in_regexp() [all …]
|
H A D | seq_axioms.cpp | 465 …add_clause(~cnt, s_eq_empty, ~mk_literal(seq.str.mk_contains(seq.str.mk_substr(t,zero,a.mk_add(i,l… in indexof_axiom() 466 add_clause(~cnt, s_eq_empty, mk_seq_eq(seq.str.mk_substr(t,zero,a.mk_add(i,len_s)), in indexof_axiom() 467 … seq.str.mk_concat(seq.str.mk_substr(t,zero,i), s))); in indexof_axiom()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | seq_axioms.cpp | 347 …add_axiom(~cnt, s_eq_empty, ~mk_literal(seq.str.mk_contains(seq.str.mk_substr(t,zero,a.mk_add(i,le… in add_indexof_axiom() 348 add_axiom(~cnt, s_eq_empty, mk_seq_eq(seq.str.mk_substr(t,zero,a.mk_add(i,len_s)), in add_indexof_axiom() 349 seq.str.mk_concat(seq.str.mk_substr(t,zero,i), s))); in add_indexof_axiom()
|
H A D | theory_seq.cpp | 2140 result = m_util.str.mk_substr(x, m_autil.mk_int(0), y); in elim_skolem() 2150 result = m_util.str.mk_substr(x, y, m_autil.mk_sub(result, y)); in elim_skolem() 2161 result = m_util.str.mk_substr(x, y1, z); in elim_skolem() 2184 …result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_autil.mk_sub(m_util.str.mk_length(x), m_auti… in elim_skolem() 2201 … result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_util.str.mk_index(x, y, m_autil.mk_int(0))); in elim_skolem() 2211 result = m_util.str.mk_substr(x, offset, m_util.str.mk_length(x)); in elim_skolem()
|
/dports/math/libpgmath/flang-d07daf3/tools/flang1/utils/ast/ |
H A D | ast.in.h | 369 int mk_substr (int, int, int, DTYPE);
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | theory_seq.cpp | 2200 result = m_util.str.mk_substr(x, m_autil.mk_int(0), y); in elim_skolem() 2210 result = m_util.str.mk_substr(x, y, m_autil.mk_sub(result, y)); in elim_skolem() 2221 result = m_util.str.mk_substr(x, y1, z); in elim_skolem() 2244 …result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_autil.mk_sub(m_util.str.mk_length(x), m_auti… in elim_skolem() 2261 … result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_util.str.mk_index(x, y, m_autil.mk_int(0))); in elim_skolem() 2271 result = m_util.str.mk_substr(x, offset, m_util.str.mk_length(x)); in elim_skolem()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
H A D | seq_rewriter.cpp | 1047 result = str().mk_substr(t1, t2, c); in mk_seq_extract() 1071 result = str().mk_substr(a1, m_autil.mk_add(b1, b), m_autil.mk_sub(c1, b)); in mk_seq_extract() 1121 result = str().mk_substr(result, pos1, c); in mk_seq_extract() 3043 …tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))… in mk_derivative_rec() 3346 re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd), in mk_str_in_regexp() 3347 re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)); in mk_str_in_regexp() 3356 re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd), in mk_str_in_regexp() 3357 re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)); in mk_str_in_regexp()
|
/dports/math/libpgmath/flang-d07daf3/tools/flang1/flang1exe/ |
H A D | func.c | 1110 return mk_substr(o, l, r, d); in convert_subscript_in_expr() 2460 retval = mk_substr(retval, 0, temp_ast, A_DTYPEG(retval)); in rewrite_func_ast() 2462 retval = mk_substr(retval, 0, A_RIGHTG(ast), A_DTYPEG(retval)); in rewrite_func_ast() 2550 retval = mk_substr(retval, 0, astnew, A_DTYPEG(retval)); in rewrite_func_ast() 2580 retval = mk_substr(retval, 0, len_ast, dtype); in rewrite_func_ast() 3667 return mk_substr(lop, l, r, A_DTYPEG(ast)); in rewrite_sub_ast() 5343 return mk_substr(ast1, A_LEFTG(inast), A_RIGHTG(inast), A_DTYPEG(inast)); in build_array_ref()
|
H A D | rest.c | 231 return mk_substr(l1, l2, l3, d); in insert_comm_before() 419 return mk_substr(l1, l2, l3, d); in _transform_func() 4097 return mk_substr(l1, l2, l3, d); in transform_all_call()
|
H A D | vsub.c | 1550 nast = mk_substr(nlop, A_LEFTG(ast), A_RIGHTG(ast), A_DTYPEG(ast)); in remove_scalar_lhs_dependency()
|
H A D | commgen.c | 1804 astnew = mk_substr(opnd, l, r, dtype); in pointer_squeezer()
|
H A D | inliner.c | 623 astNew = mk_substr(A_LOPG(ast), astNewl, astNewr, A_DTYPEG(ast)); in inline_ast()
|
H A D | semantio.c | 3145 ast1 = mk_substr(ast1, A_LEFTG(ast3), A_RIGHTG(ast3), dtype); in semantio() 5315 ast = mk_substr(newl, A_LEFTG(ast), A_RIGHTG(ast), dtype); in replace_vector_subscript()
|
H A D | ast.c | 1889 mk_substr(int chr, int left, int right, DTYPE dtype) in mk_substr() function 3480 mk_substr(p, A_LEFTG(original), A_RIGHTG(original), A_DTYPEG(original)); in replace_ast_subtree() 4281 astnew = mk_substr(lop, left, right, dtype); in ast_rewrite()
|
H A D | semutil.c | 3029 ast = mk_substr(ast, lb_ast, ub_ast, dtype); in chksubstr() 3153 ast = mk_substr(ast, lb_ast, ub_ast, dtype); in ch_substring()
|
H A D | comm.c | 1321 *pnewast = mk_substr(*pnewast, A_LEFTG(ast), A_RIGHTG(ast), A_DTYPEG(ast)); in remove_section()
|
H A D | transfrm.c | 1714 return mk_substr(ast, A_LEFTG(asgn_ast), A_RIGHTG(asgn_ast), in normalize_forall()
|
H A D | dpm_out.c | 4931 return mk_substr(l1, l2, l3, d); in get_scalar_in_expr()
|
H A D | interf.c | 4309 ast = mk_substr(lop, left, right, dtype); in fill_ast()
|
H A D | semfunc.c | 9611 ast = mk_substr(arrtmp_ast, 0, ast, dtype1); in ref_pd()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
H A D | seq_decl_plugin.h | 311 …app* mk_substr(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c }; return m.mk_app(m_fid… in mk_substr() function
|
/dports/math/z3/z3-z3-4.8.13/src/ast/ |
H A D | seq_decl_plugin.h | 292 …app* mk_substr(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c }; return m.mk_app(m_fid… in mk_substr() function
|