From 0758c930868959937b09d94568ea26bc6297a196 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Feb 2023 11:09:52 -0800 Subject: [PATCH] fix #6591 - add check for lambdas similar to as-array in context of quantifiers. MBQI is not a decision procedure for this combination and can then incorrectly conclude satisfiabiltiy. Scenario The formula contains assertions - bv = (map or (lambda ..) t) - forall y (not (select bv (pair s y))) Since bv is extensionally equal to a term that depends on a lambda, MBQI cannot just take the current finite approximation of bv when checking the quantifier for satisfiability. --- src/smt/theory_array_full.cpp | 8 ++++++++ src/smt/theory_array_full.h | 1 + 2 files changed, 9 insertions(+) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 120e124189c..a4876ab4d81 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -252,6 +252,8 @@ namespace smt { else if (m.is_lambda_def(n->get_decl())) { instantiate_default_lambda_def_axiom(n); d->m_lambdas.push_back(n); + m_lambdas.push_back(n); + ctx.push_trail(push_back_vector(m_lambdas)); } return r; } @@ -830,6 +832,12 @@ namespace smt { return true; } } + for (enode* n : m_lambdas) + for (enode* p : n->get_parents()) + if (!ctx.is_beta_redex(p, n)) { + TRACE("array", tout << "not a beta redex " << enode_pp(p, ctx) << "\n"); + return true; + } return false; } diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index 210426e10d2..98e53627c90 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -86,6 +86,7 @@ namespace smt { bool has_unitary_domain(app* array_term); std::pair mk_epsilon(sort* s); enode_vector m_as_array; + enode_vector m_lambdas; bool has_non_beta_as_array(); bool instantiate_select_const_axiom(enode* select, enode* cnst);