mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 13:19:04 +00:00
Code Activity

update defaults for new grobner featuers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-05 14:34:03 -07:00
parent d7718623a4
commit 866393a842
2 changed files with 6 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/nla_core.cpp
View file

@ -17,6 +17,7 @@ Author:
#include "math/grobner/pdd_solver.h" #include "math/grobner/pdd_solver.h"
#include "math/dd/pdd_interval.h" #include "math/dd/pdd_interval.h"
#include "math/dd/pdd_eval.h" #include "math/dd/pdd_eval.h"
using namespace nla; using namespace nla;
typedef lp::lar_term term; typedef lp::lar_term term;
@ -1575,8 +1576,4 @@ void core::refine_pseudo_linear(monic const& m) {
} }
SASSERT(nlvar != null_lpvar); SASSERT(nlvar != null_lpvar);
lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0)); lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0));
// lemma.display(verbose_stream() << "pseudo-linear lemma\n");
} }

8
src/params/smt_params_helper.pyg
View file

@ -78,12 +78,12 @@ def_module_params(module_name='smt',
('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'), ('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),
('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('arith.nl.grobner_propagate_quotients', BOOL, False, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'), ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'),
('arith.nl.grobner_gcd_test', BOOL, False, 'detect gcd conflicts for polynomial powers x^k - y = 0'), ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'),
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.grobner_expand_terms', BOOL, False, 'expand terms before computing grobner basis'), ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),
('arith.nl.reduce_pseudo_linear', BOOL, False, 'create incremental linearization axioms for pseudo-linear monomials'), ('arith.nl.reduce_pseudo_linear', BOOL, True, 'create incremental linearization axioms for pseudo-linear monomials'),
('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'), ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),