From 5ba4d8d0f1c577caaa899a02eff179b9b4c12fb4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 7 Sep 2019 18:22:16 +0300
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/fd_solver/smtfd_solver.cpp | 28 +++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 07b9c3bef33..56e6c4763de 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -590,6 +590,10 @@ namespace smtfd {
             return mk_and(r);
         }
 
+        void check_extensionality(expr* a, expr* b) {
+            // sort* s = m.get_sort(a);
+        }
+
     public:
 
         a_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl):
@@ -625,6 +629,30 @@ namespace smtfd {
 
         unsigned max_rounds() override { return 2; }
 
+        void global_check(expr_ref_vector const& core) {
+            obj_map<sort, obj_map<expr, expr*>*> sort2val2array;
+            expr_ref_vector pinned(m);
+            for (expr* t : subterms(core)) {
+                if (m_autil.is_array(t)) {
+                    sort* s = m.get_sort(t);
+                    obj_map<expr, expr*>* v2a = nullptr;
+                    if (!sort2val2array.find(s, v2a)) {
+                        v2a = alloc(obj_map<expr, expr*>);
+                        sort2val2array.insert(s, v2a);
+                    }
+                    expr* a = nullptr;
+                    expr_ref v = eval_abs(t);
+                    pinned.push_back(v);
+                    if (v2a->find(v, a)) {
+                        check_extensionality(a, t);
+                    }
+                    else {
+                        v2a->insert(v, t);
+                    }
+                }
+            }
+        }
+
     };
 
     struct stats {