Module Bddapron.Parser

module Parser: sig .. end

val expr0_of_string : string Bddapron.Env.t ->
       string Bddapron.Cond.t -> string -> string Bddapron.Expr0.t

val expr1_of_string : string Bddapron.Env.t ->
       string Bddapron.Cond.t -> string -> string Bddapron.Expr1.t

val listexpr1_of_lstring : string Bddapron.Env.t ->
       string Bddapron.Cond.t -> string list -> string Bddapron.Expr1.List.t

val listexpr2_of_lstring : ?normalize:bool ->
       ?reduce:bool ->
       ?careset:bool ->
       string Bddapron.Env.t ->
       string Bddapron.Cond.t -> string list -> string Bddapron.Expr2.List.t

val boolexpr2_of_string : ?normalize:bool ->
       ?reduce:bool ->
       ?careset:bool ->
       string Bddapron.Env.t ->
       string Bddapron.Cond.t -> string -> string Bddapron.Expr2.Bool.t

val expr0_of_lexbuf : string Bddapron.Env.t ->
       string Bddapron.Cond.t -> Lexing.lexbuf -> string Bddapron.Expr0.t

  <expr> ::= <bexpr>      Boolean expression
  	|  <iexpr>      bounded integer expression
  	|  <eexpr>      enumerated type expression
  	|  <nexpr>      numerical expression
  
  Boolean expressions
  <bexpr> ::= true | false
  	 | id                            variable
  	 | <constraint>
  	 | not <bexpr>
  	 | <bexpr> (or | and) <bexpr>
  	 | ( <bexpr> )
  	 | if <bexpr> then <bexpr> else <bexpr>
  <constraint> ::= id == <expr>
  		 <iexpr> (== | >= | > | <= | <) <iexpr>
  		 <nexpr> (== | >= | > | <= | <) <nexpr>
  
  Bounded integer expressions
  <iexpr> ::= uint[<integer>][-]<integer>  constant (snd integer) of given type
  	 |  sint[<integer>][-]<integer>  constant (snd integer) of given type
  	 |  id                           variable
  	 |  <iexpr> ( +|-|* ) <iexpr>
  	 |  ( <iexpr> )
  	 |  if <bexpr> then <iexpr> else <iexpr>
  
  Enumerated type expressions
  <eexpr> ::= id                           variable or constant (label)
  	 |  ( <eexpr> )
  	 |  if <bexpr> then <eexpr> else <eexpr>
  
  Numerical expressions
  <nexpr> ::= <coeff>
  	 |  id                           variable
  	 |  <unop> <nexpr>
  	 |  <nexpr> <binop> <nexpr>
  	 |  ( <nexpr> )
  	 |  if <bexpr> then <nexpr> else <nexpr>
  
  <binop>    ::= (+|-|*|/|%)[_(i|f|d|l|q)[,(n|0|+oo|-oo)]]
  <unop>     ::= -
  	    |  (cast|sqrt)[_(i|f|d|l|q)[,(n|0|+oo|-oo)]]
  <coeff>    ::= <float>
  	    |  <rational>
  <float>    ::= C/OCaml floating-point number syntax
  <rational> ::= <integer>  | <integer>/<integer>
 

Here are is an example (bddapron/test2.ml file). open Bddapron;;
  
  let cudd = Cudd.Man.make_v ();;
  let env = Env.make cudd;;
  let cond = Cond.make cudd;;
  Env.add_typ_with "e0" (`Benum [|"l0";"l1";"l2"|]);;
  Env.add_vars_with [
    ("b0",`Bool);
    ("b1",`Bool);
    ("i0",`Bint(false,3));
    ("i1",`Bint(false,3));
    ("e0",`Benum("e0"));
    ("x0",`Real);
    ("x1",`Real);
    ("x2",`Real);
  ];;
  
  let bexpr1 = Parser.boolexpr2_of_string env cond
    "(i0==uint[3](3) + i1 or e0==(if b0 then l0 else l1)) and x0 +_f,oo 2 *_i,0 x1 >=0";;
  
  let apron = Polka.manager_alloc_loose ();;
  let man = Domain1.make_man ~global:false apron;;
  let top = Domain1.top man env;;
  let abs = Domain0.meet_condition man cond top bexpr1;;