mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Sink some values into loops.

Browse source 
This removes some dead stores that happen prior to the loop and
ensure that no one is looking at the values outside of the
loop.
This commit is contained in:
Bruce Mitchener 2018-11-30 23:12:21 +07:00
parent 74e031ba92
commit bcfa8045fa
2 changed files with 6 additions and 10 deletions
src
math/polynomial
upolynomial.cpp
smt
theory_lra.cpp

6
src/math/polynomial/upolynomial.cpp
View file

@ -1339,12 +1339,10 @@ namespace upolynomial {
// Return the number of sign changes in the coefficients of p
unsigned manager::sign_changes(unsigned sz, numeral const * p) {
unsigned r = 0;
int sign, prev_sign;
sign = 0;
prev_sign = 0;
int prev_sign = 0;
unsigned i = 0;
for (; i < sz; i++) {
sign = sign_of(p[i]);
int sign = sign_of(p[i]);
if (sign == 0)
continue;
if (sign != prev_sign && prev_sign != 0)

10
src/smt/theory_lra.cpp
View file

@ -2283,16 +2283,14 @@ public:
iterator lo_inf = begin1, lo_sup = begin1;
iterator hi_inf = begin2, hi_sup = begin2;
iterator lo_inf1 = begin1, lo_sup1 = begin1;
iterator hi_inf1 = begin2, hi_sup1 = begin2;
bool flo_inf, fhi_inf, flo_sup, fhi_sup;
ptr_addr_hashtable<lp_api::bound> visited;
for (unsigned i = 0; i < atoms.size(); ++i) {
lp_api::bound* a1 = atoms[i];
lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
iterator hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
if (lo_inf1 != end) lo_inf = lo_inf1;
if (lo_sup1 != end) lo_sup = lo_sup1;
if (hi_inf1 != end) hi_inf = hi_inf1;