package libabsolute

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Types
Accessors
Constructors
Operations
Printing

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

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Libabsolute.Csp`

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

Types

type typ =

| Int
| Real

Types of variables

type decl = typ * string * Dom.t

declaration

type instance = Q.t Tools.VarMap.t

the instance type

type info =

| Exact of Instance.t list
| Unfeasible
| Known of (Instance.t * bool) list

annotations to test the validity of the solver

type t = {

variables : decl list;
constraints : Constraint.t list;
objective : Expr.t option;
solutions : info option;

}

type of constraint satisfaction problems

Accessors

val get_var_names : t -> string list

returns list of all variable names

Constructors

val empty : t

empty problem, with no variables and no constraints

val initialize : (typ * string * Dom.t) list -> t

initalizes and unconstrained CSP

val add_real_var : string -> Q.t -> Q.t -> t -> t

adds a real variable in the csp

val add_real_var_f : string -> float -> float -> t -> t

adds a real variable in the csp, with float bounds

val add_int_var : string -> Q.t -> Q.t -> t -> t

adds an integer variable in the csp

val add_int_var_i : string -> int -> int -> t -> t

adds an integer variable in the csp with integer bounds

val add_constr : t -> Constraint.t -> t

adds a constraint to the csp

Operations

val fix_var : t -> string -> Q.t -> t

fix_var csp var cst builds a new csp identical to the csp where all the occurences of the variable var are replaced by the constant cst, and where the variables v is removed from the csp variables.

Printing

val pp_typ : Format.formatter -> typ -> unit

val pp_declarations : Format.formatter -> (typ * string * Dom.t) list -> unit

val pp_constraints : Format.formatter -> Constraint.t list -> unit

val print : Format.formatter -> t -> unit