mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-06 15:39:37 +01:00
commit e662427060
1 changed files with 27 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

56
src/ast/rewriter/bv_trailing.cpp
View file

@ -27,7 +27,7 @@ struct bv_trailing::imp {
typedef obj_map<expr, std::pair<unsigned,unsigned> > map; typedef obj_map<expr, std::pair<unsigned,unsigned> > map;
mk_extract_proc& m_mk_extract; mk_extract_proc& m_mk_extract;
bv_util& m_util; bv_util& m_util;
ast_manager& m_m; ast_manager& m;
// keep a cache for each depth, using the convention that m_count_cache[TRAILING_DEPTH] is top-level // keep a cache for each depth, using the convention that m_count_cache[TRAILING_DEPTH] is top-level
map* m_count_cache[TRAILING_DEPTH + 1]; map* m_count_cache[TRAILING_DEPTH + 1];
@ -35,7 +35,7 @@ struct bv_trailing::imp {
imp(mk_extract_proc& mk_extract) imp(mk_extract_proc& mk_extract)
: m_mk_extract(mk_extract) : m_mk_extract(mk_extract)
, m_util(mk_extract.bvutil()) , m_util(mk_extract.bvutil())
, m_m(mk_extract.m()) { , m(mk_extract.m()) {
for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) for (unsigned i = 0; i <= TRAILING_DEPTH; ++i)
m_count_cache[i] = NULL; m_count_cache[i] = NULL;
} }
@ -44,36 +44,34 @@ struct bv_trailing::imp {
reset_cache(0); reset_cache(0);
} }
ast_manager & m() const { return m_util.get_manager(); }
br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) { br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m()) << "\n=\n" << mk_ismt2_pp(e2, m()) << "\n";); TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m) << "\n=\n" << mk_ismt2_pp(e2, m) << "\n";);
SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2)); SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2));
SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2)); SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2));
unsigned max1, min1, max2, min2; unsigned max1, min1, max2, min2;
count_trailing(e1, min1, max1, TRAILING_DEPTH); count_trailing(e1, min1, max1, TRAILING_DEPTH);
count_trailing(e2, min2, max2, TRAILING_DEPTH); count_trailing(e2, min2, max2, TRAILING_DEPTH);
if (min1 > max2 || min2 > max1) { // bounds have empty intersection if (min1 > max2 || min2 > max1) { // bounds have empty intersection
result = m().mk_false(); result = m.mk_false();
return BR_DONE; return BR_DONE;
} }
const unsigned min = std::min(min1, min2); // remove the minimum of the two lower bounds const unsigned min = std::min(min1, min2); // remove the minimum of the two lower bounds
if (min == 0) { // nothing to remove if (min == 0) { // nothing to remove
result = m().mk_eq(e1, e2); result = m.mk_eq(e1, e2);
return BR_FAILED; return BR_FAILED;
} }
const unsigned sz = m_util.get_bv_size(e1); const unsigned sz = m_util.get_bv_size(e1);
if (min == sz) { // everything removed, unlikely but we check anyhow for safety if (min == sz) { // everything removed, unlikely but we check anyhow for safety
result = m().mk_true(); result = m.mk_true();
return BR_DONE; return BR_DONE;
} }
expr_ref out1(m()); expr_ref out1(m);
expr_ref out2(m()); expr_ref out2(m);
const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH); const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH); const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
SASSERT(rm1 == min && rm2 == min); SASSERT(rm1 == min && rm2 == min);
const bool are_eq = m().are_equal(out1, out2); const bool are_eq = m.are_equal(out1, out2);
result = are_eq ? m().mk_true() : m().mk_eq(out1, out2); result = are_eq ? m.mk_true() : m.mk_eq(out1, out2);
return are_eq ? BR_DONE : BR_REWRITE2; return are_eq ? BR_DONE : BR_REWRITE2;
} }
@ -84,7 +82,7 @@ struct bv_trailing::imp {
SASSERT(e && m_util.is_bv(e)); SASSERT(e && m_util.is_bv(e));
if (is_cached(depth, e, min, max)) return; if (is_cached(depth, e, min, max)) return;
count_trailing_core(e, min, max, depth); count_trailing_core(e, min, max, depth);
TRACE("bv-trailing", tout << mk_ismt2_pp(e, m()) << "\n:" << min << " - " << max << "\n";); TRACE("bv-trailing", tout << mk_ismt2_pp(e, m) << "\n:" << min << " - " << max << "\n";);
SASSERT(min <= max); SASSERT(min <= max);
SASSERT(max <= m_util.get_bv_size(e)); SASSERT(max <= m_util.get_bv_size(e));
cache(depth, e, min, max); // store result into the cache cache(depth, e, min, max); // store result into the cache
@ -92,8 +90,8 @@ struct bv_trailing::imp {
unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) { unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) {
const unsigned retv = remove_trailing_core(e, n, result, depth); const unsigned retv = remove_trailing_core(e, n, result, depth);
CTRACE("bv-trailing", result.get(), tout << mk_ismt2_pp(e, m()) << "\n--->\n" << mk_ismt2_pp(result.get(), m()) << "\n";); CTRACE("bv-trailing", result.get(), tout << mk_ismt2_pp(e, m) << "\n--->\n" << mk_ismt2_pp(result.get(), m) << "\n";);
CTRACE("bv-trailing", !result.get(), tout << mk_ismt2_pp(e, m()) << "\n---> [EMPTY]\n";); CTRACE("bv-trailing", !result.get(), tout << mk_ismt2_pp(e, m) << "\n---> [EMPTY]\n";);
return retv; return retv;
} }
@ -120,15 +118,15 @@ struct bv_trailing::imp {
return sz; return sz;
} }
expr_ref_vector new_args(m()); expr_ref_vector new_args(m);
expr_ref tmp(m()); expr_ref tmp(m);
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
expr * const curr = a->get_arg(i); expr * const curr = a->get_arg(i);
const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1); const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1);
new_args.push_back(tmp); new_args.push_back(tmp);
SASSERT(crm == to_rm); SASSERT(crm == to_rm);
} }
result = m().mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr());
return to_rm; return to_rm;
} }
@ -139,7 +137,7 @@ struct bv_trailing::imp {
result = a; result = a;
return 0; return 0;
} }
expr_ref tmp(m()); expr_ref tmp(m);
expr * const coefficient = a->get_arg(0); expr * const coefficient = a->get_arg(0);
const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1); const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1);
SASSERT(retv <= n); SASSERT(retv <= n);
@ -147,7 +145,7 @@ struct bv_trailing::imp {
result = a; result = a;
return 0; return 0;
} }
expr_ref_vector new_args(m()); expr_ref_vector new_args(m);
numeral c_val; numeral c_val;
unsigned c_sz; unsigned c_sz;
if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one()) if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
@ -168,7 +166,7 @@ struct bv_trailing::imp {
switch (new_args.size()) { switch (new_args.size()) {
case 0: result = m_util.mk_numeral(1, new_sz); break; case 0: result = m_util.mk_numeral(1, new_sz); break;
case 1: result = new_args.get(0); break; case 1: result = new_args.get(0); break;
default: result = m().mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr()); default: result = m.mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr());
} }
return retv; return retv;
} }
@ -182,7 +180,7 @@ struct bv_trailing::imp {
const unsigned num = a->get_num_args(); const unsigned num = a->get_num_args();
unsigned retv = 0; unsigned retv = 0;
unsigned i = num; unsigned i = num;
expr_ref new_last(NULL, m()); expr_ref new_last(NULL, m);
while (i && retv < n) { while (i && retv < n) {
i--; i--;
expr * const curr = a->get_arg(i); expr * const curr = a->get_arg(i);
@ -203,8 +201,8 @@ struct bv_trailing::imp {
return retv; return retv;
} }
expr_ref_vector new_args(m()); expr_ref_vector new_args(m);
for (size_t j=0; j<i;++j) for (unsigned j = 0; j < i; ++j)
new_args.push_back(a->get_arg(j)); new_args.push_back(a->get_arg(j));
if (new_last.get()) new_args.push_back(new_last); if (new_last.get()) new_args.push_back(new_last);
result = new_args.size() == 1 ? new_args.get(0) result = new_args.size() == 1 ? new_args.get(0)
@ -342,9 +340,9 @@ struct bv_trailing::imp {
if (depth == 0) return; if (depth == 0) return;
if (m_count_cache[depth] == NULL) if (m_count_cache[depth] == NULL)
m_count_cache[depth] = alloc(map); m_count_cache[depth] = alloc(map);
m().inc_ref(e); m.inc_ref(e);
m_count_cache[depth]->insert(e, std::make_pair(min, max)); m_count_cache[depth]->insert(e, std::make_pair(min, max));
TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
} }
bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) { bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) {
@ -360,7 +358,7 @@ struct bv_trailing::imp {
if (oe == NULL) return false; if (oe == NULL) return false;
min = oe->get_data().m_value.first; min = oe->get_data().m_value.first;
max = oe->get_data().m_value.second; max = oe->get_data().m_value.second;
TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
return true; return true;
} }
@ -371,7 +369,7 @@ struct bv_trailing::imp {
if (m_count_cache[i]->size() < condition) continue; if (m_count_cache[i]->size() < condition) continue;
map::iterator it = m_count_cache[i]->begin(); map::iterator it = m_count_cache[i]->begin();
map::iterator end = m_count_cache[i]->end(); map::iterator end = m_count_cache[i]->end();
for (; it != end; ++it) m().dec_ref(it->m_key); for (; it != end; ++it) m.dec_ref(it->m_key);
dealloc(m_count_cache[i]); dealloc(m_count_cache[i]);
m_count_cache[i] = NULL; m_count_cache[i] = NULL;
} }
@ -384,7 +382,7 @@ bv_trailing::bv_trailing(mk_extract_proc& mk_extract) {
} }
bv_trailing::~bv_trailing() { bv_trailing::~bv_trailing() {
if (m_imp) dealloc(m_imp); dealloc(m_imp);
} }
br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) { br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {