<commit_before>
(*
Zipperposition: a functional superposition prover for prototyping
Copyright (c) 2013, <NAME>
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer.  Redistributions in binary
form must reproduce the above copyright notice, this list of conditions and the
following disclaimer in the documentation and/or other materials provided with
the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(** {1 Clauses} *)

open Logtk

module ST = ScopedTerm
module T = FOTerm
module S = Substs
module Lit = Literal
module Lits = Literals

let stat_fresh = Util.mk_stat "fresh_clause"
let stat_clause_create = Util.mk_stat "clause_create"
let prof_clause_create = Util.mk_profiler "clause_create"

type scope = Substs.scope

(** {2 Clauses that depend on a Context} *)
module type S = sig
  module Ctx : Ctx.S

  (* TODO: maybe a global (weak) graph of parents/descendants
   * would be leaner on memory? *)

  type t
  type clause = t

  (** {2 Flags} *)

  val flag_ground : int                       (** clause is ground *)
  val flag_lemma : int                        (** clause is a lemma *)
  val flag_persistent : int                   (** clause cannot be redundant *)

  val set_flag : int -> t -> bool -> unit     (** set boolean flag *)
  val get_flag : int -> t -> bool             (** get value of boolean flag *)
  val new_flag : unit -> int                  (** new flag that can be used on clauses *)

  (** {2 Basics} *)

  include Interfaces.EQ with type t := t
  include Interfaces.HASH with type t := t
  val compare : t -> t -> int

  val id : t -> int
  val lits : t -> Literal.t array
  val parents : t -> t list

  val compact : t -> CompactClause.t (** Turn into a compact clause *)
  val is_ground : t -> bool
  val weight : t -> int

  module CHashtbl : Hashtbl.S with type key = t

  module CHashSet : sig
    type t
    val create : unit -> t
    val is_empty : t -> bool
    val member : t -> clause -> bool
    val iter : t -> (clause -> unit) -> unit
    val add : t -> clause -> unit
    val to_list : t -> clause list
  end

  val is_child_of : child:t -> t -> unit
    (** [is_child_of ~child c] is to be called to remember that [child] is a child
        of [c], is has been infered/simplified from [c] *)

  val follow_simpl : t -> t
    (** Follow the "hcsimplto" links until the clause has None *)

  val simpl_to : from:t -> into:t -> unit
    (** [simpl_to ~from ~into] sets the link of [from] to [into], so that
        the simplification of [from] into [into] is cached. *)

  module CHashcons : Hashcons.S with type elt = clause

  val create : ?parents:t list -> ?selected:BV.t ->
               Literal.t list ->
               (CompactClause.t -> Proof.t) -> t
    (** Build a new hclause from the given literals. *)

  val create_a : ?parents:t list -> ?selected:BV.t ->
                  Literal.t array ->
                  (CompactClause.t -> Proof.t) -> t
    (** Build a new hclause from the given literals. *)

  val of_forms : ?parents:t list -> ?selected:BV.t ->
                      Formula.FO.t list ->
                      (CompactClause.t -> Proof.t) -> t
    (** Directly from list of formulas *)

  val of_forms_axiom : ?role:string -> file:string -> name:string ->
                       Formula.FO.t list -> t
    (** Construction from formulas as axiom (initial clause) *)

  val proof : t -> Proof.t
    (** Extract its proof from the clause *)

  val stats : unit -> (int*int*int*int*int*int)
    (** hashconsing stats *)

  val is_empty : t -> bool
    (** Is the clause an empty clause? *)

  val length : t -> int
    (** Number of literals *)

  val descendants : t -> int SmallSet.t
    (** set of ID of descendants of the clause *)

  val apply_subst : renaming:Substs.Renaming.t -> Substs.t -> t -> scope -> t
    (** apply the substitution to the clause *)

  val maxlits : t -> scope -> Substs.t -> BV.t
    (** List of maximal literals *)

  val is_maxlit : t -> scope -> Substs.t -> idx:int -> bool
    (** Is the i-th literal maximal in subst(clause)? Equivalent to
        Bitvector.get (maxlits ~ord c subst) i *)

  val eligible_res : t -> scope -> Substs.t -> BV.t
    (** Bitvector that indicates which of the literals of [subst(clause)]
        are eligible for resolution. THe literal has to be either maximal
        among selected literals of the same sign, if some literal is selected,
        or maximal if none is selected. *)

  val eligible_param : t -> scope -> Substs.t -> BV.t
    (** Bitvector that indicates which of the literals of [subst(clause)]
        are eligible for paramodulation. That means the literal
        is positive, no literal is selecteed, and the literal
        is maximal among literals of [subst(clause)]. *)

  val eligible_chaining : t -> scope -> Substs.t -> BV.t
    (** Bitvector of literals of [subst(clause)] that are eligible
        for equality chaining or inequality chaining. That amouns to being
        a maximal, positive inequality literal within the clause,
        and assume the clause has no selected literal. *)

  val has_selected_lits : t -> bool
    (** does the clause have some selected literals? *)

  val is_selected : t -> int -> bool
    (** check whether a literal is selected *)

  val selected_lits : t -> (Literal.t * int) list
    (** get the list of selected literals *)

  val is_unit_clause : t -> bool
    (** is the clause a unit clause? *)

  val is_oriented_rule : t -> bool
    (** Is the clause a positive oriented clause? *)

  val symbols : ?init:Symbol.Set.t -> t Sequence.t -> Symbol.Set.t
    (** symbols that occur in the clause *)

  module Seq : sig
    val lits : t -> Literal.t Sequence.t
    val terms : t -> FOTerm.t Sequence.t
    val vars : t -> FOTerm.t Sequence.t

    val abstract : t -> (bool * FOTerm.t Sequence.t) Sequence.t
      (** Easy iteration on an abstract view of literals *)
  end

  (** {2 Filter literals} *)

  module Eligible : sig
    type t = int -> Literal.t -> bool
      (** Eligibility criterion for a literal *)

    val res : clause -> t
      (** Only literals that are eligible for resolution *)

    val param : clause -> t
      (** Only literals that are eligible for paramodulation *)

    val chaining : clause -> t
      (** Eligible for chaining *)

    val eq : t
      (** Equations *)

    val ineq : clause -> t
      (** Only literals that are inequations *)

    val ineq_of : clause -> Theories.TotalOrder.t -> t
      (** Only literals that are inequations for the given ordering *)

    val arith : t

    val filter : (Literal.t -> bool) -> t

    val max : clause -> t
      (** Maximal literals of the clause *)

    val pos : t
      (** Only positive literals *)

    val neg : t
      (** Only negative literals *)

    val always : t
      (** All literals *)

    val combine : t list -> t
      (** Logical "and" of the given eligibility criteria. A literal is
          eligible only if all elements of the list say so. *)

    val ( ** ) : t -> t -> t
      (** Logical "and" *)

    val ( ++ ) : t -> t -> t
      (** Logical "or" *)

    val ( ~~ ) : t -> t
      (** Logical "not" *)
  end

  (** {2 Set of clauses} *)

  (** Simple set *)
  module ClauseSet : Set.S with type elt = t

  (** Set with access by ID, bookeeping of maximal var... *)
  module CSet : sig
    (** Set of hashconsed clauses. *)
    type t

    val empty : t
      (** the empty set *)

    val is_empty : t -> bool
      (** is the set empty? *)

    val size : t -> int
      (** number of clauses in the set *)

    val add : t -> clause -> t
      (** add the clause to the set *)

    val add_list : t -> clause list -> t
      (** add several clauses to the set *)

    val remove_id : t -> int -> t
      (** remove clause by ID *)

    val remove : t -> clause -> t
      (** remove hclause *)

    val remove_list : t -> clause list -> t
      (** remove hclauses *)

    val get : t -> int -> clause
      (** get a clause by its ID *)

    val mem : t -> clause -> bool
      (** membership test *)

    val mem_id : t -> int -> bool
      (** membership test by t ID *)

    val choose : t -> clause option
      (** Choose a clause in the set *)

    val union : t -> t -> t
      (** Union of sets *)

    val inter : t -> t -> t
      (** Intersection of sets *)

    val iter : t -> (clause -> unit) -> unit
      (** iterate on clauses in the set *)

    val iteri : t -> (int -> clause -> unit) -> unit
      (** iterate on clauses in the set with their ID *)

    val fold : t -> 'b -> ('b -> int -> clause -> 'b) -> 'b
      (** fold on clauses *)

    val to_list : t -> clause list
    val of_list : clause list -> t

    val to_seq : t -> clause Sequence.t
    val of_seq : t -> clause Sequence.t -> t
    val remove_seq : t -> clause Sequence.t -> t
    val remove_id_seq : t -> int Sequence.t -> t
  end

  (** {2 Position} *)

  module Pos : sig
    val at : t -> Position.t -> FOTerm.t
  end

  (** {2 Clauses with more data} *)

  (** Clause within which a subterm (and its position) are hilighted *)
  module WithPos : sig
    type t = {
      clause : clause;
      pos : Position.t;
      term : FOTerm.t;
    }

    val compare : t -> t -> int
    val pp : Buffer.t -> t -> unit
  end

  (** {2 IO} *)

  val pp : Buffer.t -> t -> unit
  val pp_tstp : Buffer.t -> t -> unit
  val pp_tstp_full : Buffer.t -> t -> unit  (** Print in a cnf() statement *)

  val to_string : t -> string               (** Debug printing to a  string *)
  val fmt : Format.formatter -> t -> unit   (** debug printing *)

  val pp_set : Buffer.t -> CSet.t -> unit
  val pp_set_tstp : Buffer.t -> CSet.t -> unit
end

(** {2 Type def} *)
module Make(Ctx : Ctx.S) : S with module Ctx = Ctx = struct
  module Ctx = Ctx

  type t = {
    hclits : Literal.t array;               (** the literals *)
    mutable hctag : int;                    (** unique ID of the clause *)
    mutable hcflags : int;                  (** boolean flags for the clause *)
    mutable hcselected : BV.t;              (** bitvector for selected literals *)
    mutable hcproof : Proof.t;              (** Proof of the clause *)
    mutable hcparents : t list;             (** parents of the clause *)
    mutable hcdescendants : int SmallSet.t ;(** the set of IDs of descendants of the clause *)
    mutable hcsimplto : t option;           (** simplifies into the clause *)
  }

  type clause = t

  (** {2 boolean flags} *)

  let new_flag =
    let flag_gen = Util.Flag.create () in
    fun () -> Util.Flag.get_new flag_gen

  let flag_ground = new_flag ()
  let flag_lemma = new_flag ()
  let flag_persistent = new_flag ()

  let set_flag flag c truth =
    if truth
      then c.hcflags <- c.hcflags lor flag
      else c.hcflags <- c.hcflags land (lnot flag)

  let get_flag flag c = (c.hcflags land flag) != 0

  (** {2 Hashcons} *)

  let eq hc1 hc2 = hc1.hctag = hc2.hctag

  let compare hc1 hc2 = hc1.hctag - hc2.hctag

  let hash_fun c h = Lits.hash_fun c.hclits h
  let hash c = Hash.apply hash_fun c

  let id c = c.hctag

  let parents c = c.hcparents

  let compact c = c.hclits

  let is_ground c = get_flag flag_ground c

  let weight c = Lits.weight c.hclits

  let lits c = c.hclits

  module CHashtbl = Hashtbl.Make(struct
    type t = clause
    let hash c = hash c
    let equal c1 c2 = eq c1 c2
  end)

  module CHashSet = struct
    type t = unit CHashtbl.t
    let create () = CHashtbl.create 13
    let is_empty t = CHashtbl.length t = 0
    let member t c = CHashtbl.mem t c
    let iter t f = CHashtbl.iter (fun c _ -> f c) t
    let add t c = CHashtbl.replace t c ()
    let to_list t =
      let l = ref [] in
      iter t (fun c -> l := c :: !l);
      !l
  end

  (** {2 Utils} *)

  (** [is_child_of ~child c] is to be called to remember that [child] is a child
      of [c], is has been infered/simplified from [c] *)
  let is_child_of ~child c =
    (* update the parent clauses' sets of descendants by adding [child] *)
    let descendants = SmallSet.add c.hcdescendants child.hctag in
    c.hcdescendants <- descendants

  (* see if [c] is known to simplify into some other clause *)
  let rec _follow_simpl n c =
    if n > 10_000 then
      failwith (Util.sprintf "follow_simpl loops on %a" Lits.pp c.hclits);
    match c.hcsimplto with
    | None -> c
    | Some c' ->
      Util.debug 3 "clause %a already simplified to %a"
        Lits.pp c.hclits Lits.pp c'.hclits;
      _follow_simpl (n+1) c'

  let follow_simpl c = _follow_simpl 0 c

  (* [from] simplifies into [into] *)
  let simpl_to ~from ~into =
    let from = follow_simpl from in
    assert (from.hcsimplto = None);
    let into' = follow_simpl into in
    (* avoid cycles *)
    if from != into' then
      from.hcsimplto <- Some into

  module CHashcons = Hashcons.Make(struct
    type t = clause
    let hash c = Lits.hash c.hclits
    let equal c1 c2 = Lits.eq_com c1.hclits c2.hclits
    let tag i c = (assert (c.hctag = (-1)); c.hctag <- i)
  end)

  let __no_select = BV.empty ()

  let create ?parents ?selected lits proof =
    Util.enter_prof prof_clause_create;
    let lits = lits
      |> List.filter (function Lit.False -> false | _ -> true)
      |> List.sort Lit.compare
    in
    let lits = Array.of_list lits in
    (* proof *)
    let proof' = proof lits in
    (* create the structure *)
    let c = {
      hclits = lits;
      hcflags = 0;
      hctag = (-1);
      hcselected = __no_select;
      hcproof = proof';
      hcparents = [];
      hcdescendants = SmallSet.empty ~cmp:(fun i j -> i-j);
      hcsimplto = None;
    } in
    let old_hc, c = c, CHashcons.hashcons c in
    if c == old_hc then begin
      (* select literals, if not already done *)
      begin c.hcselected <- match selected with
        | Some bv -> bv
        | None -> Ctx.select lits
      end;
      (* compute flags *)
      if Lits.is_ground lits then set_flag flag_ground c true;
      (* parents *)
      begin match parents with
      | None -> ()
      | Some parents ->
        c.hcparents <- parents;
        List.iter (fun parent -> is_child_of ~child:c parent) parents
      end
    end;
    (* return clause *)
    Util.incr_stat stat_clause_create;
    Util.exit_prof prof_clause_create;
    c

  let create_a ?parents ?selected lits proof =
    create ?parents ?selected (Array.to_list lits) proof

  let of_forms ?parents ?selected forms proof =
    let lits = List.map Ctx.Lit.of_form forms in
    create ?parents ?selected lits proof

  let of_forms_axiom ?(role="axiom") ~file ~name forms =
    let lits = List.map Lit.Conv.of_form forms in
    let proof c = Proof.mk_c_file ~role ~file ~name c in
    create lits proof

  let proof c = c.hcproof

  let is_empty c = Array.length c.hclits = 0

  let length c = Array.length c.hclits

  let stats () = CHashcons.stats ()

  (** descendants of the clause *)
  let descendants c = c.hcdescendants

  (** Apply substitution to the clause. Note that using the same renaming for all
      literals is important. *)
  let apply_subst ~renaming subst c scope =
    let lits = Array.map
      (fun lit -> Lit.apply_subst ~renaming subst lit scope)
      c.hclits in
    let descendants = c.hcdescendants in
    let proof = Proof.adapt_c c.hcproof in
    let new_hc = create_a ~parents:[c] lits proof in
    new_hc.hcdescendants <- descendants;
    new_hc

  let _apply_subst_no_simpl subst lits sc =
    let renaming = S.Renaming.create () in
    Array.map
      (fun l -> Lit.apply_subst_no_simp ~renaming subst l sc)
      lits

  (** Bitvector that indicates which of the literals of [subst(clause)]
      are maximal under [ord] *)
  let maxlits c scope subst =
    let ord = Ctx.ord () in
    let lits' = _apply_subst_no_simpl subst c.hclits scope in
    Lits.maxlits ~ord lits'

  (** Check whether the literal is maximal *)
  let is_maxlit c scope subst ~idx =
    let ord = Ctx.ord () in
    let lits' = _apply_subst_no_simpl subst c.hclits scope in
    Lits.is_max ~ord lits' idx

  (** Bitvector that indicates which of the literals of [subst(clause)]
      are eligible for resolution. *)
  let eligible_res c scope subst =
    let ord = Ctx.ord () in
    let lits' = _apply_subst_no_simpl subst c.hclits scope in
    let selected = c.hcselected in
    let n = Array.length lits' in
    (* Literals that may be eligible: all of them if none is selected,
       selected ones otherwise. *)
    let check_sign = not (BV.is_empty selected) in
    let bv = if BV.is_empty selected
      then BV.create ~size:n true
      else BV.copy selected
    in
    (* Only keep literals that are maximal. If [check_sign] is true, comparisons
       are only done between same-sign literals. *)
    for i = 0 to n-1 do
      (* i-th lit is already known not to be max? *)
      if not (BV.get bv i) then () else
      let lit = lits'.(i) in
      for j = i+1 to n-1 do
        let lit' = lits'.(j) in
        (* check if both lits are still potentially eligible, and have the same
           sign if [check_sign] is true. *)
        if (check_sign && Lit.is_pos lit <> Lit.is_pos lit')
            || not (BV.get bv j)
          then ()
          else match Lit.Comp.compare ~ord lits'.(i) lits'.(j) with
          | Comparison.Incomparable
          | Comparison.Eq -> ()     (* no further information about i-th and j-th *)
          | Comparison.Gt -> BV.reset bv j  (* j-th cannot be max *)
          | Comparison.Lt -> BV.reset bv i  (* i-th cannot be max *)
      done;
    done;
    bv

  (** Bitvector that indicates which of the literals of [subst(clause)]
      are eligible for paramodulation. *)
  let eligible_param c scope subst =
    let ord = Ctx.ord () in
    if BV.is_empty c.hcselected then begin
      let lits' = _apply_subst_no_simpl subst c.hclits scope in
      (* maximal ones *)<commit_msg>slightly updated the eligibility for resolution criterion<commit_after>
(*
Zipperposition: a functional superposition prover for prototyping
Copyright (c) 2013, <NAME>
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer.  Redistributions in binary
form must reproduce the above copyright notice, this list of conditions and the
following disclaimer in the documentation and/or other materials provided with
the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(** {1 Clauses} *)

open Logtk

module ST = ScopedTerm
module T = FOTerm
module S = Substs
module Lit = Literal
module Lits = Literals

let stat_fresh = Util.mk_stat "fresh_clause"
let stat_clause_create = Util.mk_stat "clause_create"
let prof_clause_create = Util.mk_profiler "clause_create"

type scope = Substs.scope

(** {2 Clauses that depend on a Context} *)
module type S = sig
  module Ctx : Ctx.S

  (* TODO: maybe a global (weak) graph of parents/descendants
   * would be leaner on memory? *)

  type t
  type clause = t

  (** {2 Flags} *)

  val flag_ground : int                       (** clause is ground *)
  val flag_lemma : int                        (** clause is a lemma *)
  val flag_persistent : int                   (** clause cannot be redundant *)

  val set_flag : int -> t -> bool -> unit     (** set boolean flag *)
  val get_flag : int -> t -> bool             (** get value of boolean flag *)
  val new_flag : unit -> int                  (** new flag that can be used on clauses *)

  (** {2 Basics} *)

  include Interfaces.EQ with type t := t
  include Interfaces.HASH with type t := t
  val compare : t -> t -> int

  val id : t -> int
  val lits : t -> Literal.t array
  val parents : t -> t list

  val compact : t -> CompactClause.t (** Turn into a compact clause *)
  val is_ground : t -> bool
  val weight : t -> int

  module CHashtbl : Hashtbl.S with type key = t

  module CHashSet : sig
    type t
    val create : unit -> t
    val is_empty : t -> bool
    val member : t -> clause -> bool
    val iter : t -> (clause -> unit) -> unit
    val add : t -> clause -> unit
    val to_list : t -> clause list
  end

  val is_child_of : child:t -> t -> unit
    (** [is_child_of ~child c] is to be called to remember that [child] is a child
        of [c], is has been infered/simplified from [c] *)

  val follow_simpl : t -> t
    (** Follow the "hcsimplto" links until the clause has None *)

  val simpl_to : from:t -> into:t -> unit
    (** [simpl_to ~from ~into] sets the link of [from] to [into], so that
        the simplification of [from] into [into] is cached. *)

  module CHashcons : Hashcons.S with type elt = clause

  val create : ?parents:t list -> ?selected:BV.t ->
               Literal.t list ->
               (CompactClause.t -> Proof.t) -> t
    (** Build a new hclause from the given literals. *)

  val create_a : ?parents:t list -> ?selected:BV.t ->
                  Literal.t array ->
                  (CompactClause.t -> Proof.t) -> t
    (** Build a new hclause from the given literals. *)

  val of_forms : ?parents:t list -> ?selected:BV.t ->
                      Formula.FO.t list ->
                      (CompactClause.t -> Proof.t) -> t
    (** Directly from list of formulas *)

  val of_forms_axiom : ?role:string -> file:string -> name:string ->
                       Formula.FO.t list -> t
    (** Construction from formulas as axiom (initial clause) *)

  val proof : t -> Proof.t
    (** Extract its proof from the clause *)

  val stats : unit -> (int*int*int*int*int*int)
    (** hashconsing stats *)

  val is_empty : t -> bool
    (** Is the clause an empty clause? *)

  val length : t -> int
    (** Number of literals *)

  val descendants : t -> int SmallSet.t
    (** set of ID of descendants of the clause *)

  val apply_subst : renaming:Substs.Renaming.t -> Substs.t -> t -> scope -> t
    (** apply the substitution to the clause *)

  val maxlits : t -> scope -> Substs.t -> BV.t
    (** List of maximal literals *)

  val is_maxlit : t -> scope -> Substs.t -> idx:int -> bool
    (** Is the i-th literal maximal in subst(clause)? Equivalent to
        Bitvector.get (maxlits ~ord c subst) i *)

  val eligible_res : t -> scope -> Substs.t -> BV.t
    (** Bitvector that indicates which of the literals of [subst(clause)]
        are eligible for resolution. THe literal has to be either maximal
        among selected literals of the same sign, if some literal is selected,
        or maximal if none is selected. *)

  val eligible_param : t -> scope -> Substs.t -> BV.t
    (** Bitvector that indicates which of the literals of [subst(clause)]
        are eligible for paramodulation. That means the literal
        is positive, no literal is selecteed, and the literal
        is maximal among literals of [subst(clause)]. *)

  val eligible_chaining : t -> scope -> Substs.t -> BV.t
    (** Bitvector of literals of [subst(clause)] that are eligible
        for equality chaining or inequality chaining. That amouns to being
        a maximal, positive inequality literal within the clause,
        and assume the clause has no selected literal. *)

  val has_selected_lits : t -> bool
    (** does the clause have some selected literals? *)

  val is_selected : t -> int -> bool
    (** check whether a literal is selected *)

  val selected_lits : t -> (Literal.t * int) list
    (** get the list of selected literals *)

  val is_unit_clause : t -> bool
    (** is the clause a unit clause? *)

  val is_oriented_rule : t -> bool
    (** Is the clause a positive oriented clause? *)

  val symbols : ?init:Symbol.Set.t -> t Sequence.t -> Symbol.Set.t
    (** symbols that occur in the clause *)

  module Seq : sig
    val lits : t -> Literal.t Sequence.t
    val terms : t -> FOTerm.t Sequence.t
    val vars : t -> FOTerm.t Sequence.t

    val abstract : t -> (bool * FOTerm.t Sequence.t) Sequence.t
      (** Easy iteration on an abstract view of literals *)
  end

  (** {2 Filter literals} *)

  module Eligible : sig
    type t = int -> Literal.t -> bool
      (** Eligibility criterion for a literal *)

    val res : clause -> t
      (** Only literals that are eligible for resolution *)

    val param : clause -> t
      (** Only literals that are eligible for paramodulation *)

    val chaining : clause -> t
      (** Eligible for chaining *)

    val eq : t
      (** Equations *)

    val ineq : clause -> t
      (** Only literals that are inequations *)

    val ineq_of : clause -> Theories.TotalOrder.t -> t
      (** Only literals that are inequations for the given ordering *)

    val arith : t

    val filter : (Literal.t -> bool) -> t

    val max : clause -> t
      (** Maximal literals of the clause *)

    val pos : t
      (** Only positive literals *)

    val neg : t
      (** Only negative literals *)

    val always : t
      (** All literals *)

    val combine : t list -> t
      (** Logical "and" of the given eligibility criteria. A literal is
          eligible only if all elements of the list say so. *)

    val ( ** ) : t -> t -> t
      (** Logical "and" *)

    val ( ++ ) : t -> t -> t
      (** Logical "or" *)

    val ( ~~ ) : t -> t
      (** Logical "not" *)
  end

  (** {2 Set of clauses} *)

  (** Simple set *)
  module ClauseSet : Set.S with type elt = t

  (** Set with access by ID, bookeeping of maximal var... *)
  module CSet : sig
    (** Set of hashconsed clauses. *)
    type t

    val empty : t
      (** the empty set *)

    val is_empty : t -> bool
      (** is the set empty? *)

    val size : t -> int
      (** number of clauses in the set *)

    val add : t -> clause -> t
      (** add the clause to the set *)

    val add_list : t -> clause list -> t
      (** add several clauses to the set *)

    val remove_id : t -> int -> t
      (** remove clause by ID *)

    val remove : t -> clause -> t
      (** remove hclause *)

    val remove_list : t -> clause list -> t
      (** remove hclauses *)

    val get : t -> int -> clause
      (** get a clause by its ID *)

    val mem : t -> clause -> bool
      (** membership test *)

    val mem_id : t -> int -> bool
      (** membership test by t ID *)

    val choose : t -> clause option
      (** Choose a clause in the set *)

    val union : t -> t -> t
      (** Union of sets *)

    val inter : t -> t -> t
      (** Intersection of sets *)

    val iter : t -> (clause -> unit) -> unit
      (** iterate on clauses in the set *)

    val iteri : t -> (int -> clause -> unit) -> unit
      (** iterate on clauses in the set with their ID *)

    val fold : t -> 'b -> ('b -> int -> clause -> 'b) -> 'b
      (** fold on clauses *)

    val to_list : t -> clause list
    val of_list : clause list -> t

    val to_seq : t -> clause Sequence.t
    val of_seq : t -> clause Sequence.t -> t
    val remove_seq : t -> clause Sequence.t -> t
    val remove_id_seq : t -> int Sequence.t -> t
  end

  (** {2 Position} *)

  module Pos : sig
    val at : t -> Position.t -> FOTerm.t
  end

  (** {2 Clauses with more data} *)

  (** Clause within which a subterm (and its position) are hilighted *)
  module WithPos : sig
    type t = {
      clause : clause;
      pos : Position.t;
      term : FOTerm.t;
    }

    val compare : t -> t -> int
    val pp : Buffer.t -> t -> unit
  end

  (** {2 IO} *)

  val pp : Buffer.t -> t -> unit
  val pp_tstp : Buffer.t -> t -> unit
  val pp_tstp_full : Buffer.t -> t -> unit  (** Print in a cnf() statement *)

  val to_string : t -> string               (** Debug printing to a  string *)
  val fmt : Format.formatter -> t -> unit   (** debug printing *)

  val pp_set : Buffer.t -> CSet.t -> unit
  val pp_set_tstp : Buffer.t -> CSet.t -> unit
end

(** {2 Type def} *)
module Make(Ctx : Ctx.S) : S with module Ctx = Ctx = struct
  module Ctx = Ctx

  type t = {
    hclits : Literal.t array;               (** the literals *)
    mutable hctag : int;                    (** unique ID of the clause *)
    mutable hcflags : int;                  (** boolean flags for the clause *)
    mutable hcselected : BV.t;              (** bitvector for selected literals *)
    mutable hcproof : Proof.t;              (** Proof of the clause *)
    mutable hcparents : t list;             (** parents of the clause *)
    mutable hcdescendants : int SmallSet.t ;(** the set of IDs of descendants of the clause *)
    mutable hcsimplto : t option;           (** simplifies into the clause *)
  }

  type clause = t

  (** {2 boolean flags} *)

  let new_flag =
    let flag_gen = Util.Flag.create () in
    fun () -> Util.Flag.get_new flag_gen

  let flag_ground = new_flag ()
  let flag_lemma = new_flag ()
  let flag_persistent = new_flag ()

  let set_flag flag c truth =
    if truth
      then c.hcflags <- c.hcflags lor flag
      else c.hcflags <- c.hcflags land (lnot flag)

  let get_flag flag c = (c.hcflags land flag) != 0

  (** {2 Hashcons} *)

  let eq hc1 hc2 = hc1.hctag = hc2.hctag

  let compare hc1 hc2 = hc1.hctag - hc2.hctag

  let hash_fun c h = Lits.hash_fun c.hclits h
  let hash c = Hash.apply hash_fun c

  let id c = c.hctag

  let parents c = c.hcparents

  let compact c = c.hclits

  let is_ground c = get_flag flag_ground c

  let weight c = Lits.weight c.hclits

  let lits c = c.hclits

  module CHashtbl = Hashtbl.Make(struct
    type t = clause
    let hash c = hash c
    let equal c1 c2 = eq c1 c2
  end)

  module CHashSet = struct
    type t = unit CHashtbl.t
    let create () = CHashtbl.create 13
    let is_empty t = CHashtbl.length t = 0
    let member t c = CHashtbl.mem t c
    let iter t f = CHashtbl.iter (fun c _ -> f c) t
    let add t c = CHashtbl.replace t c ()
    let to_list t =
      let l = ref [] in
      iter t (fun c -> l := c :: !l);
      !l
  end

  (** {2 Utils} *)

  (** [is_child_of ~child c] is to be called to remember that [child] is a child
      of [c], is has been infered/simplified from [c] *)
  let is_child_of ~child c =
    (* update the parent clauses' sets of descendants by adding [child] *)
    let descendants = SmallSet.add c.hcdescendants child.hctag in
    c.hcdescendants <- descendants

  (* see if [c] is known to simplify into some other clause *)
  let rec _follow_simpl n c =
    if n > 10_000 then
      failwith (Util.sprintf "follow_simpl loops on %a" Lits.pp c.hclits);
    match c.hcsimplto with
    | None -> c
    | Some c' ->
      Util.debug 3 "clause %a already simplified to %a"
        Lits.pp c.hclits Lits.pp c'.hclits;
      _follow_simpl (n+1) c'

  let follow_simpl c = _follow_simpl 0 c

  (* [from] simplifies into [into] *)
  let simpl_to ~from ~into =
    let from = follow_simpl from in
    assert (from.hcsimplto = None);
    let into' = follow_simpl into in
    (* avoid cycles *)
    if from != into' then
      from.hcsimplto <- Some into

  module CHashcons = Hashcons.Make(struct
    type t = clause
    let hash c = Lits.hash c.hclits
    let equal c1 c2 = Lits.eq_com c1.hclits c2.hclits
    let tag i c = (assert (c.hctag = (-1)); c.hctag <- i)
  end)

  let __no_select = BV.empty ()

  let create ?parents ?selected lits proof =
    Util.enter_prof prof_clause_create;
    let lits = lits
      |> List.filter (function Lit.False -> false | _ -> true)
      |> List.sort Lit.compare
    in
    let lits = Array.of_list lits in
    (* proof *)
    let proof' = proof lits in
    (* create the structure *)
    let c = {
      hclits = lits;
      hcflags = 0;
      hctag = (-1);
      hcselected = __no_select;
      hcproof = proof';
      hcparents = [];
      hcdescendants = SmallSet.empty ~cmp:(fun i j -> i-j);
      hcsimplto = None;
    } in
    let old_hc, c = c, CHashcons.hashcons c in
    if c == old_hc then begin
      (* select literals, if not already done *)
      begin c.hcselected <- match selected with
        | Some bv -> bv
        | None -> Ctx.select lits
      end;
      (* compute flags *)
      if Lits.is_ground lits then set_flag flag_ground c true;
      (* parents *)
      begin match parents with
      | None -> ()
      | Some parents ->
        c.hcparents <- parents;
        List.iter (fun parent -> is_child_of ~child:c parent) parents
      end
    end;
    (* return clause *)
    Util.incr_stat stat_clause_create;
    Util.exit_prof prof_clause_create;
    c

  let create_a ?parents ?selected lits proof =
    create ?parents ?selected (Array.to_list lits) proof

  let of_forms ?parents ?selected forms proof =
    let lits = List.map Ctx.Lit.of_form forms in
    create ?parents ?selected lits proof

  let of_forms_axiom ?(role="axiom") ~file ~name forms =
    let lits = List.map Lit.Conv.of_form forms in
    let proof c = Proof.mk_c_file ~role ~file ~name c in
    create lits proof

  let proof c = c.hcproof

  let is_empty c = Array.length c.hclits = 0

  let length c = Array.length c.hclits

  let stats () = CHashcons.stats ()

  (** descendants of the clause *)
  let descendants c = c.hcdescendants

  (** Apply substitution to the clause. Note that using the same renaming for all
      literals is important. *)
  let apply_subst ~renaming subst c scope =
    let lits = Array.map
      (fun lit -> Lit.apply_subst ~renaming subst lit scope)
      c.hclits in
    let descendants = c.hcdescendants in
    let proof = Proof.adapt_c c.hcproof in
    let new_hc = create_a ~parents:[c] lits proof in
    new_hc.hcdescendants <- descendants;
    new_hc

  let _apply_subst_no_simpl subst lits sc =
    let renaming = S.Renaming.create () in
    Array.map
      (fun l -> Lit.apply_subst_no_simp ~renaming subst l sc)
      lits

  (** Bitvector that indicates which of the literals of [subst(clause)]
      are maximal under [ord] *)
  let maxlits c scope subst =
    let ord = Ctx.ord () in
    let lits' = _apply_subst_no_simpl subst c.hclits scope in
    Lits.maxlits ~ord lits'

  (** Check whether the literal is maximal *)
  let is_maxlit c scope subst ~idx =
    let ord = Ctx.ord () in
    let lits' = _apply_subst_no_simpl subst c.hclits scope in
    Lits.is_max ~ord lits' idx

  (** Bitvector that indicates which of the literals of [subst(clause)]
      are eligible for resolution. *)
  let eligible_res c scope subst =
    let ord = Ctx.ord () in
    let lits' = _apply_subst_no_simpl subst c.hclits scope in
    let selected = c.hcselected in
    if BV.is_empty selected
    then (
      (* maximal ones *)
      let bv = Lits.maxlits ~ord lits' in
      (* only keep literals that are positive *)
      BV.filter bv (fun i -> Lit.is_pos lits'.(i));
      bv
    ) else (
      let bv = BV.copy selected in
      let n = Array.length lits' in
      (* Only keep literals that are maximal among selected literals of the
          same sign. *)
      for i = 0 to n-1 do
        (* i-th lit is already known not to be max? *)
        if not (BV.get bv i) then () else
        let lit = lits'.(i) in
        for j = i+1 to n-1 do
          let lit' = lits'.(j) in
          (* check if both lits are still potentially eligible, and have the same
             sign if [check_sign] is true. *)
          if (Lit.is_pos lit <> Lit.is_pos lit')
              || not (BV.get bv j)
            then ()
            else match Lit.Comp.compare ~ord lits'.(i) lits'.(j) with
            | Comparison.Incomparable
            | Comparison.Eq -> ()     (* no further information about i-th and j-th *)
            | Comparison.Gt -> BV.reset bv j  (* j-th cannot be max *)
            | Comparison.Lt -> BV.reset bv i  (* i-th cannot be max *)
        done;
      done;
      bv
    )

  (** Bitvector that indicates which of the literals of [subst(clause)]
      are eligible for paramodulation. *)
  let eligible_param c scope subst =
    let ord = Ctx.ord () in
    if BV.is_empty c.hcselected then begin
      let lits' = _apply_subst_no_simpl subst c.hclits scope in
      (* maximal ones *)
{'fraction_non_alphanumeric': 0.10473297089862488, 'fraction_numerical': 0.002824858757062147, 'mean_word_length': 2.2730047972088965, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 382, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5165195', 'n_tokens_mistral': 12151, 'n_tokens_neox': 11519, 'n_words': 4636}