lutin 2.71.15 · OCaml Package

Lucky Boolean and numeric expressions.

type ext_func_name = string

type ext_func_type = Type.t list

type ext_lib_name = string

type ext_func_tbl = (ext_func_type * (ext_lib_name * Ezdl.t)) Util.StringMap.t

type t =

| Formu of formula
| Numer of num
| Liste of simple_tbl
(*
struct and arrays are flattened in such a list
*)

and formula =

| And of formula * formula
| Or of formula * formula
| Xor of formula * formula
| NXor of formula list
| Nor of formula list
| Diese of formula list
| Impl of formula * formula
| IteB of formula * formula * formula
| Not of formula
| EqB of formula * formula
| True
| False
| Bvar of var
| Eq of num * num
| Sup of num * num
| SupEq of num * num
| Inf of num * num
| InfEq of num * num

and var = t Var.t

and func_call_arg = string * Ezdl.cfunc * ext_func_type * ext_lib_name * t list

and num =

| Sum of num * num
| Diff of num * num
| Prod of num * num
| Quot of num * num
| Mod of num * num
| Div of num * num
| Uminus of num
| Inf_int
| Ival of Num.num
| Fval of float
| Ivar of var
| Fvar of var
| FFC of func_call_arg
| IFC of func_call_arg
| Gcont of num * num * num
| Gstop of num * num * num
| Icont of num * num * num
| Istop of num * num * num
| Ite of formula * num * num

and simple =

| Fo of formula
| Nu of num

and simple_tbl = simple Util.StringMap.t

val ext_func_tbl_to_string : ext_func_tbl -> string

type weight =

| Wint of int
| Wexpr of num
| Infinity

A weight can be an integer, or a integer expression that depends only on inputs and memories.

val weight_to_string : weight -> string

type var_tbl = var Util.StringMap.t

val add_value : string -> simple -> simple_tbl -> simple_tbl

val add_var : string -> var -> var_tbl -> var_tbl

val empty_var_tbl : var Util.StringMap.t

val empty_simple_tbl : simple Util.StringMap.t

val remove_prefix : string -> string -> string -> string

remove from a string everything that is before the first "." or the first "". This is useful to go to var_tbl indexes (which depends on the var name) to simple_tbl indexes (which depend only on the type).

package lutin