Skip to content

Commit

Permalink
introduce notion of beta redex to deal with lambdas in non-extensiona…
Browse files Browse the repository at this point in the history 
…l positions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jun 11, 2022
1 parent b9b5377 commit 8efa3c8
Show file tree
Hide file tree
Showing 10 changed files with 65 additions and 51 deletions.
1 change: 1 addition & 0 deletions src/ast/ast.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1677,6 +1677,7 @@ quantifier* ast_manager::is_lambda_def(func_decl* f) {
return nullptr;
}


void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
SASSERT(m_plugins.get(id, 0) == 0);
m_plugins.setx(id, plugin, 0);
Expand Down
2 changes: 1 addition & 1 deletion src/ast/ast.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1618,7 +1618,7 @@ class ast_manager {
bool is_lambda_def(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(app* e) { return is_lambda_def(e->get_decl()); }

symbol const& lambda_def_qid() const { return m_lambda_def; }

Expand Down
24 changes: 14 additions & 10 deletions src/smt/smt_context.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3737,15 +3737,12 @@ namespace smt {

reset_model();

if (m_last_search_failure != OK) {
if (m_last_search_failure != OK)
return false;
}
if (status == l_false) {
if (status == l_false)
return false;
}
if (status == l_true && !m_qmanager->has_quantifiers() && m_lambdas.empty()) {
if (status == l_true && !m_qmanager->has_quantifiers() && !has_lambda())
return false;
}
if (status == l_true && m_qmanager->has_quantifiers()) {
// possible outcomes DONE l_true, DONE l_undef, CONTINUE
mk_proto_model();
Expand All @@ -3766,7 +3763,7 @@ namespace smt {
break;
}
}
if (status == l_true && !m_lambdas.empty()) {
if (status == l_true && has_lambda()) {
m_last_search_failure = LAMBDAS;
status = l_undef;
return false;
Expand Down Expand Up @@ -4010,7 +4007,7 @@ namespace smt {
TRACE("final_check_step", tout << "RESULT final_check: " << result << "\n";);
if (result == FC_GIVEUP && f != OK)
m_last_search_failure = f;
if (result == FC_DONE && !m_lambdas.empty()) {
if (result == FC_DONE && has_lambda()) {
m_last_search_failure = LAMBDAS;
result = FC_GIVEUP;
}
Expand Down Expand Up @@ -4468,9 +4465,8 @@ namespace smt {
return false;
}
case 1: {
if (m_qmanager->is_shared(n)) {
if (m_qmanager->is_shared(n) && !m.is_lambda_def(n->get_expr()) && !m_lambdas.contains(n))
return true;
}

// the variable is shared if the equivalence class of n
// contains a parent application.
Expand All @@ -4482,6 +4478,8 @@ namespace smt {
app* p = parent->get_expr();
family_id fid = p->get_family_id();
if (fid != th_id && fid != m.get_basic_family_id()) {
if (is_beta_redex(parent, n))
continue;
TRACE("is_shared", tout << enode_pp(n, *this)
<< "\nis shared because of:\n"
<< enode_pp(parent, *this) << "\n";);
Expand Down Expand Up @@ -4522,6 +4520,12 @@ namespace smt {
}
}

bool context::is_beta_redex(enode* p, enode* n) const {
family_id th_id = p->get_expr()->get_family_id();
theory * th = get_theory(th_id);
return th && th->is_beta_redex(p, n);
}

bool context::get_value(enode * n, expr_ref & value) {
sort * s = n->get_sort();
family_id fid = s->get_family_id();
Expand Down
9 changes: 6 additions & 3 deletions src/smt/smt_context.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -773,7 +773,12 @@ namespace smt {

void internalize_quantifier(quantifier * q, bool gate_ctx);

obj_hashtable<quantifier> m_lambdas, m_non_lambdas;
obj_map<enode, quantifier*> m_lambdas;

bool has_lambda();

bool is_beta_redex(enode* p, enode* n) const;

void internalize_lambda(quantifier * q);

void internalize_formula_core(app * n, bool gate_ctx);
Expand All @@ -783,8 +788,6 @@ namespace smt {
friend class set_enode_flag_trail;

public:

void add_non_lambda(quantifier* q);

void set_enode_flag(bool_var v, bool is_new_var);

Expand Down
35 changes: 17 additions & 18 deletions src/smt/smt_internalizer.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -578,49 +578,48 @@ namespace smt {
m_qmanager->add(q, generation);
}


void context::internalize_lambda(quantifier * q) {
TRACE("internalize_quantifier", tout << mk_pp(q, m) << "\n";);
SASSERT(is_lambda(q));
if (e_internalized(q)) {
if (e_internalized(q))
return;
}
app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m);
app_ref eq(m), lam_app(m);
expr_ref_vector vars(m);
vars.push_back(lam_name);
unsigned sz = q->get_num_decls();
for (unsigned i = 0; i < sz; ++i) {
for (unsigned i = 0; i < sz; ++i)
vars.push_back(m.mk_var(sz - i - 1, q->get_decl_sort(i)));
}
array_util autil(m);
lam_app = autil.mk_select(vars.size(), vars.data());
eq = m.mk_eq(lam_app, q->get_expr());
quantifier_ref fa(m);
expr * patterns[1] = { m.mk_pattern(lam_app) };
fa = m.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m.lambda_def_qid(), symbol::null, 1, patterns);
internalize_quantifier(fa, true);
if (!e_internalized(lam_name)) internalize_uninterpreted(lam_name);
m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr);
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_back(&m_mk_lambda_trail);
bool_var bv = get_bool_var(fa);
assign(literal(bv, false), nullptr);
mark_as_relevant(bv);
if (m_non_lambdas.contains(q))
return;
push_trail(insert_obj_trail<quantifier>(m_lambdas, q));
m_lambdas.insert(q);
}

void context::add_non_lambda(quantifier* q) {
if (m_non_lambdas.contains(q))
return;
m_non_lambdas.insert(q);
push_trail(insert_obj_trail<quantifier>(m_non_lambdas, q));
if (m_lambdas.contains(q)) {
m_lambdas.remove(q);
push_trail(remove_obj_trail<quantifier>(m_lambdas, q));
bool context::has_lambda() {
for (auto const & [n, q] : m_lambdas) {
if (n->get_class_size() != 1)
return true;
for (enode* p : enode::parents(n))
if (!is_beta_redex(p, n))
return true;
}
return false;
}

/**
Expand Down
7 changes: 7 additions & 0 deletions src/smt/smt_theory.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -321,6 +321,13 @@ namespace smt {
virtual bool is_shared(theory_var v) const {
return false;
}

/**
\brief Determine if node \c n under parent \c p is in a beta redex position.
*/
virtual bool is_beta_redex(enode* p, enode* n) const {
return false;
}

/**
\brief Return true if the theory has something to propagate
Expand Down
9 changes: 9 additions & 0 deletions src/smt/theory_array_base.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -473,6 +473,15 @@ namespace smt {
return false;
}

bool theory_array_base::is_beta_redex(enode* p, enode* n) const {
if (is_select(p))
return p->get_arg(0)->get_root() == n->get_root();
if (is_map(p))
return true;
return false;
}


bool theory_array_base::is_select_arg(enode* r) {
for (enode* n : r->get_parents())
if (is_select(n))
Expand Down
1 change: 1 addition & 0 deletions src/smt/theory_array_base.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,6 +142,7 @@ namespace smt {
//
// --------------------------------------------------
bool is_shared(theory_var v) const override;
bool is_beta_redex(enode* p, enode* n) const override;
void collect_shared_vars(sbuffer<theory_var> & result);
unsigned mk_interface_eqs();

Expand Down
26 changes: 8 additions & 18 deletions src/smt/theory_seq.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1457,8 +1457,6 @@ bool theory_seq::internalize_term(app* term) {
return true;
}

suppress_lambda(term);

if (m.is_bool(term) &&
(m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
bool_var bv = ctx.mk_bool_var(term);
Expand Down Expand Up @@ -1486,26 +1484,18 @@ bool theory_seq::internalize_term(app* term) {
mk_var(e);
if (!ctx.relevancy()) {
relevant_eh(term);
}


}
return true;
}

void theory_seq::suppress_lambda(app* term) {
bool theory_seq::is_beta_redex(enode* p, enode* n) const {
expr* term = p->get_expr();
if (!m_util.str.is_map(term) && !m_util.str.is_mapi(term) &&
!m_util.str.is_foldl(term) && !m_util.str.is_foldli(term))
return;

expr* fn = to_app(term)->get_arg(0);
quantifier* q = nullptr;
if (is_lambda(fn))
q = to_quantifier(fn);
else if (is_app(fn))
q = m.is_lambda_def(to_app(fn)->get_decl());

if (q)
ctx.add_non_lambda(q);
return false;
if (p->get_arg(0)->get_root() == n->get_root())
return true;
return false;
}


Expand Down Expand Up @@ -3292,7 +3282,7 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
k_min *= 2;
if (m_util.is_seq(s_min))
k_min = std::max(m_util.str.min_length(s_min), k_min);
IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << k_min << ")\n");
IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_bounded_pp(s_min, m, 3) << " " << k_min << ")\n");
add_length_limit(s_min, k_min, false);
return true;
}
Expand Down
2 changes: 1 addition & 1 deletion src/smt/theory_seq.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -388,7 +388,6 @@ namespace smt {
bool internalize_atom(app* atom, bool) override;
bool internalize_term(app*) override;
void internalize_eq_eh(app * atom, bool_var v) override;
void suppress_lambda(app* term);
void new_eq_eh(theory_var, theory_var) override;
void new_diseq_eh(theory_var, theory_var) override;
void assign_eh(bool_var v, bool is_true) override;
Expand All @@ -413,6 +412,7 @@ namespace smt {
void finalize_model(model_generator & mg) override;
void init_search_eh() override;
void validate_model(model& mdl) override;
bool is_beta_redex(enode* p, enode* n) const override;

void init_model(expr_ref_vector const& es);
app* get_ite_value(expr* a);
Expand Down

11 comments on commit 8efa3c8

@NikolajBjorner
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This commit introduces a check for whether a sub-term (array, lambda expression) occurs as a beta redex.
When lambdas occur exclusively as beta redexes, we don't have to enforce extensionality nor require the solver to bail with unknown.
It assumes that beta redex expressions are rewritten to equal term that eliminate the redex for satisfiable instances.
For example, for a satisfiable state the term (seq.map fn S) will be equalized to a sequence term T where S and T have the same length such that each element in T at position i is equal to fn applied to the same element in S at position i.
Equality reasoning for extensional arrays is then avoided for beta redexes, and the solver can produce conclusive answers for a class of uses of lambdas.
Handling of beta redexes is not complete in this commit: for example, a lambda that occurs as an argument to a recursively defined function could also be marked as a beta redex. Future updates can address these (and other) missing filters by overriding is_beta_redex in the theory interface.

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This patch has a great impact for Alive2. I'm seeing up to 40% reduction in SMT errors in some benchmarks. The number of UNSATs also goes up.

@NikolajBjorner
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Must be bad: you want Alive to produce SAT (to identify bugs) ;>

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sometimes I sleep better when LLVM is shown to be correct.

@NikolajBjorner
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, if you sleep you don't program. If ou don't program, you don't improve Alive2. If you don't improve Alive2, it will not find bugs.

Can you profile for where it instantiates extensionality axioms? The change adds a filter on unneeded axioms. A question is whether we are missing additional filters. You could validate whether extensionality is instantiated in essential scenarios.

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, I can do that! But after the semester ends. Z3 won't write a software engineering exam for me (yet).

@NikolajBjorner
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Zzzzz3

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It turns out that context::has_lambda() never returns true in my benchmarks. Our lambdas seem to be all too easy for Z3 it seems.
Though we don't use lambdas in a few cases where we could because in the past the performance wasn't great. Maybe I can give it another try at using lambdas in more places.

@NikolajBjorner
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

beta redex applies to more than lambdas. The occurrence of A in select(A,i) is a beta redex.

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about these? Simple and easy:

(select lambda!129 #x0000000000000008)
(select lambda!129 epsilon!127)

I don't know exactly what your bypass can handle, but here's another one that scream to be optimized:

(let ((a!1 (lambda ((|#off!10| (_ BitVec 64)))
             (ite (and (= ((_ extract 63 7) |#off!10|)
                          #b000000000000000000000000000000000000000000000000000000000)
                       (bvule ((_ extract 6 0) |#off!10|) #b1000011))
                  #b0100000000000000000000000000000000000000000000000000000000000000000000000
                  #b0000000000000000000000000000000000000000000000000000000000000000000000000))))
  (select a!1 epsilon!127))

@NikolajBjorner
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

has-lambda returns false for these occurrences because they are in the scope of beta redexes.
The beta-redexes should be expanded by quantifier reasoning.
I am not sure where your "Scream to be optimized" example relates. It is created during search? Then internalized as a lambda instead of beta reduced?
The rewriter can beta reduce.

Please sign in to comment.