prepare ground for general projection

src/ast/euf/ho_matcher.cpp

@@ -49,6 +49,53 @@ Author:
 
 namespace euf {
 
+    expr_ref_vector const &ho_subst::get_binding(quantifier *q) {
+        ast_manager &m = m_subst.get_manager();
+        m_binding.reset();
+        m_binding.append(m_subst);
+
+        // Shrink binding to original quantifier's num_decls
+        // The HO quantifier has extra vars at higher indices; drop them.
+        // Binding is indexed by var index: binding[i] = value for var i.
+        // First substitute any remaining vars, then keep only original vars.
+        TRACE(
+            ho_matching, tout << "num bound variables " << q->get_num_decls() << " for " << mk_bounded_pp(q, m) << "\n"
+                              << m_binding << "\n";
+            for (unsigned i = 0; i < m_binding.size(); ++i) {
+                tout << i << " - " << mk_pp(m_binding.get(i)->get_sort(), m) << ": " << mk_ll_pp(m_binding.get(i), m)
+                     << "\n";
+            });
+        if (m_binding.size() > q->get_num_decls()) {
+            // binding is indexed directly (binding[k] = value for var k),
+            // so the substitution must use direct (non-standard) order to
+            // resolve chained HO variable references; the sort guard below
+            // is checked with the matching order.
+            var_subst sub(m, false);
+            bool change = true;
+            while (change) {
+                change = false;
+                for (unsigned i = 0; i < m_binding.size(); ++i) {
+                    if (!m_binding.get(i))
+                        continue;
+                    // A misaligned higher-order binding would build an
+                    // ill-sorted term. Abandon this refinement (no instance)
+                    // rather than aborting the whole solve.
+                    SASSERT(is_well_sorted(m, m_binding.get(i)));
+                    auto r = sub(m_binding.get(i), m_binding);
+                    change |= r != m_binding.get(i);
+                    m_binding[i] = r;
+                    SASSERT(is_well_sorted(m, m_binding.get(i)));
+                    TRACE(ho_matching, tout << "setting v" << i << " <- " << r << "\n");
+                }
+            }
+            m_binding.shrink(q->get_num_decls());
+        }
+        SASSERT (m_binding.size() == q->get_num_decls());
+           
+        m_binding.reverse();
+        return m_binding;
+    }
+
 
     void ho_matcher::operator()(expr* pat, expr* t, unsigned num_vars) {
         (*this)(pat, t, 0, num_vars);
@@ -414,6 +461,16 @@ namespace euf {
                             wi.set_index(i + 1);
                             return true;
                         }
+                        // pi has sort T1 -> T2 -> T, and t has sort T.
+                        // we can project \vars . x_i (H1 vars) (H2 vars) to get a term of sort T.
+                        if (start <= i && maps_to_sort(pi->get_sort(), t->get_sort())) {
+                            IF_VERBOSE(3, verbose_stream() << "maps to " << mk_pp(pi->get_sort(), m) << " "
+                                                           << mk_pp(t->get_sort(), m) << "\n");
+                            // TODO: implement this case
+                            // v->get_sort() determines vars
+                            // x := bound variable from "project" function.
+                            // add_meta_var_apps(sort *s, sort *t, expr_ref& x, expr_ref_vector const& vars, unsigned offset)
+                        }
                         ++i;
                     }
                 }
@@ -580,6 +637,49 @@ namespace euf {
         return true;
     }
 
