package electrod

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

Install

Dune 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.4.1.tbz
sha256=b0bce9cc7126672feda5a02d5ef0c1131ba54db57654f80c0768c2f8d043cef9
sha512=92cc22f81522435e190039324767b6f69fa0b7d9dbfc3fb5561919823136fe492244dae993caf98633828e0090b67f306eec6270b86a1b2ff8630642130a3081

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 * bool option
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 -> bool option -> 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct