package libabsolute

You can search for identifiers within the package.

in-package search v0.2.0

libabsolute
- Libabsolute
  - Consistency
  - Constant
  - Constraint
  - Csp
  - Dom
  - Domains
    
    ApronBox
    
    B
    
    Make
    
    N
    
    Boolean
    
    Make
    
    N
    
    BoxF
    
    BoxS
    
    D1
    
    Make
    
    D
    
    D2
    
    Make
    
    A
    
    B
    
    Oct
    
    Poly
    
    Product
    
    Make
    
    A
    
    B
    
    Utree
    
    Make
    
    N
  - Expr
  - F
  - I
  - Instance
  - Kleene
  - Parser
  - Polynom
    
    Float
    
    Int
    
    Make
    
    R
    
    Rational
  - Q
  - Result
  - Ring
    
    T
  - Signature
    
    Domain
    
    Numeric
  - Solver
    
    Make
    
    D
  - Tools
    
    VarMap
    
    VarSet

Legend:
Library
Module
Module type
Parameter
Class
Class type

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 =

| Sat
(*
when s' = s
*)
| Unsat
(*
when s' = \emptyset
*)
| Filtered of 'a * bool
(*
filtered (s',b) : x \in s', b => p(x)
*)

type feasible =

| Unfeasible
| Maybe
| Witness of Csp.instance

val print : 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