Module `Libelectrod.Elo`Source

Sourcetype ('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

Sourceand quant = private

| All
| Some_
| No

Sourceand lbinop = private

| And
| Or
| Imp
| Iff
| U
| R
| S
| T

Sourceand lunop = private

| F
| G
| Not
| O
| X
| H
| P

Sourceand comp_op = private

| In
| NotIn
| REq
| RNEq

Sourceand icomp_op = private

| IEq
| INEq
| Lt
| Lte
| Gt
| Gte

Sourceand ('fml, 'exp, 'iexp) oexp = {

prim_exp : ('fml, 'exp, 'iexp) prim_oexp;
arity : int;

}

Sourceand ('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

Sourceand runop = private

| Transpose
| TClos
| RTClos

Sourceand rbinop = private

| Union
| Inter
| Over
| LProj
| RProj
| Prod
| Diff
| Join

Sourceand ('fml, 'exp, 'iexp) oiexp = private

| Num of int
| Card of 'exp
| IUn of iunop * 'iexp
| IBin of 'iexp * ibinop * 'iexp

Sourceand iunop = private

| Neg

Sourceand ibinop = private

| Add
| Sub

Sourcetype goal = private

| Run of fml list * bool option

Sourceand fml = private

| Fml of (fml, exp, iexp) ofml Hashcons.hash_consed

Sourceand prim_exp = (fml, exp, iexp) prim_oexp

Sourceand exp = private

| Exp of (fml, exp, iexp) oexp Hashcons.hash_consed

Sourceand iexp = private

| Iexp of (fml, exp, iexp) oiexp Hashcons.hash_consed

Sourcetype 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;

}

Source

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

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 triggered : lbinop

Sourceval not_ : lunop

Sourceval eventually : 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 lt : icomp_op

Sourceval lte : icomp_op

Sourceval gt : 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

Source

val pp_sim_bindings : 
  int ->
  Format.formatter ->
  (bool * int * exp) list ->
  unit

Sourceval pp_oblock : 'a -> ('a -> 'b Fmtc.t) -> Format.formatter -> 'b list -> unit

Source

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

Source

val pp_prim_oexp : 
  int ->
  (int -> 'a Fmtc.t) ->
  (int -> Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  ('a, 'b, 'c) prim_oexp ->
  unit

Source

val 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

Install

dune-project
Dependency

Authors

Maintainers

Sources

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

Module `Libelectrod.Elo`Source

package electrod

Install

dune-project Dependency

Authors

Maintainers

Sources

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

Module Libelectrod.EloSource

dune-project
Dependency

Module `Libelectrod.Elo`Source