libapron-ocaml-dev 0.9.10-6 / usr / lib / ocaml / apron / abstract1.idl

/* -*- mode: c -*- */

/* This file is part of the APRON Library, released under LGPL license.
   Please read the COPYING file packaged in the distribution  */


quote(C, "\n\
#include <limits.h>\n\
#include \"ap_expr0.h\"\n\
#include \"ap_abstract0.h\"\n\
#include \"ap_environment.h\"\n\
#include \"ap_expr1.h\"\n\
#include \"ap_abstract1.h\"\n\
#include \"caml/callback.h\"\n\
#include \"apron_caml.h\"\n\
")

import "scalar.idl";
import "interval.idl";
import "coeff.idl";
import "dim.idl";
import "linexpr0.idl";
import "lincons0.idl";
import "generator0.idl";
import "manager.idl";
import "abstract0.idl";
import "environment.idl";
import "linexpr1.idl";
import "lincons1.idl";
import "generator1.idl";
import "texpr1.idl";
import "tcons1.idl";

struct ap_abstract1_t {
  [mlname(mutable_abstract0)] ap_abstract0_ptr abstract0;
  [mlname(mutable_env)] ap_environment_ptr env;
};
quote(MLMLI,"(** APRON Abstract values of level 1 *)")
quote(MLMLI,"(** The type parameter ['a] allows to distinguish abstract values with different underlying abstract domains. *)\n")

quote(MLMLI,"type box1 = { mutable interval_array : Interval.t array; mutable box1_env : Environment.t }")

quote(MLMLI,"(* ********************************************************************** *)")
quote(MLMLI,"(** {2 General management} *)")
quote(MLMLI,"(* ********************************************************************** *)")

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Memory} *)")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"\n\
(** Copy a value *)
val copy : 'a Manager.t -> 'a t -> 'a t\n\
\n\
(** Return the abstract size of a value *)
val size : 'a Manager.t -> 'a t -> int\n\
")
quote(ML,"\n\
let copy man x = { abstract0 = Abstract0.copy man x.abstract0; env = x.env }\n\
let size man x = Abstract0.size man x.abstract0\n\
")

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Control of internal representation} *)")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"\n\
(** Minimize the size of the representation of the value. This may result in a later recomputation of internal information.*)
val minimize : 'a Manager.t -> 'a t -> unit\n\
\n\
(** Put the abstract value in canonical form. (not yet clear definition) *)
val canonicalize : 'a Manager.t -> 'a t -> unit\n\
\n\
val hash : 'a Manager.t -> 'a t -> int\n\
\n\
(** [approximate man abs alg] perform some transformation on the abstract value, guided by the argument [alg]. The transformation may lose information.  The argument [alg] overrides the field algorithm of the structure of type [Manager.funopt] associated to ap_abstract0_approximate (commodity feature).*)
val approximate : 'a Manager.t -> 'a t -> int -> unit\n\
\n\
")
quote(ML,"\n\
let minimize man x = Abstract0.minimize man x.abstract0\n\
let canonicalize man x = Abstract0.canonicalize man x.abstract0\n\
let hash man x = 5*(Environment.hash x.env) + Abstract0.hash man x.abstract0\n\
let approximate man x n = Abstract0.approximate man x.abstract0 n\n\
")

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Printing} *)")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"\n(** Dump on the [stdout] C stream the internal representation of an abstract value, for debugging purposes *)")
void ap_abstract1_fdump(ap_manager_ptr man, [ref]struct ap_abstract1_t* a)
  quote(call,"ap_abstract1_fdump(stdout,man, a); fflush(stdout);")
  quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Print as a set of constraints *)")
quote(MLI,"val print: Format.formatter -> 'a t -> unit")

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Serialization} *)")
quote(MLMLI,"(* ============================================================ *)")

quote(MLMLI,"(* ********************************************************************** *)")
quote(MLMLI,"(** {2 Constructor, accessors, tests and property extraction} *)")
quote(MLMLI,"(* ********************************************************************** *)")

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Basic constructors} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"(** All these functions request explicitly an environment in their arguments. *)\n")

