Searched refs:ls_le_0 (Results 1 – 3 of 3) sorted by last modified time
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_str.cpp | 1594 expr_ref ls_le_0(m_autil.mk_le(ls, zero), m); in instantiate_axiom_Substr() local
1641 expr_ref clause(m.mk_or(~ls_le_0, le_is_0), m); in instantiate_axiom_Substr()
1655 terms.push_back(ls_le_0); in instantiate_axiom_Substr()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | seq_axioms.cpp | 233 expr_ref ls_le_0 = mk_le(ls, 0); in extract_axiom() local
252 add_clause(~ls_le_0, le_is_0); in extract_axiom()
254 add_clause(~le_is_0, ~i_ge_0, ls_le_i, ls_le_0, l_le_0); in extract_axiom()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | seq_axioms.cpp | 129 literal ls_le_0 = mk_le(ls, 0); in add_extract_axiom() local
148 add_axiom(~ls_le_0, le_is_0); in add_extract_axiom()
150 add_axiom(~le_is_0, ~i_ge_0, ls_le_i, ls_le_0, l_le_0); in add_extract_axiom()
|