package libabsolute

  1. Overview
  2. Docs

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) => x in s

type 'a t =
  1. | Sat
    (*

    when s' = s

    *)
  2. | Unsat
    (*

    when s' = \emptyset

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

    filtered (s',b) : x \in s', b => p(x)

    *)
type feasible =
  1. | Unfeasible
  2. | Maybe
  3. | Witness of Csp.instance
val print : Stdlib.Format.formatter -> 'a t -> unit
val map : ('a -> 'b) -> 'a t -> 'b t
val bind : ('a -> bool -> 'b t) -> 'a t -> 'b t
val fold_and : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t

apply several filtering operation, with early termination when a unsatisfiable state is met

OCaml

Innovation. Community. Security.