electrod 0.3.2 · OCaml Package

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

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

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 -> 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 not_ : lunop

val sometime : 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

package electrod