From 2549a2cf07342aae089699fa9594c6ab409b0d76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Aug 2024 09:30:38 -0700 Subject: [PATCH] use reward as proxy for score Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 56b1af73e..d19e9c19a 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -1708,12 +1708,13 @@ namespace sls { template double arith_base::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) { bool old_sign = sign(bv); auto lit = sat::literal(bv, old_sign); auto dtt_old = dtt(old_sign, *atom(bv)); auto dtt_new = dtt(old_sign, *atom(bv), coeff, delta); +#if 0 if (dtt_new == 0 && dtt_old != 0) result += 1; @@ -1722,6 +1723,14 @@ namespace sls { return 0; 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)