sig
type var =
[ `Const of string | `FO of string | `Real of string | `SO of string ]
type const_var = [ `Const of string ]
type fo_var = [ `FO of string ]
type const_or_fo_var = [ `Const of string | `FO of string ]
type so_var = [ `SO of string ]
type real_var = [ `Real of string ]
val var_of_string : string -> Formula.var
val const_var_of_string : string -> Formula.const_var
val fo_var_of_string : string -> Formula.fo_var
val const_or_fo_var_of_string : string -> Formula.const_or_fo_var
val so_var_of_string : string -> Formula.so_var
val real_var_of_string : string -> Formula.real_var
val is_const : Formula.var -> bool
val is_fo : Formula.var -> bool
val is_so : Formula.var -> bool
val is_real : Formula.var -> bool
val to_const : Formula.var -> Formula.const_var
val to_fo : Formula.var -> Formula.fo_var
val to_const_or_fo : Formula.var -> Formula.const_or_fo_var
val to_so : Formula.var -> Formula.so_var
val to_real : Formula.var -> Formula.real_var
val var_tup : [< Formula.var ] array -> Formula.var array
val compare_vars : ([< Formula.var ] as 'a) -> 'a -> int
val compare_var_lists : ([< Formula.var ] as 'a) list -> 'a list -> int
val compare_var_tups : ([< Formula.var ] as 'a) array -> 'a array -> int
type sign_op = EQZero | GZero | LZero | GEQZero | LEQZero | NEQZero
val sign_op_str : ?unicode:bool -> Formula.sign_op -> string
type formula =
Rel of string * Formula.const_or_fo_var array
| Eq of Formula.const_or_fo_var * Formula.const_or_fo_var
| SO of Formula.so_var * Formula.const_or_fo_var array
| RealExpr of Formula.real_expr * Formula.sign_op
| Not of Formula.formula
| And of Formula.formula list
| Or of Formula.formula list
| Ex of Formula.var list * Formula.formula
| All of Formula.var list * Formula.formula
| Lfp of Formula.so_var * Formula.fo_var array * Formula.formula
| Gfp of Formula.so_var * Formula.fo_var array * Formula.formula
| Let of string * string list * Formula.formula * Formula.formula
and real_expr =
RVar of string
| Const of float
| Plus of Formula.real_expr * Formula.real_expr
| Times of Formula.real_expr * Formula.real_expr
| Pow of Formula.real_expr * Formula.real_expr
| Fun of string * Formula.const_or_fo_var
| Char of Formula.formula
| Sum of Formula.fo_var list * Formula.formula * Formula.real_expr
| RLet of string * Formula.real_expr * Formula.real_expr
val size : ?acc:int -> Formula.formula -> int
val size_real : ?acc:int -> Formula.real_expr -> int
val so_compare_weight : int Pervasives.ref
val compare : Formula.formula -> Formula.formula -> int
val compare_re : Formula.real_expr -> Formula.real_expr -> int
val is_atom : Formula.formula -> bool
val is_literal : Formula.formula -> bool
type eq_sys = ((string * string) * Formula.real_expr) list
val var_str : [< Formula.var ] -> string
val var_list_str : [< Formula.var ] list -> string
val str : ?unicode:bool -> Formula.formula -> string
val mona_str : Formula.formula -> string
val print : ?unicode:bool -> Formula.formula -> unit
val sprint : ?unicode:bool -> Formula.formula -> string
val fprint : ?unicode:bool -> Format.formatter -> Formula.formula -> unit
val real_str : ?unicode:bool -> Formula.real_expr -> string
val print_real : ?unicode:bool -> Formula.real_expr -> unit
val sprint_real : ?unicode:bool -> Formula.real_expr -> string
val fprint_real :
?unicode:bool -> Format.formatter -> Formula.real_expr -> unit
val fprint_prec :
bool -> int -> Format.formatter -> Formula.formula -> unit
val fprint_real_prec :
bool -> int -> Format.formatter -> Formula.real_expr -> unit
val fprint_eqs :
?unicode:bool -> ?diff:bool -> Format.formatter -> Formula.eq_sys -> unit
val eq_str : ?unicode:bool -> ?diff:bool -> Formula.eq_sys -> string
val syntax_ok :
?sg:(string * int) list Pervasives.ref ->
?fp:(string * bool) list -> ?pos:bool -> Formula.formula -> bool
val syntax_ok_re :
?sg:(string * int) list Pervasives.ref ->
?fp:(string * bool) list -> ?pos:bool -> Formula.real_expr -> bool
val flatten : Formula.formula -> Formula.formula
val flatten_re : Formula.real_expr -> Formula.real_expr
val flatten_sort : Formula.formula -> Formula.formula
val flatten_sort_re : Formula.real_expr -> Formula.real_expr
val compile :
string -> Formula.eq_sys -> float -> float array -> float array
val rk4_step :
float ->
float ->
(float -> float array -> float array) -> float array -> float array
val rkCK_default_start :
unit ->
float Pervasives.ref * float Pervasives.ref * float Pervasives.ref *
float Pervasives.ref
val rkCK_step :
?epsilon:float ->
float Pervasives.ref * float Pervasives.ref * float Pervasives.ref *
float Pervasives.ref ->
float ->
float ->
(float -> float array -> float array) ->
float array -> float array * float * float
type raw_formula =
HRel of string * Formula.const_or_fo_var array
| HEq of Formula.const_or_fo_var * Formula.const_or_fo_var
| HSO of Formula.so_var * Formula.const_or_fo_var array
| HRealExpr of Formula.hc_real_expr * Formula.sign_op
| HNot of Formula.hc_formula
| HAnd of Formula.hc_formula list
| HOr of Formula.hc_formula list
| HEx of Formula.var list * Formula.hc_formula
| HAll of Formula.var list * Formula.hc_formula
| HLfp of Formula.so_var * Formula.fo_var array * Formula.hc_formula
| HGfp of Formula.so_var * Formula.fo_var array * Formula.hc_formula
| HLet of string * string list * Formula.hc_formula * Formula.hc_formula
and raw_real_expr =
HRVar of string
| HConst of float
| HPlus of Formula.hc_real_expr * Formula.hc_real_expr
| HTimes of Formula.hc_real_expr * Formula.hc_real_expr
| HPow of Formula.hc_real_expr * Formula.hc_real_expr
| HFun of string * Formula.const_or_fo_var
| HChar of Formula.hc_formula
| HSum of Formula.fo_var list * Formula.hc_formula * Formula.hc_real_expr
| HRLet of string * Formula.hc_real_expr * Formula.hc_real_expr
and hc_formula = Formula.raw_formula HashCons.hc
and hc_real_expr = Formula.raw_real_expr HashCons.hc
module FormulaCons :
sig
type data = raw_formula
type t
val create : int -> t
val clear : t -> unit
val hashcons : ?log:bool -> t -> data -> data HashCons.hc
module H1 :
sig
type key = data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module H2 :
sig
type key = data HashCons.hc * data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
type other_value = int list
module HV :
sig
type key = data HashCons.hc * other_value
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
val get_h1 : t -> data HashCons.hc H1.t
val get_h2 : t -> data HashCons.hc H2.t
val get_hv : t -> data HashCons.hc HV.t
val get_h1_alpha :
(module HashCons.Type with type t = 'a) -> t -> 'a H1.t
end
module RealExprCons :
sig
type data = raw_real_expr
type t
val create : int -> t
val clear : t -> unit
val hashcons : ?log:bool -> t -> data -> data HashCons.hc
module H1 :
sig
type key = data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module H2 :
sig
type key = data HashCons.hc * data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
type other_value = int list
module HV :
sig
type key = data HashCons.hc * other_value
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
val get_h1 : t -> data HashCons.hc H1.t
val get_h2 : t -> data HashCons.hc H2.t
val get_hv : t -> data HashCons.hc HV.t
val get_h1_alpha :
(module HashCons.Type with type t = 'a) -> t -> 'a H1.t
end
val hc : Formula.formula -> Formula.hc_formula
val hc_real : Formula.real_expr -> Formula.hc_real_expr
val cAnd : Formula.hc_formula list -> Formula.hc_formula
val unhc : Formula.hc_formula -> Formula.formula
val unhc_real : Formula.hc_real_expr -> Formula.real_expr
end