quote(MLI,"\n(** Create a bottom (empty) value defined on the given environment *)")
struct ap_abstract1_t ap_abstract1_bottom(ap_manager_ptr man, ap_environment_ptr env)
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Create a top (universe) value defined on the given environment *)")
struct ap_abstract1_t ap_abstract1_top(ap_manager_ptr man, ap_environment_ptr env)
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Abstract an hypercube.\n\n[of_box man env tvar tinterval] abstracts an hypercube defined by the arrays [tvar] and [tinterval]. The result is defined on the environment [env], which should contain all the variables in [tvar] (and defines their type) *)")
struct ap_abstract1_t ap_abstract1_of_box(ap_manager_ptr man,
				    ap_environment_ptr env,
				    [size_is(size)]ap_var_t* tvar,
				    [size_is(size2)]ap_interval_ptr* tinterval,
				    unsigned int size, unsigned int size2)
  quote(call,"\n\
if (size!=size2)\n\
  caml_failwith(\"Abstract1.of_box: the two arrays are of different sizes\");\n\
_res = ap_abstract1_of_box(man,env,tvar,tinterval,size);\n\
")
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Accessors} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"\n\
val manager : 'a t -> 'a Manager.t\n\
val env : 'a t -> Environment.t\n\
val abstract0 : 'a t -> 'a Abstract0.t\n\
  (** Return resp. the underlying manager, environment and abstract value of level 0 *)\n\
")

quote(ML,"\n\
let manager x = Abstract0.manager x.abstract0\n\
let env x = x.env\n\
let abstract0 x = x.abstract0\n\
")

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Tests} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"\n\
(** Emptiness test *)
val is_bottom : 'a Manager.t -> 'a t -> bool\n\
\n\
(** Universality test *)
val is_top : 'a Manager.t -> 'a t -> bool\n\
")
quote(ML,"\n\
let is_bottom man x = Abstract0.is_bottom man x.abstract0\n\
let is_top man x = Abstract0.is_top man x.abstract0\n\
")

quote(MLI,"\n(** Inclusion test. The 2 abstract values should be compatible. *)")
boolean ap_abstract1_is_leq(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Equality test. The 2 abstract values should be compatible. *)")
boolean ap_abstract1_is_eq(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Does the abstract value satisfy the linear constraint ? *)")
boolean ap_abstract1_sat_lincons(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, [ref]struct ap_lincons1_t* v)
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Does the abstract value satisfy the tree expression constraint ? *)")
boolean ap_abstract1_sat_tcons(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, [ref]struct ap_tcons1_t* v)
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Does the abstract value satisfy the constraint [dim in interval] ? *)")
boolean ap_abstract1_sat_interval(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
				  ap_var_t v1,
				  [ref]struct ap_interval_t* v2)
    quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** Is the variable unconstrained in the abstract value ? If yes, this means that the existential quantification of the dimension does not change the value. *)")
boolean ap_abstract1_is_variable_unconstrained(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, ap_var_t v)
    quote(dealloc,"I0_CHECK_EXC(man)");


quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Extraction of properties} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"\n(** Return the interval of variation of the variable in the abstract value. *)")
[ref]struct ap_interval_t* ap_abstract1_bound_variable(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, ap_var_t v)
    quote(dealloc,"ap_interval_free(_res); I0_CHECK_EXC(man)");

quote(MLI,"\n(** Return the interval of variation of the linear expression in the abstract value. \n\nImplement a form of linear programming, where the argument linear expression is the one to optimize under the constraints induced by the abstract value. *)")
[ref]struct ap_interval_t* ap_abstract1_bound_linexpr(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, [ref]struct ap_linexpr1_t* v)
    quote(dealloc,"ap_interval_free(_res); I0_CHECK_EXC(man)");

quote(MLI,"\n(** Return the interval of variation of the tree expression in the abstract value. *)")
[ref]struct ap_interval_t* ap_abstract1_bound_texpr(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, [ref]struct ap_texpr1_t* v)
    quote(dealloc,"ap_interval_free(_res); I0_CHECK_EXC(man)");