+    // s is of the form T1 -> T2 -> .. -> Tn -> t
+    bool ho_matcher::maps_to_sort(sort* s, sort* t) const {
+        SASSERT(s != t);
+        while (m_array.is_array(s)) {
+            s = get_array_range(s); 
+            if (s == t)
+                return true;
+        }
+        return false;
+    }
+
+    // s := (T1*T1' -> T2 -> t)
+    // x is of type s
+    // x := (select (select x (H1 vars) (H2 vars)) (H3 vars)) of type t
+    void ho_matcher::add_meta_var_apps(sort *s, sort *t, expr_ref& x, expr_ref_vector const& vars, unsigned offset) {
+        
+        expr_ref_vector args(m), hargs(m);
+        ptr_buffer<sort> domain;
+        for (auto v : vars) 
+            domain.push_back(v->get_sort());        
+
+        SASSERT(s == x->get_sort());
+        while (s != t) {
+
+            SASSERT(m_array.is_array(s));
+            unsigned arity = get_array_arity(s);
+            args.reset();
+            args.push_back(x);
+            for (unsigned i = 0; i < arity; ++i) {
+                sort *d = get_array_domain(s, i);
+                auto r = m_array.mk_array_sort(domain.size(), domain.data(), d);
+                hargs.reset();
+                hargs.push_back(m.mk_var(++offset, r));
+                hargs.append(vars);
+                auto h = m_array.mk_select(hargs);
+                args.push_back(h);                       
+            }
+            x = m_array.mk_select(args);
+            s = get_array_range(s); 
+            SASSERT(s == x->get_sort());
+        }     
+    }
+
     // create a lambda abstraction for the meta variable such that
     // when applied to patterns, the result is t.
     // pre-condition: is_pattern(p, offset, t);

src/ast/euf/ho_matcher.h

