herdtools7 7.57 (latest) · OCaml Package

type atom = AST.identifier

Our basic variables.

module AtomOrdered : sig ... end

module AMap : sig ... end

A map from atoms.

type 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.

module MonomialOrdered : sig ... end

module MMap : sig ... end

A map from a monomial.

type 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$

module PolynomialOrdered : sig ... end

module PMap : sig ... end

Map from polynomials.

type sign =

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

A constraint on a numerical value.

type 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$ .

type 'a disjunction =

| Disjunction of 'a list

Case disjunctions.

type ir_expr = (ctnts * polynomial) disjunction

Constrained polynomials.

This is a branched tree of polynomials.

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

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

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

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

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

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

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

val disjunction : 'a list -> 'a disjunction

val ctnts_true : ctnts

val ctnts_false : ctnts

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

val mono_one : monomial

val mono_of_var : AMap.key -> monomial

val poly_zero : polynomial

val poly_of_var : AMap.key -> polynomial

val poly_of_z : Z.t -> polynomial

val poly_of_int : int -> polynomial

val poly_neg : polynomial -> polynomial

val poly_of_val : AST.literal -> polynomial

val sign_not : sign -> sign

val sign_minus : sign -> sign

exception ConjunctionBottomInterrupt

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

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

val ctnts_of_bool : bool -> ctnts

val ctnts_not : ctnts -> ctnts

val sign_compare : 'a -> 'a -> int

val mono_compare : monomial -> monomial -> int

val poly_compare : polynomial -> polynomial -> int

val ctnts_compare : ctnts -> ctnts -> int

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

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

val add_polys : polynomial -> polynomial -> polynomial

val mult_monos : monomial -> monomial -> monomial

val mult_polys : polynomial -> polynomial -> polynomial

val ctnts_and : ctnts -> ctnts -> ctnts

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

val disjunction_or : 'a disjunction -> 'a disjunction -> 'a disjunction

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

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

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

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

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

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

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

val loc : unit AST.annotated

val zero : AST.expr

val one : AST.expr

val cannot_happen_expr : AST.expr

val expr_of_z : Z.t -> AST.expr

val e_true : AST.expr

val e_false : AST.expr

val e_var : AST.identifier -> AST.expr

val e_band : AST.expr -> AST.expr -> AST.expr

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

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

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

val sign_of_z : Z.t -> sign

val polynomial_to_expr : polynomial -> AST.expr

val sign_to_binop : sign -> AST.binop

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

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

val ctnts_to_expr : ctnts -> AST.expr option

val of_ir : ir_expr -> AST.expr

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

val int_exp : int -> int -> int

type affectation = atom * Z.t * polynomial option

type affectations = affectation list

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

val subst_poly : affectations -> polynomial -> polynomial

val reduce_poly : affectations -> polynomial -> polynomial

val poly_get_constant_opt : polynomial -> Z.t option

val ctnt_is_trivial : polynomial -> sign -> bool

val reduce_ctnts : affectations -> ctnts -> ctnts

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

val deduce_equations : ctnts -> ctnts * affectations

val ctnts_get_trivial_opt : ctnts -> bool option

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

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

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

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

package herdtools7