<commit_before>
(* This file is free software, part of Zipperposition. See file "license" for more details. *)

type term = Term.t

module T = Term
module S = Subst
module P = Position
module M = Monome
module MF = Monome.Focus

(** {2 Type Decls} *)

type op =
  | Equal
  | Different
  | Less
  | Lesseq

type 'm divides = {
  num : Z.t;
  power : int;
  monome : 'm;
  sign : bool;
} (** [num^power divides monome] or not. *)

type t =
  | Binary of op * Z.t Monome.t * Z.t Monome.t
  | Divides of Z.t Monome.t divides
  (** Arithmetic literal (on integers) *)

type lit = t

(** {2 Basics} *)

let equal lit1 lit2 = match lit1, lit2 with
  | Binary (op1, x1, y1), Binary (op2, x2, y2) ->
    op1 = op2 && M.equal x1 x2 && M.equal y1 y2
  | Divides d1, Divides d2 ->
    d1.sign = d2.sign && d1.power = d2.power &&
    Z.equal d1.num d2.num && M.equal d1.monome d2.monome
  | _, _ -> false

let equal_com lit1 lit2 = match lit1, lit2 with
  | Binary (op1, x1, y1), Binary (op2, x2, y2)
    when op1 = op2 && (op1 = Equal || op1 = Different) ->
    (M.equal x1 x2 && M.equal y1 y2) || (M.equal x1 y2 && M.equal x2 y1)
  | _ -> equal lit1 lit2

let compare lit1 lit2 = match lit1, lit2 with
  | Binary (op1, x1, y1), Binary (op2, x2, y2) ->
    let c = compare op1 op2 in
    if c <> 0 then c
    else let c = M.compare x1 x2 in
      if c <> 0 then c else M.compare y1 y2
  | Divides d1, Divides d2 ->
    let open CCOrd in
    compare d1.sign d2.sign
    <?> (compare, d1.power, d2.power)
    <?> (Z.compare, d1.num, d2.num)
    <?> (M.compare, d1.monome, d2.monome)
  | Binary _,  Divides _ -> 1
  | Divides _, Binary _ -> -1

let hash lit = match lit with
  | Binary (op, m1, m2) ->
    Hash.combine4 10 (Hash.poly op) (M.hash m1) (M.hash m2)
  | Divides d ->
    Hash.combine5 20
      (Hash.bool d.sign) (Z.hash d.num) (M.hash d.monome) (Hash.int d.power)

let sign = function
  | Binary ((Equal | Lesseq | Less), _, _) -> true
  | Binary (Different, _, _) -> false
  | Divides d -> d.sign

(* polarity used for the literal ordering *)
let polarity = function
  | Binary ((Less | Lesseq), _, _) -> false
  | Binary (Different, _, _) -> false
  | Binary (Equal,_,_) -> true
  | Divides d -> d.sign

let is_pos = sign
let is_neg l = not (is_pos l)

let _is_bin p = function
  | Binary (op, _, _) -> p op
  | Divides _ -> false

let is_eq = _is_bin ((=) Equal)
let is_neq = _is_bin ((=) Different)
let is_eqn = _is_bin (function Equal | Different -> true | _ -> false)
let is_less = _is_bin ((=) Less)
let is_lesseq = _is_bin ((=) Lesseq)
let is_ineq = _is_bin (function Less | Lesseq -> true | _ -> false)
let is_divides = function
  | Divides _ -> true
  | Binary _ -> false

