Module Bddapron.Syntax

module Syntax: sig .. end

Types

type cst = [ `Apron of Apron.Coeff.t | `Bint of (bool * int) * int | `Bool of bool ]

Constant

type unop = [ `Apron of Apron.Texpr1.unop * Apron.Texpr1.typ * Apron.Texpr1.round | `Not ]

Unary operators

type bbinop = [ `And | `EQ | `GEQ | `GT | `LEQ | `LT | `NEQ | `Or ]

Boolean/finite-type binary operators

Binary operators

type binop = [ `Apron of Apron.Texpr1.binop * Apron.Texpr1.typ * Apron.Texpr1.round
       | `Bool of bbinop ]

type 'a expr = [ `Binop of
           binop * 'a expr * 'a expr
       | `Cst of cst
       | `If of
           'a expr * 'a expr *
           'a expr
       | `In of 'a expr * 'a expr list
       | `Ref of 'a
       | `Unop of unop * 'a expr ]

Expressions

Error and printing functions

val print_cst : Format.formatter -> cst -> unit

val print_unop : Format.formatter -> unop -> unit

val print_bbinop : Format.formatter -> bbinop -> unit

val print_binop : Format.formatter -> binop -> unit

val print_expr : (Format.formatter -> 'a -> unit) ->
       Format.formatter -> 'a expr -> unit

exception Error of string

Translation functions

Exception raised in case of typing error

val to_expr0 : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t -> 'a expr -> 'a Bddapron.Expr0.t

val to_expr1 : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t -> 'a expr -> 'a Bddapron.Expr1.t

val to_listexpr1 : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a expr list -> 'a Bddapron.Expr1.List.t

val to_listexpr2 : ?normalize:bool ->
       ?reduce:bool ->
       ?careset:bool ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a expr list -> 'a Bddapron.Expr2.List.t

val to_boolexpr2 : ?normalize:bool ->
       ?reduce:bool ->
       ?careset:bool ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t -> 'a expr -> 'a Bddapron.Expr2.Bool.t

Internal functions

val error : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a

val is_zero : 'a expr -> bool

val precedence_of_unop : unop -> int

val precedence_of_binop : binop -> int

val precedence_of_expr : 'a expr -> int

val cst_to_expr0 : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t -> [< cst ] -> 'a Bddapron.Expr0.expr

val apply_bbinop : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       bbinop ->
       'a Bddapron.Expr0.expr -> 'a Bddapron.Expr0.expr -> 'a Bddapron.Expr0.Bool.t

val apply_binop : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       binop ->
       'a Bddapron.Expr0.t -> 'a Bddapron.Expr0.t -> 'a Bddapron.Expr0.t