mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add options to allow testing the effect of non-linear hammers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-26 19:18:44 -07:00
parent 029d726eb8
commit 8d2b65b20b
4 changed files with 18 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/params/smt_params_helper.pyg
View file

@ -78,7 +78,10 @@ def_module_params(module_name='smt',
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('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.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),

6
src/smt/params/theory_arith_params.cpp
View file

@ -36,6 +36,9 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
m_arith_auto_config_simplex = p.arith_auto_config_simplex();
m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials();
m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds();
m_nl_arith_cross_nested = p.arith_nl_cross_nested();
arith_rewriter_params ap(_p);
m_arith_eq2ineq = ap.eq2ineq();
@ -89,4 +92,7 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_nl_arith_max_degree);
DISPLAY_PARAM(m_nl_arith_branching);
DISPLAY_PARAM(m_nl_arith_rounds);
DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials);
DISPLAY_PARAM(m_nl_arith_optimize_bounds);
DISPLAY_PARAM(m_nl_arith_cross_nested);
}

3
src/smt/params/theory_arith_params.h
View file

@ -105,6 +105,9 @@ struct theory_arith_params {
unsigned m_nl_arith_max_degree = 6;
bool m_nl_arith_branching = true;
unsigned m_nl_arith_rounds = 1024;
bool m_nl_arith_propagate_linear_monomials = true;
bool m_nl_arith_optimize_bounds = true;
bool m_nl_arith_cross_nested = true;
theory_arith_params(params_ref const & p = params_ref()) {

6
src/smt/theory_arith_nl.h
View file

@ -902,6 +902,8 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_linear_monomials() {
if (!m_params.m_nl_arith_propagate_linear_monomials)
return false;
if (!reflection_enabled())
return false;
TRACE("non_linear", tout << "propagating linear monomials...\n";);
@ -2278,6 +2280,8 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
*/
template<typename Ext>
bool theory_arith<Ext>::max_min_nl_vars() {
if (!m_params.m_nl_arith_optimize_bounds)
return true;
var_set already_found;
svector<theory_var> vars;
for (theory_var v : m_nl_monomials) {
@ -2360,7 +2364,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
}
break;
case 1:
if (!is_cross_nested_consistent(vars))
if (m_params.m_nl_arith_cross_nested && !is_cross_nested_consistent(vars))
progress = true;
break;
case 2: