From c9a4a5907dc86511cba1f788b01333ecd8968e45 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 18 Jul 2026 11:28:41 -0700
Subject: [PATCH] tptp: set weight 1 on parsed quantifiers

Route all forall/exists creation in the TPTP frontend through a
with_weight1() helper so quantifiers use weight 1 instead of the
default 0. Improves smt.ho_matching on higher-order TPTP problems
(+26 net solved, fewer timeouts over the ^ benchmark set).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
---
 src/cmd_context/tptp_frontend.cpp | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index 966e026ca..9409614b5 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -960,11 +960,20 @@ class tptp_parser {
         }
     };
 
+    // TPTP quantifiers are created with weight 1 (rather than the default 0)
+    // so that E-matching / ho_matching treats them uniformly.
+    expr_ref with_weight1(expr_ref q) {
+        if (is_quantifier(q) && !is_lambda(q))
+            q = expr_ref(m.update_quantifier_weight(to_quantifier(q), 1), m);
+        return q;
+    }
+
     expr_ref mk_quantifier(bool is_forall, ptr_vector<app> const& bound, expr_ref const& body) {
         SASSERT(body);
         if (bound.empty()) return body;
         expr_ref b = ensure_bool(body);
-        return is_forall ? ::mk_forall(m, bound.size(), bound.data(), b.get()) : ::mk_exists(m, bound.size(), bound.data(), b.get());
+        expr_ref q = is_forall ? ::mk_forall(m, bound.size(), bound.data(), b.get()) : ::mk_exists(m, bound.size(), bound.data(), b.get());
+        return with_weight1(q);
     }
 
     // $is_rat(x) ≡ exists a:Int, b:Int. b != 0 && x = a/b
@@ -983,7 +992,7 @@ class tptp_parser {
         ptr_vector<app> bound;
         bound.push_back(a);
         bound.push_back(b);
-        return expr_ref(::mk_exists(m, bound.size(), bound.data(), body.get()), m);
+        return with_weight1(expr_ref(::mk_exists(m, bound.size(), bound.data(), body.get()), m));
     }
 
     // Grammar: <thf_atomic_type>   ::= <type_constant> | <defined_type> | <variable> |
@@ -1808,7 +1817,7 @@ class tptp_parser {
             if (vars.size() > 1) {
                 ptr_vector<app> rest;
                 for (unsigned i = 1; i < vars.size(); ++i) rest.push_back(vars[i]);
-                pred = expr_ref(::mk_exists(m, rest.size(), rest.data(), pred.get()), m);
+                pred = with_weight1(expr_ref(::mk_exists(m, rest.size(), rest.data(), pred.get()), m));
             }
             app* xvar = vars[0];
             expr_ref abs_body(m);
@@ -1846,7 +1855,7 @@ class tptp_parser {
             app* cs[1] = { c };
             expr_ref q = is_forall ? ::mk_forall(m, 1, cs, body.get())
                                    : ::mk_exists(m, 1, cs, body.get());
-            return q;
+            return with_weight1(q);
         }
 
         expr_ref_vector args(m);