package electrod

  1. Overview
  2. Docs
package electrod
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ('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
and quant = private
  1. | All
  2. | Some_
  3. | No
and lbinop = private
  1. | And
  2. | Or
  3. | Imp
  4. | Iff
  5. | U
  6. | R
  7. | S
  8. | T
and lunop = private
  1. | F
  2. | G
  3. | Not
  4. | O
  5. | X
  6. | H
  7. | P
and comp_op = private
  1. | In
  2. | NotIn
  3. | REq
  4. | RNEq
and icomp_op = private
  1. | IEq
  2. | INEq
  3. | Lt
  4. | Lte
  5. | Gt
  6. | Gte
and ('fml, 'exp, 'iexp) oexp = {
  1. prim_exp : ('fml, 'exp, 'iexp) prim_oexp;
  2. arity : int;
}
and ('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
and runop = private
  1. | Transpose
  2. | TClos
  3. | RTClos
and rbinop = private
  1. | Union
  2. | Inter
  3. | Over
  4. | LProj
  5. | RProj
  6. | Prod
  7. | Diff
  8. | Join
and ('fml, 'exp, 'iexp) oiexp = private
  1. | Num of int
  2. | Card of 'exp
  3. | IUn of iunop * 'iexp
  4. | IBin of 'iexp * ibinop * 'iexp
and iunop = private
  1. | Neg
and ibinop = private
  1. | Add
  2. | Sub
type goal = private
  1. | Run of fml list * bool option
and fml = private
  1. | Fml of (fml, exp, iexp) ofml Hashcons.hash_consed
and prim_exp = (fml, exp, iexp) prim_oexp
and exp = private
  1. | Exp of (fml, exp, iexp) oexp Hashcons.hash_consed
and iexp = private
  1. | Iexp of (fml, exp, iexp) oiexp Hashcons.hash_consed
type 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;
}
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