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

Merge pull request #1996 from waywardmonkeys/reduce-dead-stores

Browse source 
Reduce dead stores
This commit is contained in:
Nikolaj Bjorner 2018-11-30 12:03:41 -08:00 • committed by GitHub
commit 7d4f2a2f21
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 6 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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)

1
src/smt/theory_bv.cpp
View file

@ -1083,7 +1083,6 @@ namespace smt {
for (unsigned i = 0; i <= num_args; i++) {
expr* arg = (i == num_args)?n:n->get_arg(i);
sort* s = get_manager().get_sort(arg);
s = get_manager().get_sort(arg);
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) {
if (!m_approximates_large_bvs) {
TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";);

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;

3
src/smt/theory_str.cpp
View file

@ -7501,15 +7501,12 @@ namespace smt {
expr_ref newConcat(m);
if (arg1 != a1 || arg2 != a2) {
TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;);
int iPos = 0;
expr_ref_vector item1(m);
if (a1 != arg1) {
item1.push_back(ctx.mk_eq_atom(a1, arg1));
iPos += 1;
}
if (a2 != arg2) {
item1.push_back(ctx.mk_eq_atom(a2, arg2));
iPos += 1;
}
expr_ref implyL1(mk_and(item1), m);
newConcat = mk_concat(arg1, arg2);