@@ -123,9 +123,9 @@ namespace euf {
 
     class ho_subst {
         expr_ref_vector m_subst;
+        expr_ref_vector m_binding;
     public:
-        ho_subst(ast_manager& m) :
-            m_subst(m) {            
+        ho_subst(ast_manager &m) : m_subst(m), m_binding(m) {
         }
         void resize(unsigned n) {
             m_subst.resize(n, nullptr);
@@ -158,6 +158,9 @@ namespace euf {
             }
             return out;
         }
+
+        expr_ref_vector const &get_binding(quantifier* q);
+        
     };
 
     class unitary_patterns {
@@ -343,6 +346,10 @@ namespace euf {
 
         bool is_closed(expr* v, unsigned scopes, unsigned offset) const;
 
+        bool maps_to_sort(sort *s, sort *t) const;
+
+        void add_meta_var_apps(sort *s, sort *t, expr_ref& x, expr_ref_vector const& vars, unsigned offset);
+
         void add_binding(var* v, unsigned offset, expr* t);
 
         expr_ref mk_project(unsigned num_lambdas, unsigned xi, sort* array_sort);

src/ast/value_generator.cpp

@@ -15,6 +15,7 @@
 
 --*/
 
+#include "ast/ast_pp.h"
 #include "ast/value_generator.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
@@ -267,34 +268,37 @@ public:
     // repetitions also happen when the same set of indices are updated twice
 
     expr_ref get_value(sort* s, unsigned index) override {
+
         unsigned arity = get_array_arity(s);
         sort* r = get_array_range(s);
-        sort_size const& sz = r->get_num_elements();
-        if (sz.is_finite() && sz.size() == 1) {
+        sort_size const& asz = s->get_num_elements();
+        
+        if (asz.is_finite() && asz.size() == 1) {
             return expr_ref(a.mk_const_array(s, g.get_value(r, 0)), m);           
         }
         
         unsigned z = 0;
-        if (is_small_size(sz)) {
-            z = index % sz.size();
-            index = index / (unsigned)sz.size();
+        if (is_small_size(asz)) {            
+            if (asz.size() <= index) 
+                return expr_ref(m);            
         }
         else {
             inverse_cantor(index, z, index);
         }
         expr_ref result(a.mk_const_array(s, g.get_value(r, z)), m);
+        sort *range = get_array_range(s);
         unsigned default_index = z;
         expr_ref_vector args(m);
         unsigned_vector inf;
         args.resize(arity+2);
-        while (index > 0) {            
+        while (index > 0) {  
             args[0] = result;
             for (unsigned i = 0; i < arity; ++i) {
                 sort* d = get_array_domain(s, i);
                 sort_size const& dsz = d->get_num_elements();
                 if (is_small_size(dsz)) {
-                    args[1 + i] = g.get_value(d, index % dsz.size());
-                    index = index / ((unsigned)dsz.size());
+                    inverse_cantor(index, z, index);
+                    args[1 + i] = g.get_value(d, z % dsz.size());
                 }
                 else {
                     inf.push_back(i);
@@ -305,16 +309,19 @@ public:
                 args[1 + i] = g.get_value(get_array_domain(s, i), z);
             }
 
-            // ensure z is different from default_index.
-            if (is_small_size(sz)) {
-                z = index % (sz.size() - 1);
-                index = index / (unsigned)sz.size();
+            inverse_cantor(index, z, index);
+
+            sort_size const &rsz = range->get_num_elements();
+            
+            if (is_small_size(rsz)) {
+                args[arity + 1] = g.get_value(r, z % rsz.size());
             }
             else {
-                inverse_cantor(index, z, index);
+                // ensure z is different from default_index.
+                if (z >= default_index)
+                    z++;
+                args[arity + 1] = g.get_value(r, z);
             }
-            if (z >= default_index) z++;
-            args[arity+1] = g.get_value(r, z);
             result = a.mk_store(args);
         }
         
@@ -333,8 +340,11 @@ public:
     }
 
     expr_ref get_value(sort* s, unsigned index) override {
-        index %= bv.get_bv_size(s);
-        return expr_ref(bv.mk_numeral(rational(index), s), m);
+        auto sz = s->get_num_elements();
+        if (!sz.is_finite() || index < sz.size())
+            return expr_ref(bv.mk_numeral(rational(index), s), m);
+        else
+            return expr_ref(m);
     }
 };
 
@@ -350,9 +360,11 @@ public:
     expr_ref get_value(sort* s, unsigned index) override {
         if (!m.is_bool(s))
             return expr_ref(m.mk_fresh_const("basic", s), m);
-        if (index % 2 == 0)
-            return expr_ref(m.mk_false(), m);
-        return expr_ref(m.mk_true(), m);
+        switch (index) {
+        case 0: return expr_ref(m.mk_false(), m);
+        case 1: return expr_ref(m.mk_true(), m);
+        default: return expr_ref(m);
+        }        
     }
 };
 

src/smt/smt_quantifier.cpp

@@ -668,53 +668,7 @@ namespace smt {
             auto &st = m_ho_state;
             auto *hoq = st.m_q;
             auto *q = m_ho_matcher->hoq2q(hoq);
-
-            expr_ref_vector binding(m);
-            for (unsigned i = 0; i < s.size(); ++i)
-                binding.push_back(s.get(i));
-
-            // Shrink binding to original quantifier's num_decls
-            // The HO quantifier has extra vars at higher indices; drop them.
-            // Binding is indexed by var index: binding[i] = value for var i.
-            // First substitute any remaining vars, then keep only original vars.
-            TRACE(
-                ho_matching, tout << "num bound variables " << q->get_num_decls() << " for " << mk_bounded_pp(q, m)
-                                  << "\n"
-                                  << binding << "\n";
-                for (unsigned i = 0; i < binding.size(); ++i) {
-                    tout << i << " - " << mk_pp(binding.get(i)->get_sort(), m) << ": " << mk_ll_pp(binding.get(i), m)
-                         << "\n";
-                });
-            if (binding.size() > q->get_num_decls()) {
-                // binding is indexed directly (binding[k] = value for var k),
-                // so the substitution must use direct (non-standard) order to
-                // resolve chained HO variable references; the sort guard below
-                // is checked with the matching order.
-                var_subst sub(m, false);
-                bool change = true;
-                while (change) {
-                    change = false;
-                    for (unsigned i = 0; i < binding.size(); ++i) {
-                        if (!binding.get(i))
-                            continue;
-                        // A misaligned higher-order binding would build an
-                        // ill-sorted term. Abandon this refinement (no instance)
-                        // rather than aborting the whole solve.
-                        SASSERT(is_well_sorted(m, binding.get(i)));
-                        auto r = sub(binding.get(i), binding);
-                        change |= r != binding.get(i);
-                        binding[i] = r;
-                        SASSERT(is_well_sorted(m, binding.get(i)));
-                        TRACE(ho_matching, tout << "setting v" << i << " <- " << r << "\n");
-                    }
-                }
-                binding.shrink(q->get_num_decls());
-            }
-            if (binding.size() < q->get_num_decls())
-                return;
-
-            binding.reverse();
-
+            auto const &binding = s.get_binding(q);
             st.m_matches.push_back({ q, binding });
         }
 

src/smt/theory_array.cpp

@@ -371,14 +371,14 @@ namespace smt {
             else {
                 if (mk_interface_eqs_at_final_check() == FC_CONTINUE)
                     r = FC_CONTINUE;
-                else 
+                else
                     r = assert_delayed_axioms();
             }
         }
         else {
             if (m_final_check_idx % 2 == 1) {
                 r = assert_delayed_axioms();
-                if (r == FC_DONE) 
+                if (r == FC_DONE)
                     r = mk_interface_eqs_at_final_check();
             }
             else {
@@ -389,7 +389,7 @@ namespace smt {
             }
         }
         bool should_giveup = m_found_unsupported_op || has_propagate_up_trail();
-        if (r == FC_DONE && should_giveup && !ctx.get_fparams().m_array_fake_support) 
+        if (r == FC_DONE && should_giveup && !ctx.get_fparams().m_array_fake_support)
             r = FC_GIVEUP;
         CTRACE(array, r != FC_DONE || m_found_unsupported_op, tout << r << "\n";);
         return r;

src/smt/theory_array_base.cpp

@@ -712,6 +712,7 @@ namespace smt {
         collect_defaults();
         collect_selects();
         propagate_selects();
+        TRACE(array, display_selects(tout); display(tout););
     }
 
     /**
@@ -809,12 +810,28 @@ namespace smt {
         return set;
     }
 
-    void theory_array_base::collect_selects() {
-        int num_vars = get_num_vars();
-
+    void theory_array_base::reset_selects() {
+        for (auto r : m_selects_range)
+            dealloc(r);
+        m_selects_range.reset();
         m_selects.reset();
         m_selects_domain.reset();
-        m_selects_range.reset();
+    }
+           
+    std::ostream& theory_array_base::display_selects(std::ostream& out) {
+        for (auto [r, s] : m_selects) {
+            tout << enode_pp(r, ctx) << ":\n";
+            for (auto sel : *s) 
+                tout << "   " << enode_pp(sel, ctx) << " "
+                     << enode_pp(sel->get_root(), ctx) << "\n";
+            tout << "\n";
+        }
+        return out;
+    }
+
+    void theory_array_base::collect_selects() {
+        int num_vars = get_num_vars();
+        reset_selects();
 
         for (theory_var v = 0; v < num_vars; ++v) {
             enode * r = get_enode(v)->get_root();                
@@ -889,7 +906,7 @@ namespace smt {
     }
 
     void theory_array_base::finalize_model(model_generator & m) {
-        std::for_each(m_selects_range.begin(), m_selects_range.end(), delete_proc<select_set>());
+        reset_selects();
     }
 
     class array_value_proc : public model_value_proc {

src/smt/theory_array_base.h

@@ -191,6 +191,9 @@ namespace smt {
         ptr_vector<select_set>       m_selects_range;
         bool                         m_use_unspecified_default;  // temporary field for model construction
 
+        void reset_selects();
+        std::ostream &display_selects(std::ostream &out);
+
         theory_var mg_find(theory_var v);
         void mg_merge(theory_var n, theory_var m);