mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

consolidate settings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-26 18:41:27 -07:00
parent e84d1e9d96
commit a8f867f145
13 changed files with 45 additions and 100 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/horner.cpp
View file

@ -40,7 +40,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
template <typename T>
bool horner::row_is_interesting(const T& row) const {
TRACE("nla_solver_details", c().print_row(row, tout););
if (row.size() > c().m_nla_settings.horner_row_length_limit) {
if (row.size() > c().params().arith_nl_horner_row_length_limit()) {
TRACE("nla_solver_details", tout << "disregard\n";);
return false;
}
@ -98,7 +98,7 @@ bool horner::lemmas_on_row(const T& row) {
}
bool horner::horner_lemmas() {
if (!c().m_nla_settings.run_horner) {
if (!c().params().arith_nl_horner()) {
TRACE("nla_solver", tout << "not generating horner lemmas\n";);
return false;
}

8
src/math/lp/nla_common.cpp
View file

@ -71,11 +71,11 @@ void common::add_deps_of_fixed(lpvar j, u_dependency*& dep) {
// creates a nex expression for the coeff and var,
nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_dependency*& dep) {
SASSERT(!coeff.is_zero());
if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(j)) {
if (c().params().arith_nl_horner_subs_fixed() == 1 && c().var_is_fixed(j)) {
add_deps_of_fixed(j, dep);
return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x);
}
if (c().m_nla_settings.horner_subs_fixed == 2 && c().var_is_fixed_to_zero(j)) {
if (c().params().arith_nl_horner_subs_fixed() == 2 && c().var_is_fixed_to_zero(j)) {
add_deps_of_fixed(j, dep);
return cn.mk_scalar(rational(0));
}
@ -89,10 +89,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_depende
mf *= coeff;
u_dependency * initial_dep = dep;
for (lpvar k : m.vars()) {
if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(k)) {
if (c().params().arith_nl_horner_subs_fixed() == 1 && c().var_is_fixed(k)) {
add_deps_of_fixed(k, dep);
mf *= c().m_lar_solver.column_lower_bound(k).x;
} else if (c().m_nla_settings.horner_subs_fixed == 2 &&
} else if (c().params().arith_nl_horner_subs_fixed() == 2 &&
c().var_is_fixed_to_zero(k)) {
dep = initial_dep;
add_deps_of_fixed(k, dep);

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

@ -21,7 +21,7 @@ namespace nla {
typedef lp::lar_term term;
core::core(lp::lar_solver& s, reslimit & lim) :
core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_evars(),
m_lar_solver(s),
m_reslim(lim),
@ -36,6 +36,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
m_horner(this),
m_grobner(this),
m_emons(m_evars),
m_params(p),
m_use_nra_model(false),
m_nra(s, m_nra_lim, *this)
{
@ -1504,8 +1505,11 @@ void core::check_bounded_divisions(vector<lemma>& l_vec) {
bool core::can_add_bound(unsigned j, u_map<unsigned>& bounds) {
unsigned count = 1;
if (bounds.find(j, count))
if (bounds.find(j, count)) {
if (count >= 2)
return false;
++count;
}
bounds.insert(j, count);
struct decrement : public trail {
u_map<unsigned>& bounds;
@ -1519,7 +1523,7 @@ bool core::can_add_bound(unsigned j, u_map<unsigned>& bounds) {
}
};
trail().push(decrement(bounds, j));
return count < 3;
return true;
}
void core::add_bounds() {
@ -1566,6 +1570,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
bool run_grobner = need_run_grobner();
bool run_horner = need_run_horner();
bool run_bounded_nlsat = should_run_bounded_nlsat();
bool run_bounds = true; //m_nla_settings.branch_nl;
@ -1579,7 +1584,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
{
std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
std::function<void(void)> check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); };
std::function<void(void)> check3 = [&]() { if (no_effect()) add_bounds(); };
std::function<void(void)> check3 = [&]() { if (no_effect() && run_bounds) add_bounds(); };
std::pair<unsigned, std::function<void(void)>> checks[] =
{ {1, check1},
@ -1615,11 +1620,11 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
check_weighted(3, checks);
unsigned num_calls = lp_settings().stats().m_nla_calls;
if (!conflict_found() && m_nla_settings.run_nra && num_calls % 50 == 0 && num_calls > 500)
if (!conflict_found() && params().arith_nl_nra() && num_calls % 50 == 0 && num_calls > 500)
ret = bounded_nlsat();
}
if (l_vec.empty() && !done() && m_nla_settings.run_nra && ret == l_undef) {
if (l_vec.empty() && !done() && params().arith_nl_nra() && ret == l_undef) {
ret = m_nra.check();
m_stats.m_nra_calls++;
}
@ -1639,7 +1644,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
}
bool core::should_run_bounded_nlsat() {
if (!m_nla_settings.run_nra)
if (!params().arith_nl_nra())
return false;
if (m_nlsat_delay > m_nlsat_fails)
++m_nlsat_fails;

10
src/math/lp/nla_core.h
View file

@ -28,6 +28,7 @@
#include "math/lp/monomial_bounds.h"
#include "math/lp/nla_intervals.h"
#include "nlsat/nlsat_solver.h"
#include "smt/params/smt_params_helper.hpp"
namespace nra {
class solver;
@ -103,6 +104,7 @@ class core {
mutable lp::u_set m_active_var_set;
reslimit m_nra_lim;
smt_params_helper m_params;
bool m_use_nra_model = false;
nra::solver m_nra;
@ -118,7 +120,7 @@ class core {
public:
// constructor
core(lp::lar_solver& s, reslimit&);
core(lp::lar_solver& s, params_ref const& p, reslimit&);
void insert_to_refine(lpvar j);
void erase_from_to_refine(lpvar j);
@ -173,13 +175,15 @@ public:
lpvar var(const factor& f) const { return f.var(); }
smt_params_helper const & params() const { return m_params; }
// returns true if the combination of the Horner's schema and Grobner Basis should be called
bool need_run_horner() const {
return m_nla_settings.run_horner && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency == 0;
return params().arith_nl_horner() && lp_settings().stats().m_nla_calls % params().arith_nl_horner_frequency() == 0;
}
bool need_run_grobner() const {
return m_nla_settings.run_grobner; // && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0;
return params().arith_nl_grobner(); // && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0;
}
void set_active_vars_weights(nex_creator&);

24
src/math/lp/nla_grobner.cpp
View file

@ -25,7 +25,7 @@ namespace nla {
m_pdd_manager(m_core.m_lar_solver.number_of_vars()),
m_solver(m_core.m_reslim, m_pdd_manager),
m_lar_solver(m_core.m_lar_solver),
m_quota(m_core.m_nla_settings.grobner_quota*2)
m_quota(m_core.params().arith_nl_gr_q()*2)
{}
lp::lp_settings& grobner::lp_settings() {
@ -34,9 +34,9 @@ namespace nla {
void grobner::operator()() {
if (m_quota == 0) {
m_quota = 2*c().m_nla_settings.grobner_quota;
m_quota = 2*c().params().arith_nl_gr_q();
}
if (m_quota <= c().m_nla_settings.grobner_quota) {
if (m_quota <= c().params().arith_nl_gr_q()) {
++m_quota;
return;
}
@ -360,11 +360,11 @@ namespace nla {
struct dd::solver::config cfg;
cfg.m_max_steps = m_solver.equations().size();
cfg.m_max_simplified = c().m_nla_settings.grobner_max_simplified;
cfg.m_eqs_growth = c().m_nla_settings.grobner_eqs_growth;
cfg.m_expr_size_growth = c().m_nla_settings.grobner_expr_size_growth;
cfg.m_expr_degree_growth = c().m_nla_settings.grobner_expr_degree_growth;
cfg.m_number_of_conflicts_to_report = c().m_nla_settings.grobner_number_of_conflicts_to_report;
cfg.m_max_simplified = c().params().arith_nl_grobner_max_simplified();
cfg.m_eqs_growth = c().params().arith_nl_grobner_eqs_growth();
cfg.m_expr_size_growth = c().params().arith_nl_grobner_expr_size_growth();
cfg.m_expr_degree_growth = c().params().arith_nl_grobner_expr_degree_growth();
cfg.m_number_of_conflicts_to_report = c().params().arith_nl_grobner_cnfl_to_report();
m_solver.set(cfg);
m_solver.adjust_cfg();
m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
@ -470,9 +470,9 @@ namespace nla {
CTRACE("grobner", m_lar_solver.column_is_free(k) && k != j, tout << "skip " << k << "\n");
if (false && m_lar_solver.column_is_free(k) && k != j)
continue;
CTRACE("grobner", matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit,
CTRACE("grobner", matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit(),
tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";);
if (matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit)
if (matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit())
continue;
for (auto& rc : matrix.m_rows[row])
add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
@ -495,12 +495,12 @@ namespace nla {
while (!vars.empty()) {
j = vars.back();
vars.pop_back();
if (c().m_nla_settings.grobner_subs_fixed > 0 && c().var_is_fixed_to_zero(j)) {
if (c().params().arith_nl_grobner_subs_fixed() > 0 && c().var_is_fixed_to_zero(j)) {
r = m_pdd_manager.mk_val(val_of_fixed_var_with_deps(j, zero_dep));
dep = zero_dep;
return r;
}
if (c().m_nla_settings.grobner_subs_fixed == 1 && c().var_is_fixed(j))
if (c().params().arith_nl_grobner_subs_fixed() == 1 && c().var_is_fixed(j))
r *= val_of_fixed_var_with_deps(j, dep);
else if (!c().is_monic_var(j))
r *= m_pdd_manager.mk_var(j);

2
src/math/lp/nla_order_lemmas.cpp
View file

@ -19,7 +19,7 @@ typedef lp::lar_term term;
// a > b && c > 0 => ac > bc
void order::order_lemma() {
TRACE("nla_solver", );
if (!c().m_nla_settings.run_order) {
if (!c().params().arith_nl_order()) {
TRACE("nla_solver", tout << "not generating order lemmas\n";);
return;
}

28
src/math/lp/nla_settings.h
View file

@ -10,37 +10,9 @@ Author:
#pragma once
namespace nla {
struct nla_settings {
bool run_order = true;
bool run_tangents = true;
// horner fields
bool run_horner = true;
unsigned horner_frequency = 4;
unsigned horner_row_length_limit = 10;
unsigned horner_subs_fixed = 2;
// grobner fields
bool run_grobner = true;
unsigned grobner_row_length_limit = 50;
unsigned grobner_subs_fixed = 1;
unsigned grobner_eqs_growth = 10;
unsigned grobner_tree_size_growth = 2;
unsigned grobner_expr_size_growth = 2;
unsigned grobner_expr_degree_growth = 2;
unsigned grobner_max_simplified = 10000;
unsigned grobner_number_of_conflicts_to_report = 1;
unsigned grobner_quota = 0;
unsigned grobner_frequency = 4;
// nra fields
bool run_nra = false;
// expensive patching
bool expensive_patching = false;
nla_settings() {}
};
}

4
src/math/lp/nla_solver.cpp
View file

@ -57,8 +57,8 @@ namespace nla {
m_core->pop(n);
}
solver::solver(lp::lar_solver& s, reslimit& limit):
m_core(alloc(core, s, limit)) {
solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit):
m_core(alloc(core, s, p, limit)) {
}
bool solver::influences_nl_var(lpvar j) const {

2
src/math/lp/nla_solver.h
View file

@ -25,7 +25,7 @@ namespace nla {
core* m_core;
public:
solver(lp::lar_solver& s, reslimit& limit);
solver(lp::lar_solver& s, params_ref const& p, reslimit& limit);
~solver();
void add_monic(lpvar v, unsigned sz, lpvar const* vs);

2
src/math/lp/nla_tangent_lemmas.cpp
View file

@ -186,7 +186,7 @@ tangents::tangents(core * c) : common(c) {}
void tangents::tangent_lemma() {
factorization bf(nullptr);
const monic* m = nullptr;
if (c().m_nla_settings.run_tangents && c().find_bfc_to_refine(m, bf)) {
if (c().params().arith_nl_tangents() && c().find_bfc_to_refine(m, bf)) {
lpvar j = m->var();
tangent_imp tangent(point(val(bf[0]), val(bf[1])), c().val(j), *m, bf, *this);
tangent();

20
src/sat/smt/arith_internalize.cpp
View file

@ -61,29 +61,11 @@ namespace arith {
void solver::ensure_nla() {
if (!m_nla) {
m_nla = alloc(nla::solver, *m_solver.get(), m.limit());
m_nla = alloc(nla::solver, *m_solver.get(), s().params(), m.limit());
for (auto const& _s : m_scopes) {
(void)_s;
m_nla->push();
}
smt_params_helper prms(s().params());
m_nla->settings().run_order = prms.arith_nl_order();
m_nla->settings().run_tangents = prms.arith_nl_tangents();
m_nla->settings().run_horner = prms.arith_nl_horner();
m_nla->settings().horner_subs_fixed = prms.arith_nl_horner_subs_fixed();
m_nla->settings().horner_frequency = prms.arith_nl_horner_frequency();
m_nla->settings().horner_row_length_limit = prms.arith_nl_horner_row_length_limit();
m_nla->settings().run_grobner = prms.arith_nl_grobner();
m_nla->settings().run_nra = prms.arith_nl_nra();
m_nla->settings().grobner_subs_fixed = prms.arith_nl_grobner_subs_fixed();
m_nla->settings().grobner_eqs_growth = prms.arith_nl_grobner_eqs_growth();
m_nla->settings().grobner_expr_size_growth = prms.arith_nl_grobner_expr_size_growth();
m_nla->settings().grobner_expr_degree_growth = prms.arith_nl_grobner_expr_degree_growth();
m_nla->settings().grobner_max_simplified = prms.arith_nl_grobner_max_simplified();
m_nla->settings().grobner_number_of_conflicts_to_report = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching = false;
}
}

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

@ -59,7 +59,7 @@ def_module_params(module_name='smt',
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),
('arith.nl.order', BOOL, True, 'run order lemmas'),
('arith.nl.expp', BOOL, False, 'expensive patching'),

20
src/smt/theory_lra.cpp
View file

@ -267,7 +267,7 @@ class theory_lra::imp {
void ensure_nla() {
if (!m_nla) {
m_nla = alloc(nla::solver, *m_solver.get(), m.limit());
m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
for (auto const& _s : m_scopes) {
(void)_s;
m_nla->push();
@ -277,24 +277,6 @@ class theory_lra::imp {
return ctx().is_relevant(th.get_enode(u));
};
m_nla->set_relevant(is_relevant);
smt_params_helper prms(ctx().get_params());
m_nla->settings().run_order = prms.arith_nl_order();
m_nla->settings().run_tangents = prms.arith_nl_tangents();
m_nla->settings().run_horner = prms.arith_nl_horner();
m_nla->settings().horner_subs_fixed = prms.arith_nl_horner_subs_fixed();
m_nla->settings().horner_frequency = prms.arith_nl_horner_frequency();
m_nla->settings().horner_row_length_limit = prms.arith_nl_horner_row_length_limit();
m_nla->settings().run_grobner = prms.arith_nl_grobner();
m_nla->settings().run_nra = prms.arith_nl_nra();
m_nla->settings().grobner_subs_fixed = prms.arith_nl_grobner_subs_fixed();
m_nla->settings().grobner_eqs_growth = prms.arith_nl_grobner_eqs_growth();
m_nla->settings().grobner_expr_size_growth = prms.arith_nl_grobner_expr_size_growth();
m_nla->settings().grobner_expr_degree_growth = prms.arith_nl_grobner_expr_degree_growth();
m_nla->settings().grobner_max_simplified = prms.arith_nl_grobner_max_simplified();
m_nla->settings().grobner_number_of_conflicts_to_report = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching = false;
}
}