Parameter Make.Terms

module Condition : Condition_map.CONDITION

type superterms

SUPER_TERMS of t, i.e. list/set of terms that contain t as subterm

module Relation : Union_Find.Parameters.GENERIC_GROUP

Relation between terms, used for the union-find

module Id : sig ... end

type level = int

Loop nesting where the variable was defined. When feasible, we automatically compute it to be at the highest possible scope.

type widening_id = int

A unique identifier for the widening point, needed to detect when the fixpoint is reached.

type 'a complete_term =

1. | Tuple_get : int * cfg_node -> 'res complete_term
   (*

   Phi arguments are represented using tuples (and Tuple_get represents an element in this tuple). This encodes the fact that the different variables are updated in sync. Using these tuples and path predicates to represent conditions, we have a sound and complete translation to SSA or SMT without the need for a control flow graph.

   *)
2. | Empty : 'res complete_term
   (*

   No value. Possibly should be only used as phi arguments.

   *)
3. | Unknown : level -> 'res complete_term
   (*

   A fresh value (i.e., a variable). TODO: Add an identifier for its scope, other than level.

   *)
4. | Mu_formal : {
   1. level : level;
   2. actual : 'res t * Operator.Function_symbol.boolean t;
   } -> 'res complete_term
5. | Inductive_var : {
   1. widening_id : widening_id;
   2. level : level;
   3. mutable definition : 'res t;
   } -> 'res complete_term
6. | T0 : {
   1. tag : (Operator.Function_symbol.ar0, 'res) Operator.Function_symbol.function_symbol;
   } -> 'res complete_term
   (*

   Term of arity 0.

   *)
7. | T1 : {
   1. tag : ('a Operator.Function_symbol.ar1, 'res) Operator.Function_symbol.function_symbol;
   2. a : 'a t;
   3. level : level;
   } -> 'res complete_term
   (*

   Term of arity 1.

   *)
8. | T2 : {
   1. tag : (('a, 'b) Operator.Function_symbol.ar2, 'res) Operator.Function_symbol.function_symbol;
   2. a : 'a t;
   3. b : 'b t;
   4. level : level;
   } -> 'res complete_term
   (*

   Term of arity 2.

   *)

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 'a 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;
   }

Node in the SSA graph.

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

Polymorphic term equality

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

Print the constraint/tuple. The dependencies should have already been printed.

val level : 'a t -> int

Returns the nesting level of a constraint. Constants are -1, topmost is 0.

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

Return the labeled union-find parent of the given constraint.

module UnionFind : Union_Find.Signatures.IMPERATIVE_GENERIC_RELATIONAL with type 'a t = 'a t and type ('a, 'b) relation = ('a, 'b) Relation.t

Union find structure: some terms points to their parents through the set of relations, allowing for accurate representation of relations in the group and storing fewer independent terms.