PPL  0.12.1
Parma_Polyhedra_Library::Weightwatch_Traits Struct Reference

Traits class for the deterministic timeout mechanism. More...

#include <globals.defs.hh>

List of all members.

Public Types

typedef unsigned long long Threshold
 The type used to specify thresholds for computational weight.
typedef unsigned long long Delta
 The type used to specify increments of computational weight.

Static Public Member Functions

static const Thresholdget ()
 Returns the current computational weight.
static bool less_than (const Threshold &a, const Threshold &b)
 Compares the two weights a and b.
static Delta compute_delta (unsigned long unscaled, unsigned scale)
 Computes a Delta value from unscaled and scale.
static void from_delta (Threshold &threshold, const Delta &delta)
 Sets threshold to be delta units bigger than the current weight.

Static Public Attributes

static Threshold weight = 0
 The current computational weight.
static void(* check_function )(void)
 A pointer to the function that has to be called when checking the reaching of thresholds.

Detailed Description

Traits class for the deterministic timeout mechanism.

This abstract base class should be instantiated by those users willing to provide a polynomial upper bound to the time spent by any invocation of a library operator.

Definition at line 105 of file globals.defs.hh.


Member Typedef Documentation

The type used to specify increments of computational weight.

Definition at line 110 of file globals.defs.hh.

The type used to specify thresholds for computational weight.

Definition at line 107 of file globals.defs.hh.


Member Function Documentation

Weightwatch_Traits::Delta Parma_Polyhedra_Library::Weightwatch_Traits::compute_delta ( unsigned long  unscaled,
unsigned  scale 
)
inlinestatic

Computes a Delta value from unscaled and scale.

Returns:
$u \cdot 2^s$, where $u$ is the value of unscaled and $s$ is the value of scale.
Parameters:
unscaledThe value of delta before scaling.
scaleThe scaling to be applied to unscaled.

Definition at line 57 of file globals.inlines.hh.

                                                                        {
  if ((std::numeric_limits<Delta>::max() >> scale) < unscaled)
    throw std::invalid_argument("PPL::Weightwatch_Traits::"
                                "compute_delta(u, s):\n"
                                "values of u and s cause wrap around.");
  return static_cast<Delta>(unscaled) << scale;
}
void Parma_Polyhedra_Library::Weightwatch_Traits::from_delta ( Threshold threshold,
const Delta delta 
)
inlinestatic

Sets threshold to be delta units bigger than the current weight.

Definition at line 66 of file globals.inlines.hh.

References weight.

                                                                       {
  threshold = weight + delta;
}

Returns the current computational weight.

Definition at line 47 of file globals.inlines.hh.

References weight.

                        {
  return weight;
}
bool Parma_Polyhedra_Library::Weightwatch_Traits::less_than ( const Threshold a,
const Threshold b 
)
inlinestatic

Compares the two weights a and b.

Definition at line 52 of file globals.inlines.hh.

References sizeof_to_bits.

                                                                    {
  return b - a < (1ULL << (sizeof_to_bits(sizeof(Threshold)) - 1));
}

Member Data Documentation

A pointer to the function that has to be called when checking the reaching of thresholds.

The pointer can be null if no thresholds are set.

Definition at line 144 of file globals.defs.hh.

Referenced by Parma_Polyhedra_Library::maybe_abandon().


The documentation for this struct was generated from the following files: