Normalize (p.herdtools7.7.57.doc.herdtools7.asllib.Asllib.StaticInterpreter.Normalize)

Sourcetype atom = AST.identifier

Our basic variables.

Sourcemodule AtomOrdered : sig ... end

Sourcemodule AMap : sig ... end

A map from atoms.

Sourcetype monomial =

| Prod of int AMap.t
(*
Maps each variable to its exponent.
*)

A unitary monomial.

They are unitary in the sense that they do not have any factors: $3 \times X^2$ is not unitary, while $x^2$ is.

For example: $X^2 + Y^4$ represented by $X \to 2, Y \to 4$ , and $1$ is represented by the empty map.

Sourcemodule MonomialOrdered : sig ... end

Sourcemodule MMap : sig ... end

A map from a monomial.

Sourcetype polynomial =

| Sum of Z.t MMap.t
(*
Maps each monomial to its factor.
*)

A polynomial.

For example, $X^2 - X + 4$ is represented by $X^2 \to 1, X \to -1, 1 \to 4$

Sourcemodule PolynomialOrdered : sig ... end

Sourcemodule PMap : sig ... end

Map from polynomials.

Sourcetype sign =

| Null
| StrictPositive
| Positive
| Negative
| StrictNegative
| NotNull

A constraint on a numerical value.

Sourcetype ctnts =

| Conjunction of sign PMap.t
| Bottom

A conjunctive logical formulae with polynomials.

For example, $X^2 \leq 0$ is represented with $X^2 \to \leq 0$ .

Sourcetype 'a disjunction =

| Disjunction of 'a list

Case disjunctions.

Sourcetype ir_expr = (ctnts * polynomial) disjunction

Constrained polynomials.

This is a branched tree of polynomials.

Sourceval pp_mono : Format.formatter -> (monomial * Z.t) -> unit

Sourceval pp_poly : Format.formatter -> polynomial -> unit

Sourceval pp_sign : Format.formatter -> sign -> unit

Sourceval pp_ctnt : Format.formatter -> (polynomial * sign) -> unit

Sourceval pp_ctnts : Format.formatter -> ctnts -> unit

Sourceval pp_ctnts_and_poly : Format.formatter -> (ctnts * polynomial) -> unit

Sourceval pp_ir : Format.formatter -> (ctnts * polynomial) disjunction -> unit

Sourceval disjunction : 'a list -> 'a disjunction

Sourceval ctnts_true : ctnts

Sourceval ctnts_false : ctnts

Sourceval always : 'a -> (ctnts * 'a) disjunction

Sourceval mono_one : monomial

Sourceval mono_of_var : AMap.key -> monomial

Sourceval poly_zero : polynomial

Sourceval poly_of_var : AMap.key -> polynomial

Sourceval poly_of_z : Z.t -> polynomial

Sourceval poly_of_int : int -> polynomial

Sourceval poly_neg : polynomial -> polynomial

Sourceval poly_of_val : AST.literal -> polynomial

Sourceval sign_not : sign -> sign

Sourceval sign_minus : sign -> sign

Sourceexception ConjunctionBottomInterrupt

Sourceval sign_and : 'a -> sign -> sign -> sign option

Sourceval constant_satisfies : Z.t -> sign -> bool

Sourceval ctnts_of_bool : bool -> ctnts

Sourceval ctnts_not : ctnts -> ctnts

Sourceval sign_compare : 'a -> 'a -> int

Sourceval mono_compare : monomial -> monomial -> int

Sourceval poly_compare : polynomial -> polynomial -> int

Sourceval ctnts_compare : ctnts -> ctnts -> int

Source

val ir_compare : 
  (ctnts * polynomial) disjunction ->
  (ctnts * polynomial) disjunction ->
  int

Sourceval add_mono_to_poly : MMap.key -> Z.t -> Z.t MMap.t -> Z.t MMap.t

Sourceval add_polys : polynomial -> polynomial -> polynomial

Sourceval mult_monos : monomial -> monomial -> monomial

Sourceval mult_polys : polynomial -> polynomial -> polynomial

Sourceval ctnts_and : ctnts -> ctnts -> ctnts

Source

val restrict : 
  ctnts disjunction ->
  (ctnts * 'a) disjunction ->
  (ctnts * 'a) disjunction

Sourceval disjunction_or : 'a disjunction -> 'a disjunction -> 'a disjunction

Source

val cross_num : 
  (ctnts * 'a) disjunction ->
  (ctnts * 'b) disjunction ->
  ('a -> 'b -> 'c) ->
  (ctnts * 'c) disjunction

Sourceval map_num : (polynomial -> polynomial) -> ir_expr -> ir_expr

Source

val disjunction_cross : 
  ('a -> 'b -> 'c) ->
  'a disjunction ->
  'b disjunction ->
  'c disjunction

Sourceval ir_to_cond : sign -> (ctnts * PMap.key) disjunction -> ctnts disjunction

Sourceval make_anonymous : env -> AST.ty -> AST.ty

Sourceval to_ir : StaticEnv.env -> AST.expr -> ir_expr

Source

val to_cond : 
  StaticEnv.env ->
  AST.expr ->
  ctnts disjunction * ctnts disjunction

Sourceval loc : unit AST.annotated

Sourceval zero : AST.expr

Sourceval one : AST.expr

Sourceval cannot_happen_expr : AST.expr

Sourceval expr_of_z : Z.t -> AST.expr

Sourceval e_true : AST.expr

Sourceval e_false : AST.expr

Sourceval e_var : AST.identifier -> AST.expr

Sourceval e_band : AST.expr -> AST.expr -> AST.expr

Sourceval e_cond : AST.expr -> AST.expr -> AST.expr -> AST.expr_desc AST.annotated

Sourceval unop : AST.unop -> AST.expr -> AST.expr_desc AST.annotated

Sourceval monomial_to_expr : monomial -> AST.expr -> AST.expr

Sourceval sign_of_z : Z.t -> sign

Sourceval polynomial_to_expr : polynomial -> AST.expr

Sourceval sign_to_binop : sign -> AST.binop

Sourceval sign_to_expr : sign -> AST.expr -> AST.expr

Sourceval ctnt_to_expr : polynomial -> sign -> AST.expr

Sourceval ctnts_to_expr : ctnts -> AST.expr option

Sourceval of_ir : ir_expr -> AST.expr

Sourceval reduce_mono : monomial -> Z.t -> Z.t option

Sourceval int_exp : int -> int -> int

Sourcetype affectation = atom * Z.t * polynomial option

Sourcetype affectations = affectation list

Sourceval subst_mono : affectations -> monomial -> Z.t -> monomial * Z.t

Sourceval subst_poly : affectations -> polynomial -> polynomial

Sourceval reduce_poly : affectations -> polynomial -> polynomial

Sourceval poly_get_constant_opt : polynomial -> Z.t option

Sourceval ctnt_is_trivial : polynomial -> sign -> bool

Sourceval reduce_ctnts : affectations -> ctnts -> ctnts

Sourceval poly_get_linear : polynomial -> (AMap.key * Z.t) option

Sourceval deduce_equations : ctnts -> ctnts * affectations

Sourceval ctnts_get_trivial_opt : ctnts -> bool option

Source

val reduce : 
  (ctnts * polynomial) disjunction ->
  (ctnts * polynomial) disjunction

Sourceval normalize : env -> AST.expr -> AST.expr

Sourceval free_variables : (ctnts * polynomial) disjunction -> ASTUtils.ISet.t

Source

val equal_mod_branches : 
  (ctnts * polynomial) disjunction ->
  (ctnts * polynomial) disjunction ->
  bool