<commit_before>
(*
Zipperposition: a functional superposition prover for prototyping
Copyright (c) 2013-2015, <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 Common stuff for Induction} *)

module T = Logtk.FOTerm
module F = Logtk.Formula.FO
module Ty = Logtk.Type
module Sym = Logtk.Symbol
module Util = Logtk.Util
module Lits = Literals

type term = Logtk.FOTerm.t
type sym = Logtk.Symbol.t
type formula = F.t

let section = Const.section

let ind_types_ = ref []
let cover_set_depth_ = ref 1
let show_lemmas_ = ref false

let ind_types () = !ind_types_
let cover_set_depth () = !cover_set_depth_

(* is [s] a constructor symbol for some inductive type? *)
let is_constructor s = match s with
  | Sym.Cst info ->
      let name = info.Sym.cs_name in
      List.exists (fun (_, cstors) -> List.mem name cstors) !ind_types_
  | _ -> false

let on_enable = Signal.create()

type kind = [`Full | `Simple]

let show_kind : kind -> string
  = function
  | `Full -> "qbf"
  | `Simple -> "sat"

let kind_ : kind ref = ref `Simple

let enabled_ = ref false
let enable_ () =
  if not !enabled_ then (
    enabled_ := true;
    Util.debugf ~section 1
      "Induction(%s): requires ord=rpo6; select=NoSelection" (show_kind !kind_);
    Params.ord := "rpo6";   (* new default! RPO is necessary*)
    Params.select := "NoSelection";
    Signal.send on_enable !kind_;
  )

let declare_ ty cstors =
  (* remember to declare this type as inductive *)
  Util.debug ~section 1 "user declares inductive type %s = %a"
    ty (CCList.pp CCString.pp) cstors;
  ind_types_ := (ty, cstors) :: !ind_types_;
  enable_();
  ()

let constr_cstors =
  let module C = Logtk.Comparison in
  fun s1 s2 -> match is_constructor s1, is_constructor s2 with
    | true, true
    | false, false -> if Sym.eq s1 s2 then C.Eq else C.Incomparable
    | true, false -> C.Lt
    | false, true -> C.Gt

module Make(Ctx : Ctx.S) = struct
  (* declare a list of inductive types *)
  let declare_types () =
    List.iter
      (fun (ty,cstors) ->
        (* TODO: support polymorphic types? *)
        let pattern = Ty.const (Sym.of_string ty) in
        let constructors = List.map
          (fun str ->
            let s = Sym.of_string str in
            match Ctx.find_signature s with
              | None ->
                  let msg = Util.sprintf
                    "cannot find the type of inductive constructor %s" str
                  in failwith msg
              | Some ty ->
                  s, ty
          ) cstors
        in
        (* declare type. *)
        ignore (Ctx.Induction.declare_ty pattern constructors);
        Util.debug ~section 1 "declare inductive type %a" Ty.pp pattern;
        ()
      ) !ind_types_

  (* true if [t = c] where [c] is some inductive constructor
      such as "cons" or "node" *)
  let is_a_constructor t = match T.Classic.view t with
    | T.Classic.App (s, _, _) ->
        Sequence.exists (Sym.eq s) Ctx.Induction.Seq.constructors
    | _ -> false

  (* find inductive constants in clauses of [seq] *)
  let find_inductive_cst lits : T.t Sequence.t =
    Lits.Seq.terms lits
    |> Sequence.flat_map T.Seq.subterms
    |> Sequence.filter
      (fun t ->
        T.is_ground t
        && T.is_const t
        && not (Ctx.Induction.is_blocked t)
        && Ctx.Induction.is_inductive_type (T.ty t)
        && not (is_a_constructor t)   (* 0 and nil: not inductive const *)
          )

  (* ensure s1 > s2 if s1 is an inductive constant
      and s2 is a sub-case of s1 *)
  let constr_sub_cst s1 s2 =
    let module C = Logtk.Comparison in
    let res =
      if Ctx.Induction.is_inductive_symbol s1 && Ctx.Induction.dominates s1 s2
        then C.Gt
      else if Ctx.Induction.is_inductive_symbol s2 && Ctx.Induction.dominates s2 s1
        then C.Lt
      else C.Incomparable
    in res
end

module MakeAvatar(A : Avatar.S) = struct
  module Env = A.E
  module Ctx = Env.Ctx<commit_msg>bugfix: set NoSelection properly when induction enabled<commit_after>
(*
Zipperposition: a functional superposition prover for prototyping
Copyright (c) 2013-2015, <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 Common stuff for Induction} *)

module T = Logtk.FOTerm
module F = Logtk.Formula.FO
module Ty = Logtk.Type
module Sym = Logtk.Symbol
module Util = Logtk.Util
module Lits = Literals

type term = Logtk.FOTerm.t
type sym = Logtk.Symbol.t
type formula = F.t

let section = Const.section

let ind_types_ = ref []
let cover_set_depth_ = ref 1
let show_lemmas_ = ref false

let ind_types () = !ind_types_
let cover_set_depth () = !cover_set_depth_

(* is [s] a constructor symbol for some inductive type? *)
let is_constructor s = match s with
  | Sym.Cst info ->
      let name = info.Sym.cs_name in
      List.exists (fun (_, cstors) -> List.mem name cstors) !ind_types_
  | _ -> false

let on_enable = Signal.create()

type kind = [`Full | `Simple]

let show_kind : kind -> string
  = function
  | `Full -> "qbf"
  | `Simple -> "sat"

let kind_ : kind ref = ref `Simple

