dom_polynome.ml

(*************************************************************************)
(*  This file is part of Colibri2.                                       *)
(*                                                                       *)
(*  Copyright (C) 2014-2021                                              *)
(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
(*           alternatives)                                               *)
(*                                                                       *)
(*  you can redistribute it and/or modify it under the terms of the GNU  *)
(*  Lesser General Public License as published by the Free Software      *)
(*  Foundation, version 2.1.                                             *)
(*                                                                       *)
(*  It is distributed in the hope that it will be useful,                *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
(*  GNU Lesser General Public License for more details.                  *)
(*                                                                       *)
(*  See the GNU Lesser General Public License version 2.1                *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
(*************************************************************************)

open Colibri2_popop_lib
open Colibri2_core
open Colibri2_stdlib.Std

let debug =
  Debug.register_info_flag ~desc:"for the arithmetic theory of polynome"
    "LRA.polynome"

module T = struct
  include Polynome

  let name = "SARITH_POLY"
end

module ThE = ThTerm.Register (T)

let node_of_polynome t = ThE.node (ThE.index t)

include Pivot.Total (struct
  include Polynome

  let name = "LRA.polynome"

  type data = Q.t

  let nodes p = p.poly

  let of_one_node n = monome Q.one n

  let subst p n q = fst (subst p n q)

  let normalize p ~f =
    let add acc cl c = Polynome.x_p_cy acc c (f cl) in
    Polynome.fold add (Polynome.cst p.cst) p

  let set d cl p =
    match is_one_node p with
    | None -> Egraph.set_thterm d cl (ThE.thterm (ThE.index p))
    | Some cl' -> Egraph.merge d cl cl'

  let solve p1 p2 =
    let diff = sub p1 p2 in
    (* 0 = other - repr = p1 - p2 = diff *)
    Debug.dprintf2 debug "[Arith] @[solve 0=%a@]" pp diff;
    match Polynome.extract diff with
    | Zero -> Pivot.AlreadyEqual
    | Cst c ->
        (* 0 = cst <> 0 *)
        Debug.dprintf2 Debug.contradiction
          "[LRA/Poly] Found 0 = %a when merging" Q.pp c;
        Contradiction
    | Var (q, x, p') ->
        assert (not (Q.equal Q.zero q));
        (* diff = qx + p' *)
        Subst (x, Polynome.mult_cst (Q.div Q.one (Q.neg q)) p')
end)

(** {2 Initialization} *)
let converter d (f : Ground.t) =
  let res = Ground.node f in
  let reg n = Egraph.register d n in
  match Ground.sem f with
  | { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
      let a, b = IArray.extract2_exn args in
      reg a;
      reg b;
      assume_equality d res (Polynome.of_list Q.zero [ (a, Q.one); (b, Q.one) ])
  | { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
      let a, b = IArray.extract2_exn args in
      reg a;
      reg b;
      assume_equality d res
        (Polynome.of_list Q.zero [ (a, Q.one); (b, Q.minus_one) ])
  | { app = { builtin = Expr.Minus }; tyargs = []; args; _ } ->
      let a = IArray.extract1_exn args in
      reg a;
      assume_equality d res (Polynome.of_list Q.zero [ (a, Q.minus_one) ])
  | _ -> ()

let init env =
  Daemon.attach_reg_value env RealValue.key (fun d value ->
      let v = RealValue.value value in
      let cl = RealValue.node value in
      let p1 = Polynome.of_list v [] in
      assume_equality d cl p1);
  Ground.register_converter env converter