package electrod

  1. Overview
  2. Docs
Formal analysis for the Electrod formal pivot language

Install 

dune-project
 Dependency

github.com Readme Changelog MPL-2.0 License Edit opam file Versions (10)

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

  1. D
    David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-0.3.2.tbz
sha256=c58502de17f5b8d739963b5b5d7c761883305bc2b6464fc37769aae4bb31a28c
sha512=bc15032cbda06b0eb64d55cc7800d6c992c0823bb86609ddc5e56744fd0c76ea25b4f4ad7cafdee6fcaa2f109e48ca99f4270919f9a2ea4c7bf53f30b0ee3677

doc/electrod.libelectrod/Libelectrod/Elo/index.html

Module Libelectrod.EloSource

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

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

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