quote(MLI,"\n\
(** Convert the abstract value to an hypercube *)
val to_box : 'a Manager.t -> 'a t -> box1\n\
\n\
(** Convert the abstract value to a conjunction of linear constraints. *)
val to_lincons_array : 'a Manager.t -> 'a t -> Lincons1.earray\n\
(** Convert the abstract value to a conjunction of tree expressions constraints. *)
val to_tcons_array : 'a Manager.t -> 'a t -> Tcons1.earray\n\
\n\
(** Convert the abstract value to a set of generators that defines it. *)
val to_generator_array : 'a Manager.t -> 'a t -> Generator1.earray\n\
\n\
")

quote(ML,"\n\
let to_lincons_array man x = {\n\
  Lincons1.lincons0_array = Abstract0.to_lincons_array man x.abstract0;\n\
  Lincons1.array_env = x.env\n\
}\n\
let to_tcons_array man x = {\n\
  Tcons1.tcons0_array = Abstract0.to_tcons_array man x.abstract0;\n\
  Tcons1.array_env = x.env\n\
}\n\
let to_generator_array man x = {\n\
  Generator1.generator0_array = Abstract0.to_generator_array man x.abstract0;\n\
  Generator1.array_env = x.env\n\
}\n\
let to_box man x = {\n\
  interval_array = Abstract0.to_box man x.abstract0;\n\
  box1_env = x.env\n\
}\n\
")

quote(MLMLI,"(* ********************************************************************** *)")
quote(MLMLI,"(** {2 Operations} *)")
quote(MLMLI,"(* ********************************************************************** *)")

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Meet and Join} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"(** Meet of 2 abstract values. *)")
struct ap_abstract1_t ap_abstract1_meet(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
     quote(call,"_res = ap_abstract1_meet(man,false,a1,a2);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Meet of a non empty array of abstract values. *)")
struct ap_abstract1_t ap_abstract1_meet_array(ap_manager_ptr man,
					[size_is(size)]struct ap_abstract1_t* array, unsigned int size)
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Meet of an abstract value with an array of linear constraints. *)")
struct ap_abstract1_t ap_abstract1_meet_lincons_array(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
						 [ref]struct ap_lincons1_array_t* v)
     quote(call,"_res = ap_abstract1_meet_lincons_array(man,false,a,v);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Meet of an abstract value with an array of tree expressions constraints. *)")
struct ap_abstract1_t ap_abstract1_meet_tcons_array(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
						 [ref]struct ap_tcons1_array_t* v)
     quote(call,"_res = ap_abstract1_meet_tcons_array(man,false,a,v);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Join of 2 abstract values. *)")
struct ap_abstract1_t ap_abstract1_join(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
     quote(call,"_res = ap_abstract1_join(man,false,a1,a2);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Join of a non empty array of abstract values. *)")
struct ap_abstract1_t ap_abstract1_join_array(ap_manager_ptr man, [size_is(size)]struct ap_abstract1_t* array, unsigned int size)
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Add the array of generators to the abstract value (time elapse operator).\n\n The generators should either lines or rays, not vertices. *)")
struct ap_abstract1_t ap_abstract1_add_ray_array(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
					   [ref]struct ap_generator1_array_t* v)
     quote(call,"_res = ap_abstract1_add_ray_array(man,false,a,v);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** {5 Side-effect versions of the previous functions} *)\n")

