From 0000e16851e3b2a4612556952395004b50239d1b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Jul 2026 18:54:14 -0700 Subject: [PATCH] expose avoid-skolems parameter to deal with TPTP problems --- src/params/pattern_inference_params.cpp | 2 ++ src/params/pattern_inference_params_helper.pyg | 1 + 2 files changed, 3 insertions(+) diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp index 0e548c8961..98943431a6 100644 --- a/src/params/pattern_inference_params.cpp +++ b/src/params/pattern_inference_params.cpp @@ -31,6 +31,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) { m_pi_non_nested_arith_weight = p.non_nested_arith_weight(); m_pi_pull_quantifiers = p.pull_quantifiers(); m_pi_warnings = p.warnings(); + m_pi_avoid_skolems = p.avoid_skolems(); } #define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; @@ -48,4 +49,5 @@ void pattern_inference_params::display(std::ostream & out) const { DISPLAY_PARAM(m_pi_nopat_weight); DISPLAY_PARAM(m_pi_avoid_skolems); DISPLAY_PARAM(m_pi_warnings); + DISPLAY_PARAM(m_pi_avoid_skolems); } diff --git a/src/params/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg index 80d36e3ec1..81495c8913 100644 --- a/src/params/pattern_inference_params_helper.pyg +++ b/src/params/pattern_inference_params_helper.pyg @@ -11,4 +11,5 @@ def_module_params(class_name='pattern_inference_params_helper', ('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'), + ('avoid_skolems', BOOL, True, 'avoid skolem functions when computing patterns'), ('warnings', BOOL, False, 'enable/disable warning messages in the pattern inference module')))