electrod

Formal analysis for the Electrod formal pivot language
IN THIS PACKAGE
Module Libelectrod . Elo
type ('fml, 'exp, 'iexp) ofml = private
| True
| False
| RComp of 'exp * comp_op * 'exp
| IComp of 'iexp * icomp_op * 'iexp
| LUn of lunop * 'fml
| LBin of 'fml * lbinop * 'fml
| Quant of quant * bool * int * 'exp * 'fml list
| FIte of 'fml * 'fml * 'fml
| Block of 'fml list
and quant = private
| All
| Some_
| No
and lbinop = private
| And
| Or
| Imp
| Iff
| U
| R
| S
| T
and lunop = private
| F
| G
| Not
| O
| X
| H
| P
and comp_op = private
| In
| NotIn
| REq
| RNEq
and icomp_op = private
| IEq
| INEq
| Lt
| Lte
| Gt
| Gte
and ('fml, 'exp, 'iexp) oexp = {
prim_exp : ( 'fml, 'exp, 'iexp ) prim_oexp;
arity : int;
}
and ('fml, 'exp, 'iexp) prim_oexp = private
| None_
| Univ
| Iden
| Var of int
| Name of Name.t
| RUn of runop * 'exp
| RBin of 'exp * rbinop * 'exp
| RIte of 'fml * 'exp * 'exp
| Compr of (bool * int * 'exp) list * 'fml list
| Prime of 'exp
and runop = private
| Transpose
| TClos
| RTClos
and rbinop = private
| Union
| Inter
| Over
| LProj
| RProj
| Prod
| Diff
| Join
and ('fml, 'exp, 'iexp) oiexp = private
| Num of int
| Card of 'exp
| IUn of iunop * 'iexp
| IBin of 'iexp * ibinop * 'iexp
and iunop = private
| Neg
and ibinop = private
| Add
| Sub
type goal = private
| Run of fml list * bool option
and fml = private
| Fml of ( fml, exp, iexp ) ofml Hashcons.hash_consed
and prim_exp = ( fml, exp, iexp ) prim_oexp
and exp = private
| Exp of ( fml, exp, iexp ) oexp Hashcons.hash_consed
and iexp = private
| Iexp of ( fml, exp, iexp ) oiexp Hashcons.hash_consed
type t = {
file : string option;
domain : Domain.t;
instance : Instance.t;
sym : Symmetry.t list;
invariants : fml list;
goal : goal;
atom_renaming : ( Atom.t, Atom.t ) CCList.Assoc.t;
name_renaming : ( Name.t, Name.t ) CCList.Assoc.t;
}
val make : string option -> Domain.t -> Instance.t -> Symmetry.t list -> fml list -> goal -> ( Atom.t, Atom.t ) CCList.Assoc.t -> ( Name.t, Name.t ) CCList.Assoc.t -> t
val arity : exp -> int
val run : fml list -> bool option -> goal
val true_ : fml
val false_ : fml
val rcomp : exp -> comp_op -> exp -> fml
val icomp : iexp -> icomp_op -> iexp -> fml
val lbinary : fml -> lbinop -> fml -> fml
val sim_binding : bool -> int -> exp -> bool * int * exp
val quant : quant -> (bool * int * exp) -> fml list -> fml
val lunary : lunop -> fml -> fml
val block : fml list -> fml
val fite : fml -> fml -> fml -> fml
val all : quant
val some : quant
val no_ : quant
val and_ : lbinop
val or_ : lbinop
val impl : lbinop
val iff : lbinop
val until : lbinop
val releases : lbinop
val since : lbinop
val triggered : lbinop
val not_ : lunop
val eventually : lunop
val always : lunop
val once : lunop
val next : lunop
val historically : lunop
val previous : lunop
val none : exp
val univ : exp
val iden : exp
val var : ar:int -> int -> exp
val name : ar:int -> Name.t -> exp
val runary : ar:int -> runop -> exp -> exp
val rbinary : ar:int -> exp -> rbinop -> exp -> exp
val rite : ar:int -> fml -> exp -> exp -> exp
val compr : ar:int -> (bool * int * exp) list -> fml list -> exp
val prime : ar:int -> exp -> exp
val in_ : comp_op
val not_in : comp_op
val req : comp_op
val rneq : comp_op
val ieq : icomp_op
val ineq : icomp_op
val lt : icomp_op
val lte : icomp_op
val gt : icomp_op
val gte : icomp_op
val transpose : runop
val tclos : runop
val rtclos : runop
val union : rbinop
val inter : rbinop
val over : rbinop
val lproj : rbinop
val rproj : rbinop
val prod : rbinop
val diff : rbinop
val join : rbinop
val num : int -> iexp
val card : exp -> iexp
val iunary : iunop -> iexp -> iexp
val ibinary : iexp -> ibinop -> iexp -> iexp
val neg : iunop
val add : ibinop
val sub : ibinop
val kwd_styled : 'a Fmtc.t -> 'a Fmtc.t
val pp_comp_op : Format.formatter -> comp_op -> unit
val pp_icomp_op : Format.formatter -> icomp_op -> unit
val pp_lunop : Format.formatter -> lunop -> unit
val pp_lbinop : Format.formatter -> lbinop -> unit
val pp_quant : Format.formatter -> quant -> unit
val pp_runop : Format.formatter -> runop -> unit
val pp_rbinop : Format.formatter -> rbinop -> unit
val pp_iunop : Format.formatter -> iunop -> unit
val pp_ibinop : Format.formatter -> ibinop -> unit
val pp_var : Format.formatter -> int -> unit
val pp_sim_binding : int -> Format.formatter -> (bool * int * exp) -> unit
val pp_sim_bindings : int -> Format.formatter -> (bool * int * exp) list -> unit
val pp_oblock : 'a -> ( 'a -> 'b Fmtc.t ) -> Format.formatter -> 'b list -> unit
val pp_ofml : int -> ( int -> 'a Fmtc.t ) -> ( int -> Format.formatter -> 'b -> unit ) -> ( int -> Format.formatter -> 'c -> unit ) -> Format.formatter -> ( 'a, 'b, 'c ) ofml -> unit
val pp_prim_oexp : int -> ( int -> 'a Fmtc.t ) -> ( int -> Format.formatter -> 'b -> unit ) -> Format.formatter -> ( 'a, 'b, 'c ) prim_oexp -> unit
val pp_oiexp : 'a -> ( 'a -> Format.formatter -> 'b -> unit ) -> ( 'a -> Format.formatter -> 'c -> unit ) -> Format.formatter -> ( 'env, 'b, 'c ) oiexp -> unit
val pp_fml : int -> fml Fmtc.t
val pp_block : int -> Format.formatter -> fml list -> unit
val pp_iexp : int -> Format.formatter -> iexp -> unit
val pp_prim_exp : int -> Format.formatter -> ( fml, exp, iexp ) prim_oexp -> unit
val pp_exp : int -> Format.formatter -> exp -> unit
val pp_goal : Format.formatter -> goal -> unit
val pp : Format.formatter -> t -> unit
val pp_fml_stats : Format.formatter -> int -> unit

Prints the number of times every subformula is referenced (if number > inf).

class 'c map : object ... end
class virtual 'c fold : object ... end