void ap_abstract1_meet_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
	 quote(call,"{\n\
  ap_abstract1_t res = ap_abstract1_meet(man,true,a1,a2);\n\
  value v = Field(_v_a1,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_meet_lincons_array_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
				       [ref]struct ap_lincons1_array_t* v)
	 quote(call,"{\n\
  ap_abstract1_t res = ap_abstract1_meet_lincons_array(man,true,a,v);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_meet_tcons_array_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
				       [ref]struct ap_tcons1_array_t* v)
	 quote(call,"{\n\
  ap_abstract1_t res = ap_abstract1_meet_tcons_array(man,true,a,v);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_join_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
	 quote(call,"{\n\
  ap_abstract1_t res = ap_abstract1_join(man,true,a1,a2);\n\
  value v = Field(_v_a1,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_add_ray_array_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
				  [ref]struct ap_generator1_array_t* v)
	 quote(call,"{\n\
  ap_abstract1_t res = ap_abstract1_add_ray_array(man,true,a,v);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Assignement and Substitutions} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"(** Parallel assignement of an array of dimensions by an array of same size of linear expressions *)")
struct ap_abstract1_t ap_abstract1_assign_linexpr_array(ap_manager_ptr man,
						  [ref]struct ap_abstract1_t* a,
						  [size_is(v3)]ap_var_t* v1,
						    [size_is(v4)]struct ap_linexpr1_t* v2,
						  int v3,int v4,
						  struct ap_abstract1_t* dest)
     quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.assign_linexpr_array: arrays of different size\");\n\
_res = ap_abstract1_assign_linexpr_array(man,false,a,v1,v2,v3,dest);\n\
")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Parallel substitution of an array of dimensions by an array of same size of linear expressions *)")
struct ap_abstract1_t ap_abstract1_substitute_linexpr_array(ap_manager_ptr man,
						      [ref]struct ap_abstract1_t* a,
						      [size_is(v3)]ap_var_t* v1,
						      [size_is(v4)]struct ap_linexpr1_t* v2,
						      int v3, int v4,
						      struct ap_abstract1_t* dest)
     quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.substitute_linexpr_array: arrays of different size\");\n\
_res = ap_abstract1_substitute_linexpr_array(man,false,a,v1,v2,v3,dest);\n\
")
      quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Parallel assignement of an array of dimensions by an array of same size of tree expressions *)")
struct ap_abstract1_t ap_abstract1_assign_texpr_array(ap_manager_ptr man,
						  [ref]struct ap_abstract1_t* a,
						  [size_is(v3)]ap_var_t* v1,
						    [size_is(v4)]struct ap_texpr1_t* v2,
						  int v3,int v4,
						  struct ap_abstract1_t* dest)
     quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.assign_texpr_array: arrays of different size\");\n\
_res = ap_abstract1_assign_texpr_array(man,false,a,v1,v2,v3,dest);\n\
")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Parallel substitution of an array of dimensions by an array of same size of tree expressions *)")
struct ap_abstract1_t ap_abstract1_substitute_texpr_array(ap_manager_ptr man,
						      [ref]struct ap_abstract1_t* a,
						      [size_is(v3)]ap_var_t* v1,
						      [size_is(v4)]struct ap_texpr1_t* v2,
						      int v3, int v4,
						      struct ap_abstract1_t* dest)
     quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.substitute_texpr_array: arrays of different size\");\n\
_res = ap_abstract1_substitute_texpr_array(man,false,a,v1,v2,v3,dest);\n\
")
      quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"\n(** {5 Side-effect versions of the previous functions} *)\n")

void ap_abstract1_assign_linexpr_array_with(ap_manager_ptr man,
					 [ref]struct ap_abstract1_t* a,
					 [size_is(v3)]ap_var_t* v1,
					 [size_is(v4)]struct ap_linexpr1_t* v2,
					 int v3,int v4,
					 struct ap_abstract1_t* dest)
  quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.assign_linexpr_array_with: arrays of different size\");\n\
{\n\
  ap_abstract1_t res = ap_abstract1_assign_linexpr_array(man,true,a,v1,v2,v3,dest);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_substitute_linexpr_array_with(ap_manager_ptr man,
					     [ref]struct ap_abstract1_t* a,
					     [size_is(v3)]ap_var_t* v1,
					     [size_is(v4)]struct ap_linexpr1_t* v2,
					     int v3, int v4,
					     struct ap_abstract1_t* dest)
  quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.substitute_linexpr_array_with: arrays of different size\");\n\
{\n\
  ap_abstract1_t res = ap_abstract1_substitute_linexpr_array(man,true,a,v1,v2,v3,dest);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_assign_texpr_array_with(ap_manager_ptr man,
					  [ref]struct ap_abstract1_t* a,
					  [size_is(v3)]ap_var_t* v1,
					  [size_is(v4)]struct ap_texpr1_t* v2,
					  int v3, int v4,
					  struct ap_abstract1_t* dest)
  quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.assign_texpr_array_with: arrays of different size\");\n\
{\n\
  ap_abstract1_t res = ap_abstract1_assign_texpr_array(man,true,a,v1,v2,v3,dest);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_substitute_texpr_array_with(ap_manager_ptr man,
					     [ref]struct ap_abstract1_t* a,
					     [size_is(v3)]ap_var_t* v1,
					     [size_is(v4)]struct ap_texpr1_t* v2,
					     int v3, int v4,
					     struct ap_abstract1_t* dest)
  quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.substitute_texpr_array_with: arrays of different size\");\n\
{\n\
  ap_abstract1_t res = ap_abstract1_substitute_texpr_array(man,true,a,v1,v2,v3,dest);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Projections} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"(** These functions implements forgeting (existential quantification) of (array of) variables. Both functional and side-effect versions are provided. The Boolean, if true, adds a projection onto 0-plane. *)\n\n")

