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
- 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 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