handle lambda equalities

src/smt/theory_array_base.cpp

@@ -23,6 +23,7 @@ Revision History:
 #include "smt/smt_model_generator.h"
 #include "model/func_interp.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/pattern/pattern_inference.h"
 
 namespace smt {
 
@@ -413,6 +414,16 @@ namespace smt {
         expr * eq = m.mk_eq(sel1, sel2);
         expr_ref q(m.mk_forall(dimension, sorts.data(), names.data(), eq), m);
         ctx.get_rewriter()(q);
+        // The select terms are beta-reduced away by the rewriter, so the
+        // resulting quantifier carries no patterns. Infer patterns so that the
+        // e-matching engine can instantiate it (dynamically generated
+        // quantifiers bypass the pre-processing pattern inference pass).
+        if (is_forall(q) && to_quantifier(q)->get_num_patterns() == 0) {
+            pattern_inference_rw infer(m, ctx.get_fparams());
+            expr_ref q2(m);
+            infer(q, q2);
+            q = q2;
+        }
         if (!ctx.b_internalized(q)) {
             ctx.internalize(q, true);
         }

src/smt/theory_array_full.cpp

@@ -354,6 +354,14 @@ namespace smt {
             add_as_array(v1, n);
         for (enode* n : d2->m_lambdas)
             add_lambda(v1, n);
+        // When a lambda is equated to another array term, assert the congruence
+        // axiom  n1 = n2 => forall k . select(n1, k) = select(n2, k).
+        // This lets positive equalities between lambdas (which have no select
+        // parents of their own) produce usable consequences.
+        enode* n1 = get_enode(v1);
+        enode* n2 = get_enode(v2);
+        if (is_lambda(n1->get_expr()) || is_lambda(n2->get_expr()))
+            assert_congruent(n1, n2);
         TRACE(array, 
               tout << pp(get_enode(v1), m) << "\n";
               tout << pp(get_enode(v2), m) << "\n";
@@ -854,13 +862,28 @@ namespace smt {
         }
         for (enode* n : m_lambdas) 
             for (enode* p : n->get_parents())
-                if (ctx.is_relevant(p) && !is_default(p) && !ctx.is_beta_redex(p, n)) {
+                if (ctx.is_relevant(p) && !is_default(p) && !ctx.is_beta_redex(p, n) && !is_congruent_eq(p)) {
                     TRACE(array, tout << "lambda is not a beta redex " << enode_pp(p, ctx) << "\n");
                     return true;
                 }
         return false;
     }
 
+    /**
+       \brief A relevant equality between two array terms whose roots coincide is
+       handled by the congruence axiom asserted on merge (see merge_eh /
+       assert_congruent). Such an equality parent does not make a lambda an
+       unsupported (non beta-redex) occurrence, so it should not trigger a
+       final-check give-up.
+    */
+    bool theory_array_full::is_congruent_eq(enode* p) {
+        expr* a = nullptr, * b = nullptr;
+        if (!m.is_eq(p->get_expr(), a, b))
+            return false;
+        return is_array_sort(p->get_arg(0)) &&
+               p->get_arg(0)->get_root() == p->get_arg(1)->get_root();
+    }
+
 
     bool theory_array_full::instantiate_parent_stores_default(theory_var v) {
         SASSERT(v != null_theory_var);

src/smt/theory_array_full.h

@@ -92,6 +92,7 @@ namespace smt {
         enode_vector m_as_array;
         enode_vector m_lambdas;
         bool has_non_beta_as_array();
+        bool is_congruent_eq(enode* p);
 
         bool instantiate_select_const_axiom(enode* select, enode* cnst);
         bool instantiate_select_as_array_axiom(enode* select, enode* arr);