struct ap_abstract1_t ap_abstract1_forget_array(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
					  [size_is(v2)]ap_var_t* v1, unsigned int v2, boolean v3)
     quote(call,"_res = ap_abstract1_forget_array(man,false,a,v1,v2,v3);")
     quote(dealloc,"I0_CHECK_EXC(man)");
void ap_abstract1_forget_array_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, [size_is(v2)]ap_var_t* v1, int v2, boolean v3)
     quote(call,"{\n\
  ap_abstract1_t res = ap_abstract1_forget_array(man,true,a,v1,v2,v3);
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Change and permutation of dimensions} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"(** Change the environement of the abstract values.\n\nVariables that are removed are first existentially quantified, and variables that are introduced are unconstrained. The Boolean, if true, adds a projection onto 0-plane for these ones. *)")
struct ap_abstract1_t ap_abstract1_change_environment(ap_manager_ptr man,
						 [ref]struct ap_abstract1_t* a,
						 ap_environment_ptr v1,
						 boolean v2)
     quote(call,"_res = ap_abstract1_change_environment(man,false,a,v1,v2);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Remove from the environment of the abstract value and from the abstract value itself variables that are unconstrained in it. *)")
struct ap_abstract1_t ap_abstract1_minimize_environment(ap_manager_ptr man, [ref]struct ap_abstract1_t* a)
     quote(call,"_res = ap_abstract1_minimize_environment(man,false,a);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Parallel renaming of the environment of the abstract value.\n\nThe new variables should not interfere with the variables that are not renamed. *)")
struct ap_abstract1_t ap_abstract1_rename_array(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
					  [size_is(v3)]ap_var_t* v1, [size_is(v4)]ap_var_t* v2,
					  unsigned int v3, unsigned int v4)
     quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.rename_array: arrays of different size\");\n\
_res = ap_abstract1_rename_array(man,false,a,v1,v2,v3);\n\
")
      quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_change_environment_with(ap_manager_ptr man,
				       [ref]struct ap_abstract1_t* a,
				       ap_environment_ptr v1,
				       boolean v2)
     quote(call,"\
{\n\
  ap_environment_t* oldenv = ap_environment_copy(a->env);\n		\
  ap_abstract1_t res = ap_abstract1_change_environment(man,true,a,v1,v2);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
  if (res.env==oldenv){\n\
    ap_environment_free(oldenv);\n\
  }\n\
  else {\n\
    assert(res.env==v1);\n\
    Store_field(_v_a,1,_v_v1);\n\
  }\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_minimize_environment_with(ap_manager_ptr man,
					 [ref]struct ap_abstract1_t* a)
     quote(call,"{\n\
  ap_environment_t* oldenv = ap_environment_copy(a->env);\n		\
  ap_abstract1_t res = ap_abstract1_minimize_environment(man,true,a);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
  if (res.env==oldenv){\n\
    ap_environment_free(oldenv);\n\
  }\n\
  else {\n\
    v = camlidl_apron_environment_ptr_c2ml(&res.env); \n\
    Store_field(_v_a,1,v); \n\
  }\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_rename_array_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
				 [size_is(v3)]ap_var_t* v1, [size_is(v4)]ap_var_t* v2,
				 unsigned int v3, unsigned int v4)
     quote(call,"\n\
if (v3!=v4) caml_failwith(\"Abstract1.rename_array_with: arrays of different size\");\n\
{\n\
  ap_environment_t* oldenv = ap_environment_copy(a->env);\n		\
  ap_abstract1_t res = ap_abstract1_rename_array(man,true,a,v1,v2,v3);\n\
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
  if (res.env==oldenv){\n\
    ap_environment_free(oldenv);\n\
  }\n\
  else {\n\
    v = camlidl_apron_environment_ptr_c2ml(&res.env); \n\
    Store_field(_v_a,1,v); \n\
  }\n\
}")
      quote(dealloc,"I0_CHECK_EXC(man)");


quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Expansion and folding of dimensions} *)\n")
quote(MLMLI,"(* ============================================================ *)")


