(*************************************************************************)
(*  This file is part of Colibri2.                                       *)
(*                                                                       *)
(*  Copyright (C) 2014-2021                                              *)
(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
(*           alternatives)                                               *)
(*    OCamlPro                                                           *)
(*                                                                       *)
(*  you can redistribute it and/or modify it under the terms of the GNU  *)
(*  Lesser General Public License as published by the Free Software      *)
(*  Foundation, version 2.1.                                             *)
(*                                                                       *)
(*  It is distributed in the hope that it will be useful,                *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
(*  GNU Lesser General Public License for more details.                  *)
(*                                                                       *)
(*  See the GNU Lesser General Public License version 2.1                *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
(*************************************************************************)

open Colibri2_popop_lib
open Popop_stdlib

val no_wegraph : bool Options.t
val no_res_ext : bool Options.t
val no_res_aup : bool Options.t
val extended_comb : bool Options.t
val blast_rule : bool Options.t
val default_values : bool Options.t
val debug : Debug.flag
val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t

exception Not_An_Array of Node.t
exception Not_An_Array_gty of Ground.Ty.t
exception Not_An_Array_ty of Expr.ty
exception Type_Not_Set of Node.t
exception NoIdFound of string * Node.t
exception Not_a_neighbour of (Node.t * Node.t * Node.t)
exception Empty_neighbour_set of (Node.t * Node.t * Node.t)

module STV : sig
  val ind_ty_var : Dolmen_std.Expr.ty_var
  val val_ty_var : Dolmen_std.Expr.ty_var
  val alpha_ty_var : Dolmen_std.Expr.ty_var
  val a_ty_var : Dolmen_std.Expr.ty_var
  val b_ty_var : Dolmen_std.Expr.ty_var
  val c_ty_var : Dolmen_std.Expr.ty_var
  val ind_ty : Expr.ty
  val val_ty : Expr.ty
  val a_ty : Expr.ty
  val b_ty : Expr.ty
  val c_ty : Expr.ty
  val alpha_ty : Expr.ty
  val array_ty : Expr.ty
  val array_ty_ab : Expr.ty
  val array_ty_ac : Expr.ty
  val array_ty_alpha : Expr.ty
  val term_of_var : Dolmen_std.Expr.term_var -> Expr.term
  val mk_index_var : string -> Dolmen_std.Expr.term_var
  val mk_value_var : string -> Dolmen_std.Expr.term_var
  val mk_array_var : string -> Dolmen_std.Expr.term_var
  val vi : Dolmen_std.Expr.term_var
  val vj : Dolmen_std.Expr.term_var
  val vk : Dolmen_std.Expr.term_var
  val vv : Dolmen_std.Expr.term_var
  val ti : Expr.term
  val tj : Expr.term
  val tk : Expr.term
  val tv : Expr.term
  val va : Dolmen_std.Expr.term_var
  val vb : Dolmen_std.Expr.term_var
  val ta : Expr.term
  val tb : Expr.term
end

val replicate : int -> 'a -> 'a list
val mk_store_term : Expr.term -> Expr.term -> Expr.term -> Expr.term
val mk_select_term : Expr.term -> Expr.term -> Expr.term

val apply_cst :
  Dolmen_std.Expr.term_cst -> Expr.ty list -> Expr.term list -> Expr.term

val array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t
val get_node_ty : 'a Egraph.t -> Node.t -> Ground.Ty.t
val get_array_gty : 'a Egraph.t -> Node.t -> Ground.Ty.t
val get_array_gty_args : 'a Egraph.t -> Node.t -> Ground.Ty.t * Ground.Ty.t
val add_array_gty : Egraph.wt -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> unit

module Builtin : sig
  type 'a Builtin.t +=
    | Array_diff
    | Array_const
    | Array_map
    | Array_default_index
    | Array_default_value

  val array_diff : Dolmen_std.Expr.term_cst
  val array_const : Dolmen_std.Expr.term_cst
  val array_map : int -> Dolmen_std.Expr.term_cst
  val array_default_index : Dolmen_std.Expr.term_cst
  val array_default_value : Dolmen_std.Expr.term_cst
  val apply_array_diff : Expr.term -> Expr.term -> Expr.term
  val apply_array_const : Expr.term -> Expr.term
  val apply_array_def_index : Expr.term -> Expr.term
  val apply_array_def_value : Expr.term -> Expr.term
  val apply_array_map : int -> Expr.term -> Expr.term list -> Expr.term
end

val mk_subst :
  (Dolmen_std.Expr.term_var * Node.t) list ->
  (Dolmen_std.Expr.ty_var * Ground.Ty.t) list ->
  Ground.Subst.t

val ground_apply :
  Egraph.wt ->
  Dolmen_std.Expr.term_cst ->
  Ground.Ty.t list ->
  Node.t list ->
  Node.t

val mk_or : 'a Egraph.t -> Node.t list -> Node.t
val mk_and : 'a Egraph.t -> Node.t list -> Node.t

val mk_store :
  'a Egraph.t ->
  Node.t ->
  Node.t ->
  Node.t ->
  Ground.Ty.t ->
  Ground.Ty.t ->
  Node.t

val mk_select :
  'a Egraph.t -> Node.t -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> Node.t

val mk_distinct_arrays :
  Egraph.wt -> Node.t -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> Node.t

val mk_array_const : 'a Egraph.t -> Node.t -> Ground.Ty.t -> Node.t
val distinct_arrays_term : Expr.term -> Expr.term -> Expr.term
val do_mk_eq : Egraph.wt -> Node.t -> Node.t -> unit
val do_mk_eq_if_neq : Egraph.wt -> Node.t -> Node.t -> unit

module type HTS = sig
  type key
  type t

  val set : Egraph.wt -> key -> t -> unit
  val find : Egraph.wt -> key -> t
  val find_opt : Egraph.wt -> key -> t option
  val change : f:(t option -> t option) -> Egraph.wt -> key -> unit
  val remove : Egraph.wt -> key -> unit
  val iter : f:(key -> t -> unit) -> Egraph.wt -> unit
  val fold : (key -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
  val pp : Format.formatter -> Egraph.wt -> unit
end

module MkIHT (V : sig
  type t

  val pp : t Pp.pp
  val name : string
end) : HTS with type key = int and type t = V.t

module type IdDomSig = sig
  val register_merge_hook :
    Egraph.wt ->
    (Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
    unit

  val register_new_id_hook :
    Egraph.wt -> (Egraph.wt -> int -> Node.t -> unit) -> unit

  val set_id : Egraph.wt -> Node.t -> unit
  val get_id : Egraph.wt -> Node.t -> int
end

module MkIdDom (_ : sig
  val name : string
end) : IdDomSig

module SHT (K : sig
  include Datatype

  val sort : t -> t
  val pp : t Pp.pp
end) (V : sig
  type t

  val name : string
  val pp : t Pp.pp
end) : HTS with type key = K.t and type t = V.t

module I4 :
  Datatype
    with type t = DInt.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t

module I3 :
  Datatype with type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t

module I2 : Datatype with type t = DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
module I1 : Datatype with type t = DInt.t * Ground.Ty.t * Ground.Ty.t