sig
  type source =
      PropSet
    | BlockFrontier
    | BlockRec of Clause.t
    | IndGen of Clause.t
    | CopyFwdProp of Clause.t
    | CopyBlockProp of Clause.t
    | Copy of Clause.t
  and t
  module ClauseTrie :
    sig
      type key = Term.t list
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> '-> 'a t -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val for_all : (key -> '-> bool) -> 'a t -> bool
      val exists : (key -> '-> bool) -> 'a t -> bool
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('-> 'b) -> 'a t -> 'b t
      val mapi : (key -> '-> 'b) -> 'a t -> 'b t
      val find_prefix : key -> 'a t -> 'a t
      val mem_prefix : key -> 'a t -> bool
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val fold2 : (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
      val map2 : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t
      val iter2 : (key -> '-> '-> unit) -> 'a t -> 'b t -> unit
      val for_all2 : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val exists2 : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val subsume : 'a t -> key -> (key * 'a) list * 'a t
      val is_subsumed : 'a t -> key -> bool
      val pp_print_trie :
        (Format.formatter -> key * '-> unit) ->
        ('b, Format.formatter, unit) format ->
        Format.formatter -> 'a t -> unit
    end
  val mk_clause_of_literals : Clause.source -> Term.t list -> Clause.t
  val copy_clause_block_prop : Clause.t -> Clause.t
  val copy_clause_fwd_prop : Clause.t -> Clause.t
  val copy_clause : Clause.t -> Clause.t
  val id_of_clause : Clause.t -> int
  val length_of_clause : Clause.t -> int
  val term_of_clause : Clause.t -> Term.t
  val literals_of_clause : Clause.t -> Term.t list
  val source_of_clause : Clause.t -> Clause.source
  val actlit_p0_of_clause : SMTSolver.t -> Clause.t -> Term.t
  val actlit_p1_of_clause : SMTSolver.t -> Clause.t -> Term.t
  val actlits_n0_of_clause : SMTSolver.t -> Clause.t -> Term.t list
  val actlits_n1_of_clause : SMTSolver.t -> Clause.t -> Term.t list
  val deactivate_clause : SMTSolver.t -> Clause.t -> unit
  val undo_ind_gen : Clause.t -> Clause.t option
  type prop_set
  val prop_set_of_props : (string * Term.t) list -> Clause.prop_set
  val clause_of_prop_set : Clause.prop_set -> Clause.t
  val term_of_prop_set : Clause.prop_set -> Term.t
  val props_of_prop_set : Clause.prop_set -> (string * Term.t) list
  val actlit_p0_of_prop_set : SMTSolver.t -> Clause.prop_set -> Term.t
  val actlit_p1_of_prop_set : SMTSolver.t -> Clause.prop_set -> Term.t
  val actlits_n0_of_prop_set : SMTSolver.t -> Clause.prop_set -> Term.t list
  val actlits_n1_of_prop_set : SMTSolver.t -> Clause.prop_set -> Term.t list
  val actlit_of_frame : int -> Term.t
  val actlit_symbol_of_frame : int -> UfSymbol.t
  type actlit_type = Actlit_p0 | Actlit_n0 | Actlit_p1 | Actlit_n1
  val create_and_assert_fresh_actlit :
    SMTSolver.t -> string -> Term.t -> Clause.actlit_type -> Term.t
end