quote(MLI,"\n\
(**\n\
  These functions allows to expand one dimension into several ones having the\n\
  same properties with respect to the other dimensions, and to fold several\n\
  dimensions into one. Formally,\n\
\n\
  - expand P(x,y,z) z w = P(x,y,z) inter P(x,y,w) if z is expanded in z and w\n\
  - fold Q(x,y,z,w) z w = exists w:Q(x,y,z,w) union (exist z:Q(x,y,z,w))(z<-w)\n\
    if z and w are folded onto z\n\
*)\n\n\
")

quote(MLI,"(** \
    Expansion: [expand a var tvar] expands the variable [var] into itself and\n	\
    the additional variables in [tvar], which are given the same type as [var].\n\n\
    It results in (n+1) unrelated variables having\n			\
    same relations with other variables. The additional variables are added to the environment of \n\
    the argument for making the environment of the result, so they should\n\
    not belong to the initial environement.\n\
*)")
struct ap_abstract1_t ap_abstract1_expand(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
				    ap_var_t v1,
				    [size_is(v3)]ap_var_t* v2,
				    int v3)
     quote(call,"_res = ap_abstract1_expand(man,false,a,v1,v2,v3);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI," \
  (** Folding: [fold a tvar] fold the variables in the array [tvar] of size n>=1\n\
    and put the result in the first variable of the array. The other\n\
    variables of the array are then removed, both from the environment and the abstract value.\n\
  *)")
struct ap_abstract1_t ap_abstract1_fold(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
				  [size_is(v2)]ap_var_t* v1,
				  int v2)
  quote(call,"_res = ap_abstract1_fold(man,false,a,v1,v2);")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_expand_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
			   ap_var_t v1,
			   [size_is(v3)]ap_var_t* v2,
			   int v3)
     quote(call,"{\n\
  ap_environment_t* oldenv = ap_environment_copy(a->env);\n		\
  ap_abstract1_t res = ap_abstract1_expand(man,true,a,v1,v2,v3);
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
  if (res.env==oldenv){\n\
    ap_environment_free(oldenv);\n\
  }\n\
  else {\n\
    v = camlidl_apron_environment_ptr_c2ml(&res.env); \n\
    Store_field(_v_a,1,v); \n\
  }\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

void ap_abstract1_fold_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
			 [size_is(v2)]ap_var_t* v1,
			 int v2)
     quote(call,"{\n\
  ap_environment_t* oldenv = ap_environment_copy(a->env);\n		\
  ap_abstract1_t res = ap_abstract1_fold(man,true,a,v1,v2);
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
  if (res.env==oldenv){\n\
    ap_environment_free(oldenv);\n\
  }\n\
  else {\n\
    v = camlidl_apron_environment_ptr_c2ml(&res.env); \n\
    Store_field(_v_a,1,v); \n\
  }\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Widening} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"(** Widening *)")
struct ap_abstract1_t ap_abstract1_widening(ap_manager_ptr man,
				      [ref]struct ap_abstract1_t* a1,
				      [ref]struct ap_abstract1_t* a2)
     quote(dealloc,"I0_CHECK_EXC(man)");

struct ap_abstract1_t ap_abstract1_widening_threshold(ap_manager_ptr man,
						[ref]struct ap_abstract1_t* a1,
						[ref]struct ap_abstract1_t* a2,
						[ref]struct ap_lincons1_array_t* v)
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLMLI,"(* ============================================================ *)")
quote(MLMLI,"(** {3 Closure operation} *)\n")
quote(MLMLI,"(* ============================================================ *)")

