mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

adjust heuristic in random-inc-dec for finite domains

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-12 14:23:18 -08:00
parent 97acf71d2d
commit 9770c00592
1 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/sls/sls_arith_base.cpp
View file

@ -2578,6 +2578,7 @@ namespace sls {
return 0.0; return 0.0;
auto d = value.get_double(); auto d = value.get_double();
double score = 1.0 - ((d * d) / ((double)max_value * (double)max_value)); double score = 1.0 - ((d * d) / ((double)max_value * (double)max_value));
//score = 1.0 - d / max_value;
return score; return score;
} }
@ -2855,6 +2856,9 @@ namespace sls {
unsigned idx = ctx.rand() % m_updates.size(); unsigned idx = ctx.rand() % m_updates.size();
auto& [v, delta, score] = m_updates[idx]; auto& [v, delta, score] = m_updates[idx];
m_best_expr = m_vars[v].m_expr; m_best_expr = m_vars[v].m_expr;
if (false && !m_vars[v].m_finite_domain.empty())
m_best_value = m_vars[v].m_finite_domain[ctx.rand() % m_vars[v].m_finite_domain.size()];
else
m_best_value = value(v) + delta; m_best_value = value(v) + delta;
break; break;
} }
@ -2881,7 +2885,10 @@ namespace sls {
m_best_expr = e; m_best_expr = e;
if (a.is_int_real(e)) { if (a.is_int_real(e)) {
var_t v = mk_term(e); var_t v = mk_term(e);
if (ctx.rand(2) == 0) auto& vi = m_vars[v];
if (!vi.m_finite_domain.empty())
m_best_value = vi.m_finite_domain[ctx.rand() % vi.m_finite_domain.size()];
else if (ctx.rand(2) == 0)
m_best_value = value(v) + 1; m_best_value = value(v) + 1;
else else
m_best_value = value(v) - 1; m_best_value = value(v) - 1;