[code-simplifier] Code Simplification - 2026-03-23: remove unused param and trailing whitespace in qe_lite_tactic.cpp

[github-actions]

Code Simplification — 2026-03-23

Small clean-up for src/qe/lite/qe_lite_tactic.cpp based on changes from PR #9062 ("Simplify extract_var_bound via operator normalization").

Files Simplified

• src/qe/lite/qe_lite_tactic.cpp — remove unused num_decls parameter from extract_var_bound; strip trailing whitespace

Improvements Made

1. Removed unused parameter

   • extract_var_bound(e, idx, num_decls, a_util, ...) → extract_var_bound(e, idx, a_util, ...)
   • num_decls was used in the old 109-line implementation but was never referenced after PR Simplify extract_var_bound via operator normalization #9062 condensed the logic to ~30 lines. Keeping it clutters the signature and misleads readers into thinking the function depends on the quantifier arity.

2. Removed trailing whitespace

   • Stripped four trailing spaces after return false; on the early-exit line.

Changes Based On

• Simplify extract_var_bound via operator normalization #9062 — Simplify extract_var_bound via operator normalization

Testing

No build is available in this environment, but the change is mechanical: one parameter removed from the definition and its single call site, plus whitespace cleanup. The parameter was provably unused (no reference to num_decls anywhere in the function body).

Git Diff

diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp
index 4f234a5..e6deac8 100644
--- a/src/qe/lite/qe_lite_tactic.cpp
+++ b/src/qe/lite/qe_lite_tactic.cpp
@@ -2308,7 +2308,7 @@ private:
     // Returns true if the conjunct is a bound for var(idx).
     // Sets is_lower=true for lower bounds, is_lower=false for upper bounds.
     // Sets bound_val to the bound value, inclusive.
-    bool extract_var_bound(expr* e, unsigned idx, unsigned num_decls, arith_util& a_util,
+    bool extract_var_bound(expr* e, unsigned idx, arith_util& a_util,
                            bool& is_lower, rational& bound_val) {
         expr *atom, *lhs, *rhs;
         rational val;
@@ -2332,7 +2332,7 @@ private:
         // Strict inequalities tighten the inclusive bound by 1.
         bool var_on_left = is_var(lhs) && to_var(lhs)->get_idx() == idx && a_util.is_numeral(rhs, val);
         if (!var_on_left && !(is_var(rhs) && to_var(rhs)->get_idx() == idx && a_util.is_numeral(lhs, val)))
-            return false;        
+            return false;
 
         // var_on_left: var <= val (upper bound), adjusted for strict.
         // var_on_right: val <= var (lower bound), adjusted for strict.
@@ -2398,7 +2398,7 @@ private:
                     continue;
                 bool is_lower;
                 rational bval;
-                if (extract_var_bound(conjs[ci].get(), vi, num_decls, a_util, is_lower, bval)) {
+                if (extract_var_bound(conjs[ci].get(), vi, a_util, is_lower, bval)) {
                     if (is_lower) {
                         if (!has_lb[vi] || bval > lbs[vi])
                             lbs[vi] = bval;

To apply:

git apply <<'EOF'
diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp
index 4f234a5..e6deac8 100644
--- a/src/qe/lite/qe_lite_tactic.cpp
+++ b/src/qe/lite/qe_lite_tactic.cpp
@@ -2308,7 +2308,7 @@ private:
     // Returns true if the conjunct is a bound for var(idx).
     // Sets is_lower=true for lower bounds, is_lower=false for upper bounds.
     // Sets bound_val to the bound value, inclusive.
-    bool extract_var_bound(expr* e, unsigned idx, unsigned num_decls, arith_util& a_util,
+    bool extract_var_bound(expr* e, unsigned idx, arith_util& a_util,
                            bool& is_lower, rational& bound_val) {
         expr *atom, *lhs, *rhs;
         rational val;
@@ -2332,7 +2332,7 @@ private:
         // Strict inequalities tighten the inclusive bound by 1.
         bool var_on_left = is_var(lhs) && to_var(lhs)->get_idx() == idx && a_util.is_numeral(rhs, val);
         if (!var_on_left && !(is_var(rhs) && to_var(rhs)->get_idx() == idx && a_util.is_numeral(lhs, val)))
-            return false;        
+            return false;
 
         // var_on_left: var <= val (upper bound), adjusted for strict.
         // var_on_right: val <= var (lower bound), adjusted for strict.
@@ -2398,7 +2398,7 @@ private:
                     continue;
                 bool is_lower;
                 rational bval;
-                if (extract_var_bound(conjs[ci].get(), vi, num_decls, a_util, is_lower, bval)) {
+                if (extract_var_bound(conjs[ci].get(), vi, a_util, is_lower, bval)) {
                     if (is_lower) {
                         if (!has_lb[vi] || bval > lbs[vi])
                             lbs[vi] = bval;
EOF

---

Automated by Code Simplifier Agent — analyzing code from the last 24 hours

Generated by Code Simplifier · ◷

To install this agentic workflow, run

gh aw add github/gh-aw/.github/workflows/code-simplifier.md@76d37d925abd44fee97379206f105b74b91a285b