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

Minor code cleanup

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-02 23:23:56 -07:00
parent 6464468cd8
commit e0e435582a
1 changed files with 29 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

63
src/muz/spacer/spacer_sym_mux.cpp
View file

@ -55,7 +55,12 @@ std::string sym_mux::get_suffix(unsigned i) const
return m_suffixes[i]; return m_suffixes[i];
} }
void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range, /**
populates a vector called tuple with func_decl's
tuple[0] is called primary and is used as key in various maps
*/
void sym_mux::create_tuple(func_decl* prefix, unsigned arity,
sort * const * domain, sort * range,
unsigned tuple_length, decl_vector & tuple) unsigned tuple_length, decl_vector & tuple)
{ {
SASSERT(tuple_length > 0); SASSERT(tuple_length > 0);
@ -63,16 +68,18 @@ void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * dom
tuple.push_back(0); tuple.push_back(0);
} }
SASSERT(tuple.size() == tuple_length); SASSERT(tuple.size() == tuple_length);
std::string pre = prefix->get_name().str();
for (unsigned i = 0; i < tuple_length; i++) { for (unsigned i = 0; i < tuple_length; i++) {
if (tuple[i] != 0) { if (tuple[i] != 0) {
SASSERT(tuple[i]->get_arity() == arity); SASSERT(tuple[i]->get_arity() == arity);
SASSERT(tuple[i]->get_range() == range); SASSERT(tuple[i]->get_range() == range);
//domain should match as well, but we won't bother checking an array equality //domain should match as well, but we won't bother
//checking an array equality
} else { } else {
std::string name = pre + get_suffix(i); std::string name = prefix->get_name().str();
tuple[i] = m.mk_func_decl(symbol(name.c_str()), arity, domain, range); name += get_suffix(i);
tuple[i] = m.mk_func_decl(symbol(name.c_str()), arity,
domain, range);
} }
m_ref_holder.push_back(tuple[i]); m_ref_holder.push_back(tuple[i]);
m_sym2idx.insert(tuple[i], i); m_sym2idx.insert(tuple[i], i);
@ -85,6 +92,9 @@ void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * dom
m_ref_holder.push_back(prefix); m_ref_holder.push_back(prefix);
} }
/**
extends a tuple in which prim is primary to the given size
*/
void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const
{ {
SASSERT(m_prim2all.contains(prim)); SASSERT(m_prim2all.contains(prim));
@ -98,8 +108,9 @@ void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const
std::string prefix_name = prefix->get_name().bare_str(); std::string prefix_name = prefix->get_name().bare_str();
for (unsigned i = tuple.size(); i < sz; ++i) { for (unsigned i = tuple.size(); i < sz; ++i) {
std::string name = prefix_name + get_suffix(i); std::string name = prefix_name + get_suffix(i);
func_decl * new_sym = m.mk_func_decl(symbol(name.c_str()), prefix->get_arity(), func_decl * new_sym =
prefix->get_domain(), prefix->get_range()); m.mk_func_decl(symbol(name.c_str()), prefix->get_arity(),
prefix->get_domain(), prefix->get_range());
tuple.push_back(new_sym); tuple.push_back(new_sym);
m_ref_holder.push_back(new_sym); m_ref_holder.push_back(new_sym);
@ -108,8 +119,9 @@ 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 /** given a func_decl with src_idx returns its version with tgt_idx */
{ func_decl * sym_mux::conv(func_decl * sym,
unsigned src_idx, unsigned tgt_idx) const {
if (src_idx == tgt_idx) { return sym; } if (src_idx == tgt_idx) { return sym; }
func_decl * prim = (src_idx == 0) ? sym : get_primary(sym); func_decl * prim = (src_idx == 0) ? sym : get_primary(sym);
if (tgt_idx > src_idx) { if (tgt_idx > src_idx) {
@ -121,15 +133,10 @@ func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) c
} }
struct sym_mux::formula_checker { struct sym_mux::formula_checker {
formula_checker(const sym_mux & parent, bool all, unsigned idx) : formula_checker(const sym_mux & parent, unsigned idx) :
m_parent(parent), m_all(all), m_idx(idx), m_parent(parent), m_idx(idx),
m_found_what_needed(false) m_found_what_needed(false) {}
{
}
void operator()(expr * e) void operator()(expr * e)
{ {
@ -140,28 +147,15 @@ struct sym_mux::formula_checker {
if (!m_parent.try_get_index(sym, sym_idx)) { return; } if (!m_parent.try_get_index(sym, sym_idx)) { return; }
bool have_idx = sym_idx == m_idx; bool have_idx = sym_idx == m_idx;
m_found_what_needed = !have_idx;
if (m_all ? (!have_idx) : have_idx) {
m_found_what_needed = true;
}
} }
bool all_have_idx() const bool all_have_idx() const {return !m_found_what_needed;}
{
SASSERT(m_all); //we were looking for the queried property
return !m_found_what_needed;
}
bool some_with_idx() const
{
SASSERT(!m_all); //we were looking for the queried property
return m_found_what_needed;
}
private: private:
const sym_mux & m_parent; const sym_mux & m_parent;
bool m_all;
unsigned m_idx; unsigned m_idx;
/** /**
@ -176,7 +170,7 @@ private:
bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const
{ {
expr_mark visited; expr_mark visited;
formula_checker chck(*this, true, idx); formula_checker chck(*this, idx);
for_each_expr(chck, visited, e); for_each_expr(chck, visited, e);
return chck.all_have_idx(); return chck.all_have_idx();
} }
@ -189,7 +183,8 @@ private:
unsigned m_to_idx; unsigned m_to_idx;
bool m_homogenous; bool m_homogenous;
public: public:
conv_rewriter_cfg(const sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous) conv_rewriter_cfg(const sym_mux & parent, unsigned from_idx,
unsigned to_idx, bool homogenous)
: m(parent.get_manager()), : m(parent.get_manager()),
m_parent(parent), m_parent(parent),
m_from_idx(from_idx), m_from_idx(from_idx),