package libabsolute

  1. Overview
  2. Docs

Module Libabsolute.Result

This module defines solution of the abstract solver as covers

type 'a t = {
  1. sure : 'a list;
    (*

    elements that satisfy the constraints

    *)
  2. unsure : 'a list;
    (*

    elements that MAY satisfy the constraints

    *)
  3. nb_sure : int;
    (*

    size of sure list

    *)
  4. nb_unsure : int;
    (*

    size of unsure list

    *)
  5. vol_sure : float;
    (*

    volume of the elements in the sure list

    *)
  6. vol_unsure : float;
    (*

    volume of the elements in the unsure list

    *)
  7. nb_steps : int;
    (*

    number of steps of the solving process

    *)
  8. best_value : Q.t;
    (*

    best value found during the optimization

    *)
}

The type of cover where sure is an under-approximation of the solution set and the union of sure and unsure is an over-approximaton of the solution set

val empty : 'a t

empty result

val inner_ratio : 'a t -> float

computes the inner ratio (between 0 and 1) of a solution

val add_inner : 'a t -> 'a -> 'a t

adds an inner element to a result

val add_outer : 'a t -> 'a -> 'a t

adds an outer element to a result

val print : Format.formatter -> 'a t -> unit

printer