From cadfb804c5ac90416adc33366c8d8d298715aaf9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Oct 2012 08:22:31 -0700 Subject: [PATCH] remove dead code Signed-off-by: Nikolaj Bjorner --- lib/pdr_context.cpp | 103 ++++----------------------------------- lib/pdr_context.h | 24 +-------- lib/pdr_generalizers.cpp | 13 ----- lib/pdr_generalizers.h | 8 --- lib/pdr_util.cpp | 59 ++++++++-------------- lib/pdr_util.h | 17 +++---- 6 files changed, 37 insertions(+), 187 deletions(-) diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index 53cc9aac5..00da4303b 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -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()); - 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()); 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 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 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 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); } diff --git a/lib/pdr_context.h b/lib/pdr_context.h index 15124e2cb..cd56c7536 100644 --- a/lib/pdr_context.h +++ b/lib/pdr_context.h @@ -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& 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 m_model_generalizers; ptr_vector 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: diff --git a/lib/pdr_generalizers.cpp b/lib/pdr_generalizers.cpp index 0ba4f6260..dc73148b2 100644 --- a/lib/pdr_generalizers.cpp +++ b/lib/pdr_generalizers.cpp @@ -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 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. diff --git a/lib/pdr_generalizers.h b/lib/pdr_generalizers.h index 2994beb96..3b9851ca5 100644 --- a/lib/pdr_generalizers.h +++ b/lib/pdr_generalizers.h @@ -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: diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp index e9b15c790..13f2dbb29 100644 --- a/lib/pdr_util.cpp +++ b/lib/pdr_util.cpp @@ -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 const & formulas, model_ref& mdl, expr_ref_vector & model) { +expr_ref_vector model_evaluator::minimize_model(ptr_vector const & formulas, model_ref& mdl) { setup_model(mdl); TRACE("pdr_verbose", @@ -174,7 +147,7 @@ void model_evaluator::minimize_model(ptr_vector 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 const & formulas, model_re setup_model(mdl); VERIFY(check_model(formulas)); reset();); + + return model; } expr_ref_vector model_evaluator::minimize_literals(ptr_vector const& formulas, model_ref& mdl) { @@ -340,7 +315,7 @@ void model_evaluator::collect(ptr_vector const& formulas, ptr_vector m_visited.reset(); } -void model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas, expr_ref_vector& model) { +expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas) { ptr_vector tocollect; collect(formulas, tocollect); m1.reset(); @@ -349,19 +324,23 @@ void model_evaluator::prune_by_cone_of_influence(ptr_vector 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) { diff --git a/lib/pdr_util.h b/lib/pdr_util.h index 11f780a7e..4f6ab1ad3 100644 --- a/lib/pdr_util.h +++ b/lib/pdr_util.h @@ -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 const& formulas, ptr_vector& tocollect); void process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect); - void prune_by_cone_of_influence(ptr_vector const & formulas, expr_ref_vector& model); + expr_ref_vector prune_by_cone_of_influence(ptr_vector 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 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 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 const & formulas, model_ref& mdl); - /** - \brief extract literals from formulas that satisfy formulas. - - \pre model satisfies formulas - */ - expr_ref_vector minimize_literals(ptr_vector const & formulas, expr_ref_vector const & model); // for_each_expr visitor. void operator()(expr* e) {}