let enabled_ = ref false
let enable_ () =
  if not !enabled_ then (
    enabled_ := true;
    Util.debugf ~section 1
      "Induction(%s): requires ord=rpo6; select=NoSelection" (show_kind !kind_);
    Params.ord := "rpo6";   (* new default! RPO is necessary*)
    Params.select := "NoSelection";
    Signal.send on_enable !kind_;
  )

let declare_ ty cstors =
  (* remember to declare this type as inductive *)
  Util.debug ~section 1 "user declares inductive type %s = %a"
    ty (CCList.pp CCString.pp) cstors;
  ind_types_ := (ty, cstors) :: !ind_types_;
  enable_();
  ()

let constr_cstors =
  let module C = Logtk.Comparison in
  fun s1 s2 -> match is_constructor s1, is_constructor s2 with
    | true, true
    | false, false -> if Sym.eq s1 s2 then C.Eq else C.Incomparable
    | true, false -> C.Lt
    | false, true -> C.Gt

module Make(Ctx : Ctx.S) = struct
  (* declare a list of inductive types *)
  let declare_types () =
    List.iter
      (fun (ty,cstors) ->
        (* TODO: support polymorphic types? *)
        let pattern = Ty.const (Sym.of_string ty) in
        let constructors = List.map
          (fun str ->
            let s = Sym.of_string str in
            match Ctx.find_signature s with
              | None ->
                  let msg = Util.sprintf
                    "cannot find the type of inductive constructor %s" str
                  in failwith msg
              | Some ty ->
                  s, ty
          ) cstors
        in
        (* declare type. *)
        ignore (Ctx.Induction.declare_ty pattern constructors);
        Util.debug ~section 1 "declare inductive type %a" Ty.pp pattern;
        ()
      ) !ind_types_

  (* true if [t = c] where [c] is some inductive constructor
      such as "cons" or "node" *)
  let is_a_constructor t = match T.Classic.view t with
    | T.Classic.App (s, _, _) ->
        Sequence.exists (Sym.eq s) Ctx.Induction.Seq.constructors
    | _ -> false

  (* find inductive constants in clauses of [seq] *)
  let find_inductive_cst lits : T.t Sequence.t =
    Lits.Seq.terms lits
    |> Sequence.flat_map T.Seq.subterms
    |> Sequence.filter
      (fun t ->
        T.is_ground t
        && T.is_const t
        && not (Ctx.Induction.is_blocked t)
        && Ctx.Induction.is_inductive_type (T.ty t)
        && not (is_a_constructor t)   (* 0 and nil: not inductive const *)
          )

  (* ensure s1 > s2 if s1 is an inductive constant
      and s2 is a sub-case of s1 *)
  let constr_sub_cst s1 s2 =
    let module C = Logtk.Comparison in
    let res =
      if Ctx.Induction.is_inductive_symbol s1 && Ctx.Induction.dominates s1 s2
        then C.Gt
      else if Ctx.Induction.is_inductive_symbol s2 && Ctx.Induction.dominates s2 s1
        then C.Lt
      else C.Incomparable
    in res

  let () =
    Ctx.set_selection_fun Selection.no_select
end

module MakeAvatar(A : Avatar.S) = struct
  module Env = A.E
  module Ctx = Env.Ctx
{'fraction_non_alphanumeric': 0.08560386473429951, 'fraction_numerical': 0.00676328502415459, 'mean_word_length': 2.835124120044461, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 45, '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': '7357896', 'n_tokens_mistral': 3354, 'n_tokens_neox': 3155, 'n_words': 1210}