colibri2 0.4 · OCaml Package

val restrict_ext : bool Colibri2_core.Options.t

val restrict_aup : bool Colibri2_core.Options.t

val extended_comb : bool Colibri2_core.Options.t

val blast_rule : bool Colibri2_core.Options.t

val default_values : bool Colibri2_core.Options.t

val use_diff_graph : bool Colibri2_core.Options.t

val use_choice : bool Colibri2_core.Options.t

val debug : Colibri2_core.Debug.flag

val convert : 
  subst:Colibri2_core.Ground.Subst.t ->
  'a Colibri2_core.Egraph.t ->
  Colibri2_core.Expr.term ->
  Colibri2_core.Node.t

module STV : sig ... end

val replicate : int -> 'a -> 'a list

val mk_store_term : 
  Colibri2_core.Expr.term ->
  Colibri2_core.Expr.term ->
  Colibri2_core.Expr.term ->
  Colibri2_core.Expr.term

val mk_select_term : 
  Colibri2_core.Expr.term ->
  Colibri2_core.Expr.term ->
  Colibri2_core.Expr.term

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

val array_gty_args : 
  Colibri2_core.Ground.Ty.t ->
  Colibri2_core.Ground.Ty.t * Colibri2_core.Ground.Ty.t

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

exception Not_An_Array

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

val get_array_gty_args : 
  'a Colibri2_core.Egraph.t ->
  Colibri2_core.Node.t ->
  Colibri2_core.Ground.Ty.t * Colibri2_core.Ground.Ty.t

val add_array_gty : 
  Colibri2_core.Egraph.wt ->
  Colibri2_core.Node.t ->
  Colibri2_core.Ground.Ty.t ->
  Colibri2_core.Ground.Ty.t ->
  unit

module Builtin : sig ... end

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

val mk_or : 
  'a Colibri2_core.Egraph.t ->
  Colibri2_core.Node.t ->
  Colibri2_core.Node.t ->
  Colibri2_core.Node.t

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

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

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

val distinct_arrays_term : 
  Colibri2_core.Expr.term ->
  Colibri2_core.Expr.term ->
  Colibri2_core.Expr.term

package colibri2