mirror of
https://github.com/Z3Prover/z3
synced 2025-04-30 04:15:51 +00:00
removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
60c0e73b2f
commit
5ce85aba40
8 changed files with 86 additions and 87 deletions
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -1838,7 +1838,7 @@ namespace pdr {
|
|||
|
||||
}
|
||||
|
||||
void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info>& rs) const {
|
||||
void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info>& 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<relation_info> 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);
|
||||
|
|
|
|||
|
|
@ -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<relation_info> & rs) const;
|
||||
void get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info> & 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();
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ Revision History:
|
|||
|
||||
using namespace pdr;
|
||||
|
||||
sym_mux::sym_mux(ast_manager & m, const vector<std::string> & suffixes)
|
||||
sym_mux::sym_mux(ast_manager & m, vector<std::string> & 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<std::string> & 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(); i<sz; ++i) {
|
||||
std::string name = prefix_name+get_suffix(i);
|
||||
for(unsigned i = tuple.size(); i < sz; ++i) {
|
||||
std::string name = prefix_name + get_suffix(i);
|
||||
func_decl * new_sym = m.mk_func_decl(symbol(name.c_str()), prefix->get_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(i<vect.size()) {
|
||||
if(!has_nonmodel_symbol(vect[i].get())) {
|
||||
unsigned i = 0;
|
||||
while (i < vect.size()) {
|
||||
if (!has_nonmodel_symbol(vect[i].get())) {
|
||||
i++;
|
||||
continue;
|
||||
}
|
||||
vect[i] = vect.back();
|
||||
vect.pop_back();
|
||||
else {
|
||||
vect[i] = vect.back();
|
||||
vect.pop_back();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -526,10 +524,10 @@ public:
|
|||
bool operator()(func_decl * sym1, func_decl * sym2)
|
||||
{
|
||||
unsigned idx1, idx2;
|
||||
if(!m_parent.try_get_index(sym1, idx1)) { idx1 = UINT_MAX; }
|
||||
if(!m_parent.try_get_index(sym2, idx2)) { idx2 = UINT_MAX; }
|
||||
if (!m_parent.try_get_index(sym1, idx1)) { idx1 = UINT_MAX; }
|
||||
if (!m_parent.try_get_index(sym2, idx2)) { idx2 = UINT_MAX; }
|
||||
|
||||
if(idx1!=idx2) { return idx1<idx2; }
|
||||
if (idx1 != idx2) { return idx1<idx2; }
|
||||
return lt(sym1->get_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<unsigned>(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();
|
||||
|
|
|
|||
|
|
@ -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<std::string> m_suffixes;
|
||||
vector<std::string> 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<std::string> & suffixes);
|
||||
sym_mux(ast_manager & m, vector<std::string> & 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
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -32,8 +32,8 @@ protected:
|
|||
|
||||
void free_memory() {
|
||||
if (m_buffer != reinterpret_cast<T*>(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<T *>(m_initial_buffer)),
|
||||
m_pos(0),
|
||||
m_capacity(INITIAL_SIZE) {
|
||||
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
|
||||
m_pos(0),
|
||||
m_capacity(INITIAL_SIZE) {
|
||||
}
|
||||
|
||||
|
||||
buffer(const buffer & source):
|
||||
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
|
||||
m_pos(0),
|
||||
m_capacity(INITIAL_SIZE) {
|
||||
m_buffer(reinterpret_cast<T *>(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<T *>(m_initial_buffer)),
|
||||
m_pos(0),
|
||||
m_capacity(INITIAL_SIZE) {
|
||||
m_buffer(reinterpret_cast<T *>(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<T *>(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();
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue