Skip to content
Snippets Groups Projects
Commit 5d8aa991 authored by François Bobot's avatar François Bobot
Browse files

[LRA] Factorize dom_polynome

parent f8101028
No related branches found
No related tags found
1 merge request!17Separate Abs and Sign
Hide whitespace changes
Inline Side-by-side
Showing
with 506 additions and 398 deletions
src_colibri2/theories/LRA/dom_polynome.ml
+ 61
− 181
View file @ 5d8aa991
......@@ -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
src_colibri2/theories/LRA/dom_polynome.mli
+ 11
− 5
View file @ 5d8aa991
......@@ -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
src_colibri2/theories/LRA/dom_product.ml
+ 4
− 4
View file @ 5d8aa991
......@@ -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
src_colibri2/theories/LRA/fourier.ml
+ 186
− 166
View file @ 5d8aa991
......@@ -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
src_colibri2/theories/LRA/mul.ml
+ 12
− 15
View file @ 5d8aa991
......@@ -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
src_colibri2/theories/LRA/pivot.ml
+ 196
− 1
View file @ 5d8aa991
......@@ -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
src_colibri2/theories/LRA/pivot.mli
+ 36
− 26
View file @ 5d8aa991
......@@ -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
*)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment