From 5ce85aba40746afcc0e368386f7c201d5f656bf8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Feb 2016 22:23:37 +0000 Subject: [PATCH] removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 6 +-- src/muz/pdr/pdr_context.cpp | 6 +-- src/muz/pdr/pdr_context.h | 6 +-- src/muz/pdr/pdr_manager.h | 16 ++++---- src/muz/pdr/pdr_sym_mux.cpp | 76 ++++++++++++++++++------------------- src/muz/pdr/pdr_sym_mux.h | 18 ++++----- src/sat/sat_clause.cpp | 1 + src/util/buffer.h | 44 ++++++++++----------- 8 files changed, 86 insertions(+), 87 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 0c6e2fae4..a355f8c88 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2794,9 +2794,9 @@ int main() { Z3_open_log("z3.log"); #endif display_version(); - simple_example(); - demorgan(); - find_model_example1(); + //simple_example(); + //demorgan(); + //find_model_example1(); find_model_example2(); prove_example1(); prove_example2(); diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 0c79f0393..bd7ce0b3c 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1838,7 +1838,7 @@ namespace pdr { } - void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector& rs) const { + void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector& rs) { decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); for (; it != end; ++it) { pred_transformer* r = it->m_value; @@ -1962,7 +1962,7 @@ namespace pdr { return m_search.get_trace(*this); } - expr_ref context::mk_unsat_answer() const { + expr_ref context::mk_unsat_answer() { expr_ref_vector refs(m); vector rs; get_level_property(m_inductive_lvl, refs, rs); @@ -2364,7 +2364,7 @@ namespace pdr { return result == l_false; } - void context::display_certificate(std::ostream& strm) const { + void context::display_certificate(std::ostream& strm) { switch(m_last_result) { case l_false: { expr_ref_vector refs(m); diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 54bf5a691..c3567bdd8 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -349,10 +349,10 @@ namespace pdr { lbool expand_state(model_node& n, expr_ref_vector& cube, bool& uses_level); void create_children(model_node& n); expr_ref mk_sat_answer() const; - expr_ref mk_unsat_answer() const; + expr_ref mk_unsat_answer(); // Generate inductive property - void get_level_property(unsigned lvl, expr_ref_vector& res, vector & rs) const; + void get_level_property(unsigned lvl, expr_ref_vector& res, vector & rs); // Initialization @@ -406,7 +406,7 @@ namespace pdr { std::ostream& display(std::ostream& strm) const; - void display_certificate(std::ostream& strm) const; + void display_certificate(std::ostream& strm); lbool solve(); diff --git a/src/muz/pdr/pdr_manager.h b/src/muz/pdr/pdr_manager.h index 9049e4ca9..580075b78 100644 --- a/src/muz/pdr/pdr_manager.h +++ b/src/muz/pdr/pdr_manager.h @@ -181,26 +181,26 @@ namespace pdr { return m_mux.is_homogenous_formula(f, n_index()); } - func_decl * o2n(func_decl * p, unsigned o_idx) const { + func_decl * o2n(func_decl * p, unsigned o_idx) { return m_mux.conv(p, o_index(o_idx), n_index()); } - func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) const { + func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) { return m_mux.conv(p, o_index(src_idx), o_index(tgt_idx)); } - func_decl * n2o(func_decl * p, unsigned o_idx) const { + func_decl * n2o(func_decl * p, unsigned o_idx) { return m_mux.conv(p, n_index(), o_index(o_idx)); } - void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) const + void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) { m_mux.conv_formula(f, o_index(o_idx), n_index(), result, homogenous); } - void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) const + void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) { m_mux.conv_formula(f, n_index(), o_index(o_idx), result, homogenous); } - void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) const + void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) { m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous); } - void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous=true) const + void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous=true) { m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous); } /** @@ -237,7 +237,7 @@ namespace pdr { Increase indexes of state symbols in formula by dist. The 'N' index becomes 'O' index with number dist-1. */ - void formula_shift(expr * src, expr_ref & tgt, unsigned dist) const { + void formula_shift(expr * src, expr_ref & tgt, unsigned dist) { SASSERT(n_index()==0); SASSERT(o_index(0)==1); m_mux.shift_formula(src, dist, tgt); diff --git a/src/muz/pdr/pdr_sym_mux.cpp b/src/muz/pdr/pdr_sym_mux.cpp index 08b590e16..be20c502d 100644 --- a/src/muz/pdr/pdr_sym_mux.cpp +++ b/src/muz/pdr/pdr_sym_mux.cpp @@ -28,7 +28,7 @@ Revision History: using namespace pdr; -sym_mux::sym_mux(ast_manager & m, const vector & suffixes) +sym_mux::sym_mux(ast_manager & m, vector & suffixes) : m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes) { unsigned suf_sz = m_suffixes.size(); @@ -38,7 +38,7 @@ sym_mux::sym_mux(ast_manager & m, const vector & suffixes) } } -std::string sym_mux::get_suffix(unsigned i) const { +std::string sym_mux::get_suffix(unsigned i) { while(m_suffixes.size() <= i) { std::string new_suffix; symbol new_syffix_sym; @@ -88,7 +88,7 @@ void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * dom m_ref_holder.push_back(prefix); } -void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const { +void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) { SASSERT(m_prim2all.contains(prim)); decl_vector& tuple = m_prim2all.find_core(prim)->get_data().m_value; SASSERT(tuple[0]==prim); @@ -98,10 +98,10 @@ void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const { func_decl * prefix; TRUSTME(m_prim2prefix.find(prim, prefix)); std::string prefix_name = prefix->get_name().bare_str(); - for(unsigned i=tuple.size(); iget_arity(), - prefix->get_domain(), prefix->get_range()); + prefix->get_domain(), prefix->get_range()); tuple.push_back(new_sym); m_ref_holder.push_back(new_sym); @@ -110,7 +110,7 @@ void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const { } } -func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const +func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) { if(src_idx==tgt_idx) { return sym; } func_decl * prim = (src_idx==0) ? sym : get_primary(sym); @@ -347,12 +347,12 @@ struct sym_mux::conv_rewriter_cfg : public default_rewriter_cfg { private: ast_manager & m; - const sym_mux & m_parent; + sym_mux & m_parent; unsigned m_from_idx; unsigned m_to_idx; bool m_homogenous; public: - conv_rewriter_cfg(const sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous) + conv_rewriter_cfg(sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous) : m(parent.get_manager()), m_parent(parent), m_from_idx(from_idx), @@ -374,7 +374,7 @@ public: } }; -void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous) const +void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous) { if(src_idx==tgt_idx) { res = f; @@ -389,10 +389,10 @@ struct sym_mux::shifting_rewriter_cfg : public default_rewriter_cfg { private: ast_manager & m; - const sym_mux & m_parent; + sym_mux & m_parent; int m_shift; public: - shifting_rewriter_cfg(const sym_mux & parent, int shift) + shifting_rewriter_cfg(sym_mux & parent, int shift) : m(parent.get_manager()), m_parent(parent), m_shift(shift) {} @@ -413,7 +413,7 @@ public: } }; -void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) const +void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) { if(dist==0) { res = f; @@ -425,7 +425,7 @@ void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) const } void sym_mux::conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, - expr_ref_vector & res) const + expr_ref_vector & res) { res.reset(); expr * const * begin = vect.c_ptr(); @@ -441,11 +441,11 @@ void sym_mux::filter_idx(expr_ref_vector & vect, unsigned idx) const { unsigned i = 0; while (i < vect.size()) { expr* e = vect[i].get(); - if(contains(e, idx) && is_homogenous_formula(e, idx)) { + if (contains(e, idx) && is_homogenous_formula(e, idx)) { i++; } else { - //we don't allow mixing states inside vector elements + // we don't allow mixing states inside vector elements SASSERT(!contains(e, idx)); vect[i] = vect.back(); vect.pop_back(); @@ -476,23 +476,20 @@ class sym_mux::nonmodel_sym_checker { bool m_found; public: nonmodel_sym_checker(const sym_mux & parent) : - m_parent(parent), m_found(false) - { + m_parent(parent), m_found(false) { } - void operator()(expr * e) - { + void operator()(expr * e) { if(m_found || !is_app(e)) { return; } - + func_decl * sym = to_app(e)->get_decl(); - + if(m_parent.is_non_model_sym(sym)) { m_found = true; } } - bool found() const - { + bool found() const { return m_found; } }; @@ -504,14 +501,15 @@ bool sym_mux::has_nonmodel_symbol(expr * e) const { } void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const { - unsigned i=0; - while(iget_name(), sym2->get_name()); } }; @@ -545,9 +543,9 @@ std::string sym_mux::pp_model(const model_core & mdl) const { std::sort(consts.begin(), consts.end(), decl_idx_comparator(*this)); std::stringstream res; - + decl_vector::iterator end = consts.end(); - for(decl_vector::iterator it = consts.begin(); it!=end; it++) { + for (decl_vector::iterator it = consts.begin(); it!=end; it++) { func_decl * d = *it; std::string name = d->get_name().str(); const char * arrow = " -> "; @@ -555,11 +553,11 @@ std::string sym_mux::pp_model(const model_core & mdl) const { unsigned indent = static_cast(name.length() + strlen(arrow)); res << mk_pp(mdl.get_const_interp(d), m, indent) << "\n"; - if(it+1!=end) { + if (it+1 != end) { unsigned idx1, idx2; - if(!try_get_index(*it, idx1)) { idx1 = UINT_MAX; } - if(!try_get_index(*(it+1), idx2)) { idx2 = UINT_MAX; } - if(idx1!=idx2) { res << "\n"; } + if (!try_get_index(*it, idx1)) { idx1 = UINT_MAX; } + if (!try_get_index(*(it+1), idx2)) { idx2 = UINT_MAX; } + if (idx1 != idx2) { res << "\n"; } } } return res.str(); diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h index 986d961c7..a07b712ca 100644 --- a/src/muz/pdr/pdr_sym_mux.h +++ b/src/muz/pdr/pdr_sym_mux.h @@ -46,7 +46,7 @@ private: mutable unsigned m_next_sym_suffix_idx; mutable symbols m_used_suffixes; /** Here we have default suffixes for each of the variants */ - mutable vector m_suffixes; + vector m_suffixes; /** @@ -89,12 +89,12 @@ private: class index_collector; class variable_collector; - std::string get_suffix(unsigned i) const; - void ensure_tuple_size(func_decl * prim, unsigned sz) const; + std::string get_suffix(unsigned i); + void ensure_tuple_size(func_decl * prim, unsigned sz); expr_ref isolate_o_idx(expr* e, unsigned idx) const; public: - sym_mux(ast_manager & m, const vector & suffixes); + sym_mux(ast_manager & m, vector & suffixes); ast_manager & get_manager() const { return m; } @@ -130,7 +130,7 @@ public: /** Return symbol created from prefix, or 0 if the prefix was never used. */ - func_decl * try_get_by_prefix(func_decl* prefix, unsigned idx) const { + func_decl * try_get_by_prefix(func_decl* prefix, unsigned idx) { func_decl * prim = try_get_primary_by_prefix(prefix); if(!prim) { return 0; @@ -199,22 +199,22 @@ public: /** Convert symbol sym which has to be of src_idx variant into variant tgt_idx. */ - func_decl * conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const; + func_decl * conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx); /** Convert src_idx symbols in formula f variant into tgt_idx. If homogenous is true, formula cannot contain symbols of other variants. */ - void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous=true) const; + void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous=true); void conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, - expr_ref_vector & res) const; + expr_ref_vector & res); /** Shifts the muxed symbols in f by dist. Dist can be negative, but it should never shift symbol index to a negative value. */ - void shift_formula(expr * f, int dist, expr_ref & res) const; + void shift_formula(expr * f, int dist, expr_ref & res); /** Remove from vect literals (atoms or negations of atoms) of symbols diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index fe4822406..279d84375 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -36,6 +36,7 @@ namespace sat { memcpy(m_lits, lits, sizeof(literal) * sz); mark_strengthened(); SASSERT(check_approx()); + SASSERT(sz > 1); } var_approx_set clause::approx(unsigned num, literal const * lits) { diff --git a/src/util/buffer.h b/src/util/buffer.h index 3495ca1d3..422db07aa 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -32,8 +32,8 @@ protected: void free_memory() { if (m_buffer != reinterpret_cast(m_initial_buffer)) { - memory::deallocate(m_buffer); - } + dealloc_svect(m_buffer); + } } void expand() { @@ -66,57 +66,57 @@ public: typedef const T * const_iterator; buffer(): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { } - + buffer(const buffer & source): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { unsigned sz = source.size(); for(unsigned i = 0; i < sz; i++) { push_back(source.m_buffer[i]); } } - + buffer(unsigned sz, const T & elem): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { for (unsigned i = 0; i < sz; i++) { push_back(elem); } SASSERT(size() == sz); } - + ~buffer() { destroy(); } - + void reset() { if (CallDestructors) { destroy_elements(); } m_pos = 0; } - + void finalize() { destroy(); m_buffer = reinterpret_cast(m_initial_buffer); m_pos = 0; m_capacity = INITIAL_SIZE; } - + unsigned size() const { return m_pos; } - + bool empty() const { return m_pos == 0; } - + iterator begin() { return m_buffer; } @@ -130,15 +130,15 @@ public: if (CallDestructors) { iterator e = end(); for (; it != e; ++it) { - it->~T(); + it->~T(); } } } - + const_iterator begin() const { return m_buffer; } - + const_iterator end() const { return m_buffer + size(); }