smooth.c File Reference

#include "allocate.h"
#include "internal.h"
#include "logging.h"

Include dependency graph for smooth.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	kissat_init_smooth (kissat *solver, smooth *smooth, int window, const char *name)
void	kissat_update_smooth (kissat *solver, smooth *smooth, double y)

Function Documentation

kissat_init_smooth()

ABC_NAMESPACE_IMPL_START void kissat_init_smooth	(	kissat *	solver,
		smooth *	smooth,
		int	window,
		const char *	name )

Definition at line 7 of file smooth.c.

                                           {
  KISSAT_assert (window > 0);
  const double alpha = 1.0 / window;
  LOG ("initialized %s EMA alpha %g window %d", name, alpha, window);
  smooth->value = 0;
  smooth->biased = 0;
  smooth->alpha = alpha;
  smooth->beta = 1.0 - alpha;
  KISSAT_assert (smooth->beta > 0);
  smooth->exp = 1.0;
#ifdef LOGGING
  smooth->name = name;
  smooth->updated = 0;
#else
  (void) solver;
  (void) name;
#endif
}

kissat_update_smooth()

void kissat_update_smooth	(	kissat *	solver,
		smooth *	smooth,
		double	y )

Definition at line 27 of file smooth.c.

                                                                     {
#ifdef LOGGING
  smooth->updated++;
  const double old_value = smooth->value;
#endif
  const double old_biased = smooth->biased;
  const double alpha = smooth->alpha;
  const double beta = smooth->beta;
  const double delta = y - old_biased;
  const double scaled_delta = alpha * delta;
  const double new_biased = old_biased + scaled_delta;
  LOG ("update %" PRIu64 " of biased %s EMA %g with %g (delta %g) "
       "yields %g (scaled delta %g)",
       smooth->updated, smooth->name, old_biased, y, delta, new_biased,
       scaled_delta);
  smooth->biased = new_biased;
  double old_exp = smooth->exp;
  double new_exp, div, new_value;
  if (old_exp) {
    new_exp = old_exp * beta;
    KISSAT_assert (new_exp < 1);
    if (new_exp == old_exp) {
      new_exp = 0;
      new_value = new_biased;
#ifdef LOGGING
      div = 1;
#endif
    } else {
      div = 1 - new_exp;
      KISSAT_assert (div > 0);
      new_value = new_biased / div;
    }
    smooth->exp = new_exp;
  } else {
    new_value = new_biased;
#ifdef LOGGING
    new_exp = 0;
    div = 1;
#endif
  }
  smooth->value = new_value;
  LOG ("update %" PRIu64 " of corrected %s EMA %g "
       "with %g (delta %g) yields %g (exponent %g, div %g)",
       smooth->updated, smooth->name, old_value, y, delta, new_value,
       new_exp, div);
#ifndef LOGGING
  (void) solver;
#endif
}