diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 4ee192231889c6f459e7dc0d7625bf69ca796f0b..73396151e323e93dc4f721a317d8306806b37be4 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -22,205 +22,85 @@ 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"
-
-let dom = Dom.Kind.create (module struct type t = Polynome.t let name = "ARITH_POLY" end)
+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)
+module ThE = ThTerm.Register (T)
let node_of_polynome t = ThE.node (ThE.index t)
-let used_in_poly : Node.t Bag.t Node.HC.t = Node.HC.create (Bag.pp Pp.semi Node.pp) "used_in_poly"
-
-let set_poly d cl p =
- Egraph.set_dom d dom cl p;
- match Polynome.is_one_node p with
- | None -> Egraph.set_thterm d cl (ThE.thterm (ThE.index p))
- | Some cl' -> Egraph.merge d cl cl'
-
-let add_used d cl' new_cl =
- Node.M.iter (fun used _ ->
- Node.HC.change (function
- | Some b -> Some (Bag.append b cl')
- | None ->
- begin match Egraph.get_dom d dom used with
- | None ->
- (** If a used node have no polynome associated, we set it to
- itself. This allows to be warned when this node is merged. It
- is the reason why this module doesn't specifically wait for
- representative change *)
- Egraph.set_dom d dom used (Polynome.monome Q.one used)
- | Some p ->
- assert (Polynome.equal (Polynome.monome Q.one used) p)
- end;
- Some (Bag.elt cl')
- ) used_in_poly d used
- ) new_cl
-
-let subst_doms d cl (p:Polynome.t) =
- let b = match Node.HC.find used_in_poly d cl with
- | exception Not_found -> Bag.empty
- | b -> b
- in
- Bag.iter (fun cl' ->
- match Egraph.get_dom d dom cl' with
- | None -> assert false (** absurd: can't be used and absent *)
- | Some q ->
- let new_cl = Node.M.set_diff p.poly q.poly in
- let q, _ = Polynome.subst q cl p in
- add_used d cl' new_cl;
- set_poly d cl' q
- ) b;
- add_used d cl p.poly;
- set_poly d cl p
-
-module Th = struct
+include Pivot.Total (struct
include Polynome
- let merged v1 v2 =
- match v1,v2 with
- | None, None -> true
- | Some v', Some v -> equal v' v
- | _ -> false
-
- let norm_dom cl = function
- | None ->
- let r = monome Q.one cl in
- r
- | Some p ->
- p
-
- let add_itself d cl norm =
- add_used d cl norm.poly;
- Egraph.set_dom d dom cl norm
-
- let merge d ((p1o,cl1) as a1) ((p2o,cl2) as a2) inv =
- assert (not (Egraph.is_equal d cl1 cl2));
- assert (not (Option.is_none p1o && Option.is_none p2o));
- let (pother, other), (prepr, repr) = if inv then a2,a1 else a1,a2 in
- let other = Egraph.find d other in
- let repr = Egraph.find d repr in
- let p1 = norm_dom other pother in
- let p2 = norm_dom repr prepr in
- let diff = sub p1 p2 in
- (* 0 = other - repr = p1 - p2 = diff *)
- Debug.dprintf2 debug "[Arith] @[solve 0=%a@]" pp diff;
- begin match Polynome.extract diff with
- | Zero -> (** no new equality already equal *)
- begin
- match pother, prepr with
- | Some _, Some _ | None, None ->
- assert false (** absurd: no need of merge *)
- | Some p, None ->
- (** p = repr *)
- add_itself d repr p
- | None, Some p ->
- (** p = other *)
- add_itself d other p
- end
- | Cst c ->
- (* 0 = cst <> 0 *)
- Debug.dprintf6 Debug.contradiction
- "[LRA/Poly] Found 0 = %a when merging %a and %a"
- Q.pp c
- Node.pp cl1 Node.pp cl2;
- Egraph.contradiction d
- | Var(q,x,p') ->
- (** diff = qx + p' *)
- assert ( not (Q.equal Q.zero q) );
- Debug.dprintf2 debug "[Arith] @[pivot %a@]" Node.pp x;
- let add_if_default n norm = function
- | Some _ -> ()
- | None ->
- add_itself d n norm
- in
- add_if_default other p1 pother;
- add_if_default repr p2 prepr;
- subst_doms d x (Polynome.mult_cst (Q.div Q.one (Q.neg q)) p')
- end;
- assert (Option.compare Polynome.compare
- (Egraph.get_dom d dom repr)
- (Egraph.get_dom d dom other) = 0)
-
- let solve_one d cl p1 =
- match Egraph.get_dom d dom cl with
- | None ->
- subst_doms d cl p1
- | Some p2 ->
- let diff = Polynome.sub p1 p2 in
- (* 0 = p1 - p2 = diff *)
- Debug.dprintf8 debug "[Arith] @[solve in init %a 0=(%a)-(%a)=%a@]"
- Node.pp cl Polynome.pp p1 Polynome.pp p2 Polynome.pp diff;
- begin match Polynome.extract diff with
- | Zero -> ()
- | Cst c ->
- (* 0 = cst <> 0 *)
- Debug.dprintf4 Debug.contradiction
- "[LRA/Poly] Found 0 = %a when updating %a"
- Q.pp c
- Node.pp cl;
- Egraph.contradiction d
- | Var(q,x,p') ->
- (** diff = qx + p' *)
- assert ( not (Q.equal Q.zero q) );
- Debug.dprintf2 debug "[Arith] @[pivot %a@]" Node.pp x;
- subst_doms d x (Polynome.mult_cst (Q.div Q.one (Q.neg q)) p')
- end
-
- let key = dom
-end
+ let name = "LRA.polynome"
+
+ type data = Q.t
-let () = Dom.register(module Th)
+ let nodes p = p.poly
-let norm d (p:Polynome.t) =
- let add acc cl c =
- let cl = Egraph.find_def d cl in
- match Egraph.get_dom d dom cl with
- | None -> Polynome.add acc (Polynome.monome c cl)
- | Some p -> Polynome.x_p_cy acc c p
- in
- Polynome.fold add (Polynome.cst p.cst) p
+ let of_one_node n = monome Q.one n
-let assume_poly_equality d n (p:Polynome.t) =
- (* Debug.dprintf4 debug "assume1: %a = %a" Node.pp n Polynome.pp p; *)
- let n = Egraph.find_def d n in
- let p = norm d p in
- (* Debug.dprintf4 debug "assume2: %a = %a" Node.pp n Polynome.pp p; *)
- Th.solve_one d n p
+ 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 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_poly_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_poly_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_poly_equality d res (Polynome.of_list Q.zero [a,Q.minus_one])
+ | { 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_poly_equality d cl p1
- );
- Ground.register_converter env converter
+ 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
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
index ef3a5d7b07be91f7b2dd8afbc9f027b1f9a6804a..b88d42211bc103a39df7fcbca3e15592e400c2d7 100644
--- a/src_colibri2/theories/LRA/dom_polynome.mli
+++ b/src_colibri2/theories/LRA/dom_polynome.mli
@@ -18,12 +18,18 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val assume_poly_equality: Egraph.wt -> Node.t -> Polynome.t -> unit
+val assume_equality : Egraph.wt -> Node.t -> Polynome.t -> unit
-val dom: Polynome.t Dom.Kind.t
+val get_repr : _ Egraph.t -> Node.t -> Polynome.t option
-val init: Egraph.wt -> unit
+val attach_repr_change :
+ _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
-val node_of_polynome: Polynome.t -> Node.t
+val events_repr_change :
+ _ Egraph.t -> ?node:Node.t -> (Egraph.rt -> Node.t -> Events.enqueue) -> unit
-val norm: _ Egraph.t -> Polynome.t -> Polynome.t
+val init : Egraph.wt -> unit
+
+val node_of_polynome : Polynome.t -> Node.t
+
+val normalize : _ Egraph.t -> Polynome.t -> Polynome.t
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index fbb41f95db08eb883e5f33e8f8a05c9029eebe44..63fd43051d9d8bf28a5be8b9b6666eb63af1b1c2 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -145,7 +145,7 @@ let factorize res a coef b d _ =
Debug.dprintf10 debug "[Factorize] %a = %a + %a * %a into %a" Node.pp
res Node.pp a Q.pp coef Node.pp b Polynome.pp p;
Egraph.register d n;
- Dom_polynome.assume_poly_equality d n p;
+ Dom_polynome.assume_equality d n p;
assume_equality d res (Product.of_map (Node.M.add n Q.one common)))
| _ -> ()
@@ -185,8 +185,8 @@ let converter d (f : Ground.t) =
let init env =
init env;
- Daemon.attach_any_dom env Dom_polynome.dom (fun d n ->
- match Egraph.get_dom d Dom_polynome.dom n with
+ Dom_polynome.attach_repr_change env (fun d n ->
+ match Dom_polynome.get_repr d n with
| None -> ()
| Some p ->
if Q.equal p.cst Q.zero && Node.M.is_num_elt 1 p.poly then
@@ -204,5 +204,5 @@ let init env =
let p1 = Polynome.of_list Q.zero [ (cl, Q.one) ] in
Debug.dprintf4 debug "[Product->Polynome] propagate %a is %a"
Node.pp n Node.pp cl;
- Dom_polynome.assume_poly_equality d n p1)));
+ Dom_polynome.assume_equality d n p1)));
Ground.register_converter env converter
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 672d8571a9ef125ad5420dba02ac143900cca103..0ff795e9cee0f7ea421ec19ef4cf7f0370dd61b6 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -22,218 +22,235 @@ open Colibri2_popop_lib
open Colibri2_core
let comparisons = Datastructure.Push.create Ground.pp "LRA.fourier.comparisons"
-let scheduled = Datastructure.Ref.create Base.Bool.pp "LRA.fourier.scheduled" false
-let debug = Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourier"
+let scheduled =
+ Datastructure.Ref.create Base.Bool.pp "LRA.fourier.scheduled" false
-let stats_run = Debug.register_stats_int ~name:"Fourier.run" ~init:0
+let debug =
+ Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourier"
+let stats_run = Debug.register_stats_int ~name:"Fourier.run" ~init:0
-type eq = { p: Polynome.t; bound: Bound.t; origins: Ground.S.t }
+type eq = { p : Polynome.t; bound : Bound.t; origins : Ground.S.t }
[@@deriving show]
(** p <= 0 or p < 0 *)
-let divide d (p:Polynome.t) =
+let divide d (p : Polynome.t) =
try
- begin match Polynome.is_cst p with
- | None -> ()
- | Some _ -> raise Exit
- end;
+ (match Polynome.is_cst p with None -> () | Some _ -> raise Exit);
if Q.sign p.cst <> 0 then raise Exit;
let l = Node.M.bindings p.poly in
- let l = List.fold_left (fun acc (e,q) ->
- match Dom_product.get_repr d e with
- | None when Egraph.is_equal d RealValue.zero e -> acc
- | None -> raise Exit
- | Some p -> (p,q)::acc) [] l in
- Debug.dprintf4 debug "@[eq:%a@ %a@]"
- Polynome.pp p Fmt.(list ~sep:(any "+") (using CCPair.swap (pair Q.pp Product.pp))) l;
+ let l =
+ List.fold_left
+ (fun acc (e, q) ->
+ match Dom_product.get_repr d e with
+ | None when Egraph.is_equal d RealValue.zero e -> acc
+ | None -> raise Exit
+ | Some p -> (p, q) :: acc)
+ [] l
+ in
+ Debug.dprintf4 debug "@[eq:%a@ %a@]" Polynome.pp p
+ Fmt.(list ~sep:(any "+") (using CCPair.swap (pair Q.pp Product.pp)))
+ l;
match l with
| [] -> raise Exit
- | (hd,_)::_ ->
- let common = List.fold_left (fun acc (p,_) ->
- Node.M.inter (fun _ a b -> if Q.equal a b then Some a else None) acc p.Product.poly)
- hd.Product.poly l in
- let common, pos = Node.M.fold_left
- (fun (acc,pos) n v ->
- if Dom_interval.is_strictly_positive d n
- then (Node.M.add n v acc,pos)
- else if Dom_interval.is_strictly_negative d n
- then (Node.M.add n v acc,not pos)
- else (acc,pos)
- ) (Node.M.empty,true) common
- in
- if Node.M.is_empty common then raise Exit;
- Debug.dprintf4 debug "[Fourier] found possible division: %a / %a"
- Polynome.pp p (Node.M.pp Q.pp) common;
- let (cst,l) = List.fold_left (fun (cst,acc) (p,v) ->
- let p = Product.of_map (Node.M.set_diff p.Product.poly common) in
+ | (hd, _) :: _ ->
+ let common =
+ List.fold_left
+ (fun acc (p, _) ->
+ Node.M.inter
+ (fun _ a b -> if Q.equal a b then Some a else None)
+ acc p.Product.poly)
+ hd.Product.poly l
+ in
+ let common, pos =
+ Node.M.fold_left
+ (fun (acc, pos) n v ->
+ if Dom_interval.is_strictly_positive d n then
+ (Node.M.add n v acc, pos)
+ else if Dom_interval.is_strictly_negative d n then
+ (Node.M.add n v acc, not pos)
+ else (acc, pos))
+ (Node.M.empty, true) common
+ in
+ if Node.M.is_empty common then raise Exit;
+ Debug.dprintf4 debug "[Fourier] found possible division: %a / %a"
+ Polynome.pp p (Node.M.pp Q.pp) common;
+ let cst, l =
+ List.fold_left
+ (fun (cst, acc) (p, v) ->
+ let p = Product.of_map (Node.M.set_diff p.Product.poly common) in
- let v = if pos then v else Q.neg v in
- match Product.classify p with
- | ONE ->
- (Q.add v cst,acc)
- | NODE n ->
- (cst,(n,v)::acc)
- | PRODUCT ->
- let n = Dom_product.node_of_product p in
- (Q.add Q.one cst,(n,v)::acc)
- ) (Q.zero,[]) l in
- Some (Polynome.of_list cst l,common,pos)
- with Exit ->
- None
+ let v = if pos then v else Q.neg v in
+ match Product.classify p with
+ | ONE -> (Q.add v cst, acc)
+ | NODE n -> (cst, (n, v) :: acc)
+ | PRODUCT ->
+ let n = Dom_product.node_of_product p in
+ (Q.add Q.one cst, (n, v) :: acc))
+ (Q.zero, []) l
+ in
+ Some (Polynome.of_list cst l, common, pos)
+ with Exit -> None
let delta d eq =
(* add info to delta *)
if Node.M.is_num_elt 2 eq.p.poly then
match Node.M.bindings eq.p.poly with
- | [src,a;dst,b] when Q.equal Q.one a && Q.equal Q.minus_one b ->
- Delta.add d src (Q.neg eq.p.cst) eq.bound dst
- | [dst,b;src,a] when Q.equal Q.one a && Q.equal Q.minus_one b ->
- Delta.add d src (Q.neg eq.p.cst) eq.bound dst
+ | [ (src, a); (dst, b) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
+ Delta.add d src (Q.neg eq.p.cst) eq.bound dst
+ | [ (dst, b); (src, a) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
+ Delta.add d src (Q.neg eq.p.cst) eq.bound dst
| _ -> ()
let apply d ~f truth g =
let aux d bound a b =
- let bound = if truth then bound else match bound with | Bound.Large -> Strict | Strict -> Large in
- let a,b = if truth then a,b else b,a in
- f d bound a b
+ let bound =
+ if truth then bound
+ else match bound with Bound.Large -> Strict | Strict -> Large
+ in
+ let a, b = if truth then (a, b) else (b, a) in
+ f d bound a b
in
match Ground.sem g with
- | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- aux d Bound.Strict a b
- | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- aux d Large a b
- | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- aux d Large b a
- | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- aux d Strict b a
+ | { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ aux d Bound.Strict a b
+ | { app = { builtin = Expr.Leq }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ aux d Large a b
+ | { app = { builtin = Expr.Geq }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ aux d Large b a
+ | { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ aux d Strict b a
| _ -> assert false
-
let add_eq d eqs p bound origins =
- match Polynome.is_cst p, bound with
+ match (Polynome.is_cst p, bound) with
| None, _ ->
- let eq = { p; bound; origins } in
- delta d eq;
- eq::eqs
+ let eq = { p; bound; origins } in
+ delta d eq;
+ eq :: eqs
| Some p, Bound.Large when Q.sign p = 0 ->
- Ground.S.iter (fun g ->
- let truth = Base.Option.value_exn (Boolean.is d (Ground.node g)) in
- apply d truth g ~f:(fun d bound a b ->
- match bound with
- | Strict when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
- Dom_polynome.assume_poly_equality d a (Polynome.of_list Q.minus_one [b,Q.one])
- | Large ->
- Dom_polynome.assume_poly_equality d a (Polynome.monome Q.one b)
- | Strict ->
- assert false
- )) origins;
- eqs
+ Ground.S.iter
+ (fun g ->
+ let truth = Base.Option.value_exn (Boolean.is d (Ground.node g)) in
+ apply d truth g ~f:(fun d bound a b ->
+ match bound with
+ | Strict
+ when Dom_interval.is_integer d a && Dom_interval.is_integer d b
+ ->
+ Dom_polynome.assume_equality d a
+ (Polynome.of_list Q.minus_one [ (b, Q.one) ])
+ | Large ->
+ Dom_polynome.assume_equality d a (Polynome.monome Q.one b)
+ | Strict -> assert false))
+ origins;
+ eqs
| Some p, _ when Q.sign p < 0 ->
- Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
- eqs
+ Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
+ eqs
| Some p, bound ->
- Debug.dprintf4 Debug.contradiction
- "[LRA/Fourier] Found %a%a0"
- Q.pp p Bound.pp bound;
- Egraph.contradiction d
+ Debug.dprintf4 Debug.contradiction "[LRA/Fourier] Found %a%a0" Q.pp p
+ Bound.pp bound;
+ Egraph.contradiction d
let mk_eq d bound a b =
- let (!) n =
- match Egraph.get_dom d Dom_polynome.dom n with
+ let ( ! ) n =
+ match Dom_polynome.get_repr d n with
| None -> Polynome.monome Q.one (Egraph.find_def d n)
- | Some p -> p in
- let p,bound' =
+ | Some p -> p
+ in
+ let p, bound' =
match bound with
- | Bound.Strict when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
- Polynome.add_cst (Polynome.sub (!a) (!b)) Q.one, Bound.Large
- | _ -> Polynome.sub (!a) (!b), bound
+ | Bound.Strict
+ when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
+ (Polynome.add_cst (Polynome.sub !a !b) Q.one, Bound.Large)
+ | _ -> (Polynome.sub !a !b, bound)
in
- p,bound',
- Polynome.sub (Polynome.monome Q.one a) (Polynome.monome Q.one b), bound
+ ( p,
+ bound',
+ Polynome.sub (Polynome.monome Q.one a) (Polynome.monome Q.one b),
+ bound )
-let make_equations d (eqs,vars) g =
+let make_equations d (eqs, vars) g =
Debug.dprintf2 debug "[Fourier] %a" Ground.pp g;
match Boolean.is d (Ground.node g) with
- | None ->
- (eqs,vars)
- | Some truth ->
- let p,bound,p_non_norm,bound_non_norm =
- apply d ~f:mk_eq truth g
- in
- Debug.dprintf6 debug "[Fourier] %a(%a)%a0" Polynome.pp p Polynome.pp p_non_norm Bound.pp bound;
- let eqs, vars =
- (add_eq d eqs p bound (Ground.S.singleton g),
- Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly)
- in
- match divide d p_non_norm with
- | Some (p',_,_) ->
- let p' = Dom_polynome.norm d p' in
- (add_eq d eqs p' bound_non_norm Ground.S.empty,
- Node.M.union_merge (fun _ _ _ -> Some ()) vars p'.Polynome.poly)
- | None -> eqs, vars
+ | None -> (eqs, vars)
+ | Some truth -> (
+ let p, bound, p_non_norm, bound_non_norm = apply d ~f:mk_eq truth g in
+ Debug.dprintf6 debug "[Fourier] %a(%a)%a0" Polynome.pp p Polynome.pp
+ p_non_norm Bound.pp bound;
+ let eqs, vars =
+ ( add_eq d eqs p bound (Ground.S.singleton g),
+ Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly )
+ in
+ match divide d p_non_norm with
+ | Some (p', _, _) ->
+ let p' = Dom_polynome.normalize d p' in
+ ( add_eq d eqs p' bound_non_norm Ground.S.empty,
+ Node.M.union_merge (fun _ _ _ -> Some ()) vars p'.Polynome.poly )
+ | None -> (eqs, vars))
-let fm (d:Egraph.wt) =
+let fm (d : Egraph.wt) =
Debug.dprintf0 debug "[Fourier]";
Debug.incr stats_run;
Datastructure.Ref.set scheduled d false;
- let eqs, vars = Datastructure.Push.fold comparisons d
- ~f:(make_equations d) ~init:([],Node.S.empty)
+ let eqs, vars =
+ Datastructure.Push.fold comparisons d ~f:(make_equations d)
+ ~init:([], Node.S.empty)
in
let rec split n positive negative absent = function
- | [] -> (positive,negative,absent)
- | eq::l ->
- match Node.M.find_opt n eq.p.poly with
- | None -> split n positive negative (eq::absent) l
- | Some q ->
- if Q.sign q > 0 then
- split n ((q,eq)::positive) negative absent l
- else split n positive ((q,eq)::negative) absent l
+ | [] -> (positive, negative, absent)
+ | eq :: l -> (
+ match Node.M.find_opt n eq.p.poly with
+ | None -> split n positive negative (eq :: absent) l
+ | Some q ->
+ if Q.sign q > 0 then split n ((q, eq) :: positive) negative absent l
+ else split n positive ((q, eq) :: negative) absent l)
in
let rec aux eqs vars =
match Node.S.choose vars with
| exception Not_found -> ()
- | n ->
- let vars = Node.S.remove n vars in
- let positive, negative, absent = split n [] [] [] eqs in
- match positive, negative with
- | [], _ | _ , [] -> aux absent vars
- | _, _ ->
- let eqs =
- Lists.fold_product (fun eqs (pq,peq) (nq,neq) ->
- let q = Q.div pq (Q.neg nq) in
- let p = Polynome.cx_p_cy Q.one peq.p q neq.p in
- let bound =
- match peq.bound, neq.bound with
- | Large, Large -> Bound.Large
- | _ -> Bound.Strict in
- add_eq d eqs p bound (Ground.S.union peq.origins neq.origins)
- ) absent positive negative
- in
- aux eqs vars
+ | n -> (
+ let vars = Node.S.remove n vars in
+ let positive, negative, absent = split n [] [] [] eqs in
+ match (positive, negative) with
+ | [], _ | _, [] -> aux absent vars
+ | _, _ ->
+ let eqs =
+ Lists.fold_product
+ (fun eqs (pq, peq) (nq, neq) ->
+ let q = Q.div pq (Q.neg nq) in
+ let p = Polynome.cx_p_cy Q.one peq.p q neq.p in
+ let bound =
+ match (peq.bound, neq.bound) with
+ | Large, Large -> Bound.Large
+ | _ -> Bound.Strict
+ in
+ add_eq d eqs p bound (Ground.S.union peq.origins neq.origins))
+ absent positive negative
+ in
+ aux eqs vars)
in
aux eqs vars
module Daemon = struct
let key =
Events.Dem.create
- ( module struct
+ (module struct
type t = unit
+
let name = "LRA.fourier"
- end )
+ end)
let enqueue d _ =
- if Datastructure.Ref.get scheduled d
- then Events.EnqAlready
- else begin
+ if Datastructure.Ref.get scheduled d then Events.EnqAlready
+ else (
Datastructure.Ref.set scheduled d true;
- Events.EnqRun (key,(),None)
- end
+ Events.EnqRun (key, (), None))
let delay = Events.Delayed_by 64
@@ -246,21 +263,24 @@ end
let () = Events.register (module Daemon)
-
(** {2 Initialization} *)
-let converter d (f:Ground.t) =
+let converter d (f : Ground.t) =
match Ground.sem f with
- | { app = {builtin = (Expr.Lt|Expr.Leq|Expr.Geq|Expr.Gt)}; tyargs = []; args } ->
- let attach n =
- Events.attach_dom d n Dom_polynome.dom Daemon.enqueue;
- Events.attach_repr d n Daemon.enqueue;
- in
- IArray.iter ~f:attach args;
- Events.attach_value d (Ground.node f) Boolean.dom (fun d n _ -> Daemon.enqueue d n);
- Datastructure.Push.push comparisons d f;
- Events.new_pending_daemon d Daemon.key ();
- Choice.register d (Boolean.chobool (Ground.node f))
+ | {
+ app = { builtin = Expr.Lt | Expr.Leq | Expr.Geq | Expr.Gt };
+ tyargs = [];
+ args;
+ } ->
+ let attach n =
+ Dom_polynome.events_repr_change d ~node:n Daemon.enqueue;
+ Events.attach_repr d n Daemon.enqueue
+ in
+ IArray.iter ~f:attach args;
+ Events.attach_value d (Ground.node f) Boolean.dom (fun d n _ ->
+ Daemon.enqueue d n);
+ Datastructure.Push.push comparisons d f;
+ Events.new_pending_daemon d Daemon.key ();
+ Choice.register d (Boolean.chobool (Ground.node f))
| _ -> ()
-let init env =
- Ground.register_converter env converter
+let init env = Ground.register_converter env converter
diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml
index 2d078b586480accbd5f4adbdb065c903fa07151e..c59c0dfc175cd9379b0e9e4aa17ce40126b72d20 100644
--- a/src_colibri2/theories/LRA/mul.ml
+++ b/src_colibri2/theories/LRA/mul.ml
@@ -18,23 +18,20 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-let attach d n (mul,other) =
- Daemon.attach_value d n
- RealValue.key
- (fun d _ q ->
- Dom_polynome.assume_poly_equality d mul (Polynome.monome (RealValue.value q) other)
- )
+let attach d n (mul, other) =
+ Daemon.attach_value d n RealValue.key (fun d _ q ->
+ Dom_polynome.assume_equality d mul
+ (Polynome.monome (RealValue.value q) other))
-let converter d (f:Ground.t) =
+let converter d (f : Ground.t) =
let res = Ground.node f in
match Ground.sem f with
- | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } -> begin
- let arg1,arg2 = Colibri2_popop_lib.IArray.extract2_exn args in
- Egraph.register d arg1; Egraph.register d arg2;
- attach d arg1 (res,arg2);
- attach d arg2 (res,arg1)
- end
+ | { app = { builtin = Expr.Mul }; tyargs = []; args; _ } ->
+ let arg1, arg2 = Colibri2_popop_lib.IArray.extract2_exn args in
+ Egraph.register d arg1;
+ Egraph.register d arg2;
+ attach d arg1 (res, arg2);
+ attach d arg2 (res, arg1)
| _ -> ()
-let init env =
- Ground.register_converter env converter
+let init env = Ground.register_converter env converter
diff --git a/src_colibri2/theories/LRA/pivot.ml b/src_colibri2/theories/LRA/pivot.ml
index 0c97ad4837562a0fc7b37f9fdcd2538f42e8cb26..76b0c8f419f80081ed2f55b85b32e86225e6ba2a 100644
--- a/src_colibri2/theories/LRA/pivot.ml
+++ b/src_colibri2/theories/LRA/pivot.ml
@@ -198,7 +198,7 @@ end = struct
(part d (p2.repr :: P.S.elements p2.eqs)))
with
| `Solved ->
- (* The domains have been subsituted, and possibly recursively *)
+ (* The domains have been substituted, and possibly recursively *)
merge_aux d cl1 cl2
| `Not_solved ->
(* nothing to solve *)
@@ -347,3 +347,198 @@ end = struct
let attach_repr_change = attach_eqs_change
end
+
+type 'a solve_total = AlreadyEqual | Contradiction | Subst of Node.t * 'a
+
+module Total (P : sig
+ type t
+
+ val name : string
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+
+ val of_one_node : Node.t -> t
+
+ val is_one_node : t -> Node.t option
+
+ val subst : t -> Node.t -> t -> t
+
+ val normalize : t -> f:(Node.t -> t) -> t
+
+ type data
+
+ val nodes : t -> data Node.M.t
+
+ val solve : t -> t -> t solve_total
+
+ val set : Egraph.wt -> Node.t -> t -> unit
+end) : sig
+ val assume_equality : Egraph.wt -> Node.t -> P.t -> unit
+
+ val init : Egraph.wt -> unit
+
+ val get_repr : _ Egraph.t -> Node.t -> P.t option
+
+ val attach_repr_change :
+ _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+
+ val events_repr_change :
+ _ Egraph.t ->
+ ?node:Node.t ->
+ (Egraph.rt -> Node.t -> Events.enqueue) ->
+ unit
+
+ val normalize : _ Egraph.t -> P.t -> P.t
+end = struct
+ open Colibri2_popop_lib
+
+ let dom =
+ Dom.Kind.create
+ (module struct
+ type t = P.t
+
+ let name = P.name
+ end)
+
+ let used_in_poly : Node.t Bag.t Node.HC.t =
+ Node.HC.create (Bag.pp Pp.semi Node.pp) "used_in_poly"
+
+ let set_poly d cl p =
+ Egraph.set_dom d dom cl p;
+ P.set d cl p
+
+ let add_used d cl' new_cl =
+ Node.M.iter
+ (fun used _ ->
+ Node.HC.change
+ (function
+ | Some b -> Some (Bag.append b cl')
+ | None ->
+ (match Egraph.get_dom d dom used with
+ | None ->
+ (* If a used node have no polynome associated, we set it to
+ itself. This allows to be warned when this node is merged. It
+ is the reason why this module doesn't specifically wait for
+ representative change *)
+ Egraph.set_dom d dom used (P.of_one_node used)
+ | Some p -> assert (P.equal (P.of_one_node used) p));
+ Some (Bag.elt cl'))
+ used_in_poly d used)
+ new_cl
+
+ let subst_doms d cl (p : P.t) =
+ let b =
+ match Node.HC.find used_in_poly d cl with
+ | exception Not_found -> Bag.empty
+ | b -> b
+ in
+ Bag.iter
+ (fun cl' ->
+ match Egraph.get_dom d dom cl' with
+ | None -> assert false (* absurd: can't be used and absent *)
+ | Some q ->
+ let new_cl = Node.M.set_diff (P.nodes p) (P.nodes q) in
+ let q = P.subst q cl p in
+ add_used d cl' new_cl;
+ set_poly d cl' q)
+ b;
+ add_used d cl (P.nodes p);
+ set_poly d cl p
+
+ module Th = struct
+ include P
+
+ let merged v1 v2 =
+ match (v1, v2) with
+ | None, None -> true
+ | Some v', Some v -> equal v' v
+ | _ -> false
+
+ let norm_dom cl = function
+ | None ->
+ let r = P.of_one_node cl in
+ r
+ | Some p -> p
+
+ let add_itself d cl norm =
+ add_used d cl (P.nodes norm);
+ Egraph.set_dom d dom cl norm
+
+ let merge d ((p1o, cl1) as a1) ((p2o, cl2) as a2) inv =
+ assert (not (Egraph.is_equal d cl1 cl2));
+ assert (not (Option.is_none p1o && Option.is_none p2o));
+ let (pother, other), (prepr, repr) = if inv then (a2, a1) else (a1, a2) in
+ let other = Egraph.find d other in
+ let repr = Egraph.find d repr in
+ let p1 = norm_dom other pother in
+ let p2 = norm_dom repr prepr in
+ (match P.solve p1 p2 with
+ | AlreadyEqual -> (
+ (* no new equality already equal *)
+ match (pother, prepr) with
+ | Some _, Some _ | None, None ->
+ assert false (* absurd: no need of merge *)
+ | Some p, None ->
+ (* p = repr *)
+ add_itself d repr p
+ | None, Some p ->
+ (* p = other *)
+ add_itself d other p)
+ | Contradiction -> Egraph.contradiction d
+ | Subst (x, p) ->
+ Debug.dprintf2 debug "[Arith] @[pivot %a@]" Node.pp x;
+ let add_if_default n norm = function
+ | Some _ -> ()
+ | None -> add_itself d n norm
+ in
+ add_if_default other p1 pother;
+ add_if_default repr p2 prepr;
+ subst_doms d x p);
+ assert (
+ Option.compare P.compare
+ (Egraph.get_dom d dom repr)
+ (Egraph.get_dom d dom other)
+ = 0)
+
+ let solve_one d cl p1 =
+ match Egraph.get_dom d dom cl with
+ | None -> subst_doms d cl p1
+ | Some p2 -> (
+ match P.solve p1 p2 with
+ | AlreadyEqual -> ()
+ | Contradiction -> Egraph.contradiction d
+ | Subst (x, p) ->
+ Debug.dprintf2 debug "[Arith] @[pivot %a@]" Node.pp x;
+ subst_doms d x p)
+
+ let key = dom
+ end
+
+ let () = Dom.register (module Th)
+
+ let normalize d (p : P.t) =
+ P.normalize p ~f:(fun cl ->
+ let cl = Egraph.find_def d cl in
+ match Egraph.get_dom d dom cl with
+ | None -> P.of_one_node cl
+ | Some p -> p)
+
+ let assume_equality d n (p : P.t) =
+ let n = Egraph.find_def d n in
+ let p = normalize d p in
+ Th.solve_one d n p
+
+ let get_repr d cl = Egraph.get_dom d dom cl
+
+ let attach_repr_change d ?node f =
+ match node with
+ | Some x -> Daemon.attach_dom d x dom f
+ | None -> Daemon.attach_any_dom d dom f
+
+ let events_repr_change d ?node f =
+ match node with
+ | Some x -> Events.attach_dom d x dom f
+ | None -> Events.attach_any_dom d dom f
+
+ let init _ = ()
+end
diff --git a/src_colibri2/theories/LRA/pivot.mli b/src_colibri2/theories/LRA/pivot.mli
index 0012b6968ab2e6caf3a16d10ac00a76c807125b3..72186b9c1736954ff30113ededa139fe7080a552 100644
--- a/src_colibri2/theories/LRA/pivot.mli
+++ b/src_colibri2/theories/LRA/pivot.mli
@@ -83,49 +83,59 @@ end) : sig
_ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
end
-(*
-module Total(P:sig
+type 'a solve_total = AlreadyEqual | Contradiction | Subst of Node.t * 'a
- type t
-
- include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+module Total (P : sig
+ type t
+ (** Normalizable terms *)
- val of_one_node: Node.t -> t
- (** build a value that represent one node *)
+ val name : string
- val is_one_node: t -> Node.t option
- (** test if a value represents one node *)
+ include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
- val subst: t -> Node.t -> t -> t option
- (** [subst p n q] substitute [n] by [q] in [p], if [n] is not in [p] None is
- returned, otherwise the substitution is returned *)
+ val of_one_node : Node.t -> t
+ (** Build a value that represent one node *)
- val normalize: t -> f:(Node.t -> t option) -> t
- (** [norm p ~f] normalize [p] using [f] *)
+ val is_one_node : t -> Node.t option
+ (** Test if a value represents one node *)
- type data
+ val subst : t -> Node.t -> t -> t
+ (** [subst p n q] return the result of the substitution of [n] by [q] in [p] *)
- val nodes: t -> data Node.M.t
+ val normalize : t -> f:(Node.t -> t) -> t
+ (** [norm p ~f] normalize [p] using [f] *)
- type info
+ type data
+ (** An abstract type to avoid translating the map to sets in {!nodes} *)
- val info: Egraph.ro -> t -> info
+ val nodes : t -> data Node.M.t
+ (** [nodes t] returns the node which are present in [t] *)
- val solve: info -> info -> (Node.t * t)
+ val solve : t -> t -> t solve_total
+ (** [solve t1 t2] solve the equation [t1 = t2] by returning a substitution. *)
- val attach_info_change: (Egraph.rw -> Node.t -> Events.enqueue) -> unit
+ val set : Egraph.wt -> Node.t -> t -> unit
+ (** Called a new term equal to this node is found *)
+end) : sig
+ val assume_equality : Egraph.wt -> Node.t -> P.t -> unit
+ (** [assume_equality d n p] assumes the equality [n = p] *)
- val set: Egraph.rw -> Node.t -> t -> unit
+ val init : Egraph.wt -> unit
+ (** Initialize the data-structure needed. *)
- end): sig
+ val get_repr : _ Egraph.t -> Node.t -> P.t option
- include Dom.S with type t = P.t
+ val attach_repr_change :
+ _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
- val assume_equality: Egraph.rw -> Node.t -> P.t -> unit
+ val events_repr_change :
+ _ Egraph.t ->
+ ?node:Node.t ->
+ (Egraph.rt -> Node.t -> Events.enqueue) ->
+ unit
- val init: Egraph.rw -> unit
+ val normalize : _ Egraph.t -> P.t -> P.t
end
-*)
(* LocalWords: Normalizable
*)