mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

expose avoid-skolems parameter to deal with TPTP problems

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-12 18:54:14 -07:00
parent 7d67dbfcfc
commit 0000e16851
2 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/params/pattern_inference_params.cpp
View file

@ -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);
}

1
src/params/pattern_inference_params_helper.pyg
View file

@ -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')))