Restore stable quantifier benchmark behavior

Add an opt-in legacy nested-binder pattern inference mode and restore the previous hash combiner to avoid order-sensitive solver regressions.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: NikolajBjorner

src/ast/pattern/pattern_inference.cpp

@@ -181,6 +181,10 @@ inline void pattern_inference_cfg::collect::save(expr * n, unsigned delta, info
 }
 
 void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
+    if (m_owner.m_params.m_pi_legacy_nested_binders) {
+        save_candidate_legacy(n, delta);
+        return;
+    }
     switch (n->get_kind()) {
     case AST_VAR: {
         uint_set free_vars, bound_vars;
@@ -189,7 +193,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
             free_vars.insert(idx - delta);
         else if (idx < delta)
             bound_vars.insert(idx);
-        info * i = alloc(info, free_vars, bound_vars, 1);
+        info * i = alloc(info, m, n, free_vars, bound_vars, 1);
         save(n, delta, i);
         return;
     }
@@ -201,7 +205,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
         }
 
         if (c->get_num_args() == 0) {
-            save(n, delta, alloc(info, uint_set(), uint_set(), 1));
+            save(n, delta, alloc(info, m, n, uint_set(), uint_set(), 1));
             return;
         }
 
@@ -219,7 +223,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
             size       += child_info->m_size;
         }
 
-        save(n, delta, alloc(info, free_vars, bound_vars, size));
+        save(n, delta, alloc(info, m, n, free_vars, bound_vars, size));
         // Remark: arithmetic patterns are only used if they are nested inside other terms.
         // That is, we never consider x + 1 as pattern. On the other hand, f(x+1) can be a pattern
         // if arithmetic is not in the forbidden list.        
@@ -251,7 +255,82 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
             if (b >= num_decls)
                 bound_vars.insert(b - num_decls);
 
