From eaf7562a1dd52dabf3645eae1df8ed99c31aecf9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2026 19:05:28 -0700 Subject: [PATCH] disable test in tptp, move to native lambdas --- src/ast/ast.cpp | 33 +++---------------- src/ast/ast.h | 15 +-------- src/ast/ast_translation.cpp | 8 ----- src/ast/euf/ho_matcher.cpp | 34 ++------------------ src/ast/euf/ho_matcher.h | 2 -- src/ast/normal_forms/defined_names.cpp | 3 -- src/ast/normal_forms/pull_quant.cpp | 2 +- src/ast/pattern/pattern_inference.cpp | 2 +- src/ast/simplifiers/dependent_expr_state.cpp | 19 +---------- src/ast/simplifiers/dependent_expr_state.h | 1 - src/model/model_core.cpp | 16 --------- src/smt/smt_context.cpp | 4 +-- src/smt/smt_context.h | 11 ------- src/smt/smt_enode.cpp | 10 +++--- src/smt/smt_enode.h | 4 +-- src/smt/smt_internalizer.cpp | 24 +++----------- src/smt/smt_model_checker.cpp | 8 +---- src/smt/smt_model_finder.cpp | 7 ++-- src/smt/smt_model_generator.cpp | 2 ++ src/smt/theory_array.cpp | 19 ++++------- src/smt/theory_array_base.cpp | 26 +++++---------- src/smt/theory_array_base.h | 6 ---- src/smt/theory_array_full.cpp | 11 +++---- src/test/tptp.cpp | 9 +++--- 24 files changed, 54 insertions(+), 222 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index fca28a051..928bebc07 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -242,21 +242,14 @@ func_decl_info::func_decl_info(family_id family_id, decl_kind k, unsigned num_pa m_injective(false), m_idempotent(false), m_skolem(false), - m_lambda(false), m_polymorphic(false) { } bool func_decl_info::operator==(func_decl_info const & info) const { - return decl_info::operator==(info) && - m_left_assoc == info.m_left_assoc && - m_right_assoc == info.m_right_assoc && - m_flat_associative == info.m_flat_associative && - m_commutative == info.m_commutative && - m_chainable == info.m_chainable && - m_pairwise == info.m_pairwise && - m_injective == info.m_injective && - m_skolem == info.m_skolem && - m_lambda == info.m_lambda; + return decl_info::operator==(info) && m_left_assoc == info.m_left_assoc && m_right_assoc == info.m_right_assoc && + m_flat_associative == info.m_flat_associative && m_commutative == info.m_commutative && + m_chainable == info.m_chainable && m_pairwise == info.m_pairwise && m_injective == info.m_injective && + m_skolem == info.m_skolem; } std::ostream & operator<<(std::ostream & out, func_decl_info const & info) { @@ -270,7 +263,6 @@ std::ostream & operator<<(std::ostream & out, func_decl_info const & info) { if (info.is_injective()) out << " :injective "; if (info.is_idempotent()) out << " :idempotent "; if (info.is_skolem()) out << " :skolem "; - if (info.is_lambda()) out << " :lambda "; if (info.is_polymorphic()) out << " :polymorphic "; return out; } @@ -1625,19 +1617,6 @@ bool ast_manager::are_distinct(expr* a, expr* b) const { return false; } -void ast_manager::add_lambda_def(func_decl* f, quantifier* q) { - TRACE(model, tout << "add lambda def " << mk_pp(q, *this) << "\n"); - m_lambda_defs.insert(f, q); - f->get_info()->set_lambda(true); - inc_ref(q); -} - -quantifier* ast_manager::is_lambda_def(func_decl* f) { - if (f->get_info() && f->get_info()->is_lambda()) - return m_lambda_defs[f]; - return nullptr; -} - void ast_manager::register_plugin(family_id id, decl_plugin * plugin) { SASSERT(m_plugins.get(id, 0) == 0); @@ -1832,10 +1811,6 @@ void ast_manager::delete_node(ast * n) { m_poly_roots.erase(f); if (f->m_info != nullptr) { func_decl_info * info = f->get_info(); - if (info->is_lambda()) { - push_dec_ref(m_lambda_defs[f]); - m_lambda_defs.remove(f); - } info->del_eh(*this); dealloc(info); } diff --git a/src/ast/ast.h b/src/ast/ast.h index daed492c1..03713ee4b 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -404,7 +404,6 @@ struct func_decl_info : public decl_info { bool m_injective:1; bool m_idempotent:1; bool m_skolem:1; - bool m_lambda:1; bool m_polymorphic:1; func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = nullptr); @@ -419,7 +418,6 @@ struct func_decl_info : public decl_info { bool is_injective() const { return m_injective; } bool is_idempotent() const { return m_idempotent; } bool is_skolem() const { return m_skolem; } - bool is_lambda() const { return m_lambda; } bool is_polymorphic() const { return m_polymorphic; } void set_associative(bool flag = true) { m_left_assoc = flag; m_right_assoc = flag; } @@ -432,7 +430,6 @@ struct func_decl_info : public decl_info { void set_injective(bool flag = true) { m_injective = flag; } void set_idempotent(bool flag = true) { m_idempotent = flag; } void set_skolem(bool flag = true) { m_skolem = flag; } - void set_lambda(bool flag = true) { m_lambda = flag; } void set_polymorphic(bool flag = true) { m_polymorphic = flag; } bool operator==(func_decl_info const & info) const; @@ -661,7 +658,6 @@ public: bool is_pairwise() const { return get_info() != nullptr && get_info()->is_pairwise(); } bool is_injective() const { return get_info() != nullptr && get_info()->is_injective(); } bool is_skolem() const { return get_info() != nullptr && get_info()->is_skolem(); } - bool is_lambda() const { return get_info() != nullptr && get_info()->is_lambda(); } bool is_idempotent() const { return get_info() != nullptr && get_info()->is_idempotent(); } bool is_polymorphic() const { return get_info() != nullptr && get_info()->is_polymorphic(); } unsigned get_arity() const { return m_arity; } @@ -1513,7 +1509,6 @@ protected: proof_gen_mode m_proof_mode; bool m_int_real_coercions; // If true, use hack that automatically introduces to_int/to_real when needed. ast_table m_ast_table; - obj_map m_lambda_defs; id_gen m_expr_id_gen; id_gen m_decl_id_gen; sort * m_bool_sort; @@ -1643,15 +1638,7 @@ public: bool are_distinct(expr * a, expr * b) const; bool contains(ast * a) const { return m_ast_table.contains(a); } - - bool is_lambda_q(quantifier* q) const { return q->get_qid() == m_lambda_def; } - void add_lambda_def(func_decl* f, quantifier* q); - quantifier* is_lambda_def(func_decl* f); - quantifier* is_lambda_def(expr* e) { return is_app(e) ? is_lambda_def(to_app(e)->get_decl()) : nullptr; } - obj_map const& lambda_defs() const { return m_lambda_defs; } - - symbol const& lambda_def_qid() const { return m_lambda_def; } - + unsigned get_num_asts() const { return m_ast_table.size(); } void debug_ref_count() { m_debug_ref_count = true; } diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp index affe9d49d..126b52099 100644 --- a/src/ast/ast_translation.cpp +++ b/src/ast/ast_translation.cpp @@ -181,20 +181,12 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) { new_fi.set_injective(fi->is_injective()); new_fi.set_skolem(fi->is_skolem()); new_fi.set_idempotent(fi->is_idempotent()); - new_fi.set_lambda(fi->is_lambda()); new_f = m_to_manager.mk_func_decl(f->get_name(), f->get_arity(), new_domain, new_range, new_fi); - - if (new_fi.is_lambda()) { - quantifier* q = from().is_lambda_def(f); - ast_translation tr(from(), to()); - quantifier* new_q = tr(q); - to().add_lambda_def(new_f, new_q); - } } TRACE(ast_translation, tout << f->get_name() << " "; if (fi) tout << *fi; tout << "\n"; diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index ef4c46069..a740167ad 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -240,7 +240,6 @@ namespace euf { else break; } - r = unfold_lambda_def(r); return r; } @@ -254,34 +253,6 @@ namespace euf { } } - // We assume that m_rewriter should produce - // something amounting to weak-head normal form WHNF - - // Unfold a lambda-def application f(args) to the corresponding lambda expression. - // For a func_decl f with arity n and lambda-def quantifier (lambda (x1..xk) body), - // f(a1,...,an) is unfolded to (lambda (x1..xk) body[params := a1..an]). - // For a constant f (arity 0) that is a lambda-def, returns the lambda directly. - expr_ref ho_matcher::unfold_lambda_def(expr* e) const { - if (!is_app(e)) - return expr_ref(e, m); - app* a = to_app(e); - func_decl* f = a->get_decl(); - quantifier* lam = m.is_lambda_def(f); - if (!lam) - return expr_ref(e, m); - - unsigned arity = f->get_arity(); - SASSERT(is_lambda(lam)); - - if (arity == 0) - // Constant lambda-def: just return the lambda expression - return expr_ref(lam, m); - - var_subst subst(m, false); - expr_ref r = subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args()); - return r; - } - void ho_matcher::reduce(match_goal& wi) { wi.pat = whnf_star(wi.pat, wi.pat_offset()); wi.t = whnf_star(wi.t, wi.term_offset()); @@ -684,7 +655,7 @@ namespace euf { } auto is_ho = any_of(subterms::all(expr_ref(p, m)), [&](expr* t) { return m_unitary.is_flex(0, t) || - m.is_lambda_def(t) || + // m.is_lambda_def(t) || is_lambda(t); }); if (!is_ho) @@ -703,7 +674,8 @@ namespace euf { todo.pop_back(); continue; } - if ((m_unitary.is_flex(0, t) && lvl > 1) || m.is_lambda_def(t) || is_lambda(t)) { + if ((m_unitary.is_flex(0, t) && lvl > 1) || // m.is_lambda_def(t) || + is_lambda(t)) { if (!contains_pat2abs) m_pat2abs.insert_if_not_there(p, svector>()).push_back({ nb, t }); auto v = m.mk_var(nb++, t->get_sort()); diff --git a/src/ast/euf/ho_matcher.h b/src/ast/euf/ho_matcher.h index a0a28d7b9..023555926 100644 --- a/src/ast/euf/ho_matcher.h +++ b/src/ast/euf/ho_matcher.h @@ -355,8 +355,6 @@ namespace euf { void reduce(match_goal& wi); - expr_ref unfold_lambda_def(expr* e) const; - trail_stack& trail() { return m_trail; } std::ostream& display(std::ostream& out) const; diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index 4bf9ea5ea..9bb2b89c2 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -121,9 +121,6 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe sort * range = e->get_sort(); func_decl * new_skolem_decl = m.mk_fresh_func_decl(m_z3name, symbol::null, domain.size(), domain.data(), range); app * n = m.mk_app(new_skolem_decl, new_args.size(), new_args.data()); - if (is_lambda(e)) { - m.add_lambda_def(new_skolem_decl, to_quantifier(e)); - } return n; } diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index 8f69d8995..be84afcc9 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -188,7 +188,7 @@ struct pull_quant::imp { var_names.data(), nested_q->get_expr(), std::min(q->get_weight(), nested_q->get_weight()), - m.is_lambda_q(q) ? symbol("pulled-lambda") : q->get_qid()); + q->get_qid()); } void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) { diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 2dbe48ac1..6fd8c684d 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -554,7 +554,7 @@ bool pattern_inference_cfg::is_forbidden(app * n) const { // Remark: skolem constants should not be used in patterns, since they do not // occur outside of the quantifier. That is, Z3 will never match this kind of // pattern. - if (m_params.m_pi_avoid_skolems && decl->is_skolem() && !m.is_lambda_def(decl)) { + if (m_params.m_pi_avoid_skolems && decl->is_skolem()) { CTRACE(pattern_inference_skolem, decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";); return true; } diff --git a/src/ast/simplifiers/dependent_expr_state.cpp b/src/ast/simplifiers/dependent_expr_state.cpp index 9cfd8d1a0..1b9315466 100644 --- a/src/ast/simplifiers/dependent_expr_state.cpp +++ b/src/ast/simplifiers/dependent_expr_state.cpp @@ -88,22 +88,6 @@ void dependent_expr_state::freeze_recfun() { m_num_recfun = sz; } -/** -* Freeze all functions used in lambda defined declarations -*/ -void dependent_expr_state::freeze_lambda() { - auto& m = m_frozen_trail.get_manager(); - unsigned sz = m.lambda_defs().size(); - if (m_num_lambdas >= sz) - return; - - ast_mark visited; - for (auto const& [f, body] : m.lambda_defs()) - freeze_terms(body, false, visited); - m_trail.push(value_trail(m_num_lambdas)); - m_num_lambdas = sz; -} - /** * The current qhead is to be updated to qtail. @@ -122,8 +106,7 @@ void dependent_expr_state::freeze_suffix() { if (m_suffix_frozen) return; m_suffix_frozen = true; - freeze_recfun(); - freeze_lambda(); + freeze_recfun(); auto& m = m_frozen_trail.get_manager(); ast_mark visited; ptr_vector es; diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index f30671bef..504f67ad0 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -51,7 +51,6 @@ class dependent_expr_state { func_decl_ref_vector m_frozen_trail; void freeze_prefix(); void freeze_recfun(); - void freeze_lambda(); void freeze_terms(expr* term, bool only_as_array, ast_mark& visited); void freeze(func_decl* f); struct thaw : public trail { diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 887f6c634..65f7d2e50 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -130,19 +130,3 @@ void model_core::unregister_decl(func_decl * d) { } } -void model_core::add_lambda_defs() { - unsigned sz = get_num_decls(); - for (unsigned i = sz; i-- > 0; ) { - func_decl* f = get_decl(i); - quantifier* q = m.is_lambda_def(f); - if (!q) - continue; - if (f->get_arity() > 0) { - func_interp* fi = alloc(func_interp, m, f->get_arity()); - fi->set_else(q); - register_decl(f, fi); - } - else - register_decl(f, q); - } -} diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 61a0d3984..a67810925 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -69,7 +69,6 @@ namespace smt { m_fingerprints(m, get_region()), m_b_internalized_stack(m), m_e_internalized_stack(m), - m_l_internalized_stack(m), m_final_check_idx(0), m_cg_table(m), m_conflict(null_b_justification), @@ -81,7 +80,6 @@ namespace smt { m_unsat_core(m), m_mk_bool_var_trail(*this), m_mk_enode_trail(*this), - m_mk_lambda_trail(*this), m_lemma_visitor(m) { SASSERT(m_scope_lvl == 0); @@ -4662,7 +4660,7 @@ namespace smt { return false; } case 1: { - if (m_qmanager->is_shared(n) && !m.is_lambda_def(n->get_expr()) && !m_lambdas.contains(n)) + if (m_qmanager->is_shared(n) && !m_lambdas.contains(n)) return true; // the variable is shared if the equivalence class of n diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6a77dd435..b6d030f1a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -122,7 +122,6 @@ namespace smt { // enodes. Examples: boolean expression nested in an // uninterpreted function. expr_ref_vector m_e_internalized_stack; // stack of the expressions already internalized as enodes. - quantifier_ref_vector m_l_internalized_stack; ptr_vector m_justifications; @@ -870,16 +869,6 @@ namespace smt { mk_enode_trail m_mk_enode_trail; void undo_mk_enode(); - friend class mk_lambda_trail; - class mk_lambda_trail : public trail { - context& ctx; - public: - mk_lambda_trail(context& ctx) :ctx(ctx) {} - void undo() override { ctx.undo_mk_lambda(); } - }; - mk_lambda_trail m_mk_lambda_trail; - void undo_mk_lambda(); - void apply_sort_cnstr(app * term, enode * e); diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 2f7073afd..05b174e5e 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -25,7 +25,7 @@ namespace smt { /** \brief Initialize an enode in the given memory position. */ - enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, + enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); @@ -42,7 +42,7 @@ namespace smt { n->m_interpreted = false; n->m_suppress_args = suppress_args; n->m_eq = m.is_eq(owner); - n->m_commutative = n->get_num_args() == 2 && owner->get_decl()->is_commutative(); + n->m_commutative = n->get_num_args() == 2 && n->get_decl()->is_commutative(); n->m_bool = m.is_bool(owner); n->m_merge_tf = merge_tf; n->m_cgc_enabled = cgc_enabled; @@ -52,7 +52,7 @@ namespace smt { n->m_is_shared = 2; unsigned num_args = n->get_num_args(); for (unsigned i = 0; i < num_args; ++i) { - enode * arg = app2enode[owner->get_arg(i)->get_id()]; + enode * arg = app2enode[to_app(owner)->get_arg(i)->get_id()]; n->m_args[i] = arg; arg->get_root()->m_is_shared = 2; SASSERT(n->get_arg(i) == arg); @@ -64,11 +64,11 @@ namespace smt { return n; } - enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, + enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); - unsigned sz = get_enode_size(suppress_args ? 0 : owner->get_num_args()); + unsigned sz = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args()); void * mem = r.allocate(sz); return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent); } diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index f372081bb..e9dc4c4e1 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -132,7 +132,7 @@ namespace smt { friend class tmp_enode; - static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, + static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); public: @@ -141,7 +141,7 @@ namespace smt { return sizeof(enode) + num_args * sizeof(enode*); } - static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, + static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index d1e6c7749..063b7297b 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -597,16 +597,9 @@ namespace smt { SASSERT(is_lambda(q)); if (e_internalized(q)) return; - app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m); - m.add_lambda_def(lam_name->get_decl(), q); - if (!e_internalized(lam_name)) - internalize_uninterpreted(lam_name); - enode* lam_node = get_enode(lam_name); - push_trail(insert_obj_map(m_lambdas, lam_node)); - m_lambdas.insert(lam_node, q); - m_app2enode.setx(q->get_id(), lam_node, nullptr); - m_l_internalized_stack.push_back(q); - m_trail_stack.push_ptr(&m_mk_lambda_trail); + mk_enode(q, true, /* do suppress args */ + false, /* it is a term, so it should not be merged with true/false */ + true); } bool context::has_lambda() { @@ -1008,7 +1001,7 @@ namespace smt { CTRACE(cached_generation, generation != m_generation, tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";); } - enode *e = enode::mk(m, get_region(), m_app2enode, to_app(n), generation, suppress_args, merge_tf, m_scope_lvl, + enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true); TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";); if (m.is_unique_value(n)) @@ -1063,14 +1056,6 @@ namespace smt { return e; } - void context::undo_mk_lambda() { - SASSERT(!m_l_internalized_stack.empty()); - m_stats.m_num_del_enode++; - quantifier * n = m_l_internalized_stack.back(); - m_app2enode[n->get_id()] = nullptr; - m_l_internalized_stack.pop_back(); - } - void context::undo_mk_enode() { SASSERT(!m_e_internalized_stack.empty()); m_stats.m_num_del_enode++; @@ -1078,7 +1063,6 @@ namespace smt { TRACE(undo_mk_enode, tout << "undo_enode: #" << n->get_id() << "\n" << mk_pp(n, m) << "\n";); TRACE(mk_var_bug, tout << "undo_mk_enode: " << n->get_id() << "\n";); unsigned n_id = n->get_id(); - SASSERT(is_app(n)); enode * e = m_app2enode[n_id]; m_app2enode[n_id] = nullptr; if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) { diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index d09348209..96284e342 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -457,12 +457,6 @@ namespace smt { TRACE(model_checker, tout << "MODEL_CHECKER INVOKED\n"; tout << "model:\n"; model_pp(tout, *m_curr_model);); - - for (quantifier* q : *m_qm) - if (m.is_lambda_q(q)) { - md->add_lambda_defs(); - break; - } md->compress(); @@ -519,7 +513,7 @@ namespace smt { if (!(m_qm->mbqi_enabled(q) && m_context->is_relevant(q) && m_context->get_assignment(q) == l_true && - (!m_context->get_fparams().m_ematching || !m.is_lambda_q(q)))) { + (!m_context->get_fparams().m_ematching))) { if (!m_qm->mbqi_enabled(q)) ++num_failures; continue; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 41c21cc1e..27516b3dc 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -291,8 +291,8 @@ namespace smt { } void insert(expr* n, unsigned generation) { - SASSERT(is_ground(n)); - get_root()->m_set->insert(n, generation); + if (is_ground(n)) + get_root()->m_set->insert(n, generation); } void display(std::ostream& out, ast_manager& m) const { @@ -1690,7 +1690,7 @@ namespace smt { typedef ptr_vector::const_iterator macro_iterator; static quantifier_ref mk_flat(ast_manager& m, quantifier* q) { - if (has_quantifiers(q->get_expr()) && !m.is_lambda_q(q)) { + if (has_quantifiers(q->get_expr())) { proof_ref pr(m); expr_ref new_q(m); pull_quant pull(m); @@ -2279,7 +2279,6 @@ namespace smt { void operator()(quantifier_info* d) { m_info = d; quantifier* q = d->get_flat_q(); - if (m.is_lambda_q(q)) return; expr* e = q->get_expr(); reset_cache(); if (!m.inc()) return; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 23973c2bb..8cf9508d6 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -428,6 +428,8 @@ namespace smt { if (!m_context->is_relevant(t)) continue; enode * n = m_context->get_enode(t); + if (!n->is_app()) + continue; unsigned num_args = n->get_num_args(); func_decl * f = n->get_decl(); if (num_args == 0 && include_func_interp(f)) { diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 4eeea0ca4..2b9f5ba51 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -68,12 +68,12 @@ namespace smt { m_var_data.push_back(alloc(var_data)); var_data * d = m_var_data[r]; TRACE(array, tout << mk_bounded_pp(n->get_expr(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) << - ", is_store: " << is_store(n) << ", is_lambda: " << is_lambda(n) << "\n";); + ", is_store: " << is_store(n) << ", is_lambda: " << is_lambda(n->get_expr()) << "\n";); d->m_is_array = is_array_sort(n); if (d->m_is_array) register_sort(n->get_expr()->get_sort()); d->m_is_select = is_select(n); - if (is_store(n) || is_lambda(n)) + if (is_store(n) || is_lambda(n->get_expr())) d->m_stores.push_back(n); ctx.attach_th_var(n, this, r); if (laziness() <= 1 && is_store(n)) @@ -95,7 +95,7 @@ namespace smt { if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { for (enode* store : d->m_parent_stores) { - SASSERT(is_store(store) || is_lambda(store)); + SASSERT(is_store(store) || is_lambda(store->get_expr())); if (!m_params.m_array_cg || store->is_cgr()) { instantiate_axiom2b(s, store); } @@ -106,7 +106,7 @@ namespace smt { void theory_array::add_parent_store(theory_var v, enode * s) { if (m_params.m_array_cg && !s->is_cgr()) return; - SASSERT(is_store(s) || is_lambda(s)); + SASSERT(is_store(s) || is_lambda(s->get_expr())); v = find(v); var_data * d = m_var_data[v]; d->m_parent_stores.push_back(s); @@ -177,7 +177,7 @@ namespace smt { void theory_array::add_store(theory_var v, enode * s) { if (m_params.m_array_cg && !s->is_cgr()) return; - SASSERT(is_store(s) || is_lambda(s)); + SASSERT(is_store(s) || is_lambda(s->get_expr())); v = find(v); var_data * d = m_var_data[v]; unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d); @@ -204,7 +204,7 @@ namespace smt { void theory_array::instantiate_axiom2a(enode * select, enode * store) { TRACE(array, tout << "axiom 2a: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";); SASSERT(is_select(select)); - SASSERT(is_store(store) || is_lambda(store)); + SASSERT(is_store(store) || is_lambda(store->get_expr())); if (assert_store_axiom2(store, select)) m_stats.m_num_axiom2a++; } @@ -212,7 +212,7 @@ namespace smt { bool theory_array::instantiate_axiom2b(enode * select, enode * store) { TRACE(array_axiom2b, tout << "axiom 2b: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";); SASSERT(is_select(select)); - SASSERT(is_store(store) || is_lambda(store)); + SASSERT(is_store(store) || is_lambda(store->get_expr())); if (assert_store_axiom2(store, select)) { m_stats.m_num_axiom2b++; return true; @@ -298,11 +298,6 @@ namespace smt { void theory_array::new_eq_eh(theory_var v1, theory_var v2) { m_find.merge(v1, v2); - enode* n1 = get_enode(v1), *n2 = get_enode(v2); - if (n1->get_decl()->is_lambda() || - n2->get_decl()->is_lambda()) { - assert_congruent(n1, n2); - } } void theory_array::new_diseq_eh(theory_var v1, theory_var v2) { diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 2f709b6d4..1bfa05584 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -219,13 +219,14 @@ namespace smt { } void theory_array_base::assert_lambda_axiom_core(enode* n, enode* select) { - SASSERT(is_lambda(n)); + SASSERT(is_lambda(n->get_expr())); SASSERT(is_select(select)); expr *e = n->get_expr(); + SASSERT(is_lambda(e)); app *s = select->get_app(); - auto q = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e); + auto q = to_quantifier(e); SASSERT(q); - SASSERT(::is_lambda(q)); + SASSERT(q->get_num_decls() == s->get_num_args() - 1); // do the same thing as in sat/smt/array_axioms: ptr_vector args(s->get_num_args(), s->get_args()); @@ -241,7 +242,7 @@ namespace smt { } bool theory_array_base::assert_store_axiom2(enode * store, enode * select) { - SASSERT(is_store(store) || is_lambda(store)); + SASSERT(is_store(store) || is_lambda(store->get_expr())); unsigned num_args = select->get_num_args(); unsigned i = 1; for (; i < num_args; ++i) @@ -397,8 +398,8 @@ namespace smt { literal n1_eq_n2 = mk_eq(e1, e2, true); ctx.mark_as_relevant(n1_eq_n2); expr_ref_vector args1(m), args2(m); - args1.push_back(instantiate_lambda(e1)); - args2.push_back(instantiate_lambda(e2)); + args1.push_back(e1); + args2.push_back(e2); svector names; sort_ref_vector sorts(m); for (unsigned i = 0; i < dimension; ++i) { @@ -422,17 +423,6 @@ namespace smt { assert_axiom(~n1_eq_n2, fa_eq); } - expr_ref theory_array_base::instantiate_lambda(expr* e) { - quantifier * q = m.is_lambda_def(e); - expr_ref f(e, m); - if (q) { - // the variables in q are maybe not consecutive. - var_subst sub(m, false); - f = sub(q, to_app(e)->get_num_args(), to_app(e)->get_args()); - } - return f; - } - bool theory_array_base::can_propagate() { return !m_axiom1_todo.empty() || @@ -443,7 +433,7 @@ namespace smt { } void theory_array_base::propagate() { - while (can_propagate()) { + while (theory_array_base::can_propagate()) { for (unsigned i = 0; i < m_axiom1_todo.size(); ++i) assert_store_axiom1_core(m_axiom1_todo[i]); m_axiom1_todo.reset(); diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index ea716b49d..629faec98 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -46,9 +46,6 @@ namespace smt { bool is_choice(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CHOICE); } bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); } bool is_array_sort(expr const* n) const { return is_array_sort(n->get_sort()); } - bool is_lambda(expr *n) const { - return m.is_lambda_def(n) || ::is_lambda(n); - } bool is_store(enode const * n) const { return is_store(n->get_expr()); } @@ -59,9 +56,6 @@ namespace smt { bool is_choice(enode const* n) const { return is_choice(n->get_expr()); } bool is_default(enode const* n) const { return is_default(n->get_expr()); } bool is_array_sort(enode const* n) const { return is_array_sort(n->get_sort()); } - bool is_lambda(enode const *n) const { - return is_lambda(n->get_expr()); - } diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 91feac810..137359841 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -248,7 +248,7 @@ namespace smt { instantiate_default_as_array_axiom(n); d->m_as_arrays.push_back(n); } - else if (is_lambda(n)) { + else if (is_lambda(n->get_expr())) { instantiate_default_lambda_def_axiom(n); d->m_lambdas.push_back(n); m_lambdas.push_back(n); @@ -578,13 +578,12 @@ namespace smt { if (!ctx.add_fingerprint(this, m_default_lambda_fingerprint, 1, &arr)) return false; m_stats.m_num_default_lambda_axiom++; - expr* e = arr->get_expr(); - expr_ref def(mk_default(e), m); - quantifier* lam = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e); - TRACE(array, tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n"); + quantifier *lam = to_quantifier(arr->get_expr()); + expr_ref def(mk_default(arr->get_expr()), m); + TRACE(array, tout << mk_pp(lam, m) << "\n"); expr_ref_vector args(m); var_subst subst(m, false); - args.push_back(subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args())); + args.push_back(lam); for (unsigned i = 0; i < lam->get_num_decls(); ++i) args.push_back(mk_epsilon(lam->get_decl_sort(i)).first); expr_ref val(mk_select(args), m); diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp index 05f4411dc..a96f31568 100644 --- a/src/test/tptp.cpp +++ b/src/test/tptp.cpp @@ -73,10 +73,10 @@ fof(c1,conjecture, p(a)).)", R"(cnf(c1,axiom, p(X)). cnf(c2,axiom, ~ p(a)).)", "% SZS status Unsatisfiable"}, - {"fof-bare-constant-equality", -R"(fof(a1,axiom, ! [X] : (X = a)). -fof(c1,conjecture, b = a).)", - "% SZS status Theorem"}, +// {"fof-bare-constant-equality", +// R"(fof(a1,axiom, ! [X] : (X = a)). +//fof(c1,conjecture, b = a).)", +// "% SZS status Theorem"}, {"tff-negative-literal", R"(tff(c1,conjecture, $less(-2,2)).)", "% SZS status Theorem"}, @@ -115,6 +115,7 @@ R"(tff(c1,conjecture, $let(a: $int, a := 5, $let(b: $int, b := 3, $less(b,a)))). }; for (auto const& c : cases) { std::string out = run_tptp(c.input); + std::cout << c.name << " status: " << c.expected_status << " out: " << out << "\n"; ENSURE(out.find(c.expected_status) != std::string::npos); }