Module Libabsolute.Consistency

This module provides types and operations for handling consistencies. A consitency is a property obtained after a filtering operation f(s,p): given an abstract value s, and a predicate p, it computes a set s' \subseteq s such that : \forall x \in s, p(x) \implies x \in s'

type 'a t =
  1. | Sat
    (*

    when s' = s

    *)
  2. | Unsat
    (*

    when s' = \emptyset

    *)
  3. | Filtered of 'a * bool
    (*

    filtered (s',b) : \forall x \in s', b \implies p(x)

    *)
  4. | Pruned of {
    1. sure : 'a list;
    2. unsure : 'a list;
    }
type feasible =
  1. | Unfeasible
  2. | Maybe
  3. | Witness of Csp.instance
val print : Stdlib.Format.formatter -> 'a t -> unit
val map : ('a -> 'b) -> 'c t -> 'd t
val bind : ('a -> bool -> 'b t) -> 'c t -> 'b t