<commit_before>(* This file is part of the Kind 2 model checker.

   Copyright (c) 2015-2017 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you
   may not use this file except in compliance with the License.  You
   may obtain a copy of the License at

   http://www.apache.org/licenses/LICENSE-2.0 

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   implied. See the License for the specific language governing
   permissions and limitations under the License. 

*)

open Lib

exception BVSizeError
let division_by_zero = ref false

(** Returns true iff a division by zero happened in a simplification since
    this function was last called. *)
let has_division_by_zero_happened () =
  let res = !division_by_zero in
  division_by_zero := false ;
  res

(* ********************************************************************** *)
(* Basic types                                                            *)
(* ********************************************************************** *)

(* A monomial is a non-empty ordered list of terms which are not
   polynomials to be multiplied with a constant coefficient, the
   ordering is by comparison of terms. *)
type 'a monomial = 'a * Term.t list

(* A polyomial is a constant (possibly zero) and a (possibly empty)
   orderd list of monomials to be summed up. Each monomial term occurs
   exactly once, the ordering is by lexicographic comparison of
   terms. *)
type 'a polynomial = 'a * 'a monomial list 


(* Normal forms for terms: integer and real terms are polynomials
   where all terms which are not addition or multiplication are
   abstracted to fresh variables in monomials. Boolean terms are in
   negation normal form and contain only conjunctions,
   disjunctions and negations. *)
type t = 
  | Num of Numeral.t polynomial
  | Dec of Decimal.t polynomial
  | Bool of Term.t 
  | Array of Term.t 
  | BV of Term.t

