sig
type 'a element =
'a Qed.Logic.element =
E_none
| E_true
| E_false
| E_int of int
| E_const of 'a
type 'a operator =
'a Qed.Logic.operator = {
inversible : bool;
associative : bool;
commutative : bool;
idempotent : bool;
neutral : 'a element;
absorbant : 'a element;
}
type 'a category =
'a Qed.Logic.category =
Function
| Constructor
| Injection
| Operator of 'a operator
type binder = Qed.Logic.binder = Forall | Exists | Lambda
type ('f, 'a) datatype =
('f, 'a) Qed.Logic.datatype =
Prop
| Bool
| Int
| Real
| Tvar of int
| Array of ('f, 'a) datatype * ('f, 'a) datatype
| Record of ('f * ('f, 'a) datatype) list
| Data of 'a * ('f, 'a) datatype list
type sort =
Qed.Logic.sort =
Sprop
| Sbool
| Sint
| Sreal
| Sdata
| Sarray of sort
type maybe = Qed.Logic.maybe = Yes | No | Maybe
module type Symbol =
sig
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
end
module type Data =
sig
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val basename : t -> string
end
module type Field =
sig
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val sort : t -> sort
end
module type Function =
sig
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val category : t -> t category
val params : t -> sort list
val sort : t -> sort
end
module type Variable =
sig
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val sort : t -> sort
val basename : t -> string
val dummy : t
end
type ('f, 'a) funtype =
('f, 'a) Qed.Logic.funtype = {
result : ('f, 'a) datatype;
params : ('f, 'a) datatype list;
}
type ('z, 'f, 'd, 'x, 'e) term_repr =
('z, 'f, 'd, 'x, 'e) Qed.Logic.term_repr =
True
| False
| Kint of 'z
| Kreal of Qed.R.t
| Times of 'z * 'e
| Add of 'e list
| Mul of 'e list
| Div of 'e * 'e
| Mod of 'e * 'e
| Eq of 'e * 'e
| Neq of 'e * 'e
| Leq of 'e * 'e
| Lt of 'e * 'e
| Aget of 'e * 'e
| Aset of 'e * 'e * 'e
| Rget of 'e * 'f
| Rdef of ('f * 'e) list
| And of 'e list
| Or of 'e list
| Not of 'e
| Imply of 'e list * 'e
| If of 'e * 'e * 'e
| Fun of 'd * 'e list
| Var of 'x
| Apply of 'e * 'e list
| Bind of binder * 'x * 'e
type ('z, 'a) affine =
('z, 'a) Qed.Logic.affine = {
constant : 'z;
factors : ('z * 'a) list;
}
module type Term =
sig
module Z : Qed.Arith.Z
module ADT : Data
module Field : Field
module Fun : Function
module Var : Variable
type term
type var = Var.t
type tau = (Field.t, ADT.t) datatype
type signature = (Field.t, ADT.t) funtype
module Vars :
sig
type elt = var
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val find : elt -> t -> elt
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val map : (elt -> elt) -> t -> t
val mapf : (elt -> elt option) -> t -> t
val intersect : t -> t -> bool
end
module Vmap :
sig
type key = var
type 'a t
val is_empty : 'a t -> bool
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val remove : key -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) ->
key -> 'b -> 'a t -> 'a t
end
type pool
val pool : ?copy:pool -> unit -> pool
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
val add_term : pool -> term -> unit
val fresh : pool -> ?basename:string -> tau -> var
val alpha : pool -> var -> var
val tau_of_var : var -> tau
val base_of_var : var -> string
type 'a expression = (Z.t, Field.t, Fun.t, var, 'a) term_repr
type repr = term expression
type path = int list
type record = (Field.t * term) list
val decide : term -> bool
val is_true : term -> maybe
val is_false : term -> maybe
val is_prop : term -> bool
val is_int : term -> bool
val is_real : term -> bool
val is_arith : term -> bool
val are_equal : term -> term -> maybe
val eval_eq : term -> term -> bool
val eval_neq : term -> term -> bool
val eval_lt : term -> term -> bool
val eval_leq : term -> term -> bool
val repr : term -> repr
val sort : term -> sort
val vars : term -> Vars.t
val subterm : term -> path -> term
val change_subterm : term -> path -> term -> term
val e_true : term
val e_false : term
val e_bool : bool -> term
val e_literal : bool -> term -> term
val e_int : int -> term
val e_zint : Z.t -> term
val e_real : Qed.R.t -> term
val e_var : var -> term
val e_opp : term -> term
val e_times : Z.t -> term -> term
val e_sum : term list -> term
val e_prod : term list -> term
val e_add : term -> term -> term
val e_sub : term -> term -> term
val e_mul : term -> term -> term
val e_div : term -> term -> term
val e_mod : term -> term -> term
val e_eq : term -> term -> term
val e_neq : term -> term -> term
val e_leq : term -> term -> term
val e_lt : term -> term -> term
val e_imply : term list -> term -> term
val e_equiv : term -> term -> term
val e_and : term list -> term
val e_or : term list -> term
val e_not : term -> term
val e_if : term -> term -> term -> term
val e_get : term -> term -> term
val e_set : term -> term -> term -> term
val e_getfield : term -> Field.t -> term
val e_record : record -> term
val e_fun : Fun.t -> term list -> term
val e_repr : repr -> term
val e_forall : var list -> term -> term
val e_exists : var list -> term -> term
val e_lambda : var list -> term -> term
val e_bind : binder -> var -> term -> term
val e_subst : ?pool:pool -> var -> term -> term -> term
val e_apply : ?pool:pool -> term -> term list -> term
val r_map : ('a -> term) -> 'a expression -> term
val e_map : (term -> term) -> term -> term
val e_iter : (term -> unit) -> term -> unit
val f_map : (Vars.t -> term -> term) -> Vars.t -> term -> term
val f_iter : (Vars.t -> term -> unit) -> Vars.t -> term -> unit
val set_builtin : Fun.t -> (term list -> term) -> unit
val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
val literal : term -> bool * term
val congruence_eq : term -> term -> (term * term) list option
val congruence_neq : term -> term -> (term * term) list option
val flattenable : term -> bool
val flattens : term -> term -> bool
val flatten : term -> term list
val affine : term -> (Z.t, term) affine
val record_with : record -> (term * record) option
type t = term
val id : t -> int
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val weigth : t -> int
val is_closed : t -> bool
val is_simple : t -> bool
val is_atomic : t -> bool
val is_primitive : t -> bool
val is_neutral : Fun.t -> t -> bool
val is_absorbant : Fun.t -> t -> bool
val size : t -> int
val basename : t -> string
val debug : Format.formatter -> t -> unit
val pp_id : Format.formatter -> t -> unit
val pp_rid : Format.formatter -> t -> unit
val pp_repr : Format.formatter -> repr -> unit
module Tset :
sig
type elt = term
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val find : elt -> t -> elt
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val map : (elt -> elt) -> t -> t
val mapf : (elt -> elt option) -> t -> t
val intersect : t -> t -> bool
end
module Tmap :
sig
type key = term
type 'a t
val is_empty : 'a t -> bool
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val remove : key -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) ->
key -> 'b -> 'a t -> 'a t
end
val shared :
?shared:(term -> bool) ->
?shareable:(term -> bool) -> ?closed:Vars.t -> term list -> term list
type marks
val marks :
?shared:(term -> bool) ->
?shareable:(term -> bool) -> ?closed:Vars.t -> unit -> marks
val mark : marks -> term -> unit
val defs : marks -> term list
end
end