Searched refs:indexof0 (Results 1 – 2 of 2) sorted by path
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | seq_axioms.cpp | 366 expr_ref indexof0(seq.str.mk_index(y, s, zero), m); in add_indexof_axiom() local
367 expr_ref offset_p_indexof0(a.mk_add(offset, indexof0), m); in add_indexof_axiom()
379 ~mk_eq(indexof0, minus_one), i_eq_m1); in add_indexof_axiom()
381 ~mk_ge(indexof0, 0), in add_indexof_axiom()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | seq_axioms.cpp | 484 expr_ref indexof0(seq.str.mk_index(y, s, zero), m); in indexof_axiom() local
485 expr_ref offset_p_indexof0(a.mk_add(offset, indexof0), m); in indexof_axiom()
497 ~mk_eq(indexof0, minus_one), i_eq_m1); in indexof_axiom()
499 ~mk_ge(indexof0, 0), in indexof_axiom()
|