mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Remove dead code

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-02 22:57:22 -07:00
parent aa77a918cd
commit 6464468cd8
3 changed files with 21 additions and 518 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/muz/spacer/spacer_manager.h
View file

@ -96,35 +96,6 @@ public:
func_decl * get_o_pred(func_decl * s, unsigned idx);
func_decl * get_n_pred(func_decl * s);
void get_o_index(func_decl* p, unsigned& idx) const {
m_mux.try_get_index(p, idx);
SASSERT(idx != n_index());
idx--; // m_mux has indices starting at 1
}
bool is_o(func_decl * p, unsigned idx) const
{return m_mux.has_index(p, o_index(idx));}
bool is_o(func_decl * p) const {
unsigned idx;
return m_mux.try_get_index(p, idx) && idx != n_index();
}
bool is_o(expr* e) const
{return is_app(e) && is_o(to_app(e)->get_decl());}
bool is_o(expr* e, unsigned idx) const
{return is_app(e) && is_o(to_app(e)->get_decl(), idx);}
bool is_n(func_decl * p) const
{return m_mux.has_index(p, n_index());}
bool is_n(expr* e) const
{return is_app(e) && is_n(to_app(e)->get_decl());}
/** true if f doesn't contain any n predicates */
bool is_o_formula(expr * f) const
{return !m_mux.contains(f, n_index());}
/** true if f contains only o state preds of index o_idx */
bool is_o_formula(expr * f, unsigned o_idx) const
{return m_mux.is_homogenous_formula(f, o_index(o_idx));}
/** true if f doesn't contain any o predicates */
bool is_n_formula(expr * f) const
{return m_mux.is_homogenous_formula(f, n_index());}
@ -135,18 +106,22 @@ public:
func_decl * n2o(func_decl * p, unsigned o_idx) const
{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) const
{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) const
{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
{m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous);}
{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
{m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous);}
{m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx),
tgt, homogenous);}
};

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