-        save(n, delta, alloc(info, body_info->m_free_vars, bound_vars, body_info->m_size + 1));
+        save(n, delta, alloc(info, m, n, body_info->m_free_vars, bound_vars, body_info->m_size + 1));
+        return;
+    }
+    default:
+        save(n, delta, nullptr);
+        return;
+    }
+}
+
+void pattern_inference_cfg::collect::save_candidate_legacy(expr * n, unsigned delta) {
+    switch (n->get_kind()) {
+    case AST_VAR: {
+        unsigned idx = to_var(n)->get_idx();
+        if (idx < delta) {
+            save(n, delta, nullptr);
+            return;
+        }
+        idx -= delta;
+        uint_set free_vars;
+        if (idx < m_num_bindings)
+            free_vars.insert(idx);
+        expr * new_node = delta == 0 ? n : m.mk_var(idx, to_var(n)->get_sort());
+        save(n, delta, alloc(info, m, new_node, free_vars, 1));
+        return;
+    }
+    case AST_APP: {
+        app * c = to_app(n);
+        if (m_owner.is_forbidden(c)) {
+            save(n, delta, nullptr);
+            return;
+        }
+        if (c->get_num_args() == 0) {
+            save(n, delta, alloc(info, m, n, uint_set(), 1));
+            return;
+        }
+        ptr_buffer<expr> args;
+        bool changed = false;
+        uint_set free_vars;
+        unsigned size = 1;
+        for (expr * child : *c) {
+            info * child_info = nullptr;
+            VERIFY(m_cache.find(entry(child, delta), child_info));
+            if (!child_info) {
+                save(n, delta, nullptr);
+                return;
+            }
+            args.push_back(child_info->m_node);
+            free_vars |= child_info->m_free_vars;
+            size += child_info->m_size;
+            changed |= child != child_info->m_node;
+        }
+        app * new_node = changed ? m.mk_app(c->get_decl(), args.size(), args.data()) : c;
+        save(n, delta, alloc(info, m, new_node, free_vars, size));
+        family_id fid = c->get_family_id();
+        decl_kind k = c->get_decl_kind();
+        if (!free_vars.empty() &&
+            (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only &&
+             (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL))))
+            m_owner.add_candidate(new_node, free_vars, size);
+        return;
+    }
+    case AST_QUANTIFIER: {
+        quantifier * q = to_quantifier(n);
+        unsigned num_decls = q->get_num_decls();
+        info * body_info = nullptr;
+        m_cache.find(entry(q->get_expr(), delta + num_decls), body_info);
+        if (!body_info) {
+            save(n, delta, nullptr);
+            return;
+        }
+        expr_ref new_body(m);
+        var_shifter shift(m);
+        shift(body_info->m_node, num_decls, new_body);
+        quantifier_ref new_q(m);
+        new_q = new_body == q->get_expr() ? q : m.update_quantifier(q, new_body);
+        save(n, delta, alloc(info, m, new_q, body_info->m_free_vars, body_info->m_size + 1));
         return;
     }
     default:

src/ast/pattern/pattern_inference.h

@@ -125,10 +125,13 @@ class pattern_inference_cfg :  public default_rewriter_cfg {
         };
 
         struct info {
+            expr_ref    m_node;
             uint_set    m_free_vars, m_bound_vars;
             unsigned    m_size;
-            info(uint_set const & fvars, uint_set const& bvars, unsigned sz):
-                m_free_vars(fvars), m_bound_vars(bvars), m_size(sz) {}
+            info(ast_manager& m, expr * n, uint_set const& fvars, uint_set const& bvars, unsigned sz):
+                m_node(n, m), m_free_vars(fvars), m_bound_vars(bvars), m_size(sz) {}
+            info(ast_manager& m, expr * n, uint_set const& fvars, unsigned sz):
+                m_node(n, m), m_free_vars(fvars), m_size(sz) {}
         };
 
         ast_manager &            m;
@@ -144,6 +147,7 @@ class pattern_inference_cfg :  public default_rewriter_cfg {
         bool visit_children(expr * n, unsigned delta);
         void save(expr * n, unsigned delta, info * i);
         void save_candidate(expr * n, unsigned delta);
+        void save_candidate_legacy(expr * n, unsigned delta);
         void reset();
     public:
         collect(ast_manager & m, pattern_inference_cfg & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
@@ -253,5 +257,3 @@ class pattern_inference_rw : public rewriter_tpl<pattern_inference_cfg> {
 public:
     pattern_inference_rw(ast_manager& m, pattern_inference_params const & params);
 };
-
-

src/params/pattern_inference_params.cpp

@@ -27,6 +27,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) {
     m_pi_decompose_patterns      = p.decompose_patterns();
     m_pi_arith                   = static_cast<arith_pattern_inference_kind>(p.arith());
     m_pi_use_database            = p.use_database();
+    m_pi_legacy_nested_binders   = p.legacy_nested_binders();
     m_pi_arith_weight            = p.arith_weight();
     m_pi_non_nested_arith_weight = p.non_nested_arith_weight();
     m_pi_pull_quantifiers        = p.pull_quantifiers();
@@ -43,6 +44,7 @@ void pattern_inference_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_pi_decompose_patterns);
     DISPLAY_PARAM(m_pi_arith);
     DISPLAY_PARAM(m_pi_use_database);
+    DISPLAY_PARAM(m_pi_legacy_nested_binders);
     DISPLAY_PARAM(m_pi_arith_weight);
     DISPLAY_PARAM(m_pi_non_nested_arith_weight);
     DISPLAY_PARAM(m_pi_pull_quantifiers);

src/params/pattern_inference_params.h

@@ -33,6 +33,7 @@ struct pattern_inference_params {
     bool                          m_pi_decompose_patterns;
     arith_pattern_inference_kind  m_pi_arith;
     bool                          m_pi_use_database;
+    bool                          m_pi_legacy_nested_binders;
     unsigned                      m_pi_arith_weight;
     unsigned                      m_pi_non_nested_arith_weight;
     bool                          m_pi_pull_quantifiers;
@@ -48,5 +49,3 @@ struct pattern_inference_params {
 
     void display(std::ostream & out) const;
 };
-
-

src/params/pattern_inference_params_helper.pyg

@@ -8,6 +8,7 @@ def_module_params(class_name='pattern_inference_params_helper',
                           ('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'),
                           ('use_database', BOOL, False, 'use pattern database'),
                           ('enabled', BOOL, True, 'enable a heuristic to infer patterns, when they are not provided'),	
+                          ('legacy_nested_binders', BOOL, False, 'use legacy pattern inference behavior below nested binders'),
                           ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
                           ('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
                           ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),

src/util/hash.h

@@ -57,8 +57,10 @@ static inline unsigned hash_ull(unsigned long long a) {
 }
 
 static inline unsigned combine_hash(unsigned h1, unsigned h2) {
-    h1 ^= h2 + 0x9e3779b9 + (h1 << 6) + (h1 >> 2);
-    return hash_u(h1);
+    h2 -= h1; h2 ^= (h1 << 8);
+    h1 -= h2; h2 ^= (h1 << 16);
+    h2 -= h1; h2 ^= (h1 << 10);
+    return h2;
 }
 
 static inline unsigned hash_u_u(unsigned a, unsigned b) {