Home
last modified time | relevance | path

Searched refs:zero_j (Results 1 – 6 of 6) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/math/lp/
H A Dnla_basics_lemmas.cpp34 lpvar zero_j = find_best_zero(m, fixed_zeros); in generate_zero_lemmas() local
35 SASSERT(is_set(zero_j)); in generate_zero_lemmas()
38 if (j == zero_j) { in generate_zero_lemmas()
51 add_trivial_zero_lemma(zero_j, m); in generate_zero_lemmas()
53 generate_strict_case_zero_lemma(m, zero_j, sign); in generate_zero_lemmas()
164 lpvar zero_j = null_lpvar; in find_best_zero() local
171 zero_j = j; in find_best_zero()
174 return zero_j; in find_best_zero()
179 lemma |= ineq(zero_j, llc::NE, 0); in add_trivial_zero_lemma()
187 lemma |= ineq(zero_j, sign_of_zj == 1? llc::GT : llc::LT, 0); in generate_strict_case_zero_lemma()
[all …]
H A Dnla_basics_lemmas.h83 void add_trivial_zero_lemma(lpvar zero_j, const monic& m);
84 void generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj);
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/
H A Dnla_basics_lemmas.cpp34 lpvar zero_j = find_best_zero(m, fixed_zeros); in generate_zero_lemmas() local
35 SASSERT(is_set(zero_j)); in generate_zero_lemmas()
38 if (j == zero_j) { in generate_zero_lemmas()
51 add_trivial_zero_lemma(zero_j, m); in generate_zero_lemmas()
53 generate_strict_case_zero_lemma(m, zero_j, sign); in generate_zero_lemmas()
164 lpvar zero_j = null_lpvar; in find_best_zero() local
171 zero_j = j; in find_best_zero()
174 return zero_j; in find_best_zero()
179 lemma |= ineq(zero_j, llc::NE, 0); in add_trivial_zero_lemma()
187 lemma |= ineq(zero_j, sign_of_zj == 1? llc::GT : llc::LT, 0); in generate_strict_case_zero_lemma()
[all …]
H A Dnla_basics_lemmas.h83 void add_trivial_zero_lemma(lpvar zero_j, const monic& m);
84 void generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj);
/dports/misc/vxl/vxl-3.3.2/contrib/brl/bseg/brip/
H A Dbrip_vil_float_ops.h350 const unsigned zero_i, const unsigned zero_j,
H A Dbrip_vil_float_ops.cxx1225 const unsigned zero_i, const unsigned zero_j, in velocity_by_correlation() argument
1232 auto vy0 = static_cast<float>(zero_j); in velocity_by_correlation()