1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
nla_backoff.h
Abstract:
Scheduling policies for expensive nonlinear engines.
Author:
Lev Nachmanson (levnach)
--*/
#pragma once
#include <algorithm>
namespace nla {
// Exponential backoff: on success re-engage, otherwise double the delay
// until the next run.
class backoff {
unsigned m_delay = 0;
unsigned m_delay_bound = 0;
public:
void set_delay_bound(unsigned b) { m_delay_bound = b; }
// counts the delay down; the engine runs when it is exhausted
bool should_run() {
if (m_delay > 0)
--m_delay;
return m_delay < 2;
}
void update(bool success) {
if (success)
m_delay_bound /= 2;
else if (m_delay_bound < (1u << 20))
m_delay_bound = std::max(2 * m_delay_bound, 1u);
m_delay = m_delay_bound;
}
};
// Schedules the eager bound squeeze: eager while it improves bounds,
// disabled after too many squeezes without check() finding nothing to refine.
class squeeze_schedule {
unsigned m_fail_streak = 0; // consecutive fruitless squeezes
unsigned m_squeezes_since_sat_check = 0; // squeezes since check() last found nothing to refine
public:
bool enabled() const { return m_squeezes_since_sat_check < 50; }
bool eager() const { return m_fail_streak < 3; }
void on_squeeze(bool improved_bounds) {
++m_squeezes_since_sat_check;
if (improved_bounds)
m_fail_streak = 0;
else
++m_fail_streak;
}
void on_nothing_to_refine() { m_squeezes_since_sat_check /= 2; }
};
}