package libabsolute

  1. Overview
  2. Docs

Libabsolute is a constraint solving library based on abstract domains

Core constraint language

module Csp : sig ... end

This module defines the main types used for the constraint language of AbSolute, along with the type of problems, and instance.

module Constraint : sig ... end

This module defines the constraint language, and some basic operations over it

module Expr : sig ... end

This module defines the numerical language and some basic operations over it

module Dom : sig ... end

This module defines the different kinds of definition domains of variables

module Instance : sig ... end

This module defines the type of points (also called instances), i.e mappings from variables to rational coordinates.

module Parser : sig ... end

This module defines several parsing utilities

Solver parametrization

module Signature : sig ... end

Module signature for Abstract Domains for Constraint Programming (ADCP) they must feature consistency, split and precision operators.

module Domains : sig ... end

This 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 ... end

Functor parametrized by an abstract domain and defines the three main solving functions

module Consistency : sig ... end

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

module Result : sig ... end

This module defines solution of the abstract solver as covers

module Constant : sig ... end

Arithmetic modules

module Ring : sig ... end
module Q : sig ... end

Rational arithmetic module

module F : sig ... end

Float arithmetic module

module I : sig ... end

Integer arithmetic module

module Polynom : sig ... end

Module for polynomials over an abstract arithmetic rings

Miscellaneous

module Tools : sig ... end

This module defines diverse utilities

module Kleene : sig ... end

This module implements a 3-valued logic

OCaml

Innovation. Community. Security.