diff --git a/lib/ast.h b/lib/ast.h index 685ddd4ad..8de390ee0 100644 --- a/lib/ast.h +++ b/lib/ast.h @@ -832,6 +832,7 @@ inline bool is_app(ast const * n) { return n->get_kind() == AST_APP; } inline bool is_var(ast const * n) { return n->get_kind() == AST_VAR; } inline bool is_quantifier(ast const * n) { return n->get_kind() == AST_QUANTIFIER; } inline bool is_forall(ast const * n) { return is_quantifier(n) && static_cast(n)->is_forall(); } +inline bool is_exists(ast const * n) { return is_quantifier(n) && static_cast(n)->is_exists(); } // ----------------------------------- // diff --git a/lib/dl_mk_coalesce.cpp b/lib/dl_mk_coalesce.cpp index c2ec0adc5..a19b2853c 100644 --- a/lib/dl_mk_coalesce.cpp +++ b/lib/dl_mk_coalesce.cpp @@ -20,8 +20,8 @@ Notes: Implements proof rule of the form: - a(x) & q(x) -> p(x) b(y) & q(y) -> p(y) - --------------------------------------------- + a(x) & q(x) -> p(x), b(y) & q(y) -> p(y) + ---------------------------------------------- (a(z) \/ b(z)) & q(z) -> p(z) diff --git a/lib/lib.vcxproj b/lib/lib.vcxproj index f0353db42..92193faba 100644 --- a/lib/lib.vcxproj +++ b/lib/lib.vcxproj @@ -754,6 +754,7 @@ + @@ -1161,6 +1162,7 @@ + diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index 4f8f27fca..00da4303b 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -41,6 +41,7 @@ Notes: #include "model_smt2_pp.h" #include "dl_mk_rule_inliner.h" #include "ast_smt2_pp.h" +#include "qe_lite.h" namespace pdr { @@ -124,7 +125,7 @@ namespace pdr { datalog::rule const& pred_transformer::find_rule(model_core const& model) const { obj_map::iterator it = m_tag2rule.begin(), end = m_tag2rule.end(); - TRACE("pdr", + TRACE("pdr_verbose", for (; it != end; ++it) { expr* pred = it->m_key; tout << mk_pp(pred, m) << ":\n"; @@ -394,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; @@ -522,6 +522,7 @@ namespace pdr { expr_ref_vector conj(m); app_ref_vector& var_reprs = *(alloc(app_ref_vector, m)); qinst* qi = 0; + ptr_vector aux_vars; unsigned ut_size = rule.get_uninterpreted_tail_size(); unsigned t_size = rule.get_tail_size(); @@ -534,7 +535,7 @@ namespace pdr { init_atom(pts, rule.get_tail(i), var_reprs, conj, i); } for (unsigned i = ut_size; i < t_size; ++i) { - ground_free_vars(rule.get_tail(i), var_reprs); + ground_free_vars(rule.get_tail(i), var_reprs, aux_vars); } SASSERT(check_filled(var_reprs)); expr_ref_vector tail(m); @@ -585,6 +586,7 @@ namespace pdr { m_rule2qinst.insert(&rule, qi); } m_rule2inst.insert(&rule,&var_reprs); + m_rule2vars.insert(&rule, aux_vars); } bool pred_transformer::check_filled(app_ref_vector const& v) const { @@ -595,7 +597,7 @@ namespace pdr { } // create constants for free variables in tail. - void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars) { + void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars) { ptr_vector sorts; get_free_vars(e, sorts); while (vars.size() < sorts.size()) { @@ -604,6 +606,7 @@ namespace pdr { for (unsigned i = 0; i < sorts.size(); ++i) { if (sorts[i] && !vars[i].get()) { vars[i] = m.mk_fresh_const("aux", sorts[i]); + aux_vars.push_back(vars[i].get()); } } } @@ -693,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 @@ -1102,7 +1077,6 @@ namespace pdr { } context::~context() { - reset_model_generalizers(); reset_core_generalizers(); reset(); } @@ -1164,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(); @@ -1289,25 +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(); - classifier_proc classify(m, rules); - if (classify.is_bool_arith()) { - m_model_generalizers.push_back(alloc(bool_model_evaluation_generalizer, *this, m)); - } - else { - m_model_generalizers.push_back(alloc(model_evaluation_generalizer, *this, m)); - } - if (m_params.get_bool(":use-precondition-generalizer", false)) { - m_model_generalizers.push_back(alloc(model_precond_generalizer, *this)); - } - } - void context::reset_core_generalizers() { std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc()); m_core_generalizers.reset(); @@ -1553,13 +1507,8 @@ namespace pdr { close_node(n); } else { - TRACE("pdr", tout << "node: " << &n << "\n"; - expr_ref cb(m.mk_and(cube.size(),cube.c_ptr()), m); - tout << mk_pp(cb.get(), m) << "\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)); + TRACE("pdr", tout << "node: " << &n << "\n";); + create_children(n); } break; case l_false: { @@ -1630,40 +1579,6 @@ namespace pdr { } } - // create children states from model cube. - void context::create_children(model_node& n, expr* model) { - 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. @@ -1713,35 +1628,126 @@ namespace pdr { - Create sub-goals for L0 and L1. */ - void context::create_children2(model_node& n, expr* psi) { + void context::create_children(model_node& n) { SASSERT(n.level() > 0); pred_transformer& pt = n.pt(); - model_core const& M = n.model(); - datalog::rule const& r = pt.find_rule(M); + model_ref M = n.model_ptr(); + datalog::rule const& r = pt.find_rule(*M); expr* T = pt.get_transition(r); expr* phi = n.state(); - ternary_model_evaluator tmev(m); - expr_ref_vector mdl(m); - ptr_vector forms; + IF_VERBOSE(2, verbose_stream() << "Model:\n"; + model_smt2_pp(verbose_stream(), m, *M, 0); + verbose_stream() << "\n"; + verbose_stream() << "Transition:\n" << mk_pp(T, m) << "\n"; + verbose_stream() << "Phi:\n" << mk_pp(phi, m) << "\n";); + + model_evaluator mev(m); + expr_ref_vector mdl(m), forms(m), Phi(m); forms.push_back(T); forms.push_back(phi); - datalog::flatten_and(psi, mdl); - expr_ref_vector Phi = tmev.minimize_literals(forms, mdl); - + datalog::flatten_and(forms); + ptr_vector forms1(forms.size(), forms.c_ptr()); + 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); - expr_ref_vector vars(m); + app_ref_vector vars(m); unsigned sig_size = pt.head()->get_arity(); for (unsigned i = 0; i < sig_size; ++i) { vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0))); } - // TBD: reduce_vars(vars, Phi); + ptr_vector aux_vars; + pt.get_aux_vars(r, aux_vars); + vars.append(aux_vars.size(), aux_vars.c_ptr()); + + qe_lite qe(m); + expr_ref phi1 = m_pm.mk_and(Phi); + qe(vars, phi1); + + IF_VERBOSE(2, + verbose_stream() << "Vars:\n"; + for (unsigned i = 0; i < vars.size(); ++i) { + verbose_stream() << mk_pp(vars[i].get(), m) << "\n"; + } + verbose_stream() << "Literals\n"; + verbose_stream() << mk_pp(m_pm.mk_and(Phi), m) << "\n"; + verbose_stream() << "Reduced\n" << mk_pp(phi1, m) << "\n";); + + if (!vars.empty()) { + // also fresh names for auxiliary variables in body? + expr_substitution sub(m); + expr_ref tmp(m); + proof_ref pr(m); + pr = m.mk_asserted(m.mk_true()); + + for (unsigned i = 0; i < vars.size(); ++i) { + M->eval(vars[i]->get_decl(), tmp); + sub.insert(vars[i].get(), tmp, pr); + } + scoped_ptr rep = mk_default_expr_replacer(m); + rep->set_substitution(&sub); + (*rep)(phi1); + IF_VERBOSE(2, verbose_stream() << "Projected:\n" << mk_pp(phi1, m) << "\n";); + } + Phi.reset(); + datalog::flatten_and(phi1, Phi); + unsigned_vector indices; + vector child_states; + child_states.resize(preds.size(), expr_ref_vector(m)); + for (unsigned i = 0; i < Phi.size(); ++i) { + m_pm.collect_indices(Phi[i].get(), indices); + if (indices.size() == 0) { + IF_VERBOSE(2, verbose_stream() << "Skipping " << mk_pp(Phi[i].get(), m) << "\n";); + } + else if (indices.size() == 1) { + child_states[indices.back()].push_back(Phi[i].get()); + } + else { + expr_substitution sub(m); + expr_ref tmp(m); + proof_ref pr(m); + pr = m.mk_asserted(m.mk_true()); + vector > vars; + m_pm.collect_variables(Phi[i].get(), vars); + SASSERT(vars.size() == indices.back()+1); + for (unsigned j = 1; j < indices.size(); ++j) { + ptr_vector const& vs = vars[indices[j]]; + for (unsigned k = 0; k < vs.size(); ++k) { + M->eval(vs[k]->get_decl(), tmp); + sub.insert(vs[k], tmp, pr); + child_states[indices[j]].push_back(m.mk_eq(vs[k], tmp)); + } + } + tmp = Phi[i].get(); + scoped_ptr rep = mk_default_expr_replacer(m); + rep->set_substitution(&sub); + (*rep)(tmp); + child_states[indices[0]].push_back(tmp); + } + } + + expr_ref n_cube(m); + for (unsigned i = 0; i < preds.size(); ++i) { + pred_transformer& pt = *m_rels.find(preds[i]); + SASSERT(pt.head() == preds[i]); + expr_ref o_cube = m_pm.mk_and(child_states[i]); + m_pm.formula_o2n(o_cube, n_cube, i); + model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1); + ++m_stats.m_num_nodes; + m_search.add_leaf(*child); + IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";); + } + check_pre_closed(n); + - // TBD ... TRACE("pdr", m_search.display(tout);); } @@ -1754,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 ce01c3100..cd56c7536 100644 --- a/lib/pdr_context.h +++ b/lib/pdr_context.h @@ -60,6 +60,7 @@ namespace pdr { }; typedef obj_map rule2expr; + typedef obj_map > rule2apps; manager& pm; // pdr-manager ast_manager& m; // manager @@ -77,6 +78,7 @@ namespace pdr { qinst_map m_rule2qinst; // map tag to quantifier instantiation. rule2inst m_rule2inst; // map rules to instantiations of indices rule2expr m_rule2transition; // map rules to transition + rule2apps m_rule2vars; // map rule to auxiliary variables expr_ref m_transition; // transition relation. expr_ref m_initial_state; // initial state. reachable_cache m_reachable; @@ -94,10 +96,7 @@ namespace pdr { void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init, ptr_vector& rules, expr_ref_vector& transition); 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); - - 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 ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars); void simplify_formulas(tactic& tac, expr_ref_vector& fmls); @@ -137,6 +136,7 @@ namespace pdr { void find_predecessors(model_core const& model, ptr_vector& preds) const; datalog::rule const& find_rule(model_core const& model) const; expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); } + void get_aux_vars(datalog::rule const& r, ptr_vector& vs) { m_rule2vars.find(&r, vs); } bool propagate_to_next_level(unsigned level); void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level. @@ -154,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); @@ -194,7 +192,8 @@ namespace pdr { ptr_vector const& children() { return m_children; } pred_transformer& pt() const { return m_pt; } model_node* parent() const { return m_parent; } - model_core const& model() const { return *m_model; } + model* model_ptr() const { return m_model.get(); } + model const& model() const { return *m_model; } unsigned index() const; bool is_closed() const { return m_closed; } @@ -262,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 { @@ -301,7 +288,6 @@ namespace pdr { stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; - front_end_params& m_fparams; params_ref const& m_params; @@ -315,7 +301,6 @@ namespace pdr { model_search m_search; lbool m_last_result; unsigned m_inductive_lvl; - ptr_vector m_model_generalizers; ptr_vector m_core_generalizers; stats m_stats; volatile bool m_cancel; @@ -332,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* cube); - void create_children2(model_node& n, expr* cube); + void create_children(model_node& n); expr_ref mk_sat_answer() const; expr_ref mk_unsat_answer() const; @@ -343,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); @@ -355,7 +338,6 @@ namespace pdr { void simplify_formulas(); - void reset_model_generalizers(); void reset_core_generalizers(); public: diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp index d26ce5a4d..cb7d88fd6 100644 --- a/lib/pdr_dl_interface.cpp +++ b/lib/pdr_dl_interface.cpp @@ -202,7 +202,7 @@ void dl_interface::collect_params(param_descrs& p) { p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area"); p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring"); - PRIVATE_PARAMS(p.insert(":use-precondition-generalizer", CPK_BOOL, "PDR: (default false) enable generalizations from weakest pre-conditions");); + p.insert(":use-model-generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"); PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");); PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening");); PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation");); diff --git a/lib/pdr_generalizers.cpp b/lib/pdr_generalizers.cpp index 6de57b39f..dc73148b2 100644 --- a/lib/pdr_generalizers.cpp +++ b/lib/pdr_generalizers.cpp @@ -28,66 +28,6 @@ Revision History: namespace pdr { - static void solve_for_next_vars(expr_ref& F, model_node& n, expr_substitution& sub) { - ast_manager& m = F.get_manager(); - manager& pm = n.pt().get_pdr_manager(); - const model_core & mdl = n.model(); - unsigned sz = mdl.get_num_constants(); - expr_ref_vector refs(m); - - for (unsigned i = 0; i < sz; i++) { - func_decl * d = mdl.get_constant(i); - expr_ref interp(m); - ptr_vector cs; - if (m.is_bool(d->get_range())) { - get_value_from_model(mdl, d, interp); - app* c = m.mk_const(d); - refs.push_back(c); - refs.push_back(interp); - sub.insert(c, interp); - } - } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - (*rep)(F); - th_rewriter rw(m); - rw(F); - ptr_vector todo; - todo.push_back(F); - expr* e1, *e2; - while (!todo.empty()) { - expr* e = todo.back(); - todo.pop_back(); - if (m.is_and(e)) { - todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - } - else if ((m.is_eq(e, e1, e2) && pm.is_n(e1) && pm.is_o_formula(e2)) || - (m.is_eq(e, e2, e1) && pm.is_n(e1) && pm.is_o_formula(e2))) { - sub.insert(e1, e2); - TRACE("pdr", tout << mk_pp(e1, m) << " |-> " << mk_pp(e2, m) << "\n";); - } - } - } - - // - // eliminate conjuncts from cube as long as state is satisfied. - // - void model_evaluation_generalizer::operator()(model_node& n, expr_ref_vector& cube) { - ptr_vector forms; - forms.push_back(n.state()); - forms.push_back(n.pt().transition()); - m_model_evaluator.minimize_model(forms, cube); - } - - // - // eliminate conjuncts from cube as long as state is satisfied. - // - void bool_model_evaluation_generalizer::operator()(model_node& n, expr_ref_vector& cube) { - ptr_vector forms; - forms.push_back(n.state()); - forms.push_back(n.pt().transition()); - m_model_evaluator.minimize_model(forms, cube); - } // // main propositional induction generalizer. @@ -203,31 +143,6 @@ namespace pdr { m_farkas_learner.collect_statistics(st); } - void model_precond_generalizer::operator()(model_node& n, expr_ref_vector& cube) { - ast_manager& m = n.pt().get_manager(); - manager& pm = n.pt().get_pdr_manager(); - expr_ref A(m), state(m); - expr_ref_vector states(m); - A = n.pt().get_formulas(n.level(), true); - - // extract substitution for next-state variables. - expr_substitution sub(m); - solve_for_next_vars(A, n, sub); - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - A = m.mk_and(A, n.state()); - (*rep)(A); - - datalog::flatten_and(A, states); - - for (unsigned i = 0; i < states.size(); ++i) { - expr* s = states[i].get(); - if (pm.is_o_formula(s) && pm.is_homogenous_formula(s)) { - cube.push_back(s); - } - } - TRACE("pdr", for (unsigned i = 0; i < cube.size(); ++i) tout << mk_pp(cube[i].get(), m) << "\n";); - } /** < F, phi, i + 1 > diff --git a/lib/pdr_generalizers.h b/lib/pdr_generalizers.h index 5a1d9a0e4..3b9851ca5 100644 --- a/lib/pdr_generalizers.h +++ b/lib/pdr_generalizers.h @@ -25,14 +25,6 @@ Revision History: namespace pdr { - class bool_model_evaluation_generalizer : public model_generalizer { - ternary_model_evaluator m_model_evaluator; - public: - bool_model_evaluation_generalizer(context& ctx, ast_manager& m) : model_generalizer(ctx), m_model_evaluator(m) {} - virtual ~bool_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: @@ -50,21 +42,6 @@ namespace pdr { virtual void collect_statistics(statistics& st) const; }; - class model_precond_generalizer : public model_generalizer { - public: - model_precond_generalizer(context& ctx): model_generalizer(ctx) {} - virtual ~model_precond_generalizer() {} - virtual void operator()(model_node& n, expr_ref_vector& cube); - }; - - class model_evaluation_generalizer : public model_generalizer { - th_rewriter_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_multi_generalizer : public core_generalizer { core_bool_inductive_generalizer m_gen; public: diff --git a/lib/pdr_manager.h b/lib/pdr_manager.h index e7bfb38c8..87eaa03bf 100644 --- a/lib/pdr_manager.h +++ b/lib/pdr_manager.h @@ -223,6 +223,20 @@ namespace pdr { bool is_homogenous_formula(expr * e) const { return m_mux.is_homogenous_formula(e); } + + /** + Collect indices used in expression. + */ + void collect_indices(expr* e, unsigned_vector& indices) const { + m_mux.collect_indices(e, indices); + } + + /** + Collect used variables of each index. + */ + void collect_variables(expr* e, vector >& vars) const { + m_mux.collect_variables(e, vars); + } /** Return true iff both s1 and s2 are either "n" or "o" of the same index. @@ -275,8 +289,6 @@ namespace pdr { bool try_get_state_and_value_from_atom(expr * atom, app *& state, app_ref& value); bool try_get_state_decl_from_atom(expr * atom, func_decl *& state); - void get_state_cube_from_model(const model_core & mdl, expr_ref_vector & cube) const - { return m_mux.get_muxed_cube_from_model(mdl, cube); } std::string pp_model(const model_core & mdl) const { return m_mux.pp_model(mdl); } diff --git a/lib/pdr_sym_mux.cpp b/lib/pdr_sym_mux.cpp index f17177a7f..08b590e16 100644 --- a/lib/pdr_sym_mux.cpp +++ b/lib/pdr_sym_mux.cpp @@ -228,6 +228,76 @@ bool sym_mux::is_homogenous(const expr_ref_vector & vect, unsigned idx) const return true; } +class sym_mux::index_collector { + sym_mux const& m_parent; + svector 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 >& m_vars; +public: + variable_collector(sym_mux const& s, vector >& 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()); + } + m_vars[idx].push_back(to_app(e)); + } + } + } +}; + +void sym_mux::collect_variables(expr* e, vector >& 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; @@ -445,38 +515,6 @@ void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const { } } -void sym_mux::get_muxed_cube_from_model(const model_core & mdl, expr_ref_vector & res) const -{ - res.reset(); - unsigned sz = mdl.get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * d = mdl.get_constant(i); - - if(!is_muxed(d) || m_non_model_syms.contains(get_primary(d))) { continue; } - - SASSERT(d->get_arity()==0); - expr_ref interp(m); - get_value_from_model(mdl, d, interp); - - app_ref constant(m.mk_const(d), m); - app_ref lit(m); - if(m.is_bool(d->get_range())) { - if(m.is_true(interp)) { - lit = constant; - } - else { - SASSERT(m.is_false(interp)); - lit = m.mk_not(constant); - } - } - else { - lit = m.mk_eq(constant, interp); - } - res.push_back(lit); - } - //LOGV(5, " got cube "< >& vars) const; /** Convert symbol sym which has to be of src_idx variant into variant tgt_idx. diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp index 5deb2a189..13f2dbb29 100644 --- a/lib/pdr_util.cpp +++ b/lib/pdr_util.cpp @@ -86,230 +86,93 @@ std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) { ///////////////////////// -// model_evaluator_base +// model_evaluator // -void model_evaluator_base::minimize_model(ptr_vector const & formulas, expr_ref_vector & model) -{ - ast_manager & m = model.get_manager(); - bool has_unknown, has_false; - DEBUG_CODE( - check_model(formulas, model, has_unknown, has_false); - if (has_false) { - std::cout<<"formulas: "<& m_assignment; -public: - expr_rewriter_cfg(const obj_map& assignment) - : m_assignment(assignment) - { - } - - bool get_subst(expr * s, expr * & t, proof * & t_pr) { - return m_assignment.find(s,t); - } -}; - -void th_rewriter_model_evaluator::setup_assignment(expr_ref_vector const& model, obj_map& assignment) { - - for (unsigned i = 0; i < model.size(); ++i) { - expr * mlit = model[i]; //model literal - if (is_uninterp(mlit)) { - assignment.insert(mlit, m.mk_true()); - } - expr * arg1; - expr * arg2; - if (m.is_not(mlit, arg1)) { - assignment.insert(arg1, m.mk_false()); - } - else if (m.is_eq(mlit, arg1, arg2)) { - if (!is_uninterp(arg1)) { - std::swap(arg1, arg2); - } - if (is_uninterp(arg1)) { - assignment.insert(arg1, arg2); - } - else { - assignment.insert(mlit, m.mk_true()); - } - } - } -} - -void th_rewriter_model_evaluator::check_model(ptr_vector const & formulas, expr_ref_vector & model, - bool & has_unknown, bool & has_false) -{ - obj_map assignment; - - setup_assignment(model, assignment); - - expr_rewriter_cfg r_cfg(assignment); - rewriter_tpl rwr(m, false, r_cfg); - - has_false = false; - has_unknown = false; - - for (unsigned i = 0; i < formulas.size(); ++i) { - expr * form = formulas[i]; - expr_ref asgn_form(m); - rwr(form, asgn_form); - expr_ref simpl_form(m); - m_rewriter(asgn_form, simpl_form); - if (m.is_false(simpl_form)) { - has_false = true; - } - else if (!m.is_true(simpl_form)) { - IF_VERBOSE(7, verbose_stream() << "formula evaluated as unknown:\noriginal: " - << mk_pp(form, m) << "\n" - << "simplified: " << mk_pp(simpl_form,m) << "\n";); - has_unknown = true; - } - } - m_rewriter.reset(); -} - -bool ternary_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 ternary_model_evaluator::add_model(expr* e) { - expr* var, *val; +void model_evaluator::assign_value(expr* e, expr* val) { rational r; - // SASSERT(is_unknown(e)); - if (get_assignment(e, var, val)) { - if (is_unknown(var)) { - if (m.is_true(val)) { - set_true(var); - } - else if (m.is_false(val)) { - set_false(var); - } - else if (m_arith.is_numeral(val, r)) { - set_value(var, r); - } - } + if (m.is_true(val)) { + set_true(e); + } + else if (m.is_false(val)) { + set_false(e); + } + else if (m_arith.is_numeral(val, r)) { + set_number(e, r); + } + else if (m.is_value(val)) { + set_value(e, val); } else { - TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";); + TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";); + set_x(e); } } -void ternary_model_evaluator::del_model(expr* e) { - expr *var, *val; - if (get_assignment(e, var, val)) { - set_unknown(var); - if (!m.is_bool(var)) { - m_values.remove(var); - } - } - else { - TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";); - } -} - -void ternary_model_evaluator::setup_model(expr_ref_vector const& model) { +void model_evaluator::setup_model(model_ref& model) { + m_numbers.reset(); m_values.reset(); - for (unsigned i = 0; i < model.size(); ++i) { - expr* e = model[i]; - if (is_unknown(e)) { - add_model(e); - } + m_model = model; + rational r; + unsigned sz = model->get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * d = model->get_constant(i); + expr* val = model->get_const_interp(d); + expr* e = m.mk_const(d); + m_refs.push_back(e); + assign_value(e, val); } + m_level1 = m1.get_level(); m_level2 = m2.get_level(); } -void ternary_model_evaluator::minimize_model(ptr_vector const & formulas, expr_ref_vector & model) -{ - setup_model(model); - - TRACE("pdr_verbose", - for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n"; - tout << "formulas\n"; - for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; - ); - - prune_by_cone_of_influence(formulas, model); - - // prune_by_probing(formulas, model); - +void model_evaluator::reset() { m1.reset(); m2.reset(); m_values.reset(); + m_visited.reset(); + m_numbers.reset(); + m_refs.reset(); + m_model = 0; } -expr_ref_vector ternary_model_evaluator::minimize_literals(ptr_vector const& formulas, expr_ref_vector const& model) { - - setup_model(model); +expr_ref_vector model_evaluator::minimize_model(ptr_vector const & formulas, model_ref& mdl) { + setup_model(mdl); + TRACE("pdr_verbose", + tout << "formulas:\n"; + for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; + ); + + 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";); + + reset(); + + DEBUG_CODE( + setup_model(mdl); + VERIFY(check_model(formulas)); + reset();); + + return model; +} + +expr_ref_vector model_evaluator::minimize_literals(ptr_vector const& formulas, model_ref& mdl) { + + TRACE("pdr", + tout << "formulas:\n"; + for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; + ); + + setup_model(mdl); expr_ref_vector result(m); ptr_vector tocollect; - m_visited.reset(); - m1.set_level(m_level1); - m2.set_level(m_level2); - - VERIFY(check_model(formulas)); + collect(formulas, tocollect); for (unsigned i = 0; i < tocollect.size(); ++i) { expr* e = tocollect[i]; @@ -322,49 +185,11 @@ expr_ref_vector ternary_model_evaluator::minimize_literals(ptr_vector cons result.push_back(m.mk_not(e)); } } - m_visited.reset(); - m1.reset(); - m2.reset(); - m_values.reset(); + reset(); return result; } -void ternary_model_evaluator::prune_by_probing(ptr_vector const& formulas, expr_ref_vector& model) { - unsigned sz1 = model.size(); - for (unsigned i = 0; i < model.size(); ) { - expr_ref removed(model[i].get(), m); - if (i + 1 < model.size()) { - model[i] = model.back(); - } - model.pop_back(); - del_model(removed); - m1.set_level(m_level1); - m2.set_level(m_level2); - - bool formulas_hold = check_model(formulas); - - m1.set_level(m_level1); - m2.set_level(m_level2); - - if (!formulas_hold) { - // if we introduced unknown, we restore the removed element - add_model(removed); - m_level1 = m1.get_level(); - m_level2 = m2.get_level(); - if (i < model.size()) { - model.push_back(model[i].get()); - model[i] = removed; - } - else { - model.push_back(removed); - } - i++; - } - } - TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";); -} - -void ternary_model_evaluator::process_formula(app* e, ptr_vector todo, ptr_vector& tocollect) { +void model_evaluator::process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect) { SASSERT(m.is_bool(e)); SASSERT(is_true(e) || is_false(e)); unsigned v = is_true(e); @@ -378,10 +203,11 @@ void ternary_model_evaluator::process_formula(app* e, ptr_vector todo, ptr break; case OP_EQ: case OP_IFF: - if (e->get_arg(0) == e->get_arg(1)) { + if (args[0] == args[1]) { + SASSERT(v); // no-op } - else if (!m.is_bool(e->get_arg(0))) { + else if (!m.is_bool(args[0])) { tocollect.push_back(e); } else { @@ -393,17 +219,16 @@ void ternary_model_evaluator::process_formula(app* e, ptr_vector todo, ptr break; case OP_ITE: if (args[1] == args[2]) { - // + tocollect.push_back(args[1]); } else if (is_true(args[1]) && is_true(args[2])) { todo.append(2, args+1); } - else if (is_false(args[2]) && is_false(args[2])) { + else if (is_false(args[1]) && is_false(args[2])) { todo.append(2, args+1); } else if (is_true(args[0])) { - todo.push_back(args[0]); - todo.push_back(args[1]); + todo.append(2, args); } else { SASSERT(is_false(args[0])); @@ -452,6 +277,7 @@ void ternary_model_evaluator::process_formula(app* e, ptr_vector todo, ptr todo.push_back(args[0]); } else { + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); UNREACHABLE(); } } @@ -460,6 +286,7 @@ void ternary_model_evaluator::process_formula(app* e, ptr_vector todo, ptr } break; default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); UNREACHABLE(); } } @@ -468,7 +295,7 @@ void ternary_model_evaluator::process_formula(app* e, ptr_vector todo, ptr } } -void ternary_model_evaluator::collect(ptr_vector const& formulas, ptr_vector& tocollect) { +void model_evaluator::collect(ptr_vector const& formulas, ptr_vector& tocollect) { ptr_vector todo; todo.append(formulas); m_visited.reset(); @@ -485,44 +312,372 @@ void ternary_model_evaluator::collect(ptr_vector const& formulas, ptr_vect m_visited.mark(e, true); } } - m1.set_level(m_level1); - m2.set_level(m_level2); m_visited.reset(); } -void ternary_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); - for (unsigned i = 0; i < tocollect.size(); ++i) { + m1.reset(); + m2.reset(); + for (unsigned i = 0; i < tocollect.size(); ++i) { + 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)) { - del_model(e); - 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) { + rational r, r2; -bool ternary_model_evaluator::check_model(ptr_vector const& formulas) { +#define ARG1 e->get_arg(0) +#define ARG2 e->get_arg(1) + + unsigned arity = e->get_num_args(); + for (unsigned i = 0; i < arity; ++i) { + expr* arg = e->get_arg(i); + if (is_x(arg)) { + set_x(e); + return; + } + SASSERT(!is_unknown(arg)); + } + switch(e->get_decl_kind()) { + case OP_NUM: + VERIFY(m_arith.is_numeral(e, r)); + set_number(e, r); + break; + case OP_IRRATIONAL_ALGEBRAIC_NUM: + set_x(e); + break; + case OP_LE: + set_bool(e, get_number(ARG1) <= get_number(ARG2)); + break; + case OP_GE: + set_bool(e, get_number(ARG1) >= get_number(ARG2)); + break; + case OP_LT: + set_bool(e, get_number(ARG1) < get_number(ARG2)); + break; + case OP_GT: + set_bool(e, get_number(ARG1) > get_number(ARG2)); + break; + case OP_ADD: + r = rational::zero(); + for (unsigned i = 0; i < arity; ++i) { + r += get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_SUB: + r = get_number(e->get_arg(0)); + for (unsigned i = 1; i < arity; ++i) { + r -= get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_UMINUS: + SASSERT(arity == 1); + set_number(e, get_number(e->get_arg(0))); + break; + case OP_MUL: + r = rational::one(); + for (unsigned i = 0; i < arity; ++i) { + r *= get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_DIV: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, get_number(ARG1) / r); + } + break; + case OP_IDIV: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, div(get_number(ARG1), r)); + } + break; + case OP_REM: + // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + r2 = mod(get_number(ARG1), r); + if (r.is_neg()) r2.neg(); + set_number(e, r2); + } + break; + case OP_MOD: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, mod(get_number(ARG1), r)); + } + break; + case OP_TO_REAL: + SASSERT(arity == 1); + set_number(e, get_number(ARG1)); + break; + case OP_TO_INT: + SASSERT(arity == 1); + set_number(e, floor(get_number(ARG1))); + break; + case OP_IS_INT: + SASSERT(arity == 1); + set_bool(e, get_number(ARG1).is_int()); + break; + case OP_POWER: + set_x(e); + break; + default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + break; + } +} + +void model_evaluator::inherit_value(expr* e, expr* v) { + SASSERT(!is_unknown(v)); + SASSERT(m.get_sort(e) == m.get_sort(v)); + if (m.is_bool(e)) { + SASSERT(m.is_bool(v)); + if (is_true(v)) set_true(e); + else if (is_false(v)) set_false(e); + else set_x(e); + } + else if (m_arith.is_int_real(e)) { + set_number(e, get_number(v)); + } + else if (m.is_value(v)) { + set_value(e, v); + } + else { + set_x(e); + } +} + +void model_evaluator::eval_iff(app* e, expr* arg1, expr* arg2) { + if (arg1 == arg2) { + set_true(e); + } + else if (is_x(arg1) || is_x(arg2)) { + set_x(e); + } + else { + bool val = is_true(arg1) == is_true(arg2); + SASSERT(val == (is_false(arg1) == is_false(arg2))); + if (val) { + set_true(e); + } + else { + set_false(e); + } + } +} + +void model_evaluator::eval_basic(app* e) { + expr* arg1, *arg2; + expr *argCond, *argThen, *argElse, *arg; + bool has_x = false; + unsigned arity = e->get_num_args(); + switch(e->get_decl_kind()) { + case OP_AND: + for (unsigned j = 0; j < arity; ++j) { + expr * arg = e->get_arg(j); + if (is_false(arg)) { + set_false(e); + return; + } + else if (is_x(arg)) { + has_x = true; + } + else { + SASSERT(is_true(arg)); + } + } + if (has_x) { + set_x(e); + } + else { + set_true(e); + } + break; + case OP_OR: + for (unsigned j = 0; j < arity; ++j) { + expr * arg = e->get_arg(j); + if (is_true(arg)) { + set_true(e); + return; + } + else if (is_x(arg)) { + has_x = true; + } + else { + SASSERT(is_false(arg)); + } + } + if (has_x) { + set_x(e); + } + else { + set_false(e); + } + break; + case OP_NOT: + VERIFY(m.is_not(e, arg)); + if (is_true(arg)) { + set_false(e); + } + else if (is_false(arg)) { + set_true(e); + } + else { + SASSERT(is_x(arg)); + set_x(e); + } + break; + case OP_IMPLIES: + VERIFY(m.is_implies(e, arg1, arg2)); + if (is_false(arg1) || is_true(arg2)) { + set_true(e); + } + else if (arg1 == arg2) { + set_true(e); + } + else if (is_true(arg1) && is_false(arg2)) { + set_false(e); + } + else { + SASSERT(is_x(arg1) || is_x(arg2)); + set_x(e); + } + break; + case OP_IFF: + VERIFY(m.is_iff(e, arg1, arg2)); + eval_iff(e, arg1, arg2); + break; + case OP_ITE: + VERIFY(m.is_ite(e, argCond, argThen, argElse)); + if (is_true(argCond)) { + inherit_value(e, argThen); + } + else if (is_false(argCond)) { + inherit_value(e, argElse); + } + else if (argThen == argElse) { + inherit_value(e, argThen); + } + else if (m.is_bool(e)) { + SASSERT(is_x(argCond)); + if (is_x(argThen) || is_x(argElse)) { + set_x(e); + } + else if (is_true(argThen) == is_true(argElse)) { + inherit_value(e, argThen); + } + else { + set_x(e); + } + } + else { + set_x(e); + } + break; + case OP_TRUE: + set_true(e); + break; + case OP_FALSE: + set_false(e); + break; + case OP_EQ: + VERIFY(m.is_eq(e, arg1, arg2)); + if (m.is_bool(arg1)) { + eval_iff(e, arg1, arg2); + } + else if (arg1 == arg2) { + set_true(e); + } + else if (is_x(arg1) || is_x(arg2)) { + set_x(e); + } + else if (m_arith.is_int_real(arg1)) { + set_bool(e, get_number(arg1) == get_number(arg2)); + } + else { + expr* e1 = get_value(arg1); + expr* e2 = get_value(arg2); + if (m.is_value(e1) && m.is_value(e2)) { + set_bool(e, e1 == e2); + } + else { + set_x(e); + } + } + break; + case OP_DISTINCT: { + vector values; + for (unsigned i = 0; i < arity; ++i) { + expr* arg = e->get_arg(i); + if (is_x(arg)) { + set_x(e); + return; + } + values.push_back(get_number(arg)); + } + std::sort(values.begin(), values.end()); + for (unsigned i = 0; i + 1 < values.size(); ++i) { + if (values[i] == values[i+1]) { + set_false(e); + return; + } + } + set_true(e); + break; + } + default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + } +} + +bool model_evaluator::check_model(ptr_vector const& formulas) { ptr_vector todo; assign_vector_with_casting(todo, formulas); - expr *argCond, *argThen, *argElse, *arg; - rational r, r2; - - while(!todo.empty()) { + while (!todo.empty()) { expr * curr_e = todo.back(); - unsigned pre_curr_depth = todo.size()-1; if (!is_app(curr_e)) { todo.pop_back(); @@ -530,381 +685,38 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) { } app * curr = to_app(curr_e); -#define ARG1 curr->get_arg(0) -#define ARG2 curr->get_arg(1) - if (!is_unknown(curr)) { todo.pop_back(); continue; } unsigned arity = curr->get_num_args(); - - if (curr->get_family_id() == m_arith.get_family_id()) { - bool all_set = true, some_x = false; - for (unsigned i = 0; !some_x && i < arity; ++i) { - expr* arg = curr->get_arg(i); - if (is_unknown(arg)) { - todo.push_back(arg); - all_set = false; - } - else if (is_x(arg)) { - some_x = true; - } - } - if (some_x) { - set_x(curr); - } - else if (!all_set) { - continue; - } - else { - switch(curr->get_decl_kind()) { - case OP_NUM: - VERIFY(m_arith.is_numeral(curr,r)); - set_value(curr, r); - break; - case OP_IRRATIONAL_ALGEBRAIC_NUM: - set_x(curr); - break; - case OP_LE: - set_bool(curr, get_value(ARG1) <= get_value(ARG2)); - break; - case OP_GE: - set_bool(curr, get_value(ARG1) >= get_value(ARG2)); - break; - case OP_LT: - set_bool(curr, get_value(ARG1) < get_value(ARG2)); - break; - case OP_GT: - set_bool(curr, get_value(ARG1) > get_value(ARG2)); - break; - case OP_ADD: - r = rational::zero(); - for (unsigned i = 0; i < arity; ++i) { - r += get_value(curr->get_arg(i)); - } - set_value(curr, r); - break; - case OP_SUB: - r = get_value(curr->get_arg(0)); - for (unsigned i = 1; i < arity; ++i) { - r -= get_value(curr->get_arg(i)); - } - set_value(curr, r); - break; - case OP_UMINUS: - SASSERT(arity == 1); - set_value(curr, get_value(curr->get_arg(0))); - break; - case OP_MUL: - r = rational::one(); - for (unsigned i = 0; i < arity; ++i) { - r *= get_value(curr->get_arg(i)); - } - set_value(curr, r); - break; - case OP_DIV: - SASSERT(arity == 2); - r = get_value(ARG2); - if (r.is_zero()) { - set_x(curr); - } - else { - set_value(curr, get_value(ARG1) / r); - } - break; - case OP_IDIV: - SASSERT(arity == 2); - r = get_value(ARG2); - if (r.is_zero()) { - set_x(curr); - } - else { - set_value(curr, div(get_value(ARG1), r)); - } - break; - case OP_REM: - // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) - SASSERT(arity == 2); - r = get_value(ARG2); - if (r.is_zero()) { - set_x(curr); - } - else { - r2 = mod(get_value(ARG1), r); - if (r.is_neg()) r2.neg(); - set_value(curr, r2); - } - break; - case OP_MOD: - SASSERT(arity == 2); - r = get_value(ARG2); - if (r.is_zero()) { - set_x(curr); - } - else { - set_value(curr, mod(get_value(ARG1), r)); - } - break; - case OP_TO_REAL: - SASSERT(arity == 1); - set_value(curr, get_value(ARG1)); - break; - case OP_TO_INT: - SASSERT(arity == 1); - set_value(curr, floor(get_value(ARG1))); - break; - case OP_IS_INT: - SASSERT(arity == 1); - set_bool(curr, get_value(ARG1).is_int()); - break; - case OP_POWER: - set_x(curr); - break; - default: - UNREACHABLE(); - break; - } + for (unsigned i = 0; i < arity; ++i) { + if (is_unknown(curr->get_arg(i))) { + todo.push_back(curr->get_arg(i)); } } - else if (curr->get_family_id() == m_bv.get_family_id()) { - throw default_exception("PDR engine currently does not support bit-vectors"); + if (todo.back() != curr) { + continue; + } + todo.pop_back(); + if (curr->get_family_id() == m_arith.get_family_id()) { + eval_arith(curr); } else if (curr->get_family_id() == m.get_basic_family_id()) { - expr* arg1, *arg2; - if (m.is_and(curr)) { - // we're adding unknowns on the top of the todo stack, if there is none added, - // all arguments were known - bool has_x = false, has_false = false; - unsigned sz = todo.size(); - for (unsigned j = 0; !has_false && j < arity; ++j) { - expr * arg = curr->get_arg(j); - if (is_false(arg)) { - has_false = true; - } - else if (is_x(arg)) { - has_x = true; - } - else if (is_unknown(arg)) { - todo.push_back(arg); - } - } - if (has_false) { - todo.resize(sz); - set_false(curr); - } - else { - if (todo.back() != curr) { - continue; - } - else if (has_x) { - set_x(curr); - } - else { - set_true(curr); - } - } - } - else if (m.is_or(curr)) { - bool has_x = false, has_true = false; - unsigned sz = todo.size(); - for (unsigned j = 0; !has_true && j < arity; ++j) { - expr * arg = curr->get_arg(j); - if (is_true(arg)) { - has_true = true; - } - else if (is_x(arg)) { - has_x = true; - } - else if (is_unknown(arg)) { - todo.push_back(arg); - } - } - if (has_true) { - todo.resize(sz); - set_true(curr); - } - else { - if (todo.back() != curr) { - continue; - } - else if (has_x) { - set_x(curr); - } - else { - set_false(curr); - } - } - } - else if (m.is_not(curr, arg)) { - if (is_unknown(arg)) { - todo.push_back(arg); - continue; - } - if (is_true(arg)) { - set_false(curr); - } - else if (is_false(arg)) { - set_true(curr); - } - else { - SASSERT(is_x(arg)); - set_x(curr); - } - } - else if (m.is_implies(curr, arg1, arg2)) { - if (is_false(arg1) || is_true(arg2)) { - set_true(curr); - } - else if (is_unknown(arg1) || is_unknown(arg2)) { - if (is_unknown(arg1)) { todo.push_back(arg1); } - if (is_unknown(arg2)) { todo.push_back(arg2); } - continue; - } - else if (is_true(arg1) && is_false(arg2)) { - set_false(curr); - } - else { - SASSERT(is_x(arg1) || is_x(arg2)); - set_x(curr); - } - } - else if (m.is_iff(curr, arg1, arg2) || - (m.is_eq(curr, arg1, arg2) && m.is_bool(arg1))) { - if (is_x(arg1) || is_x(arg2)) { - set_x(curr); - } - else if (is_unknown(arg1) || is_unknown(arg2)) { - if (is_unknown(arg1)) { todo.push_back(arg1); } - if (is_unknown(arg2)) { todo.push_back(arg2); } - continue; - } - else { - bool val = is_true(arg1)==is_true(arg2); - SASSERT(val == (is_false(arg1)==is_false(arg2))); - if (val) { - set_true(curr); - } - else { - set_false(curr); - } - } - } - else if (m.is_ite(curr, argCond, argThen, argElse) && m.is_bool(argThen)) { - if (is_true(argCond)) { - if (is_true(argThen)) { set_true(curr); } - else if (is_false(argThen)) { set_false(curr); } - else if (is_x(argThen)) { set_x(curr); } - else { - todo.push_back(argThen); - continue; - } - } - else if (is_false(argCond)) { - if (is_true(argElse)) { set_true(curr); } - else if (is_false(argElse)) { set_false(curr); } - else if (is_x(argElse)) { set_x(curr); } - else { - todo.push_back(argElse); - continue; - } - } - else if (is_true(argThen) && is_true(argElse)) { - set_true(curr); - } - else if (is_false(argThen) && is_false(argElse)) { - set_false(curr); - } - else if (is_x(argCond) && (is_x(argThen) || is_x(argElse)) ) { - set_x(curr); - } else if (is_unknown(argCond) || is_unknown(argThen) || is_unknown(argElse)) { - if (is_unknown(argCond)) { todo.push_back(argCond); } - if (is_unknown(argThen)) { todo.push_back(argThen); } - if (is_unknown(argElse)) { todo.push_back(argElse); } - continue; - } - else { - SASSERT(is_x(argCond)); - SASSERT((is_true(argThen) && is_false(argElse)) || - (is_false(argThen) && is_true(argElse))); - set_x(curr); - } - } - else if (m.is_true(curr)) { - set_true(curr); - } - else if (m.is_false(curr)) { - set_false(curr); - } - else if (m.is_eq(curr, arg1, arg2) && arg1 == arg2) { - set_true(curr); - } - else if (m.is_eq(curr, arg1, arg2)) { - if (is_unknown(arg1)) { - todo.push_back(arg1); - } - if (is_unknown(arg2)) { - todo.push_back(arg2); - } - if (curr != todo.back()) { - continue; - } - if (is_x(arg1) || is_x(arg2)) { - set_x(curr); - } - else { - set_bool(curr, get_value(arg1) == get_value(arg2)); - } - } - else if (m.is_ite(curr, argCond, argThen, argElse) && m_arith.is_int_real(argThen)) { - if (is_true(argCond) || (argThen == argElse)) { - if (is_unknown(argThen)) { - todo.push_back(argThen); - continue; - } - if (is_x(argThen)) { - set_x(curr); - } - else { - set_value(curr, get_value(argThen)); - } - } - else if (is_false(argCond)) { - if (is_unknown(argElse)) { - todo.push_back(argElse); - continue; - } - if (is_x(argElse)) { - set_x(curr); - } - else { - set_value(curr, get_value(argElse)); - } - } - else if (is_unknown(argCond)) { - todo.push_back(argCond); - continue; - } - else { - set_x(curr); - } - } - else { - UNREACHABLE(); - } + eval_basic(curr); } else { - TRACE("pdr_verbse", tout << "Not evaluated " << mk_pp(curr, m) << "\n";); - set_x(curr); + expr_ref vl(m); + m_model->eval(curr, vl); + assign_value(curr, vl); } IF_VERBOSE(35,verbose_stream() << "assigned "< const& formulas) { tout << "formula is " << (is_true(form) ? "true" : is_false(form) ? "false" : "unknown") << "\n" <get_arity()==0); - expr_ref interp(m); - pdr::get_value_from_model(mdl, d, interp); - - app_ref constant(m.mk_const(d), m); - app_ref lit(m); - if (m.is_bool(d->get_range())) { - if (m.is_true(interp)) { - lit = constant; - } - else { - SASSERT(m.is_false(interp)); - lit = m.mk_not(constant); - } - } - else { - lit = m.mk_eq(constant, interp); - } - res.push_back(lit); - } -} } diff --git a/lib/pdr_util.h b/lib/pdr_util.h index 8372f6fcc..4f6ab1ad3 100644 --- a/lib/pdr_util.h +++ b/lib/pdr_util.h @@ -170,34 +170,15 @@ void vect_set_union(ref_vector & tgt, ref_vector & src, Comp } -class model_evaluator_base { -protected: - virtual void check_model(ptr_vector const & formulas, - expr_ref_vector & model, bool & has_unknown, bool & has_false) = 0; -public: - virtual void minimize_model(ptr_vector const & formulas, expr_ref_vector & model); -}; -class th_rewriter_model_evaluator : public model_evaluator_base { - class expr_rewriter_cfg; - ast_manager& m; - th_rewriter m_rewriter; - - void setup_assignment(expr_ref_vector const& model, obj_map& assignment); - -protected: - virtual void check_model(ptr_vector const & formulas, - expr_ref_vector & model, bool & has_unknown, - bool & has_false); -public: - th_rewriter_model_evaluator(ast_manager& m) : m(m), m_rewriter(m) {} -}; - -class ternary_model_evaluator : public model_evaluator_base { +class model_evaluator { ast_manager& m; arith_util m_arith; bv_util m_bv; - obj_map m_values; + obj_map m_numbers; + expr_ref_vector m_refs; + obj_map m_values; + model_ref m_model; //00 -- non-visited //01 -- X @@ -209,16 +190,17 @@ class ternary_model_evaluator : public model_evaluator_base { unsigned m_level2; expr_mark m_visited; - void setup_model(expr_ref_vector const& model); - void add_model(expr* e); - void del_model(expr* e); - - bool get_assignment(expr* e, expr*& var, expr*& val); + void reset(); + void setup_model(model_ref& model); + void assign_value(expr* e, expr* v); 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); - void prune_by_probing(ptr_vector const & formulas, expr_ref_vector& model); + void process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect); + 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); + void inherit_value(expr* e, expr* v); //00 -- non-visited //01 -- X @@ -234,27 +216,34 @@ class ternary_model_evaluator : public model_evaluator_base { inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); } inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } } - inline rational const& get_value(expr* x) const { return m_values.find(x); } - inline void set_value(expr* x, rational const& v) { set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_values.insert(x,v); } - + inline rational const& get_number(expr* x) const { return m_numbers.find(x); } + inline void set_number(expr* x, rational const& v) { set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v); } + inline expr* get_value(expr* x) { return m_values.find(x); } + inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); } + protected: + bool check_model(ptr_vector const & formulas); - virtual void check_model(ptr_vector const & formulas, expr_ref_vector & model, - bool & has_unknown, bool & has_false) { - UNREACHABLE(); - } public: - ternary_model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m) {} - virtual void minimize_model(ptr_vector const & formulas, expr_ref_vector & model); + model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m), m_refs(m) {} + + /** + \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. \pre model satisfies formulas */ - expr_ref_vector minimize_literals(ptr_vector const & formulas, expr_ref_vector const & model); + expr_ref_vector minimize_literals(ptr_vector const & formulas, model_ref& mdl); + // for_each_expr visitor. void operator()(expr* e) {} @@ -262,11 +251,6 @@ public: void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res); -/** -If the solver argument is non-zero, we will exclude its auxiliary symbols from the generated cube. -*/ -void get_cube_from_model(const model_core & mdl, expr_ref_vector & res, pdr::prop_solver& solver); - } #endif diff --git a/lib/qe_lite.cpp b/lib/qe_lite.cpp new file mode 100644 index 000000000..d295327da --- /dev/null +++ b/lib/qe_lite.cpp @@ -0,0 +1,536 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + qe_lite.cpp + +Abstract: + + Light weight partial quantifier-elimination procedure + +Author: + + Nikolaj Bjorner (nbjorner) 2012-10-17 + +Revision History: + + - TBD: integrate Fourier Motzkin elimination + integrate Gaussean elimination + +--*/ +#include "qe_lite.h" +#include "expr_abstract.h" +#include "used_vars.h" +#include"occurs.h" +#include"for_each_expr.h" +#include"rewriter_def.h" +#include"ast_pp.h" +#include"ast_ll_pp.h" +#include"ast_smt2_pp.h" +#include"tactical.h" +#include"bool_rewriter.h" +#include"var_subst.h" + +class der2 { + ast_manager & m; + var_subst m_subst; + expr_ref_buffer m_new_exprs; + + ptr_vector m_map; + int_vector m_pos2var; + ptr_vector m_inx2var; + unsigned_vector m_order; + expr_ref_vector m_subst_map; + expr_ref_buffer m_new_args; + + /** + \brief Return true if e can be viewed as a variable disequality. + Store the variable id in v and the definition in t. + For example: + + if e is (not (= (VAR 1) T)), then v assigned to 1, and t to T. + if e is (iff (VAR 2) T), then v is assigned to 2, and t to (not T). + (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))), + and can be viewed as a disequality. + */ + bool is_var_diseq(expr * e, unsigned num_decls, var *& v, expr_ref & t); + + /** + \brief Return true if e can be viewed as a variable equality. + */ + bool is_var_eq(expr * e, unsigned num_decls, var *& v, expr_ref & t); + + bool is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t); + + void get_elimination_order(); + void create_substitution(unsigned sz); + void apply_substitution(quantifier * q, expr_ref & r); + void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr); + void elim_unused_vars(expr_ref& r, proof_ref &pr); + +public: + der2(ast_manager & m):m(m),m_subst(m),m_new_exprs(m),m_subst_map(m),m_new_args(m) {} + void operator()(quantifier * q, expr_ref & r, proof_ref & pr); + void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr); + ast_manager& get_manager() const { return m; } +}; + +static bool is_var(expr * e, unsigned num_decls) { + return is_var(e) && to_var(e)->get_idx() < num_decls; +} + +static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) { + expr* e1; + return m.is_not(e, e1) && is_var(e1, num_decls); +} + +bool der2::is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t) { + if (check_eq) { + return is_var_eq(e, num_decls, v, t); + } + else { + return is_var_diseq(e, num_decls, v, t); + } +} + +bool der2::is_var_eq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { + expr* lhs, *rhs; + + // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases + if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) { + // (iff (not VAR) t) (iff t (not VAR)) cases + if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls) && m.is_bool(lhs)) { + if (!is_neg_var(m, lhs, num_decls)) { + std::swap(lhs, rhs); + } + if (!is_neg_var(m, lhs, num_decls)) { + return false; + } + v = to_var(lhs); + t = m.mk_not(rhs); + m_new_exprs.push_back(t); + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + } + if (!is_var(lhs, num_decls)) + std::swap(lhs, rhs); + if (!is_var(lhs, num_decls)) + return false; + v = to_var(lhs); + t = rhs; + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + } + + // (ite cond (= VAR t) (= VAR t2)) case + expr* cond, *e2, *e3; + if (m.is_ite(e, cond, e2, e3)) { + if (is_var_eq(e2, num_decls, v, t)) { + expr_ref t2(m); + var* v2; + if (is_var_eq(e3, num_decls, v2, t2) && v2 == v) { + t = m.mk_ite(cond, t, t2); + m_new_exprs.push_back(t); + return true; + } + } + return false; + } + + // VAR = true case + if (is_var(e, num_decls)) { + t = m.mk_true(); + v = to_var(e); + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + } + + // VAR = false case + if (is_neg_var(m, e, num_decls)) { + t = m.mk_false(); + v = to_var(to_app(e)->get_arg(0)); + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + } + + return false; +} + +/** + \brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or + (iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)). + The last case can be viewed +*/ +bool der2::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { + expr* e1; + if (m.is_not(e, e1)) { + return is_var_eq(e, num_decls, v, t); + } + else if (is_var_eq(e, num_decls, v, t) && m.is_bool(v)) { + bool_rewriter(m).mk_not(t, t); + m_new_exprs.push_back(t); + return true; + } + else { + return false; + } +} + +void der2::elim_unused_vars(expr_ref& r, proof_ref& pr) { + if (is_quantifier(r)) { + quantifier * q = to_quantifier(r); + ::elim_unused_vars(m, q, r); + if (m.proofs_enabled()) { + proof * p1 = m.mk_elim_unused_vars(q, r); + pr = m.mk_transitivity(pr, p1); + } + } +} + +/** + Reduce the set of definitions in quantifier. + Then eliminate variables that have become unused +*/ +void der2::operator()(quantifier * q, expr_ref & r, proof_ref & pr) { + TRACE("der", tout << mk_pp(q, m) << "\n";); + pr = 0; + r = q; + reduce_quantifier(q, r, pr); + if (r != q) { + elim_unused_vars(r, pr); + } +} + +void der2::reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) { + r = q; + // Keep applying reduce_quantifier1 until r doesn't change anymore + do { + proof_ref curr_pr(m); + q = to_quantifier(r); + reduce_quantifier1(q, r, curr_pr); + if (m.proofs_enabled()) { + pr = m.mk_transitivity(pr, curr_pr); + } + } while (q != r && is_quantifier(r)); + + m_new_exprs.reset(); +} + +void der2::reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) { + expr * e = q->get_expr(); + unsigned num_decls = q->get_num_decls(); + var * v = 0; + expr_ref t(m); + unsigned num_args = 1; + expr* const* args = &e; + if ((q->is_forall() && m.is_or(e)) || + (q->is_exists() && m.is_and(e))) { + num_args = to_app(e)->get_num_args(); + args = to_app(e)->get_args(); + } + + unsigned def_count = 0; + unsigned largest_vinx = 0; + + m_map.reset(); + m_pos2var.reset(); + m_inx2var.reset(); + m_pos2var.reserve(num_args, -1); + + // Find all definitions + for (unsigned i = 0; i < num_args; i++) { + if (is_var_def(q->is_exists(), args[i], num_decls, v, t)) { + unsigned idx = v->get_idx(); + if(m_map.get(idx, 0) == 0) { + m_map.reserve(idx + 1, 0); + m_inx2var.reserve(idx + 1, 0); + m_map[idx] = t; + m_inx2var[idx] = v; + m_pos2var[i] = idx; + def_count++; + largest_vinx = std::max(idx, largest_vinx); + } + } + } + + if (def_count > 0) { + get_elimination_order(); + SASSERT(m_order.size() <= def_count); // some might be missing because of cycles + + if (!m_order.empty()) { + create_substitution(largest_vinx + 1); + apply_substitution(q, r); + } + else { + r = q; + } + } + else { + TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";); + r = q; + } + + if (m.proofs_enabled()) { + pr = r == q ? 0 : m.mk_der(q, r); + } +} + +static void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { + order.reset(); + + // eliminate self loops, and definitions containing quantifiers. + bool found = false; + for (unsigned i = 0; i < definitions.size(); i++) { + var * v = vars[i]; + expr * t = definitions[i]; + if (t == 0 || has_quantifiers(t) || occurs(v, t)) + definitions[i] = 0; + else + found = true; // found at least one candidate + } + + if (!found) + return; + + typedef std::pair frame; + svector todo; + + expr_fast_mark1 visiting; + expr_fast_mark2 done; + + unsigned vidx, num; + + for (unsigned i = 0; i < definitions.size(); i++) { + if (definitions[i] == 0) + continue; + var * v = vars[i]; + SASSERT(v->get_idx() == i); + SASSERT(todo.empty()); + todo.push_back(frame(v, 0)); + while (!todo.empty()) { + start: + frame & fr = todo.back(); + expr * t = fr.first; + if (t->get_ref_count() > 1 && done.is_marked(t)) { + todo.pop_back(); + continue; + } + switch (t->get_kind()) { + case AST_VAR: + vidx = to_var(t)->get_idx(); + if (fr.second == 0) { + CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); + // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula. + if (definitions.get(vidx, 0) != 0) { + if (visiting.is_marked(t)) { + // cycle detected: remove t + visiting.reset_mark(t); + definitions[vidx] = 0; + } + else { + visiting.mark(t); + fr.second = 1; + todo.push_back(frame(definitions[vidx], 0)); + goto start; + } + } + } + else { + SASSERT(fr.second == 1); + if (definitions.get(vidx, 0) != 0) { + visiting.reset_mark(t); + order.push_back(vidx); + } + else { + // var was removed from the list of candidate vars to elim cycle + // do nothing + } + } + if (t->get_ref_count() > 1) + done.mark(t); + todo.pop_back(); + break; + case AST_QUANTIFIER: + UNREACHABLE(); + todo.pop_back(); + break; + case AST_APP: + num = to_app(t)->get_num_args(); + while (fr.second < num) { + expr * arg = to_app(t)->get_arg(fr.second); + fr.second++; + if (arg->get_ref_count() > 1 && done.is_marked(arg)) + continue; + todo.push_back(frame(arg, 0)); + goto start; + } + if (t->get_ref_count() > 1) + done.mark(t); + todo.pop_back(); + break; + default: + UNREACHABLE(); + todo.pop_back(); + break; + } + } + } +} + +void der2::get_elimination_order() { + m_order.reset(); + + TRACE("top_sort", + tout << "DEFINITIONS: " << std::endl; + for(unsigned i = 0; i < m_map.size(); i++) + if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl; + ); + + // der2::top_sort ts(m); + der_sort_vars(m_inx2var, m_map, m_order); + + TRACE("der", + tout << "Elimination m_order:" << std::endl; + for(unsigned i=0; iget_expr(); + unsigned num_args=to_app(e)->get_num_args(); + bool_rewriter rw(m); + + // get a new expression + m_new_args.reset(); + for(unsigned i = 0; i < num_args; i++) { + int x = m_pos2var[i]; + if (x != -1 && m_map[x] != 0) + continue; // this is a disequality with definition (vanishes) + + m_new_args.push_back(to_app(e)->get_arg(i)); + } + + expr_ref t(m); + if (q->is_forall()) { + rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t); + } + else { + rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t); + } + expr_ref new_e(m); + m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e); + + // don't forget to update the quantifier patterns + expr_ref_buffer new_patterns(m); + expr_ref_buffer new_no_patterns(m); + for (unsigned j = 0; j < q->get_num_patterns(); j++) { + expr_ref new_pat(m); + m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat); + new_patterns.push_back(new_pat); + } + + for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { + expr_ref new_nopat(m); + m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat); + new_no_patterns.push_back(new_nopat); + } + + r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), + new_no_patterns.size(), new_no_patterns.c_ptr(), new_e); +} + + + + + +class qe_lite::impl { + ast_manager& m; + der2 m_der; + +public: + impl(ast_manager& m): m(m), m_der(m) {} + + void operator()(app_ref_vector& vars, expr_ref& fml) { + expr_ref tmp(fml); + quantifier_ref q(m); + proof_ref pr(m); + symbol qe_lite("QE"); + expr_abstract(m, 0, vars.size(), (expr*const*)vars.c_ptr(), fml, tmp); + ptr_vector sorts; + svector names; + for (unsigned i = 0; i < vars.size(); ++i) { + sorts.push_back(m.get_sort(vars[i].get())); + names.push_back(vars[i]->get_decl()->get_name()); + } + q = m.mk_exists(vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qe_lite); + m_der.reduce_quantifier(q, tmp, pr); + // assumes m_der just updates the quantifier and does not change things more. + if (is_exists(tmp) && to_quantifier(tmp)->get_qid() == qe_lite) { + used_vars used; + tmp = to_quantifier(tmp)->get_expr(); + used.process(tmp); + var_subst vs(m, true); + vs(tmp, vars.size(), (expr*const*)vars.c_ptr(), fml); + // collect set of variables that were used. + unsigned j = 0; + for (unsigned i = 0; i < vars.size(); ++i) { + if (used.contains(vars.size()-i-1)) { + vars[j] = vars[i]; + ++j; + } + } + vars.resize(j); + } + else { + fml = tmp; + } + } + + void operator()(expr_ref& fml, proof_ref& pr) { + // TODO apply der everywhere as a rewriting rule. + // TODO add cancel method. + if (is_quantifier(fml)) { + m_der(to_quantifier(fml), fml, pr); + } + } + +}; + +qe_lite::qe_lite(ast_manager& m) { + m_impl = alloc(impl, m); +} + +qe_lite::~qe_lite() { + dealloc(m_impl); +} + +void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) { + (*m_impl)(vars, fml); +} + +void qe_lite::operator()(expr_ref& fml, proof_ref& pr) { + (*m_impl)(fml, pr); +} diff --git a/lib/qe_lite.h b/lib/qe_lite.h new file mode 100644 index 000000000..1a2f98294 --- /dev/null +++ b/lib/qe_lite.h @@ -0,0 +1,49 @@ +/*++ +Copyright (c) 2010 Microsoft Corporation + +Module Name: + + qe_lite.h + +Abstract: + + Light weight partial quantifier-elimination procedures + +Author: + + Nikolaj Bjorner (nbjorner) 2012-10-17 + +Revision History: + + +--*/ + +#ifndef __QE_LITE_H__ +#define __QE_LITE_H__ + +#include "ast.h" + +class qe_lite { + class impl; + impl * m_impl; +public: + qe_lite(ast_manager& m); + + ~qe_lite(); + + /** + \brief + Apply light-weight quantifier elimination + on constants provided as vector of variables. + Return the updated formula and updated set of variables that were not eliminated. + + */ + void operator()(app_ref_vector& vars, expr_ref& fml); + + /** + \brief full rewriting based light-weight quantifier elimination round. + */ + void operator()(expr_ref& fml, proof_ref& pr); +}; + +#endif __QE_LITE_H__