From e54928679f52c44246069f95a4fdd207583d75e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 19:15:20 -0700 Subject: [PATCH] add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/solve_eqs.cpp | 9 ++++++++- src/ast/simplifiers/solve_eqs.h | 1 + src/params/smt_params_helper.pyg | 1 + 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index 71484590a..335dd1ae1 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -119,7 +119,10 @@ namespace euf { SASSERT(j == var2id(v)); if (m_fmls.frozen(v)) continue; - + + if (!m_config.m_enable_non_ground && has_quantifiers(t)) + continue; + bool is_safe = true; unsigned todo_sz = todo.size(); @@ -127,7 +130,10 @@ namespace euf { // all time-stamps must be at or above current level // unexplored variables that are part of substitution are appended to work list. SASSERT(m_todo.empty()); + + m_todo.push_back(t); + verbose_stream() << "check " << mk_pp(t, m) << "\n"; expr_fast_mark1 visited; while (!m_todo.empty()) { expr* e = m_todo.back(); @@ -336,6 +342,7 @@ namespace euf { m_rewriter.updt_params(p); smt_params_helper sp(p); m_config.m_enabled = sp.solve_eqs(); + m_config.m_enable_non_ground = sp.solve_eqs_non_ground(); } void solve_eqs::collect_param_descrs(param_descrs& r) { diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h index 4e3ae6aa1..5f9a993aa 100644 --- a/src/ast/simplifiers/solve_eqs.h +++ b/src/ast/simplifiers/solve_eqs.h @@ -42,6 +42,7 @@ namespace euf { bool m_context_solve = true; unsigned m_max_occs = UINT_MAX; bool m_enabled = true; + bool m_enable_non_ground = true; }; stats m_stats; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index c1eb0148a..39a737829 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -20,6 +20,7 @@ def_module_params(module_name='smt', ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'), ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'), ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'), + ('solve_eqs.non_ground', BOOL, True, 'pre-processing: solve equalities. Allow eliminating variables by non-ground solutions which can break behavior for model evaluation.'), ('propagate_values', BOOL, True, 'pre-processing: propagate values'), ('bound_simplifier', BOOL, True, 'apply bounds simplification during pre-processing'), ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),