mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-04 16:10:50 +00:00
Code Activity

disable test in tptp, move to native lambdas

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-01 19:05:28 -07:00
parent 3e0a350411
commit eaf7562a1d
24 changed files with 54 additions and 222 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/ast/ast.cpp
View file

@ -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);
}

15
src/ast/ast.h
View file

@ -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<func_decl, quantifier*> 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<func_decl, quantifier*> 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; }

8
src/ast/ast_translation.cpp
View file

@ -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";

34
src/ast/euf/ho_matcher.cpp
View file

@ -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<std::pair<unsigned, expr*>>()).push_back({ nb, t });
auto v = m.mk_var(nb++, t->get_sort());

2
src/ast/euf/ho_matcher.h
View file

@ -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;

3
src/ast/normal_forms/defined_names.cpp
View file

@ -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;
}

2
src/ast/normal_forms/pull_quant.cpp
View file

@ -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) {

2
src/ast/pattern/pattern_inference.cpp
View file

@ -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;
}

19
src/ast/simplifiers/dependent_expr_state.cpp
View file

@ -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<expr> es;

1
src/ast/simplifiers/dependent_expr_state.h
View file

@ -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 {

16
src/model/model_core.cpp
View file

@ -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);
}
}

4
src/smt/smt_context.cpp
View file

@ -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

11
src/smt/smt_context.h
View file

@ -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<justification> 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);

10
src/smt/smt_enode.cpp
View file

@ -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);
}

4
src/smt/smt_enode.h
View file

@ -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);

24
src/smt/smt_internalizer.cpp
View file

@ -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<enode, quantifier*>(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()) {

8
src/smt/smt_model_checker.cpp
View file

@ -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;

7
src/smt/smt_model_finder.cpp
View file

@ -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<cond_macro>::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;

2
src/smt/smt_model_generator.cpp
View file

@ -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)) {

19
src/smt/theory_array.cpp
View file

@ -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) {

26
src/smt/theory_array_base.cpp
View file

@ -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<expr> 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<symbol> 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();

6
src/smt/theory_array_base.h
View file

@ -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());
}

11
src/smt/theory_array_full.cpp
View file

@ -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);

9
src/test/tptp.cpp
View file

@ -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);
}