mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
remove dead code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
b22fb74c5c
commit
cadfb804c5
|
|
@ -395,7 +395,6 @@ namespace pdr {
|
|||
lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
|
||||
if (is_sat == l_true && core) {
|
||||
core->reset();
|
||||
model2cube(*model,*core);
|
||||
n.set_model(model);
|
||||
}
|
||||
return is_sat;
|
||||
|
|
@ -697,34 +696,6 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
|
||||
void pred_transformer::model2cube(app* c, expr* val, expr_ref_vector& res) const {
|
||||
if (m.is_bool(val)) {
|
||||
res.push_back(m.is_true(val)?c:m.mk_not(c));
|
||||
}
|
||||
else {
|
||||
res.push_back(m.mk_eq(c, val));
|
||||
}
|
||||
}
|
||||
|
||||
void pred_transformer::model2cube(const model_core& mdl, func_decl * d, expr_ref_vector& res) const {
|
||||
expr_ref interp(m);
|
||||
get_value_from_model(mdl, d, interp);
|
||||
app* c = m.mk_const(d);
|
||||
model2cube(c, interp, res);
|
||||
}
|
||||
|
||||
void pred_transformer::model2cube(const model_core & mdl, expr_ref_vector & res) const {
|
||||
unsigned sz = mdl.get_num_constants();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
func_decl * d = mdl.get_constant(i);
|
||||
SASSERT(d->get_arity()==0);
|
||||
if (!m_solver.is_aux_symbol(d)) {
|
||||
model2cube(mdl, d, res);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// ----------------
|
||||
// model_node
|
||||
|
||||
|
|
@ -1103,11 +1074,9 @@ namespace pdr {
|
|||
m_inductive_lvl(0),
|
||||
m_cancel(false)
|
||||
{
|
||||
m_use_model_generalizer = m_params.get_bool("use-model-generalizer", false);
|
||||
}
|
||||
|
||||
context::~context() {
|
||||
reset_model_generalizers();
|
||||
reset_core_generalizers();
|
||||
reset();
|
||||
}
|
||||
|
|
@ -1169,7 +1138,6 @@ namespace pdr {
|
|||
|
||||
void context::update_rules(datalog::rule_set& rules) {
|
||||
decl2rel rels;
|
||||
init_model_generalizers(rules);
|
||||
init_core_generalizers(rules);
|
||||
init_rules(rules, rels);
|
||||
decl2rel::iterator it = rels.begin(), end = rels.end();
|
||||
|
|
@ -1294,18 +1262,6 @@ namespace pdr {
|
|||
};
|
||||
|
||||
|
||||
void context::reset_model_generalizers() {
|
||||
std::for_each(m_model_generalizers.begin(), m_model_generalizers.end(), delete_proc<model_generalizer>());
|
||||
m_model_generalizers.reset();
|
||||
}
|
||||
|
||||
void context::init_model_generalizers(datalog::rule_set& rules) {
|
||||
reset_model_generalizers();
|
||||
if (m_use_model_generalizer) {
|
||||
m_model_generalizers.push_back(alloc(model_evaluation_generalizer, *this, m));
|
||||
}
|
||||
}
|
||||
|
||||
void context::reset_core_generalizers() {
|
||||
std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc<core_generalizer>());
|
||||
m_core_generalizers.reset();
|
||||
|
|
@ -1552,11 +1508,7 @@ namespace pdr {
|
|||
}
|
||||
else {
|
||||
TRACE("pdr", tout << "node: " << &n << "\n";);
|
||||
for (unsigned i = 0; i < m_model_generalizers.size(); ++i) {
|
||||
(*m_model_generalizers[i])(n, cube);
|
||||
}
|
||||
|
||||
create_children(n, m_pm.mk_and(cube));
|
||||
create_children(n);
|
||||
}
|
||||
break;
|
||||
case l_false: {
|
||||
|
|
@ -1627,45 +1579,6 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
|
||||
// create children states from model cube.
|
||||
void context::create_children(model_node& n, expr* model) {
|
||||
if (!m_use_model_generalizer) {
|
||||
create_children2(n);
|
||||
return;
|
||||
}
|
||||
expr_ref_vector literals(m), sub_lits(m);
|
||||
expr_ref o_cube(m), n_cube(m);
|
||||
datalog::flatten_and(model, literals);
|
||||
ptr_vector<func_decl> preds;
|
||||
unsigned level = n.level();
|
||||
SASSERT(level > 0);
|
||||
n.pt().find_predecessors(n.model(), preds);
|
||||
n.pt().remove_predecessors(literals);
|
||||
TRACE("pdr",
|
||||
model_v2_pp(tout, n.model());
|
||||
tout << "Model cube\n";
|
||||
tout << mk_pp(model, m) << "\n";
|
||||
tout << "Predecessors\n";
|
||||
for (unsigned i = 0; i < preds.size(); ++i) {
|
||||
tout << preds[i]->get_name() << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
for (unsigned i = 0; i < preds.size(); ++i) {
|
||||
pred_transformer& pt = *m_rels.find(preds[i]);
|
||||
SASSERT(pt.head() == preds[i]);
|
||||
assign_ref_vector(sub_lits, literals);
|
||||
m_pm.filter_o_atoms(sub_lits, i);
|
||||
o_cube = m_pm.mk_and(sub_lits);
|
||||
m_pm.formula_o2n(o_cube, n_cube, i);
|
||||
model_node* child = alloc(model_node, &n, n_cube, pt, level-1);
|
||||
++m_stats.m_num_nodes;
|
||||
m_search.add_leaf(*child);
|
||||
}
|
||||
check_pre_closed(n);
|
||||
|
||||
TRACE("pdr", m_search.display(tout););
|
||||
}
|
||||
|
||||
/**
|
||||
\brief create children states from model cube.
|
||||
|
|
@ -1715,7 +1628,7 @@ namespace pdr {
|
|||
- Create sub-goals for L0 and L1.
|
||||
|
||||
*/
|
||||
void context::create_children2(model_node& n) {
|
||||
void context::create_children(model_node& n) {
|
||||
SASSERT(n.level() > 0);
|
||||
|
||||
pred_transformer& pt = n.pt();
|
||||
|
|
@ -1731,12 +1644,17 @@ namespace pdr {
|
|||
verbose_stream() << "Phi:\n" << mk_pp(phi, m) << "\n";);
|
||||
|
||||
model_evaluator mev(m);
|
||||
expr_ref_vector mdl(m), forms(m);
|
||||
expr_ref_vector mdl(m), forms(m), Phi(m);
|
||||
forms.push_back(T);
|
||||
forms.push_back(phi);
|
||||
datalog::flatten_and(forms);
|
||||
ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
|
||||
expr_ref_vector Phi = mev.minimize_literals(forms1, M);
|
||||
if (m_params.get_bool(":use-model-generalizer", false)) {
|
||||
Phi.append(mev.minimize_model(forms1, M));
|
||||
}
|
||||
else {
|
||||
Phi.append(mev.minimize_literals(forms1, M));
|
||||
}
|
||||
ptr_vector<func_decl> preds;
|
||||
pt.find_predecessors(r, preds);
|
||||
pt.remove_predecessors(Phi);
|
||||
|
|
@ -1842,9 +1760,6 @@ namespace pdr {
|
|||
st.update("PDR max depth", m_stats.m_max_depth);
|
||||
m_pm.collect_statistics(st);
|
||||
|
||||
for (unsigned i = 0; i < m_model_generalizers.size(); ++i) {
|
||||
m_model_generalizers[i]->collect_statistics(st);
|
||||
}
|
||||
for (unsigned i = 0; i < m_core_generalizers.size(); ++i) {
|
||||
m_core_generalizers[i]->collect_statistics(st);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -98,9 +98,6 @@ namespace pdr {
|
|||
void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx);
|
||||
void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
|
||||
|
||||
void model2cube(const model_core& md, func_decl * d, expr_ref_vector& res) const;
|
||||
void model2cube(app* c, expr* val, expr_ref_vector& res) const;
|
||||
|
||||
void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
|
||||
|
||||
// Debugging
|
||||
|
|
@ -157,8 +154,6 @@ namespace pdr {
|
|||
manager& get_pdr_manager() const { return pm; }
|
||||
ast_manager& get_manager() const { return m; }
|
||||
|
||||
void model2cube(const model_core & mdl, expr_ref_vector & res) const;
|
||||
|
||||
void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r);
|
||||
|
||||
void close(expr* e);
|
||||
|
|
@ -266,18 +261,6 @@ namespace pdr {
|
|||
|
||||
class context;
|
||||
|
||||
// 'state' is satisifiable with predecessor 'cube'.
|
||||
// Generalize predecessor still forcing satisfiability.
|
||||
class model_generalizer {
|
||||
protected:
|
||||
context& m_ctx;
|
||||
public:
|
||||
model_generalizer(context& ctx): m_ctx(ctx) {}
|
||||
virtual ~model_generalizer() {}
|
||||
virtual void operator()(model_node& n, expr_ref_vector& cube) = 0;
|
||||
virtual void collect_statistics(statistics& st) {}
|
||||
};
|
||||
|
||||
// 'state' is unsatisfiable at 'level' with 'core'.
|
||||
// Minimize or weaken core.
|
||||
class core_generalizer {
|
||||
|
|
@ -317,9 +300,7 @@ namespace pdr {
|
|||
pred_transformer* m_query;
|
||||
model_search m_search;
|
||||
lbool m_last_result;
|
||||
bool m_use_model_generalizer;
|
||||
unsigned m_inductive_lvl;
|
||||
ptr_vector<model_generalizer> m_model_generalizers;
|
||||
ptr_vector<core_generalizer> m_core_generalizers;
|
||||
stats m_stats;
|
||||
volatile bool m_cancel;
|
||||
|
|
@ -336,8 +317,7 @@ namespace pdr {
|
|||
void check_pre_closed(model_node& n);
|
||||
void expand_node(model_node& n);
|
||||
lbool expand_state(model_node& n, expr_ref_vector& cube);
|
||||
void create_children(model_node& n, expr* model);
|
||||
void create_children2(model_node& n);
|
||||
void create_children(model_node& n);
|
||||
expr_ref mk_sat_answer() const;
|
||||
expr_ref mk_unsat_answer() const;
|
||||
|
||||
|
|
@ -347,7 +327,6 @@ namespace pdr {
|
|||
|
||||
// Initialization
|
||||
class classifier_proc;
|
||||
void init_model_generalizers(datalog::rule_set& rules);
|
||||
void init_core_generalizers(datalog::rule_set& rules);
|
||||
|
||||
bool check_invariant(unsigned lvl);
|
||||
|
|
@ -359,7 +338,6 @@ namespace pdr {
|
|||
|
||||
void simplify_formulas();
|
||||
|
||||
void reset_model_generalizers();
|
||||
void reset_core_generalizers();
|
||||
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -29,19 +29,6 @@ Revision History:
|
|||
namespace pdr {
|
||||
|
||||
|
||||
//
|
||||
// eliminate conjuncts from cube as long as state is satisfied.
|
||||
//
|
||||
void model_evaluation_generalizer::operator()(model_node& n, expr_ref_vector& cube) {
|
||||
expr_ref_vector forms(cube.get_manager());
|
||||
forms.push_back(n.state());
|
||||
forms.push_back(n.pt().transition());
|
||||
datalog::flatten_and(forms);
|
||||
ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
|
||||
model_ref mdl = n.model_ptr();
|
||||
m_model_evaluator.minimize_model(forms1, mdl, cube);
|
||||
}
|
||||
|
||||
//
|
||||
// main propositional induction generalizer.
|
||||
// drop literals one by one from the core and check if the core is still inductive.
|
||||
|
|
|
|||
|
|
@ -25,14 +25,6 @@ Revision History:
|
|||
|
||||
namespace pdr {
|
||||
|
||||
class model_evaluation_generalizer : public model_generalizer {
|
||||
model_evaluator m_model_evaluator;
|
||||
public:
|
||||
model_evaluation_generalizer(context& ctx, ast_manager& m) : model_generalizer(ctx), m_model_evaluator(m) {}
|
||||
virtual ~model_evaluation_generalizer() {}
|
||||
virtual void operator()(model_node& n, expr_ref_vector& cube);
|
||||
};
|
||||
|
||||
class core_bool_inductive_generalizer : public core_generalizer {
|
||||
unsigned m_failure_limit;
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -90,33 +90,6 @@ std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) {
|
|||
//
|
||||
|
||||
|
||||
|
||||
bool model_evaluator::get_assignment(expr* e, expr*& var, expr*& val) {
|
||||
if (m.is_eq(e, var, val)) {
|
||||
if (!is_uninterp(var)) {
|
||||
std::swap(var, val);
|
||||
}
|
||||
if (m.is_true(val) || m.is_false(val) || m_arith.is_numeral(val)) {
|
||||
return true;
|
||||
}
|
||||
TRACE("pdr_verbose", tout << "no value for " << mk_pp(val, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
else if (m.is_not(e, var)) {
|
||||
val = m.mk_false();
|
||||
return true;
|
||||
}
|
||||
else if (m.is_bool(e)) {
|
||||
val = m.mk_true();
|
||||
var = e;
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
void model_evaluator::assign_value(expr* e, expr* val) {
|
||||
rational r;
|
||||
if (m.is_true(val)) {
|
||||
|
|
@ -166,7 +139,7 @@ void model_evaluator::reset() {
|
|||
m_model = 0;
|
||||
}
|
||||
|
||||
void model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl, expr_ref_vector & model) {
|
||||
expr_ref_vector model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl) {
|
||||
setup_model(mdl);
|
||||
|
||||
TRACE("pdr_verbose",
|
||||
|
|
@ -174,7 +147,7 @@ void model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_re
|
|||
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
|
||||
);
|
||||
|
||||
prune_by_cone_of_influence(formulas, model);
|
||||
expr_ref_vector model = prune_by_cone_of_influence(formulas);
|
||||
TRACE("pdr_verbose",
|
||||
tout << "pruned model:\n";
|
||||
for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";);
|
||||
|
|
@ -185,6 +158,8 @@ void model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_re
|
|||
setup_model(mdl);
|
||||
VERIFY(check_model(formulas));
|
||||
reset(););
|
||||
|
||||
return model;
|
||||
}
|
||||
|
||||
expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formulas, model_ref& mdl) {
|
||||
|
|
@ -340,7 +315,7 @@ void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>
|
|||
m_visited.reset();
|
||||
}
|
||||
|
||||
void model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model) {
|
||||
expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas) {
|
||||
ptr_vector<expr> tocollect;
|
||||
collect(formulas, tocollect);
|
||||
m1.reset();
|
||||
|
|
@ -349,19 +324,23 @@ void model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formul
|
|||
TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";);
|
||||
for_each_expr(*this, m_visited, tocollect[i]);
|
||||
}
|
||||
unsigned sz1 = model.size();
|
||||
for (unsigned i = 0; i < model.size(); ++i) {
|
||||
expr* e = model[i].get(), *var, *val;
|
||||
if (get_assignment(e, var, val)) {
|
||||
if (!m_visited.is_marked(var)) {
|
||||
model[i] = model.back();
|
||||
model.pop_back();
|
||||
--i;
|
||||
}
|
||||
unsigned sz = m_model->get_num_constants();
|
||||
expr_ref e(m), eq(m);
|
||||
expr_ref_vector model(m);
|
||||
bool_rewriter rw(m);
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
func_decl * d = m_model->get_constant(i);
|
||||
expr* val = m_model->get_const_interp(d);
|
||||
e = m.mk_const(d);
|
||||
if (m_visited.is_marked(e)) {
|
||||
rw.mk_eq(e, val, eq);
|
||||
model.push_back(eq);
|
||||
}
|
||||
}
|
||||
m_visited.reset();
|
||||
TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";);
|
||||
TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";);
|
||||
return model;
|
||||
|
||||
}
|
||||
|
||||
void model_evaluator::eval_arith(app* e) {
|
||||
|
|
|
|||
|
|
@ -194,10 +194,9 @@ class model_evaluator {
|
|||
void reset();
|
||||
void setup_model(model_ref& model);
|
||||
void assign_value(expr* e, expr* v);
|
||||
bool get_assignment(expr* e, expr*& var, expr*& val);
|
||||
void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
|
||||
void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
|
||||
void prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model);
|
||||
expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
|
||||
void eval_arith(app* e);
|
||||
void eval_basic(app* e);
|
||||
void eval_iff(app* e, expr* arg1, expr* arg2);
|
||||
|
|
@ -230,7 +229,13 @@ protected:
|
|||
public:
|
||||
model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m), m_refs(m) {}
|
||||
|
||||
virtual void minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl, expr_ref_vector& model);
|
||||
/**
|
||||
\brief extract equalities from model that suffice to satisfy formula.
|
||||
|
||||
\pre model satisfies formulas
|
||||
*/
|
||||
|
||||
expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
|
||||
|
||||
/**
|
||||
\brief extract literals from formulas that satisfy formulas.
|
||||
|
|
@ -239,12 +244,6 @@ public:
|
|||
*/
|
||||
expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
|
||||
|
||||
/**
|
||||
\brief extract literals from formulas that satisfy formulas.
|
||||
|
||||
\pre model satisfies formulas
|
||||
*/
|
||||
expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, expr_ref_vector const & model);
|
||||
|
||||
// for_each_expr visitor.
|
||||
void operator()(expr* e) {}
|
||||
|
|
|
|||
Loading…
Reference in a new issue