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

use reward as proxy for score

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-26 09:30:38 -07:00
parent cd92b38697
commit 2549a2cf07
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1708,12 +1708,13 @@ namespace sls {
template<typename num_t> template<typename num_t>
double arith_base<num_t>::compute_score(var_t x, num_t const& delta) { double arith_base<num_t>::compute_score(var_t x, num_t const& delta) {
int result = 0; double result = 0;
for (auto const& [coeff, bv] : m_vars[x].m_bool_vars) { for (auto const& [coeff, bv] : m_vars[x].m_bool_vars) {
bool old_sign = sign(bv); bool old_sign = sign(bv);
auto lit = sat::literal(bv, old_sign); auto lit = sat::literal(bv, old_sign);
auto dtt_old = dtt(old_sign, *atom(bv)); auto dtt_old = dtt(old_sign, *atom(bv));
auto dtt_new = dtt(old_sign, *atom(bv), coeff, delta); auto dtt_new = dtt(old_sign, *atom(bv), coeff, delta);
#if 0
if (dtt_new == 0 && dtt_old != 0) if (dtt_new == 0 && dtt_old != 0)
result += 1; result += 1;
@ -1722,6 +1723,14 @@ namespace sls {
return 0; return 0;
result -= 1; result -= 1;
} }
#else
if (dtt_new == dtt_old)
continue;
if (m_use_tabu && ctx.is_unit(lit) && dtt_new != 0)
return 0;
double reward = ctx.reward(bv);
result += reward;
#endif
} }
if (result < 0) if (result < 0)