Libabsolute is a constraint solving library based on abstract domains
module Csp : sig ... endThis module defines the main types used for the constraint language of AbSolute, along with the type of problems, and instance.
module Constraint : sig ... endThis module defines the constraint language, and some basic operations over it
module Expr : sig ... endThis module defines the numerical language and some basic operations over it
module Dom : sig ... endThis module defines the different kinds of definition domains of variables
module Instance : sig ... endThis module defines the type of points (also called instances), i.e mappings from variables to rational coordinates.
module Parser : sig ... endThis module defines several parsing utilities
module Signature : sig ... endModule signature for Abstract Domains for Constraint Programming (ADCP) they must feature consistency, split and precision operators.
module Domains : sig ... endThis module handle the domain environment, already equipped with some basic domains. You can add your own using the register_* functions, and combine them with the already defined ones.
module Solver : sig ... endFunctor parametrized by an abstract domain and defines the three main solving functions
module Consistency : sig ... endThis 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
module Result : sig ... endThis module defines solution of the abstract solver as covers
module Constant : sig ... endmodule Ring : sig ... endmodule Q : sig ... endRational arithmetic module
module F : sig ... endFloat arithmetic module
module I : sig ... endInteger arithmetic module
module Polynom : sig ... endModule for polynomials over an abstract arithmetic rings
module Tools : sig ... endThis module defines diverse utilities
module Kleene : sig ... endThis module implements a 3-valued logic