mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix compiler warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-04 13:08:23 -07:00
parent 47f194e4c9
commit 253870c6d7
8 changed files with 46 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/muz/rel/dl_relation_manager.cpp
View file

@ -36,13 +36,10 @@ namespace datalog {
void relation_manager::reset_relations() {
relation_map::iterator it=m_relations.begin();
relation_map::iterator end=m_relations.end();
for(;it!=end;++it) {
func_decl * pred = it->m_key;
for (auto const& kv : m_relations) {
func_decl * pred = kv.m_key;
get_context().get_manager().dec_ref(pred); //inc_ref in get_relation
relation_base * r=(*it).m_value;
r->deallocate();
kv.m_value->deallocate();
}
m_relations.reset();
}
@ -119,35 +116,25 @@ namespace datalog {
}
void relation_manager::collect_non_empty_predicates(decl_set & res) const {
relation_map::iterator it = m_relations.begin();
relation_map::iterator end = m_relations.end();
for(; it!=end; ++it) {
if(!it->m_value->fast_empty()) {
res.insert(it->m_key);
for (auto const& kv : m_relations) {
if (!kv.m_value->fast_empty()) {
res.insert(kv.m_key);
}
}
}
void relation_manager::restrict_predicates(const decl_set & preds) {
typedef ptr_vector<func_decl> fd_vector;
fd_vector to_remove;
ptr_vector<func_decl> to_remove;
relation_map::iterator rit = m_relations.begin();
relation_map::iterator rend = m_relations.end();
for(; rit!=rend; ++rit) {
func_decl * pred = rit->m_key;
for (auto const& kv : m_relations) {
func_decl* pred = kv.m_key;
if (!preds.contains(pred)) {
to_remove.insert(pred);
}
}
fd_vector::iterator pit = to_remove.begin();
fd_vector::iterator pend = to_remove.end();
for(; pit!=pend; ++pit) {
func_decl * pred = *pit;
relation_base * rel;
VERIFY( m_relations.find(pred, rel) );
rel->deallocate();
for (func_decl* pred : to_remove) {
m_relations.find(pred)->deallocate();
m_relations.remove(pred);
get_context().get_manager().dec_ref(pred);
}
@ -283,11 +270,9 @@ namespace datalog {
}
table_plugin * relation_manager::get_table_plugin(symbol const& k) {
table_plugin_vector::iterator tpit = m_table_plugins.begin();
table_plugin_vector::iterator tpend = m_table_plugins.end();
for(; tpit!=tpend; ++tpit) {
if((*tpit)->get_name()==k) {
return *tpit;
for (table_plugin * tp : m_table_plugins) {
if (tp->get_name()==k) {
return tp;
}
}
return 0;
@ -341,10 +326,9 @@ namespace datalog {
return res;
}
for (unsigned i = 0; i < m_relation_plugins.size(); ++i) {
p = m_relation_plugins[i];
if (p->can_handle_signature(s)) {
return p->mk_empty(s);
for (relation_plugin* p1 : m_relation_plugins) {
if (p1->can_handle_signature(s)) {
return p1->mk_empty(s);
}
}

13
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -250,7 +250,7 @@ namespace datalog {
bool detect_equivalences(expr_ref_vector& v, bool inside_disjunction)
{
bool have_pair = false;
unsigned prev_pair_idx;
unsigned prev_pair_idx = 0;
arg_pair ap;
unsigned read_idx = 0;
@ -296,21 +296,20 @@ namespace datalog {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if (m.is_not(f) && (m.is_and(args[0]) || m.is_or(args[0]))) {
SASSERT(num==1);
SASSERT(num == 1);
expr_ref tmp(m);
app* a = to_app(args[0]);
m_app_args.reset();
for (unsigned i = 0; i < a->get_num_args(); ++i) {
m_brwr.mk_not(a->get_arg(i), tmp);
for (expr* arg : *a) {
m_brwr.mk_not(arg, tmp);
m_app_args.push_back(tmp);
}
if (m.is_and(args[0])) {
result = m.mk_or(m_app_args.size(), m_app_args.c_ptr());
result = mk_or(m_app_args);
}
else {
result = m.mk_and(m_app_args.size(), m_app_args.c_ptr());
result = mk_and(m_app_args);
}
return BR_REWRITE2;
}

6
src/test/old_interval.cpp
View file

@ -120,9 +120,9 @@ class interval_tester {
interval singleton(int i) { return interval(m, rational(i)); }
interval all() { return interval(m); }
interval l(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
interval r(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
interval b(int l, int u, bool lo = false, bool uo = false, int idx_l = 0, int idx_u = 0) {
interval l(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
interval r(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
interval b(int l, int u, bool lo = false, bool uo = false, size_t idx_l = 0, size_t idx_u = 0) {
return interval(m, rational(l), lo, idx_l == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx_l)), rational(u), uo, idx_u == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx_u)));
}

9
src/test/small_object_allocator.cpp
View file

@ -36,5 +36,14 @@ void tst_small_object_allocator() {
r3 = new (soa) char[1];
TRACE("small_object_allocator",
tout << "r1: " << (void*)r1 << " r2: " << (void*)r2 << " r3: " << (void*)r3 << " r4: " << (void*)r4 << "\n";);
(void)r1;
(void)r2;
(void)r3;
(void)r4;
(void)q1;
(void)p1;
(void)p2;
(void)p3;
}

10
src/test/sorting_network.cpp
View file

@ -364,15 +364,13 @@ void test_at_most_1(unsigned n, bool full) {
for (unsigned i = 0; i < ext.m_clauses.size(); ++i) {
solver.assert_expr(ext.m_clauses[i].get());
}
lbool res;
if (full) {
solver.push();
solver.assert_expr(m.mk_not(m.mk_eq(result1, result2)));
std::cout << result1 << "\n";
res = solver.check();
SASSERT(res == l_false);
VERIFY(l_false == solver.check());
solver.pop(1);
}
@ -390,8 +388,7 @@ void test_at_most_1(unsigned n, bool full) {
std::cout << atom << "\n";
if (is_true) ++k;
}
res = solver.check();
SASSERT(res == l_true);
VERIFY(l_false == solver.check());
if (k > 1) {
solver.assert_expr(result1);
}
@ -402,8 +399,7 @@ void test_at_most_1(unsigned n, bool full) {
else {
solver.assert_expr(m.mk_not(result1));
}
res = solver.check();
SASSERT(res == l_false);
VERIFY(l_false == solver.check());
solver.pop(1);
}
}

2
src/test/substitution.cpp
View file

@ -35,6 +35,8 @@ void tst_substitution()
bool ok1 = unif(v1.get(), v2.get(), subst, false);
bool ok2 = unif(v2.get(), v1.get(), subst, false);
(void)ok1;
(void)ok2;
expr_ref res(m);

7
src/util/total_order.h
View file

@ -79,12 +79,7 @@ class total_order {
}
cell * to_cell(T const & a) const {
void * r;
#ifdef Z3DEBUG
bool ok =
#endif
m_map.find(a, r);
SASSERT(ok);
void * r = m_map.find(a);
return reinterpret_cast<cell*>(r);
}

5
src/util/uint_map.h
View file

@ -38,6 +38,11 @@ public:
return v != 0;
}
}
T * find(unsigned k) const {
SASSERT(k < m_map.size() && m_map[k] != 0);
return m_map[k];
}
void insert(unsigned k, T * v) {
m_map.reserve(k+1);