@ -82,7 +82,6 @@ void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * dom
m_prim2all.insert(tuple[0], tuple);
m_prefix2prim.insert(prefix, tuple[0]);
m_prim2prefix.insert(tuple[0], prefix);
m_prim_preds.push_back(tuple[0]);
m_ref_holder.push_back(prefix);
}
@ -122,32 +121,7 @@ func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) c
}
func_decl * sym_mux::get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx,
unsigned arity, sort * const * domain, sort * range)
{
func_decl * prim = try_get_primary_by_prefix(prefix);
if (prim) {
SASSERT(prim->get_arity() == arity);
SASSERT(prim->get_range() == range);
//domain should match as well, but we won't bother checking an array equality
return conv(prim, 0, idx);
}
decl_vector syms;
create_tuple(prefix, arity, domain, range, idx + 1, syms);
return syms[idx];
}
bool sym_mux::is_muxed_lit(expr * e, unsigned idx) const
{
if (!is_app(e)) { return false; }
app * a = to_app(e);
if (m.is_not(a) && is_app(a->get_arg(0))) {
a = to_app(a->get_arg(0));
}
return is_muxed(a->get_decl());
}
struct sym_mux::formula_checker {
@ -198,155 +172,15 @@ private:
bool m_found_what_needed;
};
bool sym_mux::contains(expr * e, unsigned idx) const
{
formula_checker chck(*this, false, idx);
for_each_expr(chck, m_visited, e);
m_visited.reset();
return chck.some_with_idx();
}
bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const
{
expr_mark visited;
formula_checker chck(*this, true, idx);
for_each_expr(chck, m_visited, e);
m_visited.reset();
for_each_expr(chck, visited, e);
return chck.all_have_idx();
}
bool sym_mux::is_homogenous(const expr_ref_vector & vect, unsigned idx) const
{
expr * const * begin = vect.c_ptr();
expr * const * end = begin + vect.size();
for (expr * const * it = begin; it != end; it++) {
if (!is_homogenous_formula(*it, idx)) {
return false;
}
}
return true;
}
class sym_mux::index_collector {
sym_mux const& m_parent;
svector<bool> m_indices;
public:
index_collector(sym_mux const& s):
m_parent(s) {}
void operator()(expr * e)
{
if (is_app(e)) {
func_decl * sym = to_app(e)->get_decl();
unsigned idx;
if (m_parent.try_get_index(sym, idx)) {
SASSERT(idx > 0);
--idx;
if (m_indices.size() <= idx) {
m_indices.resize(idx + 1, false);
}
m_indices[idx] = true;
}
}
}
void extract(unsigned_vector& indices)
{
for (unsigned i = 0; i < m_indices.size(); ++i) {
if (m_indices[i]) {
indices.push_back(i);
}
}
}
};
void sym_mux::collect_indices(expr* e, unsigned_vector& indices) const
{
indices.reset();
index_collector collector(*this);
for_each_expr(collector, m_visited, e);
m_visited.reset();
collector.extract(indices);
}
class sym_mux::variable_collector {
sym_mux const& m_parent;
vector<ptr_vector<app> >& m_vars;
public:
variable_collector(sym_mux const& s, vector<ptr_vector<app> >& vars):
m_parent(s), m_vars(vars) {}
void operator()(expr * e)
{
if (is_app(e)) {
func_decl * sym = to_app(e)->get_decl();
unsigned idx;
if (m_parent.try_get_index(sym, idx)) {
SASSERT(idx > 0);
--idx;
if (m_vars.size() <= idx) {
m_vars.resize(idx + 1, ptr_vector<app>());
}
m_vars[idx].push_back(to_app(e));
}
}
}
};
void sym_mux::collect_variables(expr* e, vector<ptr_vector<app> >& vars) const
{
vars.reset();
variable_collector collector(*this, vars);
for_each_expr(collector, m_visited, e);
m_visited.reset();
}
class sym_mux::hmg_checker {
const sym_mux & m_parent;
bool m_found_idx;
unsigned m_idx;
bool m_multiple_indexes;
public:
hmg_checker(const sym_mux & parent) :
m_parent(parent), m_found_idx(false), m_multiple_indexes(false)
{
}
void operator()(expr * e)
{
if (m_multiple_indexes || !is_app(e)) { return; }
func_decl * sym = to_app(e)->get_decl();
unsigned sym_idx;
if (!m_parent.try_get_index(sym, sym_idx)) { return; }
if (!m_found_idx) {
m_found_idx = true;
m_idx = sym_idx;
return;
}
if (m_idx == sym_idx) { return; }
m_multiple_indexes = true;
}
bool has_multiple_indexes() const
{
return m_multiple_indexes;
}
};
bool sym_mux::is_homogenous_formula(expr * e) const
{
hmg_checker chck(*this);
for_each_expr(chck, m_visited, e);
m_visited.reset();
return !chck.has_multiple_indexes();
}
struct sym_mux::conv_rewriter_cfg : public default_rewriter_cfg {
private:
ast_manager & m;
@ -379,8 +213,8 @@ 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) const {
if (src_idx == tgt_idx) {
res = f;
return;
@ -389,220 +223,3 @@ void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_re
rewriter_tpl<conv_rewriter_cfg> rwr(m, false, r_cfg);
rwr(f, res);
}
struct sym_mux::shifting_rewriter_cfg : public default_rewriter_cfg {
private:
ast_manager & m;
const sym_mux & m_parent;
int m_shift;
public:
shifting_rewriter_cfg(const sym_mux & parent, int shift)
: m(parent.get_manager()),
m_parent(parent),
m_shift(shift) {}
bool get_subst(expr * s, expr * & t, proof * & t_pr)
{
if (!is_app(s)) { return false; }
app * a = to_app(s);
func_decl * sym = a->get_decl();
unsigned idx;
if (!m_parent.try_get_index(sym, idx)) {
return false;
}
SASSERT(static_cast<int>(idx) + m_shift >= 0);
func_decl * tgt = m_parent.conv(sym, idx, idx + m_shift);
t = m.mk_app(tgt, a->get_args());
return true;
}
};
void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) const
{
if (dist == 0) {
res = f;
return;
}
shifting_rewriter_cfg r_cfg(*this, dist);
rewriter_tpl<shifting_rewriter_cfg> rwr(m, false, r_cfg);
rwr(f, res);
}
void sym_mux::conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx,
expr_ref_vector & res) const
{
res.reset();
expr * const * begin = vect.c_ptr();
expr * const * end = begin + vect.size();
for (expr * const * it = begin; it != end; it++) {
expr_ref converted(m);
conv_formula(*it, src_idx, tgt_idx, converted);
res.push_back(converted);
}
}
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)) {
i++;
} else {
//we don't allow mixing states inside vector elements
SASSERT(!contains(e, idx));
vect[i] = vect.back();
vect.pop_back();
}
}
}
void sym_mux::partition_o_idx(
expr_ref_vector const& lits,
expr_ref_vector& o_lits,
expr_ref_vector& other, unsigned idx) const
{
for (unsigned i = 0; i < lits.size(); ++i) {
if (contains(lits[i], idx) && is_homogenous_formula(lits[i], idx)) {
o_lits.push_back(lits[i]);
} else {
other.push_back(lits[i]);
}
}
}
class sym_mux::nonmodel_sym_checker {
const sym_mux & m_parent;
bool m_found;
public:
nonmodel_sym_checker(const sym_mux & parent) :
m_parent(parent), m_found(false)
{
}
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
{
return m_found;
}
};
bool sym_mux::has_nonmodel_symbol(expr * e) const
{
nonmodel_sym_checker chck(*this);
for_each_expr(chck, e);
return chck.found();
}
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())) {
i++;
continue;
}
vect[i] = vect.back();
vect.pop_back();
}
}
class sym_mux::decl_idx_comparator {
const sym_mux & m_parent;
public:
decl_idx_comparator(const sym_mux & parent)
: m_parent(parent)
{ }
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 (idx1 != idx2) { return idx1 < idx2; }
return lt(sym1->get_name(), sym2->get_name());
}
};
std::string sym_mux::pp_model(const model_core & mdl) const
{
decl_vector consts;
unsigned sz = mdl.get_num_constants();
for (unsigned i = 0; i < sz; i++) {
func_decl * d = mdl.get_constant(i);
consts.push_back(d);
}
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++) {
func_decl * d = *it;
std::string name = d->get_name().str();
const char * arrow = " -> ";
res << name << arrow;
unsigned indent = static_cast<unsigned>(name.length() + strlen(arrow));
res << mk_pp(mdl.get_const_interp(d), m, indent) << "\n";
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"; }
}
}
return res.str();
}
#if 0
class sym_mux::index_renamer_cfg : public default_rewriter_cfg {
const sym_mux & m_parent;
unsigned m_idx;
public:
index_renamer_cfg(const sym_mux & p, unsigned idx) : m_parent(p), m_idx(idx) {}
bool get_subst(expr * s, expr * & t, proof * & t_pr)
{
if (!is_app(s)) { return false; }
app * a = to_app(s);
if (a->get_family_id() != null_family_id) {
return false;
}
func_decl * sym = a->get_decl();
unsigned idx;
if (!m_parent.try_get_index(sym, idx)) {
return false;
}
if (m_idx == idx) {
return false;
}
ast_manager& m = m_parent.get_manager();
symbol name = symbol((sym->get_name().str() + "!").c_str());
func_decl * tgt = m.mk_func_decl(name, sym->get_arity(), sym->get_domain(), sym->get_range());
t = m.mk_app(tgt, a->get_num_args(), a->get_args());
return true;
}
};
#endif