(* main constructor *)
let make op m1 m2 =
  let m1, m2 = M.normalize m1, M.normalize m2 in
  let m = M.difference m1 m2 in
  (* build from a single monome *)
  let _make_split op m =
    let m1, m2 = M.split m in
    Binary (op, m1, m2)
  in
  match op with
    | Equal
    | Different ->
      (* divide by gcd *)
      let m = M.Int.normalize_wrt_zero m in
      _make_split op m
    | Less ->
      (* should be removed *)
      _make_split op m
    | Lesseq ->
      let c = M.const m in
      let m' = M.remove_const m in
      begin match Monome.Int.factorize m' with
        | Some (m'', g) when Z.gt g Z.one ->
          if Z.sign c > 0
          then
            (* a constant occurs in m1, so m1' + k ≤ m2. In this
               case we check whether m2 - m1' can be factored by some d,
               and we replace k with ceil (k/d).
               Example: 3 ≤ 2a  ----> 3/2 ≤ a ---> 2 ≤ a  *)
            let c' = Z.cdiv c g in
            _make_split op (M.add_const m'' c')
          else if Z.equal c Z.zero
          then
            (* no constant, just divide by gcd *)
            _make_split op m''
          else
            (* m1 ≤ k + m2'. If g is the gcd of m1 and m2' then
                we replace k with floor(k/g) *)
            let c' = Z.neg (Z.fdiv (Z.abs c) g) in
            _make_split op (M.add_const m'' c')
        | _ ->
          (* no gcd other than 1 *)
          _make_split op m
      end

let mk_eq = make Equal
let mk_neq = make Different
let mk_less = make Less
let mk_lesseq = make Lesseq

module U = struct
  module ZTbl = Hashtbl.Make(Z)

  type divisor = {
    prime : Z.t;
    power : int;
  }

  let two = Z.of_int 2

  (* table from numbers to some of their divisor (if any) *)
  let _table = lazy (
    let t = ZTbl.create 256 in
    ZTbl.add t two None;
    t)

  let _divisors n = ZTbl.find (Lazy.force _table) n

  let _add_prime n =
    ZTbl.replace (Lazy.force _table) n None

  (* add to the table the fact that [d] is a divisor of [n] *)
  let _add_divisor n d =
    assert (not (ZTbl.mem (Lazy.force _table) n));
    ZTbl.add (Lazy.force _table) n (Some d)

  (* primality test, modifies _table *)
  let _is_prime n0 =
    let n = ref two in
    let bound = Z.succ (Z.sqrt n0) in
    let is_prime = ref true in
    while !is_prime && Z.leq !n bound do
      if Z.sign (Z.rem n0 !n) = 0
      then begin
        is_prime := false;
        _add_divisor n0 !n;
      end;
      n := Z.succ !n;
    done;
    if !is_prime then _add_prime n0;
    !is_prime

  let is_prime n =
    try
      begin match _divisors n with
        | None -> true
        | Some _ -> false
      end
    with Not_found ->
    match Z.probab_prime n 7 with
      | 0 -> false
      | 2 -> (_add_prime n; true)
      | 1 ->
        _is_prime n
      | _ -> assert false

  let rec _merge l1 l2 = match l1, l2 with
    | [], _ -> l2
    | _, [] -> l1
    | p1::l1', p2::l2' ->
      match Z.compare p1.prime p2.prime with
        | 0 ->
          {prime=p1.prime; power=p1.power+p2.power} :: _merge l1' l2'
        | n when n < 0 ->
          p1 :: _merge l1' l2
        | _ -> p2 :: _merge l1 l2'

  let rec _decompose n =
    try
      begin match _divisors n with
        | None -> [{prime=n; power=1;}]
        | Some q1 ->
          let q2 = Z.divexact n q1 in
          _merge (_decompose q1) (_decompose q2)
      end
    with Not_found ->
      ignore (_is_prime n);
      _decompose n

  let prime_decomposition n =
    if is_prime n
    then [{prime=n; power=1;}]
    else _decompose n

  let primes_leq n0 k =
    let n = ref two in
    while Z.leq !n n0 do
      if is_prime !n then k !n
    done
end

(* reduce 8^1 to 2^3 *)
let _normalize_n n power =
  let divisors = U.prime_decomposition (Z.pow n power) in
  match divisors with
    | [] -> assert false
    | [d] -> d.U.prime, d.U.power
    | _::_::_ -> n, power

(* normalize coefficients of [m] in Z/n^power Z *)
let _normalize_in_div n ~power m =
  let nk = Z.pow n power in
  (* normalize coefficients so that they are within [0...nk-1] *)
  let norm_coeff c = Z.erem c nk in
  M.map_num norm_coeff m

let mk_divides ?(sign=true) n ~power m =
  let m = Monome.normalize m in
  let n, power = _normalize_n n power in
  let m = _normalize_in_div n ~power m in
  (* factorize m by some k; if k is n^p, then make the literal
     n^{power-p} | m/k *)
  let rec factor m power =
    if power <= 1 then m,power
    else match M.Int.quotient m n with
      | None -> m, power
      | Some m' ->  factor m' (power-1)
  in
  let m, power = factor m power in
  Divides { sign; num=n; power; monome=m; }

let mk_not_divides = mk_divides ~sign:false

let negate = function
  | Binary (op, m1, m2) ->
    begin match op with
      | Equal -> Binary (Different, m1, m2)
      | Different -> Binary (Equal, m1, m2)
      | Less -> make Lesseq m2 m1 (* a<b --> b≤a *)
      | Lesseq -> make Lesseq (M.succ m2) m1 (* a≤b --> b<a --> b+1≤a *)
    end
  | Divides d -> Divides { d with sign=not d.sign; }

let pp out = function
  | Binary (op, l, r) ->
    Format.fprintf out "%a %s %a"
      M.pp l
      (match op with Equal -> "=" | Different -> "≠"
                   | Less -> "<" | Lesseq -> "≤")
      M.pp r
  | Divides d when d.sign ->
    let nk = Z.pow d.num d.power in
    Format.fprintf out "%s div %a" (Z.to_string nk) M.pp d.monome
  | Divides d ->
    let nk = Z.pow d.num d.power in
    Format.fprintf out "¬(%s div %a)" (Z.to_string nk) M.pp d.monome

let pp_tstp out = function
  | Binary (Equal, l, r) ->
    Format.fprintf out "%a = %a" M.pp_tstp l M.pp_tstp r
  | Binary (Different, l, r) ->
    Format.fprintf out "%a != %a" M.pp_tstp l M.pp_tstp r
  | Binary (Less, l, r) ->
    Format.fprintf out "$less(%a, %a)" M.pp_tstp l M.pp_tstp r
  | Binary (Lesseq, l, r) ->
    Format.fprintf out "$lesseq(%a, %a)" M.pp_tstp l M.pp_tstp r
  | Divides d when d.sign -><commit_msg>printing<commit_after>
(* This file is free software, part of Zipperposition. See file "license" for more details. *)

type term = Term.t

module T = Term
module S = Subst
module P = Position
module M = Monome
module MF = Monome.Focus

(** {2 Type Decls} *)

type op =
  | Equal
  | Different
  | Less
  | Lesseq

type 'm divides = {
  num : Z.t;
  power : int;
  monome : 'm;
  sign : bool;
} (** [num^power divides monome] or not. *)

type t =
  | Binary of op * Z.t Monome.t * Z.t Monome.t
  | Divides of Z.t Monome.t divides
  (** Arithmetic literal (on integers) *)

type lit = t

(** {2 Basics} *)

let equal lit1 lit2 = match lit1, lit2 with
  | Binary (op1, x1, y1), Binary (op2, x2, y2) ->
    op1 = op2 && M.equal x1 x2 && M.equal y1 y2
  | Divides d1, Divides d2 ->
    d1.sign = d2.sign && d1.power = d2.power &&
    Z.equal d1.num d2.num && M.equal d1.monome d2.monome
  | _, _ -> false

let equal_com lit1 lit2 = match lit1, lit2 with
  | Binary (op1, x1, y1), Binary (op2, x2, y2)
    when op1 = op2 && (op1 = Equal || op1 = Different) ->
    (M.equal x1 x2 && M.equal y1 y2) || (M.equal x1 y2 && M.equal x2 y1)
  | _ -> equal lit1 lit2

let compare lit1 lit2 = match lit1, lit2 with
  | Binary (op1, x1, y1), Binary (op2, x2, y2) ->
    let c = compare op1 op2 in
    if c <> 0 then c
    else let c = M.compare x1 x2 in
      if c <> 0 then c else M.compare y1 y2
  | Divides d1, Divides d2 ->
    let open CCOrd in
    compare d1.sign d2.sign
    <?> (compare, d1.power, d2.power)
    <?> (Z.compare, d1.num, d2.num)
    <?> (M.compare, d1.monome, d2.monome)
  | Binary _,  Divides _ -> 1
  | Divides _, Binary _ -> -1

let hash lit = match lit with
  | Binary (op, m1, m2) ->
    Hash.combine4 10 (Hash.poly op) (M.hash m1) (M.hash m2)
  | Divides d ->
    Hash.combine5 20
      (Hash.bool d.sign) (Z.hash d.num) (M.hash d.monome) (Hash.int d.power)

let sign = function
  | Binary ((Equal | Lesseq | Less), _, _) -> true
  | Binary (Different, _, _) -> false
  | Divides d -> d.sign

(* polarity used for the literal ordering *)
let polarity = function
  | Binary ((Less | Lesseq), _, _) -> false
  | Binary (Different, _, _) -> false
  | Binary (Equal,_,_) -> true
  | Divides d -> d.sign

let is_pos = sign
let is_neg l = not (is_pos l)

let _is_bin p = function
  | Binary (op, _, _) -> p op
  | Divides _ -> false

let is_eq = _is_bin ((=) Equal)
let is_neq = _is_bin ((=) Different)
let is_eqn = _is_bin (function Equal | Different -> true | _ -> false)
let is_less = _is_bin ((=) Less)
let is_lesseq = _is_bin ((=) Lesseq)
let is_ineq = _is_bin (function Less | Lesseq -> true | _ -> false)
let is_divides = function
  | Divides _ -> true
  | Binary _ -> false

(* main constructor *)
let make op m1 m2 =
  let m1, m2 = M.normalize m1, M.normalize m2 in
  let m = M.difference m1 m2 in
  (* build from a single monome *)
  let _make_split op m =
    let m1, m2 = M.split m in
    Binary (op, m1, m2)
  in
  match op with
    | Equal
    | Different ->
      (* divide by gcd *)
      let m = M.Int.normalize_wrt_zero m in
      _make_split op m
    | Less ->
      (* should be removed *)
      _make_split op m
    | Lesseq ->
      let c = M.const m in
      let m' = M.remove_const m in
      begin match Monome.Int.factorize m' with
        | Some (m'', g) when Z.gt g Z.one ->
          if Z.sign c > 0
          then
            (* a constant occurs in m1, so m1' + k ≤ m2. In this
               case we check whether m2 - m1' can be factored by some d,
               and we replace k with ceil (k/d).
               Example: 3 ≤ 2a  ----> 3/2 ≤ a ---> 2 ≤ a  *)
            let c' = Z.cdiv c g in
            _make_split op (M.add_const m'' c')
          else if Z.equal c Z.zero
          then
            (* no constant, just divide by gcd *)
            _make_split op m''
          else
            (* m1 ≤ k + m2'. If g is the gcd of m1 and m2' then
                we replace k with floor(k/g) *)
            let c' = Z.neg (Z.fdiv (Z.abs c) g) in
            _make_split op (M.add_const m'' c')
        | _ ->
          (* no gcd other than 1 *)
          _make_split op m
      end

let mk_eq = make Equal
let mk_neq = make Different
let mk_less = make Less
let mk_lesseq = make Lesseq

module U = struct
  module ZTbl = Hashtbl.Make(Z)

  type divisor = {
    prime : Z.t;
    power : int;
  }

  let two = Z.of_int 2

  (* table from numbers to some of their divisor (if any) *)
  let _table = lazy (
    let t = ZTbl.create 256 in
    ZTbl.add t two None;
    t)

  let _divisors n = ZTbl.find (Lazy.force _table) n

  let _add_prime n =
    ZTbl.replace (Lazy.force _table) n None

  (* add to the table the fact that [d] is a divisor of [n] *)
  let _add_divisor n d =
    assert (not (ZTbl.mem (Lazy.force _table) n));
    ZTbl.add (Lazy.force _table) n (Some d)

  (* primality test, modifies _table *)
  let _is_prime n0 =
    let n = ref two in
    let bound = Z.succ (Z.sqrt n0) in
    let is_prime = ref true in
    while !is_prime && Z.leq !n bound do
      if Z.sign (Z.rem n0 !n) = 0
      then begin
        is_prime := false;
        _add_divisor n0 !n;
      end;
      n := Z.succ !n;
    done;
    if !is_prime then _add_prime n0;
    !is_prime

  let is_prime n =
    try
      begin match _divisors n with
        | None -> true
        | Some _ -> false
      end
    with Not_found ->
    match Z.probab_prime n 7 with
      | 0 -> false
      | 2 -> (_add_prime n; true)
      | 1 ->
        _is_prime n
      | _ -> assert false

  let rec _merge l1 l2 = match l1, l2 with
    | [], _ -> l2
    | _, [] -> l1
    | p1::l1', p2::l2' ->
      match Z.compare p1.prime p2.prime with
        | 0 ->
          {prime=p1.prime; power=p1.power+p2.power} :: _merge l1' l2'
        | n when n < 0 ->
          p1 :: _merge l1' l2
        | _ -> p2 :: _merge l1 l2'

  let rec _decompose n =
    try
      begin match _divisors n with
        | None -> [{prime=n; power=1;}]
        | Some q1 ->
          let q2 = Z.divexact n q1 in
          _merge (_decompose q1) (_decompose q2)
      end
    with Not_found ->
      ignore (_is_prime n);
      _decompose n

  let prime_decomposition n =
    if is_prime n
    then [{prime=n; power=1;}]
    else _decompose n

  let primes_leq n0 k =
    let n = ref two in
    while Z.leq !n n0 do
      if is_prime !n then k !n
    done
end

(* reduce 8^1 to 2^3 *)
let _normalize_n n power =
  let divisors = U.prime_decomposition (Z.pow n power) in
  match divisors with
    | [] -> assert false
    | [d] -> d.U.prime, d.U.power
    | _::_::_ -> n, power

(* normalize coefficients of [m] in Z/n^power Z *)
let _normalize_in_div n ~power m =
  let nk = Z.pow n power in
  (* normalize coefficients so that they are within [0...nk-1] *)
  let norm_coeff c = Z.erem c nk in
  M.map_num norm_coeff m

let mk_divides ?(sign=true) n ~power m =
  let m = Monome.normalize m in
  let n, power = _normalize_n n power in
  let m = _normalize_in_div n ~power m in
  (* factorize m by some k; if k is n^p, then make the literal
     n^{power-p} | m/k *)
  let rec factor m power =
    if power <= 1 then m,power
    else match M.Int.quotient m n with
      | None -> m, power
      | Some m' ->  factor m' (power-1)
  in
  let m, power = factor m power in
  Divides { sign; num=n; power; monome=m; }

let mk_not_divides = mk_divides ~sign:false

let negate = function
  | Binary (op, m1, m2) ->
    begin match op with
      | Equal -> Binary (Different, m1, m2)
      | Different -> Binary (Equal, m1, m2)
      | Less -> make Lesseq m2 m1 (* a<b --> b≤a *)
      | Lesseq -> make Lesseq (M.succ m2) m1 (* a≤b --> b<a --> b+1≤a *)
    end
  | Divides d -> Divides { d with sign=not d.sign; }

let pp out = function
  | Binary (op, l, r) ->
    Format.fprintf out "@[%a %s@ %a@]"
      M.pp l
      (match op with Equal -> "=" | Different -> "≠"
                   | Less -> "<" | Lesseq -> "≤")
      M.pp r
  | Divides d when d.sign ->
    let nk = Z.pow d.num d.power in
    Format.fprintf out "@[<2>%s div@ %a@]" (Z.to_string nk) M.pp d.monome
  | Divides d ->
    let nk = Z.pow d.num d.power in
    Format.fprintf out "@<1>¬(%s div %a)" (Z.to_string nk) M.pp d.monome

let pp_tstp out = function
  | Binary (Equal, l, r) ->
    Format.fprintf out "%a = %a" M.pp_tstp l M.pp_tstp r
  | Binary (Different, l, r) ->
    Format.fprintf out "%a != %a" M.pp_tstp l M.pp_tstp r
  | Binary (Less, l, r) ->
    Format.fprintf out "$less(%a, %a)" M.pp_tstp l M.pp_tstp r
  | Binary (Lesseq, l, r) ->
    Format.fprintf out "$lesseq(%a, %a)" M.pp_tstp l M.pp_tstp r
  | Divides d when d.sign ->
{'fraction_non_alphanumeric': 0.12858642407277818, 'fraction_numerical': 0.021926755306741312, 'mean_word_length': 2.0282535758431925, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 167, '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': '2715344', 'n_tokens_mistral': 6772, 'n_tokens_neox': 6565, 'n_words': 2290}