Home
last modified time | relevance | path

Searched refs:mk_substr (Results 1 – 22 of 22) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/
H A Dseq_rewriter.cpp912 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 Dseq_axioms.cpp465 …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 Dseq_axioms.cpp347 …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 Dtheory_seq.cpp2140 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 Dast.in.h369 int mk_substr (int, int, int, DTYPE);
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dtheory_seq.cpp2200 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 Dseq_rewriter.cpp1047 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 Dfunc.c1110 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 Drest.c231 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 Dvsub.c1550 nast = mk_substr(nlop, A_LEFTG(ast), A_RIGHTG(ast), A_DTYPEG(ast)); in remove_scalar_lhs_dependency()
H A Dcommgen.c1804 astnew = mk_substr(opnd, l, r, dtype); in pointer_squeezer()
H A Dinliner.c623 astNew = mk_substr(A_LOPG(ast), astNewl, astNewr, A_DTYPEG(ast)); in inline_ast()
H A Dsemantio.c3145 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 Dast.c1889 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 Dsemutil.c3029 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 Dcomm.c1321 *pnewast = mk_substr(*pnewast, A_LEFTG(ast), A_RIGHTG(ast), A_DTYPEG(ast)); in remove_section()
H A Dtransfrm.c1714 return mk_substr(ast, A_LEFTG(asgn_ast), A_RIGHTG(asgn_ast), in normalize_forall()
H A Ddpm_out.c4931 return mk_substr(l1, l2, l3, d); in get_scalar_in_expr()
H A Dinterf.c4309 ast = mk_substr(lop, left, right, dtype); in fill_ast()
H A Dsemfunc.c9611 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 Dseq_decl_plugin.h311 …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 Dseq_decl_plugin.h292 …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