Theory IsaSAT_EMA
theory IsaSAT_EMA
imports IsaSAT_Literals
begin
section ‹Moving averages›
definition EMA_FIXPOINT_SIZE :: ‹nat› where
‹EMA_FIXPOINT_SIZE = 32›
text ‹We use (at least hopefully) the variant of EMA-14 implemented in Cadical, but with fixed-point
calculations (\<^term>‹1 :: nat› is \<^term>‹(1 :: nat) >> EMA_FIXPOINT_SIZE›).
Remark that the coefficient \<^term>‹β› already should take care of the fixed-point conversion of the glue.
Otherwise, \<^term>‹value› is wrongly updated.
›
type_synonym ema = ‹64 word × 64 word × 64 word × 64 word × 64 word›
definition ema_bitshifting where
‹ema_bitshifting = (1 << EMA_FIXPOINT_SIZE)›
definition EMA_MULT_SHIFT :: ‹nat› where
‹EMA_MULT_SHIFT = 8›
text ‹TODO: some precision is lost here in the difference calculation.›
definition (in -) ema_update :: ‹nat ⇒ ema ⇒ ema› where
‹ema_update = (λlbd (value, α, β, wait, period).
let lbd = (of_nat lbd) * ema_bitshifting in
let value = if lbd > value
then value + ((β >> (EMA_FIXPOINT_SIZE - EMA_MULT_SHIFT)) * ((lbd - value) >> EMA_MULT_SHIFT))
else value - ((β >> (EMA_FIXPOINT_SIZE - EMA_MULT_SHIFT)) * ((value - lbd) >> EMA_MULT_SHIFT))
in
let wait = wait - 1 in
if β ≤ α ∨ wait > 0 then (value, α, β, wait, period)
else
let wait = 2 * (period+1)-1 in
let period = wait in
let β = β >> 1 in
let β = if β < α then α else β in
(value, α, β, wait, period))›
definition (in -) ema_init :: ‹64 word ⇒ ema› where
‹ema_init α = (0, α >> (EMA_FIXPOINT_SIZE - 32), ema_bitshifting, 1, 0)›
fun ema_reinit where
‹ema_reinit (value, α, β, wait, period) = (value, α, ema_bitshifting, 1, 0)›
fun ema_get_value :: ‹ema ⇒ 64 word› where
‹ema_get_value (v, _) = v›
:: ‹ema ⇒ 64 word› where
‹ema_extract_value (v, _) = v >> EMA_FIXPOINT_SIZE›
text ‹We use the default values for Cadical: \<^term>‹(3 / 10 ^2)› and \<^term>‹(1 / 10 ^ 5)› in our fixed-point
version.
›
value ‹((3 :: 64 word) << EMA_FIXPOINT_SIZE) >> (15)›
value ‹((4 :: 64 word) << EMA_FIXPOINT_SIZE >> 7)›
abbreviation ema_fast_init :: ema where
‹ema_fast_init ≡ ema_init (128849010)›
abbreviation ema_slow_init :: ema where
‹ema_slow_init ≡ ema_init (429450)›
text ‹Small test below. It was useful once to detect an overflow that lead to very bad
initialisation behaviour.›
value ‹let α = shiftr 128849010 (EMA_FIXPOINT_SIZE - 32);
x = (((ema_update 10)^^ 400) (7 * ema_bitshifting, α, ema_bitshifting, 1, 0))
in (ema_extract_value x, ema_get_value x, x)›
end