mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Remove dead code

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-22 08:57:17 -07:00
parent 00f870b7ff
commit 4e9023b8fe
2 changed files with 0 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/muz/spacer/spacer_context.cpp
View file

@ -854,35 +854,6 @@ void pred_transformer::find_predecessors(datalog::rule const& r, ptr_vector<func
}
}
void pred_transformer::find_predecessors(vector<std::pair<func_decl*, unsigned> >& preds) const
{
preds.reset();
obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
for (; it != end; it++) {
datalog::rule const& r = *it->m_value;
unsigned tail_sz = r.get_uninterpreted_tail_size();
for (unsigned ti = 0; ti < tail_sz; ti++) {
preds.push_back(std::make_pair (r.get_tail(ti)->get_decl(), ti));
}
}
}
void pred_transformer::remove_predecessors(expr_ref_vector& literals)
{
// remove tags
for (unsigned i = 0; i < literals.size(); ) {
expr* l = literals[i].get();
m.is_not(l, l);
if (m_tag2rule.contains(l)) {
literals[i] = literals.back();
literals.pop_back();
} else {
++i;
}
}
}
void pred_transformer::simplify_formulas()
{m_frames.simplify_formulas ();}

2
src/muz/spacer/spacer_context.h
View file

@ -370,9 +370,7 @@ public:
unsigned level, unsigned oidx, bool must,
const ptr_vector<app> **aux);
void remove_predecessors(expr_ref_vector& literals);
void find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& predicates) const;
void find_predecessors(vector<std::pair<func_decl*, unsigned> >& predicates) const;
datalog::rule const* find_rule(model &mev, bool& is_concrete,
vector<bool>& reach_pred_used,
unsigned& num_reuse_reach);