quote(MLI,"(** Closure: transform strict constraints into non-strict ones.*)")
struct ap_abstract1_t ap_abstract1_closure(ap_manager_ptr man,[ref]struct ap_abstract1_t* a)
     quote(call,"_res = ap_abstract1_closure(man,false,a);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Side-effect version *)")
void ap_abstract1_closure_with(ap_manager_ptr man,[ref]struct ap_abstract1_t* a)
     quote(call,"{\n\
  ap_abstract1_t res = ap_abstract1_closure(man,true,a);
  value v = Field(_v_a,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");
quote(MLMLI,"(* ********************************************************************** *)")
quote(MLMLI,"(** {2 Additional operations} *)")
quote(MLMLI,"(* ********************************************************************** *)")

quote(MLI,"\n\
val of_lincons_array : 'a Manager.t -> Environment.t -> Lincons1.earray -> 'a t\n\
val of_tcons_array   : 'a Manager.t -> Environment.t -> Tcons1.earray   -> 'a t\n\
  (** Abstract a conjunction of constraints *)\n\
\n\
val assign_linexpr     : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> 'a t\n\
val substitute_linexpr : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> 'a t\n\
val assign_texpr       : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t   -> 'a t option -> 'a t\n\
val substitute_texpr   : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t   -> 'a t option -> 'a t\n\
  (** Assignement/Substitution of a single dimension by a single expression *)\n\
\n\
val assign_linexpr_with     : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> unit\n\
val substitute_linexpr_with : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> unit\n\
val assign_texpr_with       : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t   -> 'a t option -> unit\n\
val substitute_texpr_with   : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t   -> 'a t option -> unit\n\
  (** Side-effect version of the previous functions *)\n\
\n\
")

quote(ML,"\n\
let of_lincons_array man env array =\n\
  let res = top man env in\n\
  meet_lincons_array_with man res array;\n\
  res\n\
let of_tcons_array man env array =\n\
  let res = top man env in\n\
  meet_tcons_array_with man res array;\n\
  res\n\
let assign_linexpr man abs dim expr odest =\n\
  assign_linexpr_array man abs [|dim|] [|expr|] odest\n\
let assign_texpr man abs dim expr odest =\n\
  assign_texpr_array man abs [|dim|] [|expr|] odest\n\
let substitute_linexpr man abs dim expr odest =\n\
  substitute_linexpr_array man abs [|dim|] [|expr|] odest\n\
let substitute_texpr man abs dim expr odest =\n\
  substitute_texpr_array man abs [|dim|] [|expr|] odest\n\
let assign_linexpr_with man abs dim expr odest =\n\
  assign_linexpr_array_with man abs [|dim|] [|expr|] odest\n\
let assign_texpr_with man abs dim expr odest =\n\
  assign_texpr_array_with man abs [|dim|] [|expr|] odest\n\
let substitute_linexpr_with man abs dim expr odest =\n\
  substitute_linexpr_array_with man abs [|dim|] [|expr|] odest\n\
let substitute_texpr_with man abs dim expr odest =\n\
  substitute_texpr_array_with man abs [|dim|] [|expr|] odest\n\
")

quote(MLI,"(** Unification of 2 abstract values on their least common environment *)")
struct ap_abstract1_t ap_abstract1_unify(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
     quote(call,"_res = ap_abstract1_unify(man,false,a1,a2);")
     quote(dealloc,"I0_CHECK_EXC(man)");
quote(MLI,"(** Side-effect version *)")
void ap_abstract1_unify_with(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
	 quote(call,"\
{\n\
  ap_abstract1_t res = ap_abstract1_unify(man,true,a1,a2);\n\
  value v = Field(_v_a1,0);\n\
  *((ap_abstract0_ptr *) Data_custom_val(v)) = res.abstract0;\n\
  v = Field(_v_a1,1);\n\
  *((ap_environment_ptr *) Data_custom_val(v)) = res.env;\n\
}")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(ML,"\n\
let print fmt a =\n\
let man = manager a in\n\
if is_bottom man a then\n\
  Format.pp_print_string fmt \"bottom\"\n\
else if is_top man a then\n\
  Format.pp_print_string fmt \"top\"\n\
else begin\n\
  let tab = to_lincons_array man a in\n\
  Lincons1.array_print fmt tab;\n\
end\n\
")