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 dimensions : t -> int

returns the number of variables of a csp

val 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 sat : t -> Instance.t -> bool

Evaluates the CSP at the given point, i.e true iff all constraints are satisfied

  • raises [Invalid_arg]

    if a division by zero occurs or if an exponentitation by a non integer exponant is made.

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 : Stdlib.Format.formatter -> typ -> unit
val pp_decl : Stdlib.Format.formatter -> (typ * string * Dom.t) -> unit
val pp_declarations : Stdlib.Format.formatter -> (typ * string * Dom.t) list -> unit
val pp_constraints : Stdlib.Format.formatter -> Constraint.t list -> unit
val print : Stdlib.Format.formatter -> t -> unit
val to_graphviz : t -> string -> unit