Source file poly.ml

(* File generated from poly.idl *)

type tbool =
  | Bottom
  | True
  | False
  | Top
and t
and equation =  Matrix.equation = {
  var : int;
  expr : Vector.t
}

(* Constructors *)
external empty : int -> t
	= "camlidl_poly_poly_empty"

let dummy = empty 0
external universe : int -> t
	= "camlidl_poly_poly_universe"

external of_constraints : Matrix.t -> t
	= "camlidl_poly_poly_of_constraints"

external of_frames : Matrix.t -> t
	= "camlidl_poly_poly_of_frames"

external minimize : t -> unit
	= "camlidl_poly_poly_minimize"

external canonicalize : t -> unit
	= "camlidl_poly_poly_canonicalize"

(* Access functions *)
external dim : t -> int
	= "camlidl_poly_poly_dim"

external nbequations : t -> int
	= "camlidl_poly_poly_nbequations"

external nblines : t -> int
	= "camlidl_poly_poly_nblines"

external nbconstraints : t -> int
	= "camlidl_poly_poly_nbconstraints"

external nbframes : t -> int
	= "camlidl_poly_poly_nbframes"

 
external constraints : t -> Matrix.t option = "camlidl_polka_poly_constraints" 
external frames : t -> Matrix.t option = "camlidl_polka_poly_frames" 

(* Tests *)
external is_minimal : t -> bool
	= "camlidl_poly_poly_is_minimal"

external is_empty : t -> bool
	= "camlidl_poly_poly_is_empty"

external is_universe : t -> bool
	= "camlidl_poly_poly_is_universe"

external is_empty_lazy : t -> tbool
	= "camlidl_poly_poly_is_empty_lazy"

external is_universe_lazy : t -> tbool
	= "camlidl_poly_poly_is_universe_lazy"

external constraints_available : t -> bool
	= "camlidl_poly_poly_constraints_available"

external frames_available : t -> bool
	= "camlidl_poly_poly_frames_available"

external poly_versus_constraint : t -> Vector.t -> tbool
	= "camlidl_poly_poly_poly_versus_constraint"

external is_generator_included_in : Vector.t -> t -> bool
	= "camlidl_poly_poly_is_generator_included_in"

external is_included_in : t -> t -> bool
	= "camlidl_poly_poly_is_included_in"

external is_equal : t -> t -> bool
	= "camlidl_poly_poly_is_equal"

(* Change of dimensions *)
external add_dims_and_embed : t -> int -> t
	= "camlidl_poly_poly_add_dims_and_embed"

external add_dims_and_project : t -> int -> t
	= "camlidl_poly_poly_add_dims_and_project"

external del_dims : t -> int -> t
	= "camlidl_poly_poly_del_dims"

external add_dims_and_embed_multi : t -> Vector.dimsup array -> t
	= "camlidl_poly_poly_add_dims_and_embed_multi"

external add_dims_and_project_multi : t -> Vector.dimsup array -> t
	= "camlidl_poly_poly_add_dims_and_project_multi"

external del_dims_multi : t -> Vector.dimsup array -> t
	= "camlidl_poly_poly_del_dims_multi"

external add_permute_dims_and_embed : t -> int -> int array -> t
	= "camlidl_poly_poly_add_permute_dims_and_embed"

external add_permute_dims_and_project : t -> int -> int array -> t
	= "camlidl_poly_poly_add_permute_dims_and_project"

external permute_del_dims : t -> int -> int array -> t
	= "camlidl_poly_poly_permute_del_dims"

(* Intersection and convex hull *)
external inter_array : t array -> t
	= "camlidl_poly_poly_inter_array"

external inter : t -> t -> t
	= "camlidl_poly_poly_inter"

external add_constraints : t -> Matrix.t -> t
	= "camlidl_poly_poly_add_constraints"

external add_constraint : t -> Vector.t -> t
	= "camlidl_poly_poly_add_constraint"

external union_array : t array -> t
	= "camlidl_poly_poly_union_array"

external union : t -> t -> t
	= "camlidl_poly_poly_union"

external add_frames : t -> Matrix.t -> t
	= "camlidl_poly_poly_add_frames"

external add_frame : t -> Vector.t -> t
	= "camlidl_poly_poly_add_frame"

external inter_array_lazy : t array -> t
	= "camlidl_poly_poly_inter_array_lazy"

external inter_lazy : t -> t -> t
	= "camlidl_poly_poly_inter_lazy"

external add_constraints_lazy : t -> Matrix.t -> t
	= "camlidl_poly_poly_add_constraints_lazy"

external add_constraint_lazy : t -> Vector.t -> t
	= "camlidl_poly_poly_add_constraint_lazy"

external union_array_lazy : t array -> t
	= "camlidl_poly_poly_union_array_lazy"

external union_lazy : t -> t -> t
	= "camlidl_poly_poly_union_lazy"

external add_frames_lazy : t -> Matrix.t -> t
	= "camlidl_poly_poly_add_frames_lazy"

external add_frame_lazy : t -> Vector.t -> t
	= "camlidl_poly_poly_add_frame_lazy"

 
let inter_list l = inter_array (Array.of_list l) 
let union_list l = union_array (Array.of_list l) 
let inter_list_lazy l = inter_array_lazy (Array.of_list l) 
let union_list_lazy l = union_array_lazy (Array.of_list l) 

(* Linear transformation *)
external assign_var : t -> int -> Vector.t -> t
	= "camlidl_poly_poly_assign_var"

external substitute_var : t -> int -> Vector.t -> t
	= "camlidl_poly_poly_substitute_var"

external assign_vars : t -> equation array -> t
	= "camlidl_poly_poly_assign_vars"

external substitute_vars : t -> equation array -> t
	= "camlidl_poly_poly_substitute_vars"

(* Widening *)
external widening : t -> t -> t
	= "camlidl_poly_poly_widening"

external limited_widening : t -> t -> Matrix.t -> t
	= "camlidl_poly_poly_limited_widening"

(* Closure *)
external closure : t -> t
	= "camlidl_poly_poly_closure"

external closure_lazy : t -> t
	= "camlidl_poly_poly_closure_lazy"

 
let print_constraints assoc formatter poly = 
if is_empty_lazy poly = True then 
Format.fprintf formatter "empty(%i)" (dim poly) 
else 
match (constraints poly) with 
| Some(cons) -> (Matrix.print_constraints assoc) formatter cons 
| None -> Format.fprintf formatter "constraints not available(%i)" 
(dim poly) 
let print_frames assoc formatter poly = 
if is_empty_lazy poly = True then 
Format.fprintf formatter "empty(%i)" (dim poly) 
else 
match (frames poly) with 
| Some(frames) -> (Matrix.print_frames assoc) formatter frames 
| None -> Format.fprintf formatter "frames not available(%i)" 
(dim poly) 

let print assoc formatter poly = 
if is_empty_lazy poly = True then 
Format.fprintf formatter "empty(%i)" (dim poly) 
else begin 
Format.fprintf formatter "(@[<v>%a,@ %a@])"  
(print_constraints assoc) poly        
(print_frames assoc) poly 
end 

let of_lconstraints assoc dim lstr = 
of_constraints (Matrix.of_lconstraints assoc dim lstr) 

let of_lframes assoc dim lstr = 
of_frames (Matrix.of_lframes assoc dim lstr)