package libabsolute

  1. Overview
  2. Docs

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 =
  1. | Int
  2. | Real

Types of variables

type decl = typ * string * Dom.t

declaration

type instance = Q.t Tools.VarMap.t

the instance type

type info =
  1. | Exact of Instance.t list
  2. | Unfeasible
  3. | Known of (Instance.t * bool) list

annotations to test the validity of the solver

type t = {
  1. variables : decl list;
  2. constraints : Constraint.t list;
  3. objective : Expr.t option;
  4. 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