mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

setup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-22 15:19:40 +03:00
parent b02b0cf31f
commit 9579064671
2 changed files with 22 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/lp_params_helper.pyg
View file

@ -9,6 +9,5 @@ def_module_params(module_name='lp',
('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'), ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'), ('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
('enable_relevancy', BOOL, False, 'enable relevancy propagation to filter emons (experiment)')
)) ))

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

@ -163,16 +163,18 @@ rational core::product_value(const monic& m) const {
// return true iff the monic value is equal to the product of the values of the factors // return true iff the monic value is equal to the product of the values of the factors
// or if the variable associated with the monomial is not relevant. // or if the variable associated with the monomial is not relevant.
bool core::check_monic(const monic& m) const { bool core::check_monic(const monic& m) const {
#if 0
// TODO test this // TODO test this
if (!is_relevant(m.var())) if (lp_settings().m_enable_relevancy && !is_relevant(m.var()))
return true; return true;
#endif
if (lra.column_is_int(m.var()) && !lra.get_column_value(m.var()).is_int()) if (lra.column_is_int(m.var()) && !lra.get_column_value(m.var()).is_int())
return true; return true;
bool ret = product_value(m) == lra.get_column_value(m.var()).x; bool ret = product_value(m) == lra.get_column_value(m.var()).x;
CTRACE(nla_solver_check_monic, !ret, print_monic(m, tout) << '\n';); CTRACE(nla_solver_check_monic, !ret, print_monic(m, tout) << '\n';);
if (!ret) {
// check if m.var() actually occurs in lra.constraints()...
}
return ret; return ret;
} }
@ -1343,24 +1345,29 @@ lbool core::check() {
if (no_effect()) if (no_effect())
m_divisions.check(); m_divisions.check();
if (no_effect())
m_order.order_lemma();
if (no_effect()) { if (no_effect()) {
std::function<void(void)> check1 = [&]() { m_order.order_lemma();
};
std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma();
};
std::function<void(void)> check3 = [&]() { m_tangents.tangent_lemma();
};
std::pair<unsigned, std::function<void(void)>> checks[] =
{ { 6, check1 },
{ 2, check2 },
{ 1, check3 }};
check_weighted(3, checks);
unsigned num_calls = lp_settings().stats().m_nla_calls; unsigned num_calls = lp_settings().stats().m_nla_calls;
if (!conflict_found() && params().arith_nl_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(); ret = bounded_nlsat();
// both tangent and monotonicity are expensive
std::function<void(void)> check1 = [&]() { m_monotone.monotonicity_lemma();
};
std::function<void(void)> check2 = [&]() { m_tangents.tangent_lemma();
};
std::pair<unsigned, std::function<void(void)>> checks[] =
{
{ 2, check1 },
{ 1, check2 }};
check_weighted(2, checks);
} }
if (no_effect() && params().arith_nl_nra()) { if (no_effect() && params().arith_nl_nra()) {