Module While_analysis.Terms

module Condition : sig ... end

type superterms

module Relation : sig ... end

module Id : sig ... end

type level = int

type widening_id = int

type !'a1 complete_term =

1. | Tuple_get : int * cfg_node -> 'res complete_term
2. | Empty : 'res0 complete_term
3. | Unknown : level -> 'res1 complete_term
4. | Mu_formal : {
   1. level : level;
   2. actual : 'res2 t * Operator.Function_symbol.boolean t;
   } -> 'res2 complete_term
5. | Inductive_var : {
   1. widening_id : widening_id;
   2. level : level;
   3. mutable definition : 'res3 t;
   } -> 'res3 complete_term
6. | T0 : {
   1. tag : (Operator.Function_symbol.ar0, 'res4) Operator.Function_symbol.function_symbol;
   } -> 'res4 complete_term
7. | T1 : {
   1. tag : ('a Operator.Function_symbol.ar1, 'res5) Operator.Function_symbol.function_symbol;
   2. a : 'a t;
   3. level : level;
   } -> 'res5 complete_term
8. | T2 : {
   1. tag : (('a0, 'b) Operator.Function_symbol.ar2, 'res6) Operator.Function_symbol.function_symbol;
   2. a : 'a0 t;
   3. b : 'b t;
   4. level : level;
   } -> 'res6 complete_term

and !'a t =

1. | Bool : {
   1. mutable superterms : superterms;
   2. id : Operator.Function_symbol.boolean Id.t;
   3. mutable parent : Operator.Function_symbol.boolean parent;
   4. term : Operator.Function_symbol.boolean complete_term;
   5. bdd : Condition.t;
   } -> Operator.Function_symbol.boolean t
2. | Integer : {
   1. mutable superterms : superterms;
   2. id : Operator.Function_symbol.integer Id.t;
   3. mutable parent : Operator.Function_symbol.integer parent;
   4. term : Operator.Function_symbol.integer complete_term;
   } -> Operator.Function_symbol.integer t
3. | Binary : {
   1. mutable superterms : superterms;
   2. id : Operator.Function_symbol.binary Id.t;
   3. mutable parent : Operator.Function_symbol.binary parent;
   4. term : Operator.Function_symbol.binary complete_term;
   5. size : Units.In_bits.t;
   } -> Operator.Function_symbol.binary t
4. | Enum : {
   1. mutable superterms : superterms;
   2. id : Operator.Function_symbol.enum Id.t;
   3. mutable parent : Operator.Function_symbol.enum parent;
   4. term : Operator.Function_symbol.enum complete_term;
   } -> Operator.Function_symbol.enum t

and !'a0 parent =

1. | Node : 'b t * ('a, 'b) Relation.t -> 'a parent
2. | Root

and any =

1. | Any : 'res t -> any

and tuple = any Immutable_array.t

and cfg_node = private

1. | Nondet of {
   1. id : tuple Id.t;
   2. level : level;
   3. a : tuple;
   4. conda_bool : Operator.Function_symbol.boolean t;
   5. b : tuple;
   6. condb_bool : Operator.Function_symbol.boolean t;
   }
2. | Mu of {
   1. id : tuple Id.t;
   2. level : level;
   3. init : tuple;
   4. var : tuple;
   5. body : tuple;
   6. body_cond : Operator.Function_symbol.boolean t;
   }
3. | Inductive_vars of {
   1. id : tuple Id.t;
   2. widening_id : widening_id;
   3. level : int;
   4. mutable def : tuple;
   }

val polyeq : 'a t -> 'b t -> ('a, 'b) PatriciaTree.cmp

module Any : sig ... end

module CFG_Node : sig ... end

module SUPER_TERMS : sig ... end

val compare : 'a t -> 'b t -> int

val hash : 'a t -> int

val equal : 'a t -> 'b t -> bool

val pretty : Stdlib.Format.formatter -> 'a t -> unit

val level : 'a t -> int

val size_of : Operator.Function_symbol.binary t -> Units.In_bits.t

module Build : sig ... end

module Utils : sig ... end

val get_parent : 'a t -> 'a parent

module UnionFind : sig ... end