107
src/muz/spacer/spacer_sym_mux.h
View file

@ -7,7 +7,8 @@ Module Name:
Abstract:
A symbol multiplexer that helps with having multiple versions of each of a set of symbols.
A symbol multiplexer that helps with having multiple versions of
each of a set of symbols.
Author:
@ -20,18 +21,17 @@ Revision History:
#ifndef _SYM_MUX_H_
#define _SYM_MUX_H_
#include <vector>
#include <string>
#include "ast/ast.h"
#include "util/map.h"
#include "util/vector.h"
#include <vector>
class model_core;
namespace spacer {
class sym_mux {
public:
typedef ptr_vector<app> app_vector;
typedef ptr_vector<func_decl> decl_vector;
private:
typedef obj_map<func_decl, unsigned> sym2u;
typedef obj_map<func_decl, decl_vector> sym2dv;
@ -41,7 +41,6 @@ private:
ast_manager & m;
mutable ast_ref_vector m_ref_holder;
mutable expr_mark m_visited;
mutable unsigned m_next_sym_suffix_idx;
mutable symbols m_used_suffixes;
@ -75,24 +74,15 @@ private:
*/
sym2sym m_prim2prefix;
decl_vector m_prim_preds;
obj_hashtable<func_decl> m_non_model_syms;
struct formula_checker;
struct conv_rewriter_cfg;
struct shifting_rewriter_cfg;
class decl_idx_comparator;
class hmg_checker;
class nonmodel_sym_checker;
class index_renamer_cfg;
class index_collector;
class variable_collector;
std::string get_suffix(unsigned i) const;
void ensure_tuple_size(func_decl * prim, unsigned sz) const;
expr_ref isolate_o_idx(expr* e, unsigned idx) const;
// expr_ref isolate_o_idx(expr* e, unsigned idx) const;
public:
sym_mux(ast_manager & m, const std::vector<std::string> & suffixes);
@ -101,9 +91,7 @@ public:
bool is_muxed(func_decl * sym) const { return m_sym2idx.contains(sym); }
bool try_get_index(func_decl * sym, unsigned & idx) const
{
return m_sym2idx.find(sym, idx);
}
{return m_sym2idx.find(sym, idx);}
bool has_index(func_decl * sym, unsigned idx) const
{
@ -143,30 +131,6 @@ public:
return conv(prim, 0, idx);
}
/**
Marks symbol as non-model which means it will not appear in models collected by
get_muxed_cube_from_model function.
This is to take care of auxiliary symbols introduced by the disjunction relations
to relativize lemmas coming from disjuncts.
*/
void mark_as_non_model(func_decl * sym)
{
SASSERT(is_muxed(sym));
m_non_model_syms.insert(get_primary(sym));
}
func_decl * get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx,
unsigned arity, sort * const * domain, sort * range);
bool is_muxed_lit(expr * e, unsigned idx) const;
bool is_non_model_sym(func_decl * s) const
{
return is_muxed(s) && m_non_model_syms.contains(get_primary(s));
}
/**
Create a multiplexed tuple of propositional constants.
Symbols may be suplied in the tuple vector,
@ -181,27 +145,7 @@ public:
Return true if the only multiplexed symbols which e contains are of index idx.
*/
bool is_homogenous_formula(expr * e, unsigned idx) const;
bool is_homogenous(const expr_ref_vector & vect, unsigned idx) const;
/**
Return true if all multiplexed symbols which e contains are of one index.
*/
bool is_homogenous_formula(expr * e) const;
/**
Return true if expression e contains a muxed symbol of index idx.
*/
bool contains(expr * e, unsigned idx) const;
/**
Collect indices used in expression.
*/
void collect_indices(expr* e, unsigned_vector& indices) const;
/**
Collect used variables of each index.
*/
void collect_variables(expr* e, vector<ptr_vector<app> >& vars) const;
/**
Convert symbol sym which has to be of src_idx variant into variant tgt_idx.
@ -213,43 +157,10 @@ public:
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_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx,
expr_ref_vector & res) const;
void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx,
expr_ref & res, bool homogenous = true) const;
/**
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;
/**
Remove from vect literals (atoms or negations of atoms) of symbols
that contain multiplexed symbols with indexes other than idx.
Each of the literals can contain only symbols multiplexed with one index
(this trivially holds if the literals are propositional).
Order of elements in vect may be modified by this function
*/
void filter_idx(expr_ref_vector & vect, unsigned idx) const;
/**
Partition literals into o_literals and others.
*/
void partition_o_idx(expr_ref_vector const& lits,
expr_ref_vector& o_lits,
expr_ref_vector& other, unsigned idx) const;
bool has_nonmodel_symbol(expr * e) const;
void filter_non_model_lits(expr_ref_vector & vect) const;
func_decl * const * begin_prim_preds() const { return m_prim_preds.begin(); }
func_decl * const * end_prim_preds() const { return m_prim_preds.end(); }
void get_muxed_cube_from_model(const model_core & model, expr_ref_vector & res) const;
std::string pp_model(const model_core & mdl) const;
};
}