let pp_print_monomial pp ppf ((c, t) : 'a monomial) = 
  Format.fprintf 
    ppf
    "%a * %a"
    pp c
    (pp_print_list Term.pp_print_term "@ *") t

let pp_print_polynomial pp ppf (c, p) = 
  Format.fprintf ppf
    "%a + %a"
    pp c
    (pp_print_list (pp_print_monomial pp) "@ +")
    p
  

let pp_print_int_polynomial = pp_print_polynomial Numeral.pp_print_numeral

let pp_print_dec_polynomial = pp_print_polynomial Decimal.pp_print_decimal



(* ********************************************************************** *)
(* Conversions from normal forms to terms                                 *)
(* ********************************************************************** *)

(* Convert a list of monomials to a list of terms

   This function is polymorphic in the type of the monomial, hence we
   need constructors and predicates. *)
let term_list_of_monomial_list is_zero is_one mk_zero mk_const l = 

  (* Tail-recursive function with accumulator *)
  let rec term_list_of_monomial_list' accum = function 
    
    (* Base case: reverse accumulator to preserve original order *)
    | [] -> List.rev accum
              
    (* Take monomial at head of list *)
    | (c, v) :: tl -> 
      
      (* Convert monomial to the term (c * v) *)
      let t = 
        
        if is_one c then 
          
          (* Omit factor one *)
          Term.mk_times v 
            
        else 
          
        if is_zero c then 
          
          (* Return zero for coeffcient zero *)
          mk_zero ()
            
        else
          
          (* Return product of coefficient and monomials *)
          Term.mk_times ((mk_const c) :: v)

      in

      (* Recurse for tail of list *)
      term_list_of_monomial_list' (t :: accum) tl

  in

  (* Call recursive function with initial value for accumulator *)
  term_list_of_monomial_list' [] l


(* Convert a polynomial to a term

   This function is polymorphic in the type of the monomial, hence we
   need constructors and predicates. *)
let term_of_polynomial is_zero is_one mk_zero mk_const = function 

  (* Polynomial has constant zero and an empty list of monomials *)
  | (c, []) when is_zero c -> mk_zero ()

  (* Polynomial has constant zero and a non-empty list of monomials *)
  | (c, l) when is_zero c -> 

    (* Convert polynomial to the term (c1 * v1) + ... + (cn * vn) *)
    Term.mk_plus 
      (term_list_of_monomial_list is_zero is_one mk_zero mk_const l)

  (* Polynomial has a non-zero constant and an empty list of
     monomials *)
  | (c, []) -> mk_const c

  (* Polynomial has a non-zero constant and a non-empty list of
     monomials *)
  | (c, l) -> 

    (* Convert polynomial to the term (c + (c1 * v1) + ... + (cn * vn)) *)
    Term.mk_plus 
      (mk_const c :: 
         term_list_of_monomial_list is_zero is_one mk_zero mk_const l)


(* Convert an integer polynomial to a term *)
let term_of_num_polynomial = 
  term_of_polynomial 
    (Numeral.equal Numeral.zero)
    (Numeral.equal Numeral.one)
    (function () -> Term.mk_num Numeral.zero)
    Term.mk_num


(* Convert a real polynomial to a term *)
let term_of_dec_polynomial = 
  term_of_polynomial 
    (Decimal.equal Decimal.zero)
    (Decimal.equal Decimal.one) 
    (function () -> Term.mk_dec Decimal.zero)
    Term.mk_dec


(* Convert a normal form to a term *)
let term_of_nf = function 
  | Num p -> term_of_num_polynomial p
  | Dec p -> term_of_dec_polynomial p
  | Bool b -> b
  | Array b -> b
  | BV b -> b


(* ********************************************************************** *)
(* Conversions from normal forms                                          *)
(* ********************************************************************** *)


(* Return the integer polynomial in an integer normal form *)
let num_polynomial_of_nf = function 
  | Num p -> p
  | _ -> assert false


(* Return the real polynomial in a real normal form *)
let dec_polynomial_of_nf = function 
  | Dec p -> p
  | _ -> assert false


(* Return the term in a Boolean normal form *)
let bool_of_nf = function
  | Bool b -> b
  | _ -> assert false


(* ********************************************************************** *)
(* Variable-free normal forms                                             *)
(* ********************************************************************** *)


(* Return true if normal form is variable-free *)
let is_constant = function 
  | Num (_, [])
  | Dec (_, [])  -> true
  | Bool b when b == Term.t_true || b == Term.t_false -> true
  | BV _ -> true
  | Num _ | Dec _ | Bool _ | Array _ -> false


(* Return true if value is variable-free *)
let is_constant_polynomial = function 
  | (_, []) -> true
  | _ -> false
    

(* Return the constant of a polynomial *)
let const_of_polynomial = function (c, _) -> c


(* Return the constant of an integer polynomial *)
let const_of_num_polynomial = function 
  | Num p -> const_of_polynomial p
  | _ -> assert false 


(* Return the constant of a real polynomial *)
let const_of_dec_polynomial = function 
  | Dec p -> const_of_polynomial p
  | Num p -> const_of_polynomial p |> Numeral.to_big_int  |> Decimal.of_big_int 
  | _ -> assert false 

(* ********************************************************************** *)
(* Arithmetic functions on polynomials (polymorphic)                      *)
(* ********************************************************************** *)


(* Compare monomials by comparing their terms *)
let compare_monomials (_, t1) (_, t2) = compare_lists Term.compare t1 t2 


(* Add two lists of sorted monomials *)
let add_monomial_lists add is_zero l1 l2 = 

  (* Tail-recursive function with accumulator *)
  let rec add_monomial_lists' accum l1 l2 = match l1, l2 with 

    (* Base case: one of the lists is empty *)
    | _, [] -> List.rev_append accum l1
    | [], _ -> List.rev_append accum l2

    (* Terms are equal: add coefficients *)
    | (c1, t1) :: tl1, (c2, t2) :: tl2 
      when 
        List.length t1 = List.length t2 &&
        List.for_all2 Term.equal t1 t2 -> 

      (* Add coefficients *)
      let c' = add c1 c2 in

      (* Check sum of coefficients *)
      if is_zero c' then 
        
        (* Remove monomial if the coefficient vanishes *)
        add_monomial_lists' accum tl1 tl2 

      else

        (* Add coefficients of two monomials with equal terms *)
        add_monomial_lists' ((add c1 c2, t1) :: accum) tl1 tl2 

    (* First term is smaller: add to accumulator first *)
    | (c1, t1) :: tl1, (_, t2) :: _ 
      when 
        compare_lists Term.compare t1 t2 < 0 -> 

      add_monomial_lists' ((c1, t1) :: accum) tl1 l2 

    (* Second term is smaller: add to accumulator first *)
    | (_, t1) :: _, (c2, t2) :: tl2 -> 

      add_monomial_lists' ((c2, t2) :: accum) l1 tl2 

  in

  (* Call recursive function with initial value for accumulator *)
  add_monomial_lists' [] l1 l2 


(* Sum up a list of polynomials *)
let add_polynomials add zero is_zero p = 

  (* Split off coefficients of polynomials *)
  let c, m = List.split p in

  (* Sum up coefficients *)
  let c' = List.fold_left add zero c in
            
  (* Add lists of monomials *)
  let m' = List.fold_left (add_monomial_lists add is_zero) [] m in
  
  (* Return merged polynomials *)
  (c', m')


(* Multiply each monomial in the list with a constant *)
let const_multiply_monomial_list mult d m = 
  List.map (function (c, t) -> (mult c d, t)) m


(* Multiply a polynomial with a constant *)
let const_multiply_polynomial mult d (c, m) = 
  (mult d c, const_multiply_monomial_list mult d m)


(* Multiply each monomial in the list with negative one *)
let negate_monomial_list mult minus_one m = 
  const_multiply_monomial_list mult minus_one m


(* Multiply polynomial with negative one *)
let negate_polynomial mult minus_one p = 
  const_multiply_polynomial mult minus_one p


(* Multiply two lists of monomials *)
let multiply_monomial_lists mult l1 l2 = 

  (* Tail-recursive function with accumulator

     multiply_monomial_lists' l2 a m1 i2 i1

     folds over i2, multiplies each monomial with m1 and adds the
     result to the accumulator a. If i1 is not empty, take its head
     element as new m1 and repeat folding over l2.

     If l2 is empty, an empty list is returned. In the inital call i2
     must be equal to l2. *)
  let rec multiply_monomial_lists' l2 accum (c1, t1) = function 

    (* One iteration over l2 finished *)
    | [] -> 

      (function  

        (* No more elements left in l1: Return a sorted list of
           monomials *)
        | [] -> List.sort compare_monomials accum

        (* Take next element of l1 and multiply it with all elements
           of l2 *)
        | h :: tl1 -> multiply_monomial_lists' l2 accum h l2 tl1)

    (* Take head element of l2 *)
    | (c2, t2) :: tl2 -> 

      (* Pass through tail of l1 *)
      (function tl1 -> 

        (* Merge two sorted lists of terms as a new monomial *)
        let t' = List.merge Term.compare t1 t2 in 
             
        (* Continue merging tail of l2 with current head of l1 *)
        multiply_monomial_lists' 
          l2
          ((mult c1 c2, t') :: accum)
          (c1, t1)
          tl2
          tl1)

  in
  
  match l1, l2 with 
    
    (* Catch special cases of l1 or l2 empty *)
    | [], _ -> []
    | _, [] -> [] 

    (* Multiply two lists of monomials *)
    | h :: tl1, _ -> multiply_monomial_lists' l2 [] h l2 tl1
  

(* Multiply two polynomials *)
let multiply_polynomials mult is_zero zero (c1, m1) (c2, m2) = 

  (* Return polynomial as
     ((ax + c) * (bx + d)) = (abxy + adx + bcx + cd) *)
  let m' = 
    List.sort 
      compare_monomials
      (multiply_monomial_lists mult m1 m2 @ 
         const_multiply_monomial_list mult c2 m1 @ 
         const_multiply_monomial_list mult c1 m2)
  in

  (mult c1 c2, m')


(* Subtract second polynomial from first and normalize so that either
   the constant or the first coefficient of the polynomial is greater
   than zero 

   Return the sign of the factor, [true] for positive and [false] for
   negative together with the normalized result *)
let subtract_and_normalize_polynomials
    add_polynomials negate_polynomial zero is_zero lt_zero p q =

  (* Subtract second polynomial from first *)
  let r = add_polynomials [p; negate_polynomial q] in

  (* Normalize so that either the constant or the first coefficient of
     the polynomial is greater than zero *)
  match r with 

    (* Polynomial is the constanst zero *)
    | (c, []) when is_zero c -> true, r

    (* Constant is zero, first coefficient is negative *)
    | (c, (h, _) :: tl) when is_zero c && lt_zero h -> false, negate_polynomial r

    (* Constant is zero, first coefficient is not negative *)
    | (c, (h, _) :: tl) when is_zero c -> true, r

    (* Constant is not zero and negative *)
    | (c, _) when lt_zero c -> false, negate_polynomial r

    (* Constant is not zero and positive *)
    | (c, _) -> true, r


(* ********************************************************************** *)
(* Integer arithmetic functions on polynomials                            *)
(* ********************************************************************** *)


let add_num_monomial_lists = add_monomial_lists Numeral.(+) (Numeral.equal Numeral.zero)

let add_num_polynomials = add_polynomials Numeral.(+) Numeral.zero (Numeral.equal Numeral.zero)

let const_multiply_num_monomial_list = const_multiply_monomial_list Numeral.( * )

let const_multiply_num_polynomial = const_multiply_polynomial Numeral.( * )

let negate_num_monomial_list = negate_monomial_list Numeral.( * ) (Numeral.neg Numeral.one)

let negate_num_polynomial = negate_polynomial Numeral.( * ) (Numeral.neg Numeral.one)

let multiply_num_polynomials = 
  multiply_polynomials Numeral.( * ) (Numeral.equal Numeral.zero) Numeral.zero

let subtract_and_normalize_num_polynomials = 
  subtract_and_normalize_polynomials 
    add_num_polynomials 
    negate_num_polynomial 
    Numeral.zero
    (Numeral.equal Numeral.zero)
    (Numeral.gt Numeral.zero)

(* ********************************************************************** *)
(* Real arithmetic functions on polynomials                               *)
(* ********************************************************************** *)


let add_dec_monomial_lists = add_monomial_lists Decimal.(+) (Decimal.equal Decimal.zero)

let add_dec_polynomials = add_polynomials Decimal.(+) Decimal.zero (Decimal.equal Decimal.zero)

let const_multiply_dec_monomial_list = const_multiply_monomial_list Decimal.( * )

let const_multiply_dec_polynomial = const_multiply_polynomial Decimal.( * )

let negate_dec_monomial_list = negate_monomial_list Decimal.( * ) (Decimal.neg Decimal.one)

let negate_dec_polynomial = negate_polynomial Decimal.( * ) (Decimal.neg Decimal.one)

let multiply_dec_polynomials = 
  multiply_polynomials Decimal.( * ) (Decimal.equal Decimal.zero) Decimal.zero

let subtract_and_normalize_dec_polynomials = 
  subtract_and_normalize_polynomials 
    add_dec_polynomials 
    negate_dec_polynomial 
    Decimal.zero
    (Decimal.equal Decimal.zero) 
    (Decimal.gt Decimal.zero) 

(* ********************************************************************** *)
(* Functions used in {!simplify_term_node}                                *)
(* ********************************************************************** *)


(* Sum up a list of integer polynomials *)
let add_num args = 

  let args' = List.map num_polynomial_of_nf args in

  add_num_polynomials args'


(* Sum up a list of real polynomials *)
let add_dec args = 

  let args' = List.map dec_polynomial_of_nf args in

  add_dec_polynomials args'


(* Multiply two integer polynomials *)
let multiply_num p1 p2 = 

  let p1', p2' = num_polynomial_of_nf p1, num_polynomial_of_nf p2 in

  multiply_num_polynomials p1' p2'


(* Multiply two real polynomials *)
let multiply_dec p1 p2 = 

  let p1', p2' = dec_polynomial_of_nf p1, dec_polynomial_of_nf p2 in

  multiply_dec_polynomials p1' p2'


(* Sum up a list of real or integer normal forms *)
let add = function

  (* Addition is not nullary  *)
  | [] -> assert false 
    
  (* Add as integer polynomials if head of list is integer *)
  | Num _ :: _ as args -> Num (add_num args)
                    
  (* Add as real polynomials if head of list is real *)
  | Dec _ :: _ as args -> Dec (add_dec args)
                     
  (* Cannot add other types *)
  | _ -> assert false


(* Subtract a list of polynomials *)
let minus = function 

  (* Subtraction is not nullary  *)
  | [] -> assert false 

  (* Unary integer minus: negate polynomial to (- c - p) *)
  | [Num p] -> Num (negate_num_polynomial p)

  (* Unary real minus: negate polynomial to (- c - p) *)
  | [Dec p] -> Dec (negate_dec_polynomial p)

  (* Binary integer minus or higher arity: (h - s1 - ... - sn) reduce
     to (h - (s1 + ... + sn) *)
  | Num p :: tl -> 

    Num (add_num_polynomials [p; negate_num_polynomial (add_num tl)])

  (* Binary real minus or higher arity: (h - s1 - ... - sn) reduce to
     (h - (s1 + ... + sn) *)
  | Dec p :: tl -> 

    Dec (add_dec_polynomials [p; negate_dec_polynomial (add_dec tl)])

  (* Cannot subtract other types *)
  | _ -> assert false


(* Multiply a list of polynomials *)
let times = function 

  (* Multiplication is not nullary  *)
  | [] -> assert false 
    
  (* Multiply as integer polynomials if head of list is integer *)
  | Num p :: tl -> 
    
    Num 
      (List.fold_left 
         multiply_num_polynomials 
         p 
         (List.map num_polynomial_of_nf tl))
                    
  (* Multiply as real polynomials if head of list is real *)
  | Dec p :: tl -> 

    Dec
      (List.fold_left 
         multiply_dec_polynomials 
         p 
         (List.map dec_polynomial_of_nf tl))
                     
  (* Cannot multiply other types *)
  | _ -> assert false


(* Flatten nested associative Boolean operators by lifting the
   subterms of a nested operator as subterms of the top operator: 
   (a & (b & c)) becomes (a & b & c)

   The arguments must be Boolean, real and integer terms are
   normalized to polynomials. *)
let flatten_bool_subterms s l = 

  (* Tail-recursive function with accumulator *)
  let rec flatten_bool_subterms' symbol accum = function 

    (* No more subterms, return accumulator in original order *)
    | [] -> List.rev accum

    (* Boolean operator *)
    | Bool t :: tl -> 

      let accum' =
        
        (* Get symbol of term *)
        match Term.destruct t with

          (* Symbol is the same as the top-level symbol? *)
          | Term.T.App (s, l) when s == symbol -> 

            (* Add subterms of term in reverse order to subterms of
               top term *)
            List.rev_append l accum 

          (* Keep term unchanged *)
          | _ -> t :: accum

      in

      (* Recurse for remaining subterms *)
      flatten_bool_subterms' symbol accum' tl

    (* Fail on non-boolean arguments *)
    | (Num _ | Dec _ | Array _ | BV _ ) :: _ -> assert false

  in

  (* Call tail-recursive function with initial accumulator *)
  flatten_bool_subterms' s [] l 


(* Return true if a complement of a term in the second list is in the
   first list *)
let rec has_complement l = function 
  | [] -> false 
  | h :: tl -> 
    if List.memq (Term.negate h) l then true else has_complement l tl


(* Negate a term in negation normal form

   The term must only contain conjunctions and disjunctions as Boolean
   operators, the argument of a Boolean negation must be an atom. *)
let rec negate_nnf term = match Term.destruct term with 

  (* Negate a variable *)
  | Term.T.Var v -> Term.mk_not (Term.mk_var v)

  (* Negate a constant *)
  | Term.T.Const s ->

    (* Unhashcons constant symbol *)
    (match Symbol.node_of_symbol s with 

      | `TRUE -> Term.t_false
      | `FALSE -> Term.t_true
      | `UF u -> Term.mk_not (Term.mk_uf u [])
      | _ -> assert false

    )

  (* Negate a function application *)
  | Term.T.App (s, l) -> 

    (* Unhashcons constant symbol *)
    (match Symbol.node_of_symbol s, l with 

      (* Double unary negation *)
      | `NOT, [a] -> a

      (* Negation must be unary *)
      | `NOT, _ -> assert false 

      (* Conjunction *)
      | `AND, l -> 
        Term.mk_or (List.map (function t -> negate_nnf t) l)

      (* Disjunction *)
      | `OR, l -> 
        Term.mk_and (List.map (function t -> negate_nnf t) l)

      (* Disjunction and conjunction are the only Boolean operators *)
      | `IMPLIES, _
      | `XOR, _ -> assert false

      (* Boolean equivalence must not occur *)
      | `EQ, [] -> assert false 

      | `EQ, h :: _ 
        when 
          Term.type_of_term h == Type.t_bool -> 
        assert false 

      (* Negate atoms *)
      | `EQ, _ 
      | `DISTINCT, _
      | `LEQ, _
      | `LT, _
      | `GEQ, _
      | `GT, _
      | `IS_INT, _
      | `DIVISIBLE _, _
      | `UF _, _
      | `SELECT _, _
      | `STORE, _ -> Term.mk_not term

      (* Negate both cases of ite term *)
      | `ITE, [p; l; r] -> 
        Term.mk_ite 
          p
          (negate_nnf l)
          (negate_nnf r)

      (* Non-ternary ite *)
      | `ITE, _ -> assert false

      (* Constant symbols *)
      | `FALSE, _
      | `TRUE, _
      | `NUMERAL _, _
      | `DECIMAL _, _ -> assert false

      | `BV _, _ -> assert false

      (* Can only negate Boolean terms *)
      | `MINUS, _
      | `PLUS, _
      | `TIMES, _
      | `DIV, _
      | `INTDIV, _
      | `MOD, _
      | `ABS, _
      | `TO_REAL, _
      | `TO_INT, _
      | `TO_INT8, _
      | `TO_INT16, _
      | `TO_INT32, _
      | `TO_INT64, _ 

      | `CONCAT, _
      | `EXTRACT _, _
      | `BVNEG, _
      | `BVADD, _
      | `BVMUL, _
      | `BVUDIV, _
      | `BVUREM, _
      | `BVSHL, _
      | `BVLSHR, _
      | `BVULT, _ 
      | `BVULE, _
      | `BVUGT, _
      | `BVUGE, _
      | `BVNOT, _
      | `BVOR, _ 
      | `BVAND, _ -> assert false 
    )    

  | Term.T.Attr (t, _) -> t


(* Negate all but the last term *)
let implies_to_or args = 

  (* Tail-recursive function with accumulator *)
  let rec implies_to_or' accum = function 
    | [] -> assert false
    | [a] -> List.rev (a :: accum)
    | Bool h :: tl -> implies_to_or' (Bool (negate_nnf h) :: accum) tl
    | (Num _ | Dec _ | Array _ | BV _ ) :: _ -> assert false
  in

  implies_to_or' [] args 


(* Subtract two normal forms and make constant or first coefficient
   positive *)
let subtract_and_normalize a b = match a, b with 

  (* Two integer polynomials *)
  | Num a, Num b -> 
    let s, r = subtract_and_normalize_num_polynomials a b in s, Num r

  (* Two real polynomials *)
  | Dec a, Dec b -> 
    let s, r = subtract_and_normalize_dec_polynomials a b in s, Dec r

  (* Cannot subtract *)
  | _ -> assert false

let relation_to_nf_bv rel = function
  (* Relation must be binary *)
  | [] 
  | [_] -> assert false

  (* Binary relation *)
  | [a; b] -> (match (rel (Term.bitvector_of_term (term_of_nf a)) (Term.bitvector_of_term (term_of_nf b))) with
    | true -> Bool Term.t_true
    | false -> Bool Term.t_false)
  (*assert false (*Bool (rel [(term_of_nf a); (term_of_nf b)])*)*)

  (* Arity greater than 2 *)
  | _ -> assert false

(* Normalize an n-ary relation by unchaining it into a conjunction of
   binary relations, subtracting the right-hand side from the
   left-hand side and evaluating to true or false if possible

   When normalizing, we might multiply with a negative factor and then
   need to replace the relation symbol by its converse. Hence we need
   to know the converse of the relation (primed parameters). *)
let rec relation_to_nf 
    simplify_term_node 
    rel 
    rel'
    mk_rel 
    mk_rel' 
    zero 
    t_zero = function

  (* Relation must be at least binary *)
  | [] 
  | [_] -> assert false<commit_msg>Fixed assertion failures from simplify.ml at least for the single working example pt 2<commit_after>(* This file is part of the Kind 2 model checker.

   Copyright (c) 2015-2017 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you
   may not use this file except in compliance with the License.  You
   may obtain a copy of the License at

   http://www.apache.org/licenses/LICENSE-2.0 

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   implied. See the License for the specific language governing
   permissions and limitations under the License. 

*)

open Lib

exception BVSizeError
let division_by_zero = ref false

(** Returns true iff a division by zero happened in a simplification since
    this function was last called. *)
let has_division_by_zero_happened () =
  let res = !division_by_zero in
  division_by_zero := false ;
  res

(* ********************************************************************** *)
(* Basic types                                                            *)
(* ********************************************************************** *)

(* A monomial is a non-empty ordered list of terms which are not
   polynomials to be multiplied with a constant coefficient, the
   ordering is by comparison of terms. *)
type 'a monomial = 'a * Term.t list

(* A polyomial is a constant (possibly zero) and a (possibly empty)
   orderd list of monomials to be summed up. Each monomial term occurs
   exactly once, the ordering is by lexicographic comparison of
   terms. *)
type 'a polynomial = 'a * 'a monomial list 


(* Normal forms for terms: integer and real terms are polynomials
   where all terms which are not addition or multiplication are
   abstracted to fresh variables in monomials. Boolean terms are in
   negation normal form and contain only conjunctions,
   disjunctions and negations. *)
type t = 
  | Num of Numeral.t polynomial
  | Dec of Decimal.t polynomial
  | Bool of Term.t 
  | Array of Term.t 
  | BV of Term.t

let pp_print_monomial pp ppf ((c, t) : 'a monomial) = 
  Format.fprintf 
    ppf
    "%a * %a"
    pp c
    (pp_print_list Term.pp_print_term "@ *") t

let pp_print_polynomial pp ppf (c, p) = 
  Format.fprintf ppf
    "%a + %a"
    pp c
    (pp_print_list (pp_print_monomial pp) "@ +")
    p
  

let pp_print_int_polynomial = pp_print_polynomial Numeral.pp_print_numeral

let pp_print_dec_polynomial = pp_print_polynomial Decimal.pp_print_decimal



(* ********************************************************************** *)
(* Conversions from normal forms to terms                                 *)
(* ********************************************************************** *)

(* Convert a list of monomials to a list of terms

   This function is polymorphic in the type of the monomial, hence we
   need constructors and predicates. *)
let term_list_of_monomial_list is_zero is_one mk_zero mk_const l = 

  (* Tail-recursive function with accumulator *)
  let rec term_list_of_monomial_list' accum = function 
    
    (* Base case: reverse accumulator to preserve original order *)
    | [] -> List.rev accum
              
    (* Take monomial at head of list *)
    | (c, v) :: tl -> 
      
      (* Convert monomial to the term (c * v) *)
      let t = 
        
        if is_one c then 
          
          (* Omit factor one *)
          Term.mk_times v 
            
        else 
          
        if is_zero c then 
          
          (* Return zero for coeffcient zero *)
          mk_zero ()
            
        else
          
          (* Return product of coefficient and monomials *)
          Term.mk_times ((mk_const c) :: v)

      in

      (* Recurse for tail of list *)
      term_list_of_monomial_list' (t :: accum) tl

  in

  (* Call recursive function with initial value for accumulator *)
  term_list_of_monomial_list' [] l


(* Convert a polynomial to a term

   This function is polymorphic in the type of the monomial, hence we
   need constructors and predicates. *)
let term_of_polynomial is_zero is_one mk_zero mk_const = function 

  (* Polynomial has constant zero and an empty list of monomials *)
  | (c, []) when is_zero c -> mk_zero ()

  (* Polynomial has constant zero and a non-empty list of monomials *)
  | (c, l) when is_zero c -> 

    (* Convert polynomial to the term (c1 * v1) + ... + (cn * vn) *)
    Term.mk_plus 
      (term_list_of_monomial_list is_zero is_one mk_zero mk_const l)

  (* Polynomial has a non-zero constant and an empty list of
     monomials *)
  | (c, []) -> mk_const c

  (* Polynomial has a non-zero constant and a non-empty list of
     monomials *)
  | (c, l) -> 

    (* Convert polynomial to the term (c + (c1 * v1) + ... + (cn * vn)) *)
    Term.mk_plus 
      (mk_const c :: 
         term_list_of_monomial_list is_zero is_one mk_zero mk_const l)


(* Convert an integer polynomial to a term *)
let term_of_num_polynomial = 
  term_of_polynomial 
    (Numeral.equal Numeral.zero)
    (Numeral.equal Numeral.one)
    (function () -> Term.mk_num Numeral.zero)
    Term.mk_num


(* Convert a real polynomial to a term *)
let term_of_dec_polynomial = 
  term_of_polynomial 
    (Decimal.equal Decimal.zero)
    (Decimal.equal Decimal.one) 
    (function () -> Term.mk_dec Decimal.zero)
    Term.mk_dec


(* Convert a normal form to a term *)
let term_of_nf = function 
  | Num p -> term_of_num_polynomial p
  | Dec p -> term_of_dec_polynomial p
  | Bool b -> b
  | Array b -> b
  | BV b -> b


(* ********************************************************************** *)
(* Conversions from normal forms                                          *)
(* ********************************************************************** *)


(* Return the integer polynomial in an integer normal form *)
let num_polynomial_of_nf = function 
  | Num p -> p
  | _ -> assert false


(* Return the real polynomial in a real normal form *)
let dec_polynomial_of_nf = function 
  | Dec p -> p
  | _ -> assert false


(* Return the term in a Boolean normal form *)
let bool_of_nf = function
  | Bool b -> b
  | _ -> assert false


(* ********************************************************************** *)
(* Variable-free normal forms                                             *)
(* ********************************************************************** *)


(* Return true if normal form is variable-free *)
let is_constant = function 
  | Num (_, [])
  | Dec (_, [])  -> true
  | Bool b when b == Term.t_true || b == Term.t_false -> true
  | BV _ -> true
  | Num _ | Dec _ | Bool _ | Array _ -> false


(* Return true if value is variable-free *)
let is_constant_polynomial = function 
  | (_, []) -> true
  | _ -> false
    

(* Return the constant of a polynomial *)
let const_of_polynomial = function (c, _) -> c


(* Return the constant of an integer polynomial *)
let const_of_num_polynomial = function 
  | Num p -> const_of_polynomial p
  | _ -> assert false 


(* Return the constant of a real polynomial *)
let const_of_dec_polynomial = function 
  | Dec p -> const_of_polynomial p
  | Num p -> const_of_polynomial p |> Numeral.to_big_int  |> Decimal.of_big_int 
  | _ -> assert false 

(* ********************************************************************** *)
(* Arithmetic functions on polynomials (polymorphic)                      *)
(* ********************************************************************** *)


(* Compare monomials by comparing their terms *)
let compare_monomials (_, t1) (_, t2) = compare_lists Term.compare t1 t2 


(* Add two lists of sorted monomials *)
let add_monomial_lists add is_zero l1 l2 = 

  (* Tail-recursive function with accumulator *)
  let rec add_monomial_lists' accum l1 l2 = match l1, l2 with 

    (* Base case: one of the lists is empty *)
    | _, [] -> List.rev_append accum l1
    | [], _ -> List.rev_append accum l2

    (* Terms are equal: add coefficients *)
    | (c1, t1) :: tl1, (c2, t2) :: tl2 
      when 
        List.length t1 = List.length t2 &&
        List.for_all2 Term.equal t1 t2 -> 

      (* Add coefficients *)
      let c' = add c1 c2 in

      (* Check sum of coefficients *)
      if is_zero c' then 
        
        (* Remove monomial if the coefficient vanishes *)
        add_monomial_lists' accum tl1 tl2 

      else

        (* Add coefficients of two monomials with equal terms *)
        add_monomial_lists' ((add c1 c2, t1) :: accum) tl1 tl2 

    (* First term is smaller: add to accumulator first *)
    | (c1, t1) :: tl1, (_, t2) :: _ 
      when 
        compare_lists Term.compare t1 t2 < 0 -> 

      add_monomial_lists' ((c1, t1) :: accum) tl1 l2 

    (* Second term is smaller: add to accumulator first *)
    | (_, t1) :: _, (c2, t2) :: tl2 -> 

      add_monomial_lists' ((c2, t2) :: accum) l1 tl2 

  in

  (* Call recursive function with initial value for accumulator *)
  add_monomial_lists' [] l1 l2 


(* Sum up a list of polynomials *)
let add_polynomials add zero is_zero p = 

  (* Split off coefficients of polynomials *)
  let c, m = List.split p in

  (* Sum up coefficients *)
  let c' = List.fold_left add zero c in
            
  (* Add lists of monomials *)
  let m' = List.fold_left (add_monomial_lists add is_zero) [] m in
  
  (* Return merged polynomials *)
  (c', m')


(* Multiply each monomial in the list with a constant *)
let const_multiply_monomial_list mult d m = 
  List.map (function (c, t) -> (mult c d, t)) m


(* Multiply a polynomial with a constant *)
let const_multiply_polynomial mult d (c, m) = 
  (mult d c, const_multiply_monomial_list mult d m)


(* Multiply each monomial in the list with negative one *)
let negate_monomial_list mult minus_one m = 
  const_multiply_monomial_list mult minus_one m


(* Multiply polynomial with negative one *)
let negate_polynomial mult minus_one p = 
  const_multiply_polynomial mult minus_one p


(* Multiply two lists of monomials *)
let multiply_monomial_lists mult l1 l2 = 

  (* Tail-recursive function with accumulator

     multiply_monomial_lists' l2 a m1 i2 i1

     folds over i2, multiplies each monomial with m1 and adds the
     result to the accumulator a. If i1 is not empty, take its head
     element as new m1 and repeat folding over l2.

     If l2 is empty, an empty list is returned. In the inital call i2
     must be equal to l2. *)
  let rec multiply_monomial_lists' l2 accum (c1, t1) = function 

    (* One iteration over l2 finished *)
    | [] -> 

      (function  

        (* No more elements left in l1: Return a sorted list of
           monomials *)
        | [] -> List.sort compare_monomials accum

        (* Take next element of l1 and multiply it with all elements
           of l2 *)
        | h :: tl1 -> multiply_monomial_lists' l2 accum h l2 tl1)

    (* Take head element of l2 *)
    | (c2, t2) :: tl2 -> 

      (* Pass through tail of l1 *)
      (function tl1 -> 

        (* Merge two sorted lists of terms as a new monomial *)
        let t' = List.merge Term.compare t1 t2 in 
             
        (* Continue merging tail of l2 with current head of l1 *)
        multiply_monomial_lists' 
          l2
          ((mult c1 c2, t') :: accum)
          (c1, t1)
          tl2
          tl1)

  in
  
  match l1, l2 with 
    
    (* Catch special cases of l1 or l2 empty *)
    | [], _ -> []
    | _, [] -> [] 

    (* Multiply two lists of monomials *)
    | h :: tl1, _ -> multiply_monomial_lists' l2 [] h l2 tl1
  

(* Multiply two polynomials *)
let multiply_polynomials mult is_zero zero (c1, m1) (c2, m2) = 

  (* Return polynomial as
     ((ax + c) * (bx + d)) = (abxy + adx + bcx + cd) *)
  let m' = 
    List.sort 
      compare_monomials
      (multiply_monomial_lists mult m1 m2 @ 
         const_multiply_monomial_list mult c2 m1 @ 
         const_multiply_monomial_list mult c1 m2)
  in

  (mult c1 c2, m')


(* Subtract second polynomial from first and normalize so that either
   the constant or the first coefficient of the polynomial is greater
   than zero 

   Return the sign of the factor, [true] for positive and [false] for
   negative together with the normalized result *)
let subtract_and_normalize_polynomials
    add_polynomials negate_polynomial zero is_zero lt_zero p q =

  (* Subtract second polynomial from first *)
  let r = add_polynomials [p; negate_polynomial q] in

  (* Normalize so that either the constant or the first coefficient of
     the polynomial is greater than zero *)
  match r with 

    (* Polynomial is the constanst zero *)
    | (c, []) when is_zero c -> true, r

    (* Constant is zero, first coefficient is negative *)
    | (c, (h, _) :: tl) when is_zero c && lt_zero h -> false, negate_polynomial r

    (* Constant is zero, first coefficient is not negative *)
    | (c, (h, _) :: tl) when is_zero c -> true, r

    (* Constant is not zero and negative *)
    | (c, _) when lt_zero c -> false, negate_polynomial r

    (* Constant is not zero and positive *)
    | (c, _) -> true, r


(* ********************************************************************** *)
(* Integer arithmetic functions on polynomials                            *)
(* ********************************************************************** *)


let add_num_monomial_lists = add_monomial_lists Numeral.(+) (Numeral.equal Numeral.zero)

let add_num_polynomials = add_polynomials Numeral.(+) Numeral.zero (Numeral.equal Numeral.zero)

let const_multiply_num_monomial_list = const_multiply_monomial_list Numeral.( * )

let const_multiply_num_polynomial = const_multiply_polynomial Numeral.( * )

let negate_num_monomial_list = negate_monomial_list Numeral.( * ) (Numeral.neg Numeral.one)

let negate_num_polynomial = negate_polynomial Numeral.( * ) (Numeral.neg Numeral.one)

let multiply_num_polynomials = 
  multiply_polynomials Numeral.( * ) (Numeral.equal Numeral.zero) Numeral.zero

let subtract_and_normalize_num_polynomials = 
  subtract_and_normalize_polynomials 
    add_num_polynomials 
    negate_num_polynomial 
    Numeral.zero
    (Numeral.equal Numeral.zero)
    (Numeral.gt Numeral.zero)

(* ********************************************************************** *)
(* Real arithmetic functions on polynomials                               *)
(* ********************************************************************** *)


let add_dec_monomial_lists = add_monomial_lists Decimal.(+) (Decimal.equal Decimal.zero)

let add_dec_polynomials = add_polynomials Decimal.(+) Decimal.zero (Decimal.equal Decimal.zero)

let const_multiply_dec_monomial_list = const_multiply_monomial_list Decimal.( * )

let const_multiply_dec_polynomial = const_multiply_polynomial Decimal.( * )

let negate_dec_monomial_list = negate_monomial_list Decimal.( * ) (Decimal.neg Decimal.one)

let negate_dec_polynomial = negate_polynomial Decimal.( * ) (Decimal.neg Decimal.one)

let multiply_dec_polynomials = 
  multiply_polynomials Decimal.( * ) (Decimal.equal Decimal.zero) Decimal.zero

let subtract_and_normalize_dec_polynomials = 
  subtract_and_normalize_polynomials 
    add_dec_polynomials 
    negate_dec_polynomial 
    Decimal.zero
    (Decimal.equal Decimal.zero) 
    (Decimal.gt Decimal.zero) 

(* ********************************************************************** *)
(* Functions used in {!simplify_term_node}                                *)
(* ********************************************************************** *)


(* Sum up a list of integer polynomials *)
let add_num args = 

  let args' = List.map num_polynomial_of_nf args in

  add_num_polynomials args'


(* Sum up a list of real polynomials *)
let add_dec args = 

  let args' = List.map dec_polynomial_of_nf args in

  add_dec_polynomials args'


(* Multiply two integer polynomials *)
let multiply_num p1 p2 = 

  let p1', p2' = num_polynomial_of_nf p1, num_polynomial_of_nf p2 in

  multiply_num_polynomials p1' p2'


(* Multiply two real polynomials *)
let multiply_dec p1 p2 = 

  let p1', p2' = dec_polynomial_of_nf p1, dec_polynomial_of_nf p2 in

  multiply_dec_polynomials p1' p2'


(* Sum up a list of real or integer normal forms *)
let add = function

  (* Addition is not nullary  *)
  | [] -> assert false 
    
  (* Add as integer polynomials if head of list is integer *)
  | Num _ :: _ as args -> Num (add_num args)
                    
  (* Add as real polynomials if head of list is real *)
  | Dec _ :: _ as args -> Dec (add_dec args)
                     
  (* Cannot add other types *)
  | _ -> assert false


(* Subtract a list of polynomials *)
let minus = function 

  (* Subtraction is not nullary  *)
  | [] -> assert false 

  (* Unary integer minus: negate polynomial to (- c - p) *)
  | [Num p] -> Num (negate_num_polynomial p)

  (* Unary real minus: negate polynomial to (- c - p) *)
  | [Dec p] -> Dec (negate_dec_polynomial p)

  (* Binary integer minus or higher arity: (h - s1 - ... - sn) reduce
     to (h - (s1 + ... + sn) *)
  | Num p :: tl -> 

    Num (add_num_polynomials [p; negate_num_polynomial (add_num tl)])

  (* Binary real minus or higher arity: (h - s1 - ... - sn) reduce to
     (h - (s1 + ... + sn) *)
  | Dec p :: tl -> 

    Dec (add_dec_polynomials [p; negate_dec_polynomial (add_dec tl)])

  (* Cannot subtract other types *)
  | _ -> assert false


(* Multiply a list of polynomials *)
let times = function 

  (* Multiplication is not nullary  *)
  | [] -> assert false 
    
  (* Multiply as integer polynomials if head of list is integer *)
  | Num p :: tl -> 
    
    Num 
      (List.fold_left 
         multiply_num_polynomials 
         p 
         (List.map num_polynomial_of_nf tl))
                    
  (* Multiply as real polynomials if head of list is real *)
  | Dec p :: tl -> 

    Dec
      (List.fold_left 
         multiply_dec_polynomials 
         p 
         (List.map dec_polynomial_of_nf tl))
                     
  (* Cannot multiply other types *)
  | _ -> assert false


(* Flatten nested associative Boolean operators by lifting the
   subterms of a nested operator as subterms of the top operator: 
   (a & (b & c)) becomes (a & b & c)

   The arguments must be Boolean, real and integer terms are
   normalized to polynomials. *)
let flatten_bool_subterms s l = 

  (* Tail-recursive function with accumulator *)
  let rec flatten_bool_subterms' symbol accum = function 

    (* No more subterms, return accumulator in original order *)
    | [] -> List.rev accum

    (* Boolean operator *)
    | Bool t :: tl -> 

      let accum' =
        
        (* Get symbol of term *)
        match Term.destruct t with

          (* Symbol is the same as the top-level symbol? *)
          | Term.T.App (s, l) when s == symbol -> 

            (* Add subterms of term in reverse order to subterms of
               top term *)
            List.rev_append l accum 

          (* Keep term unchanged *)
          | _ -> t :: accum

      in

      (* Recurse for remaining subterms *)
      flatten_bool_subterms' symbol accum' tl

    (* Fail on non-boolean arguments *)
    | (Num _ | Dec _ | Array _ | BV _ ) :: _ -> assert false

  in

  (* Call tail-recursive function with initial accumulator *)
  flatten_bool_subterms' s [] l 


(* Return true if a complement of a term in the second list is in the
   first list *)
let rec has_complement l = function 
  | [] -> false 
  | h :: tl -> 
    if List.memq (Term.negate h) l then true else has_complement l tl


(* Negate a term in negation normal form

   The term must only contain conjunctions and disjunctions as Boolean
   operators, the argument of a Boolean negation must be an atom. *)
let rec negate_nnf term = match Term.destruct term with 

  (* Negate a variable *)
  | Term.T.Var v -> Term.mk_not (Term.mk_var v)

  (* Negate a constant *)
  | Term.T.Const s ->

    (* Unhashcons constant symbol *)
    (match Symbol.node_of_symbol s with 

      | `TRUE -> Term.t_false
      | `FALSE -> Term.t_true
      | `UF u -> Term.mk_not (Term.mk_uf u [])
      | _ -> assert false

    )

  (* Negate a function application *)
  | Term.T.App (s, l) -> 

    (* Unhashcons constant symbol *)
    (match Symbol.node_of_symbol s, l with 

      (* Double unary negation *)
      | `NOT, [a] -> a

      (* Negation must be unary *)
      | `NOT, _ -> assert false 

      (* Conjunction *)
      | `AND, l -> 
        Term.mk_or (List.map (function t -> negate_nnf t) l)

      (* Disjunction *)
      | `OR, l -> 
        Term.mk_and (List.map (function t -> negate_nnf t) l)

      (* Disjunction and conjunction are the only Boolean operators *)
      | `IMPLIES, _
      | `XOR, _ -> assert false

      (* Boolean equivalence must not occur *)
      | `EQ, [] -> assert false 

      | `EQ, h :: _ 
        when 
          Term.type_of_term h == Type.t_bool -> 
        assert false 

      (* Negate atoms *)
      | `EQ, _ 
      | `DISTINCT, _
      | `LEQ, _
      | `LT, _
      | `GEQ, _
      | `GT, _
      | `IS_INT, _
      | `DIVISIBLE _, _
      | `UF _, _
      | `SELECT _, _
      | `STORE, _ -> Term.mk_not term

      (* Negate both cases of ite term *)
      | `ITE, [p; l; r] -> 
        Term.mk_ite 
          p
          (negate_nnf l)
          (negate_nnf r)

      (* Non-ternary ite *)
      | `ITE, _ -> assert false

      (* Constant symbols *)
      | `FALSE, _
      | `TRUE, _
      | `NUMERAL _, _
      | `DECIMAL _, _ -> assert false

      | `BV _, _ -> assert false

      (* Can only negate Boolean terms *)
      | `MINUS, _
      | `PLUS, _
      | `TIMES, _
      | `DIV, _
      | `INTDIV, _
      | `MOD, _
      | `ABS, _
      | `TO_REAL, _
      | `TO_INT, _
      | `TO_INT8, _
      | `TO_INT16, _
      | `TO_INT32, _
      | `TO_INT64, _ 

      | `CONCAT, _
      | `EXTRACT _, _
      | `BVNEG, _
      | `BVADD, _
      | `BVMUL, _
      | `BVUDIV, _
      | `BVUREM, _
      | `BVSHL, _
      | `BVLSHR, _
      | `BVULT, _ 
      | `BVULE, _
      | `BVUGT, _
      | `BVUGE, _
      | `BVNOT, _
      | `BVOR, _ 
      | `BVAND, _ -> assert false 
    )    

  | Term.T.Attr (t, _) -> t


(* Negate all but the last term *)
let implies_to_or args = 

  (* Tail-recursive function with accumulator *)
  let rec implies_to_or' accum = function 
    | [] -> assert false
    | [a] -> List.rev (a :: accum)
    | Bool h :: tl -> implies_to_or' (Bool (negate_nnf h) :: accum) tl
    | (Num _ | Dec _ | Array _ | BV _ ) :: _ -> assert false
  in

  implies_to_or' [] args 


(* Subtract two normal forms and make constant or first coefficient
   positive *)
let subtract_and_normalize a b = match a, b with 

  (* Two integer polynomials *)
  | Num a, Num b -> 
    let s, r = subtract_and_normalize_num_polynomials a b in s, Num r

  (* Two real polynomials *)
  | Dec a, Dec b -> 
    let s, r = subtract_and_normalize_dec_polynomials a b in s, Dec r

  (* Cannot subtract *)
  | _ -> assert false

let relation_to_nf_bv rel = function
  (* Relation must be binary *)
  | [] 
  | [_] -> assert false

  (* Binary relation *)
  | [a; b] -> (match (rel (Term.bitvector_of_term (term_of_nf a)) (Term.bitvector_of_term (term_of_nf b))) with
    | true -> Bool Term.t_true
    | false -> Bool Term.t_false)

  (* Arity greater than 2 *)
  | _ -> assert false

(* Normalize an n-ary relation by unchaining it into a conjunction of
   binary relations, subtracting the right-hand side from the
   left-hand side and evaluating to true or false if possible

   When normalizing, we might multiply with a negative factor and then
   need to replace the relation symbol by its converse. Hence we need
   to know the converse of the relation (primed parameters). *)
let rec relation_to_nf 
    simplify_term_node 
    rel 
    rel'
    mk_rel 
    mk_rel' 
    zero 
    t_zero = function

  (* Relation must be at least binary *)
  | [] 
  | [_] -> assert false
{'fraction_non_alphanumeric': 0.1377740655669242, 'fraction_numerical': 0.006702860722489037, 'mean_word_length': 2.564644585039077, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 221, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2433902', 'n_tokens_mistral': 15818, 'n_tokens_neox': 14537, 'n_words': 4984}