From 6fee9b90cb6fb4a82b9d3acd26ab31dd1c7c7273 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Apr 2019 11:39:27 -0700 Subject: [PATCH] fix model generation for tc/po Signed-off-by: Nikolaj Bjorner --- src/ast/recfun_decl_plugin.cpp | 17 +-- src/ast/recfun_decl_plugin.h | 10 +- src/ast/rewriter/bool_rewriter.cpp | 33 +++-- src/ast/rewriter/bool_rewriter.h | 1 + src/ast/rewriter/bool_rewriter_params.pyg | 1 + src/ast/special_relations_decl_plugin.cpp | 6 +- src/ast/special_relations_decl_plugin.h | 8 -- src/model/model.cpp | 15 ++- src/model/model_evaluator.cpp | 27 ++-- src/model/model_smt2_pp.cpp | 2 +- src/smt/theory_special_relations.cpp | 157 ++++++---------------- src/smt/theory_special_relations.h | 11 +- src/util/obj_hashtable.h | 6 +- 13 files changed, 117 insertions(+), 177 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 0feb21d86..ba1b4f171 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -50,7 +50,7 @@ namespace recfun { } def::def(ast_manager &m, family_id fid, symbol const & s, - unsigned arity, sort* const * domain, sort* range) + unsigned arity, sort* const * domain, sort* range, bool is_generated) : m(m), m_name(s), m_domain(m, arity, domain), m_range(range, m), m_vars(m), m_cases(), @@ -59,7 +59,8 @@ namespace recfun { m_fid(fid) { SASSERT(arity == get_arity()); - func_decl_info info(fid, OP_FUN_DEFINED); + parameter p(is_generated); + func_decl_info info(fid, OP_FUN_DEFINED, 1, &p); m_decl = m.mk_func_decl(s, arity, domain, range, info); } @@ -315,8 +316,8 @@ namespace recfun { util::~util() { } - def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) { - return alloc(def, m(), m_fid, name, n, domain, range); + def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range, bool is_generated) { + return alloc(def, m(), m_fid, name, n, domain, range, is_generated); } @@ -386,15 +387,15 @@ namespace recfun { return *(m_util.get()); } - promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range) { - def* d = u().decl_fun(name, n, params, range); + promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) { + def* d = u().decl_fun(name, n, params, range, is_generated); SASSERT(!m_defs.contains(d->get_decl())); m_defs.insert(d->get_decl(), d); return promise_def(&u(), d); } - promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range) { - def* d = u().decl_fun(name, n, params, range); + promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) { + def* d = u().decl_fun(name, n, params, range, is_generated); def* d2 = nullptr; if (m_defs.find(d->get_decl(), d2)) { dealloc(d2); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 33b5294f5..786ea9dd2 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -108,7 +108,7 @@ namespace recfun { expr_ref m_rhs; //!< definition family_id m_fid; - def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range); + def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range, bool is_generated); // compute cases for a function, given its RHS (possibly containing `ite`). void compute_cases(replace& subst, is_immediate_pred &, @@ -147,6 +147,7 @@ namespace recfun { class plugin : public decl_plugin { typedef obj_map def_map; typedef obj_map case_def_map; + mutable scoped_ptr m_util; def_map m_defs; // function->def @@ -171,9 +172,9 @@ namespace recfun { func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) override; - promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range); + promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false); - promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range); + promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false); void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); @@ -216,6 +217,7 @@ namespace recfun { bool is_case_pred(expr * e) const { return is_app_of(e, m_fid, OP_FUN_CASE_PRED); } bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); } bool is_defined(func_decl* f) const { return is_decl_of(f, m_fid, OP_FUN_DEFINED); } + bool is_generated(func_decl* f) const { return is_defined(f) && f->get_parameter(0).get_int() == 1; } bool is_depth_limit(expr * e) const { return is_app_of(e, m_fid, OP_DEPTH_LIMIT); } bool owns_app(app * e) const { return e->get_family_id() == m_fid; } @@ -223,7 +225,7 @@ namespace recfun { bool has_defs() const { return m_plugin->has_defs(); } //has_def(f)); diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index d26c55fda..ce29eb9cf 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -24,6 +24,7 @@ void bool_rewriter::updt_params(params_ref const & _p) { bool_rewriter_params p(_p); m_flat = p.flat(); m_elim_and = p.elim_and(); + m_elim_ite = p.elim_ite(); m_local_ctx = p.local_ctx(); m_local_ctx_limit = p.local_ctx_limit(); m_blast_distinct = p.blast_distinct(); @@ -797,48 +798,52 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = c; return BR_DONE; } - mk_or(c, e, result); - return BR_DONE; + if (m_elim_ite) { + mk_or(c, e, result); + return BR_DONE; + } } if (m().is_false(t)) { if (m().is_true(e)) { mk_not(c, result); return BR_DONE; } - expr_ref tmp(m()); - mk_not(c, tmp); - mk_and(tmp, e, result); - return BR_DONE; + if (m_elim_ite) { + expr_ref tmp(m()); + mk_not(c, tmp); + mk_and(tmp, e, result); + return BR_DONE; + } } - if (m().is_true(e)) { + if (m().is_true(e) && m_elim_ite) { expr_ref tmp(m()); mk_not(c, tmp); mk_or(tmp, t, result); return BR_DONE; } - if (m().is_false(e)) { + if (m().is_false(e) && m_elim_ite) { mk_and(c, t, result); return BR_DONE; } - if (c == e) { + if (c == e && m_elim_ite) { mk_and(c, t, result); return BR_DONE; } - if (c == t) { + if (c == t && m_elim_ite) { mk_or(c, e, result); return BR_DONE; } - if (m().is_complement_core(t, e)) { // t = not(e) + if (m().is_complement_core(t, e) && m_elim_ite) { // t = not(e) mk_eq(c, t, result); return BR_DONE; } - if (m().is_complement_core(e, t)) { // e = not(t) + if (m().is_complement_core(e, t) && m_elim_ite) { // e = not(t) mk_eq(c, t, result); return BR_DONE; } } - if (m().is_ite(t) && m_ite_extra_rules) { + if (m().is_ite(t) && m_ite_extra_rules && m_elim_ite) { // (ite c1 (ite c2 t1 t2) t1) ==> (ite (and c1 (not c2)) t2 t1) if (e == to_app(t)->get_arg(1)) { expr_ref not_c2(m()); @@ -891,7 +896,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re } } - if (m().is_ite(e) && m_ite_extra_rules) { + if (m().is_ite(e) && m_ite_extra_rules && m_elim_ite) { // (ite c1 t1 (ite c2 t1 t2)) ==> (ite (or c1 c2) t1 t2) if (t == to_app(e)->get_arg(1)) { expr_ref new_c(m()); diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 83ece2aae..cd122791b 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -59,6 +59,7 @@ class bool_rewriter { bool m_ite_extra_rules; unsigned m_local_ctx_limit; unsigned m_local_ctx_cost; + bool m_elim_ite; br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result); diff --git a/src/ast/rewriter/bool_rewriter_params.pyg b/src/ast/rewriter/bool_rewriter_params.pyg index 531bf4db9..85583cbca 100644 --- a/src/ast/rewriter/bool_rewriter_params.pyg +++ b/src/ast/rewriter/bool_rewriter_params.pyg @@ -4,6 +4,7 @@ def_module_params(module_name='rewriter', params=(("ite_extra_rules", BOOL, False, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"), ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"), ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"), + ('elim_ite', BOOL, True, "eliminate ite in favor of and/or"), ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"), ("local_ctx_limit", UINT, UINT_MAX, "limit for applying local context simplifier"), ("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities"), diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp index 149f37aef..2b280b28a 100644 --- a/src/ast/special_relations_decl_plugin.cpp +++ b/src/ast/special_relations_decl_plugin.cpp @@ -45,7 +45,7 @@ func_decl * special_relations_decl_plugin::mk_func_decl( if (!range) { range = m_manager->mk_bool_sort(); } - if (!m_manager->is_bool(range) && k != OP_SPECIAL_RELATION_NEXT) { + if (!m_manager->is_bool(range)) { m_manager->raise_exception("range type is expected to be Boolean for special relations"); } func_decl_info info(m_family_id, k, num_parameters, parameters); @@ -57,7 +57,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl( case OP_SPECIAL_RELATION_TO: name = m_to; break; case OP_SPECIAL_RELATION_TC: name = m_tc; break; case OP_SPECIAL_RELATION_TRC: name = m_trc; break; - case OP_SPECIAL_RELATION_NEXT: name = symbol("next"); break; } return m_manager->mk_func_decl(name, arity, domain, range, info); } @@ -70,8 +69,6 @@ void special_relations_decl_plugin::get_op_names(svector & op_name op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO)); op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC)); op_names.push_back(builtin_name(m_trc.bare_str(), OP_SPECIAL_RELATION_TRC)); - // next is an internal skolem function used for unfolding a relation R to satisfy a relation that - // is asserted for the transitive closure of R. } } @@ -83,7 +80,6 @@ sr_property special_relations_util::get_property(func_decl* f) const { case OP_SPECIAL_RELATION_TO: return sr_to; case OP_SPECIAL_RELATION_TC: return sr_tc; case OP_SPECIAL_RELATION_TRC: return sr_trc; - case OP_SPECIAL_RELATION_NEXT: return sr_none; default: UNREACHABLE(); return sr_po; diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index 8e32e9817..f7a3b963d 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -30,7 +30,6 @@ enum special_relations_op_kind { OP_SPECIAL_RELATION_TO, OP_SPECIAL_RELATION_TC, OP_SPECIAL_RELATION_TRC, - OP_SPECIAL_RELATION_NEXT, LAST_SPECIAL_RELATIONS_OP }; @@ -95,12 +94,6 @@ public: func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); } func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); } func_decl* mk_trc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TRC); } - func_decl* mk_next(func_decl* f) { - sort* s = f->get_domain(0); - sort* domain[2] = { s, s }; - parameter p(f); SASSERT(f->get_arity() == 2); - return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_NEXT, 1, &p, 2, domain, s); - } bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); } bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); } @@ -108,7 +101,6 @@ public: bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); } bool is_tc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TC); } bool is_trc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TRC); } - bool is_next(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_NEXT); } app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); } app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); } diff --git a/src/model/model.cpp b/src/model/model.cpp index aa3976cb9..15344b35d 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -170,7 +170,11 @@ struct model::top_sort : public ::top_sort { top_sort(ast_manager& m): m_rewrite(m) - {} + { + params_ref p; + p.set_bool("elim_ite", false); + m_rewrite.updt_params(p); + } void add_occurs(func_decl* f) { m_occur_count.insert(f, occur_count(f) + 1); @@ -428,7 +432,12 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) } #endif else { - new_t = ts.m_rewrite.mk_app(f, args.size(), args.c_ptr()); + if (m.is_ite(f)) { + new_t = m.mk_app(f, args.size(), args.c_ptr()); + } + else { + new_t = ts.m_rewrite.mk_app(f, args.size(), args.c_ptr()); + } } if (t != new_t.get()) trail.push_back(new_t); @@ -443,7 +452,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) break; } } - + ts.m_rewrite(cache[e], new_t); return new_t; } diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 229ed875e..a060be8cf 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -99,7 +99,11 @@ struct evaluator_cfg : public default_rewriter_cfg { bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { func_interp * fi = m_model.get_func_interp(f); - return (fi != nullptr) && eval_fi(fi, num, args, result); + bool r = (fi != nullptr) && eval_fi(fi, num, args, result); + CTRACE("model_evaluator", r, tout << "reduce_app " << f->get_name() << "\n"; + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n"; + tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";); + return r; } // Try to use the entries to quickly evaluate the fi @@ -138,6 +142,7 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + TRACE("model_evaluator", tout << f->get_name() << "\n";); result_pr = nullptr; family_id fid = f->get_family_id(); bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f); @@ -188,7 +193,7 @@ struct evaluator_cfg : public default_rewriter_cfg { } return m_b_rw.mk_app_core(f, num, args, result); } - + CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";); if (fid == m_a_rw.get_fid()) st = m_a_rw.mk_app_core(f, num, args, result); else if (fid == m_bv_rw.get_fid()) @@ -208,21 +213,19 @@ struct evaluator_cfg : public default_rewriter_cfg { st = BR_DONE; } else if (evaluate(f, num, args, result)) { - TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n"; - tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";); st = BR_REWRITE1; } - if (st == BR_FAILED && !m.is_builtin_family_id(fid)) + CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";); + if (st == BR_FAILED && !m.is_builtin_family_id(fid)) { st = evaluate_partial_theory_func(f, num, args, result, result_pr); + CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";); + } if (st == BR_DONE && is_app(result)) { app* a = to_app(result); if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) { st = BR_REWRITE1; } } -#if 1 - TRACE("model_evaluator", tout << st << " " << num << " " << m_ar.is_as_array(f) << " " << m_model_completion << "\n";); if (st == BR_FAILED && num == 0 && m_ar.is_as_array(f) && m_model_completion) { func_decl* g = nullptr; VERIFY(m_ar.is_as_array(f, g)); @@ -253,7 +256,6 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_DONE; } } -#endif CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";); return st; @@ -296,7 +298,7 @@ struct evaluator_cfg : public default_rewriter_cfg { return false; } def = fi->get_interp(); - SASSERT(def != 0); + SASSERT(def != nullptr); return true; } @@ -320,7 +322,7 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status evaluate_partial_theory_func(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - SASSERT(f != 0); + SASSERT(f != nullptr); SASSERT(!m.is_builtin_family_id(f->get_family_id())); result = nullptr; result_pr = nullptr; @@ -433,8 +435,7 @@ struct evaluator_cfg : public default_rewriter_cfg { args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae); // stores with smaller index take precedence - for (unsigned i = stores1.size(); i > 0; ) { - --i; + for (unsigned i = stores1.size(); i-- > 0; ) { table1.insert(stores1[i].c_ptr()); } diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index b2a4f02aa..196843de4 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -196,7 +196,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co sort_fun_decls(m, md, func_decls); for (unsigned i = 0; i < func_decls.size(); i++) { func_decl * f = func_decls[i]; - if (recfun_util.is_defined(f)) { + if (recfun_util.is_defined(f) && !recfun_util.is_generated(f)) { continue; } func_interp * f_i = md.get_func_interp(f); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 4e3205c4f..03f11dd26 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -34,6 +34,15 @@ Notes: namespace smt { + func_decl* theory_special_relations::relation::next() { + if (!m_next) { + sort* s = decl()->get_domain(0); + sort* domain[2] = {s, s}; + m_next = m.mk_fresh_func_decl("next", "", 2, domain, s); + } + return m_next; + } + void theory_special_relations::relation::push() { m_scopes.push_back(scope()); scope& s = m_scopes.back(); @@ -104,37 +113,35 @@ namespace smt { assert f(term,c) or term != b assert f(term,c) or term != a */ - bool theory_special_relations::internalize_term(app * term) { - if (m_util.is_next(term)) { - return false; - } - mk_var(term); + void theory_special_relations::internalize_next(func_decl* f, app* term) { context& ctx = get_context(); ast_manager& m = get_manager(); - func_decl* f = to_func_decl(term->get_decl()->get_parameter(0).get_ast()); + func_decl* nxt = term->get_decl(); expr* src = term->get_arg(0); expr* dst = term->get_arg(1); expr_ref f_rel(m.mk_app(f, src, dst), m); + ensure_enode(term); + ensure_enode(f_rel); literal f_lit = ctx.get_literal(f_rel); src = term; - while (m_util.is_next(src)) { + while (to_app(src)->get_decl() == nxt) { dst = to_app(src)->get_arg(1); src = to_app(src)->get_arg(0); ctx.mk_th_axiom(get_id(), f_lit, ~mk_eq(term, src, false)); ctx.mk_th_axiom(get_id(), f_lit, ~mk_eq(term, dst, false)); } - return true; + } + + bool theory_special_relations::internalize_term(app * term) { + return false; } bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) { SASSERT(m_util.is_special_relation(atm)); relation* r = 0; - if (m_util.is_next(atm)) { - return internalize_term(atm); - } ast_manager& m = get_manager(); if (!m_relations.find(atm->get_decl(), r)) { - r = alloc(relation, m_util.get_property(atm), atm->get_decl()); + r = alloc(relation, m_util.get_property(atm), atm->get_decl(), m); m_relations.insert(atm->get_decl(), r); for (unsigned i = 0; i < m_atoms_lim.size(); ++i) r->push(); } @@ -350,7 +357,8 @@ namespace smt { // TBD: perhaps replace by recursion unfolding similar to theory_rec_fun // - expr_ref next(m.mk_app(m_util.mk_next(f), arg1, arg2), m); + app_ref next(r.next(arg1, arg2), m); + internalize_next(f, next); expr_ref a2next(m.mk_app(f, arg1, next), m); expr_ref next2b(m.mk_app(tcf, next, arg2), m); expr_ref next_b(m.mk_app(f, next, arg2), m); @@ -365,7 +373,7 @@ namespace smt { ctx.mk_th_axiom(get_id(), ~literal(bv), f_lit, a2next_l); ctx.mk_th_axiom(get_id(), ~literal(bv), f_lit, next2b_l); expr* nxt = next; - while (m_util.is_next(nxt)) { + while (r.is_next(nxt)) { expr* left = to_app(nxt)->get_arg(0); expr* right = to_app(nxt)->get_arg(1); ctx.assign(~mk_eq(next, left, false), nullptr); @@ -896,9 +904,9 @@ namespace smt { Take 2: connected(A, dst, S) = - if A = nil then false else - if member(dst, A) then true else - let (A',S') = next1(a1, b1, A, next1(a2, b2, A, ... S, (nil, nil))) + let (A',S') = next1(a1, b1, A, next1(a2, b2, A, ... S, (nil, S))) + if A' = nil then false else + if member(dst, A') then true else connected(A', dst, S') next1(a, b, A, S, (A',S')) = @@ -915,6 +923,7 @@ Take 2: func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), hd(m), tl(m); sort_ref listS(dt.mk_list_datatype(s, symbol("List"), cons, is_cons, hd, tl, nil, is_nil), m); func_decl_ref fst(m), snd(m), pair(m); + expr_ref nilc(m.mk_const(nil), m); expr* T = m.mk_true(); expr* F = m.mk_false(); @@ -923,7 +932,7 @@ Take 2: { sort* dom[2] = { s, listS }; - recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom, m.mk_bool_sort()); + recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom, m.mk_bool_sort(), true); memf = mem.get_def()->get_decl(); var_ref xV(m.mk_var(1, s), m); @@ -941,14 +950,12 @@ Take 2: var* vars[2] = { xV, SV }; p.set_definition(rep, mem, 2, vars, mem_body); } - -#if 1 sort_ref tup(dt.mk_pair_datatype(listS, listS, fst, snd, pair), m); { sort* dom[5] = { s, s, listS, listS, tup }; - recfun::promise_def nxt = p.ensure_def(symbol("next"), 5, dom, tup); + recfun::promise_def nxt = p.ensure_def(symbol("next"), 5, dom, tup, true); nextf = nxt.get_def()->get_decl(); expr_ref next_body(m); @@ -969,7 +976,7 @@ Take 2: { sort* dom[3] = { listS, s, listS }; - recfun::promise_def connected = p.ensure_def(symbol("connected"), 3, dom, m.mk_bool_sort()); + recfun::promise_def connected = p.ensure_def(symbol("connected"), 3, dom, m.mk_bool_sort(), true); connectedf = connected.get_def()->get_decl(); var_ref AV(m.mk_var(2, listS), m); var_ref dstV(m.mk_var(1, s), m); @@ -977,7 +984,7 @@ Take 2: expr* A = AV, *dst = dstV, *S = SV; expr_ref connected_body(m); - connected_body = m.mk_app(pair, m.mk_const(nil), m.mk_const(nil)); + connected_body = m.mk_app(pair, nilc, S); for (atom* ap : r.m_asserted_atoms) { atom& a = *ap; @@ -989,7 +996,14 @@ Take 2: expr* args[5] = { x, y, A, S, cb }; connected_body = m.mk_app(nextf, 5, args); } + expr_ref Ap(m.mk_app(fst, connected_body), m); + expr_ref Sp(m.mk_app(snd, connected_body), m); + + connected_body = m.mk_ite(m.mk_eq(Ap, nilc), F, + m.mk_ite(m.mk_app(memf, dst, Ap), T, + m.mk_app(connectedf, Ap, dst, Sp))); + TRACE("special_relations", tout << connected_body << "\n";); recfun_replace rep(m); var* vars[3] = { AV, dstV, SV }; p.set_definition(rep, connected, 3, vars, connected_body); @@ -1001,91 +1015,14 @@ Take 2: expr* x = xV, *y = yV; func_interp* fi = alloc(func_interp, m, 2); - expr_ref pred(m.mk_app(connectedf, m.mk_app(cons, x, m.mk_const(nil)), y, m.mk_const(nil)), m); + expr_ref consx(m.mk_app(cons, x, nilc), m); + expr_ref pred(m.mk_app(connectedf, consx, y, consx), m); if (is_reflexive) { pred = m.mk_or(pred, m.mk_eq(x, y)); } fi->set_else(pred); mg.get_model().register_decl(r.decl(), fi); - } - -#else - sort_ref tup(dt.mk_pair_datatype(listS, m.mk_bool_sort(), fst, snd, pair), m); - sort* dom1[5] = { s, s, listS, s, s }; - recfun::promise_def c1 = p.ensure_def(symbol("connected1"), 5, dom1, tup); - sort* dom2[3] = { s, s, listS }; - recfun::promise_def c2 = p.ensure_def(symbol("connected2"), 3, dom2, tup); - - func_decl* conn1 = c1.get_def()->get_decl(); - func_decl* conn2 = c2.get_def()->get_decl(); - - var_ref xV(m.mk_var(4, s), m); - var_ref yV(m.mk_var(3, s), m); - var_ref SV(m.mk_var(2, listS), m); - var_ref vV(m.mk_var(1, s), m); - var_ref wV(m.mk_var(0, s), m); - expr* y = yV, *v = vV, *w = wV; - expr* x = xV, *S = SV; - - expr_ref ST(m.mk_app(pair, S, T), m); - expr_ref SF(m.mk_app(pair, S, F), m); - - expr_ref connected_body(m); - connected_body = - m.mk_ite(m.mk_not(m.mk_eq(x, v)), - SF, - m.mk_ite(m.mk_eq(y, w), - ST, - m.mk_ite(m.mk_app(memf, w, S), - SF, - m.mk_app(conn2, w, y, m.mk_app(cons, w, S))))); - { - var* vars2[5] = { xV, yV, SV, vV, wV }; - recfun_replace rep(m); - p.set_definition(rep, c1, 5, vars2, connected_body); - } - - xV = m.mk_var(2, s); - yV = m.mk_var(1, s); - SV = m.mk_var(0, listS); - x = xV, y = yV, S = SV; - ST = m.mk_app(pair, S, T); - SF = m.mk_app(pair, S, F); - expr_ref connected_rec_body(m); - connected_rec_body = SF; - - for (atom* ap : r.m_asserted_atoms) { - atom& a = *ap; - if (!a.phase()) continue; - SASSERT(get_context().get_assignment(a.var()) == l_true); - expr* n1 = get_enode(a.v1())->get_root()->get_owner(); - expr* n2 = get_enode(a.v2())->get_root()->get_owner(); - expr* Sr = connected_rec_body; - expr* args[5] = { x, y, m.mk_app(fst, Sr), n1, n2}; - expr* Sc = m.mk_app(conn1, 5, args); - connected_rec_body = m.mk_ite(m.mk_app(snd, Sr), ST, Sc); - } - { - var* vars3[3] = { xV, yV, SV }; - recfun_replace rep(m); - p.set_definition(rep, c2, 3, vars3, connected_rec_body); - } - - // r.m_decl(x,y) -> snd(connected2(x,y,nil)) - xV = m.mk_var(0, s); - yV = m.mk_var(1, s); - x = xV, y = yV; - - func_interp* fi = alloc(func_interp, m, 2); - expr_ref pred(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_app(cons, y, m.mk_const(nil)))), m); - if (is_reflexive) { - pred = m.mk_or(pred, m.mk_eq(x, y)); - } - fi->set_else(pred); - mg.get_model().register_decl(r.decl(), fi); - -#endif - + } } /** @@ -1208,10 +1145,6 @@ Take 2: } } - bool theory_special_relations::has_quantifiers() { - return get_context().has_quantifiers(); - } - void theory_special_relations::init_model(model_generator & m) { for (auto const& kv : m_relations) { switch (kv.m_value->m_property) { @@ -1228,16 +1161,10 @@ Take 2: init_model_po(*kv.m_value, m, true); break; case sr_tc: - if (has_quantifiers()) { - // model construction for transitive relation is reserved for quantified formulas where - // TC(R) may be needed to perform MBQI - init_model_po(*kv.m_value, m, true); - } + init_model_po(*kv.m_value, m, true); break; case sr_trc: - if (has_quantifiers()) { - init_model_po(*kv.m_value, m, true); - } + init_model_po(*kv.m_value, m, true); break; default: // other 28 combinations of 0x1F diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 0f69bc1d9..fd88cc456 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -92,6 +92,8 @@ namespace smt { typedef union_find union_find_t; struct relation { + ast_manager& m; + func_decl_ref m_next; sr_property m_property; func_decl* m_decl; atoms m_asserted_atoms; // set of asserted atoms @@ -102,9 +104,14 @@ namespace smt { union_find_t m_uf; literal_vector m_explanation; - relation(sr_property p, func_decl* d): m_property(p), m_decl(d), m_asserted_qhead(0), m_uf(m_ufctx) {} + relation(sr_property p, func_decl* d, ast_manager& m): m(m), m_next(m), m_property(p), m_decl(d), m_asserted_qhead(0), m_uf(m_ufctx) {} func_decl* decl() { return m_decl; } + + app_ref next(expr* a, expr* b) { return app_ref(m.mk_app(next(), a, b), m); } + bool is_next(expr* n) { return is_app(n) && next() == to_app(n)->get_decl(); } + func_decl* next(); + void push(); void pop(unsigned num_scopes); void ensure_var(theory_var v); @@ -172,7 +179,7 @@ namespace smt { void collect_asserted_po_atoms(vector< std::pair >& atoms) const; void display_atom(std::ostream & out, atom& a) const; - bool has_quantifiers(); + void internalize_next(func_decl* f, app * term); public: theory_special_relations(ast_manager& m); diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index c5cb0c319..f407120cf 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -222,10 +222,8 @@ public: */ template void reset_dealloc_values(obj_map & m) { - typename obj_map::iterator it = m.begin(); - typename obj_map::iterator end = m.end(); - for (; it != end; ++it) { - dealloc(it->m_value); + for (auto & kv : m) { + dealloc(kv.m_value); } m.reset(); }