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

use exponential decay with breaks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-26 10:21:46 -07:00
parent 62a8512401
commit e3b92fec82
2 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1708,13 +1708,14 @@ 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) {
double result = 0; int result = 0;
int breaks = 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 1
if (dtt_new == 0 && dtt_old != 0) if (dtt_new == 0 && dtt_old != 0)
result += 1; result += 1;
@ -1722,6 +1723,7 @@ namespace sls {
if (m_use_tabu && ctx.is_unit(lit)) if (m_use_tabu && ctx.is_unit(lit))
return 0; return 0;
result -= 1; result -= 1;
breaks += 1;
} }
#else #else
if (dtt_new == dtt_old) if (dtt_new == dtt_old)
@ -1736,9 +1738,10 @@ namespace sls {
if (result < 0) if (result < 0)
return 0.1; return 0.1;
else if (result == 0) else if (result == 0)
return 0.2; return 0.2;
else for (int i = m_prob_break.size(); i <= breaks; ++i)
return result; m_prob_break.push_back(pow(m_config.cb, -i));
return m_prob_break[breaks];
} }
template<typename num_t> template<typename num_t>

3
src/ast/sls/sls_arith_base.h
View file

@ -37,7 +37,7 @@ namespace sls {
typedef unsigned atom_t; typedef unsigned atom_t;
struct config { struct config {
double cb = 0.0; double cb = 2.85;
unsigned L = 20; unsigned L = 20;
unsigned t = 45; unsigned t = 45;
unsigned max_no_improve = 500000; unsigned max_no_improve = 500000;
@ -160,6 +160,7 @@ namespace sls {
bool m_use_tabu = true; bool m_use_tabu = true;
unsigned m_updates_max_size = 45; unsigned m_updates_max_size = 45;
arith_util a; arith_util a;
svector<double> m_prob_break;
void invariant(); void invariant();
void invariant(ineq const& i); void invariant(ineq const& i);