Searched refs:t_eq_empty (Results 1 – 2 of 2) sorted by relevance
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | seq_axioms.cpp | 319 literal t_eq_empty = mk_eq_empty(t); in add_indexof_axiom() local
325 add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1); in add_indexof_axiom()
416 literal t_eq_empty = mk_eq_empty(t); in add_last_indexof_axiom() local
420 add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1); in add_last_indexof_axiom()
421 add_axiom(~t_eq_empty, ~s_eq_empty, i_eq_0); in add_last_indexof_axiom()
422 add_axiom(t_eq_empty, ~cnt, mk_seq_eq(t, xsy)); in add_last_indexof_axiom()
423 add_axiom(t_eq_empty, ~cnt, mk_eq(i, mk_len(x))); in add_last_indexof_axiom()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | seq_axioms.cpp | 437 expr_ref t_eq_empty = mk_eq_empty(t); in indexof_axiom() local
443 add_clause(~t_eq_empty, s_eq_empty, i_eq_m1); in indexof_axiom()
532 expr_ref t_eq_empty = mk_eq_empty(t); in last_indexof_axiom() local
536 add_clause(~t_eq_empty, s_eq_empty, i_eq_m1); in last_indexof_axiom()
537 add_clause(~t_eq_empty, ~s_eq_empty, i_eq_0); in last_indexof_axiom()
538 add_clause(t_eq_empty, ~cnt, mk_seq_eq(t, xsy)); in last_indexof_axiom()
539 add_clause(t_eq_empty, ~cnt, mk_eq(i, mk_len(x))); in last_indexof_axiom()
|