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

[LRA] split the module in part 

 - RealValue: constants
 - Dom_interval: interval domaine
 - Dom_polynome: Polynome, pivot (shostak theory like)
parent 10f1159c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 432 additions and 317 deletions
src_colibri2/tests/tests_LRA.ml
+ 22
− 22
View file @ cba25d6a
...@@ -42,7 +42,7 @@ open Expr ...@@ -42,7 +42,7 @@ open Expr
let solve0a _ = let solve0a _ =
let a = fresh Ty.real "ar" in let a = fresh Ty.real "ar" in
let _1 = LRA.cst Q.one in let _1 = LRA.RealValue.cst Q.one in
let a1 = LRA.add a _1 in let a1 = LRA.add a _1 in
let env = run $$ fun env -> let env = run $$ fun env ->
register env a1; register env _1; register env a1; register env _1;
...@@ -52,9 +52,9 @@ let solve0a _ = ...@@ -52,9 +52,9 @@ let solve0a _ =
(* let solve0b _ = (* let solve0b _ =
* let a = fresh Term._Real "ar" in * let a = fresh Term._Real "ar" in
* let _1 = LRA.cst Q.one in * let _1 = LRA.RealValue.cst Q.one in
* let _2 = LRA.cst Q.two in * let _2 = LRA.RealValue.cst Q.two in
* let _4 = LRA.cst (Q.of_int 4) in * let _4 = LRA.RealValue.cst (Q.of_int 4) in
* let a1 = LRA.add a _1 in * let a1 = LRA.add a _1 in
* let _2a2 = LRA.add' Q.two a Q.one _2 in * let _2a2 = LRA.add' Q.two a Q.one _2 in
* let env = run $$ fun env -> * let env = run $$ fun env ->
...@@ -66,7 +66,7 @@ let solve0a _ = ...@@ -66,7 +66,7 @@ let solve0a _ =
let solve0c _ = let solve0c _ =
let a = fresh Ty.real "ar" in let a = fresh Ty.real "ar" in
let b = fresh Ty.real "br" in let b = fresh Ty.real "br" in
let _1 = LRA.cst Q.one in let _1 = LRA.RealValue.cst Q.one in
let a1 = LRA.add a _1 in let a1 = LRA.add a _1 in
let b1 = LRA.add b _1 in let b1 = LRA.add b _1 in
let env = run_dec $$ fun env -> let env = run_dec $$ fun env ->
...@@ -77,10 +77,10 @@ let solve0c _ = ...@@ -77,10 +77,10 @@ let solve0c _ =
let solve1 _ = let solve1 _ =
let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in
let _1 = LRA.cst Q.one in let _1 = LRA.RealValue.cst Q.one in
let a1 = LRA.add a _1 in let a1 = LRA.add a _1 in
let b1 = LRA.add b _1 in let b1 = LRA.add b _1 in
let _2 = LRA.cst (Q.of_int 2) in let _2 = LRA.RealValue.cst (Q.of_int 2) in
let a2 = LRA.add a _2 in let a2 = LRA.add a _2 in
let b2 = LRA.add b _2 in let b2 = LRA.add b _2 in
let env = run_dec $$ fun env -> let env = run_dec $$ fun env ->
...@@ -91,10 +91,10 @@ let solve1 _ = ...@@ -91,10 +91,10 @@ let solve1 _ =
let solve2 _ = let solve2 _ =
let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in
let _1 = LRA.cst Q.one in let _1 = LRA.RealValue.cst Q.one in
let a1 = LRA.add a _1 in let a1 = LRA.add a _1 in
let b1 = LRA.add b _1 in let b1 = LRA.add b _1 in
let _2 = LRA.cst (Q.of_int 2) in let _2 = LRA.RealValue.cst (Q.of_int 2) in
let a2 = LRA.add a _2 in let a2 = LRA.add a _2 in
let b2 = LRA.add b _2 in let b2 = LRA.add b _2 in
let env = run_dec $$ fun env -> let env = run_dec $$ fun env ->
...@@ -105,11 +105,11 @@ let solve2 _ = ...@@ -105,11 +105,11 @@ let solve2 _ =
let solve3 _ = let solve3 _ =
let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in
let _1 = LRA.cst Q.one in let _1 = LRA.RealValue.cst Q.one in
let b1 = LRA.add b _1 in let b1 = LRA.add b _1 in
let _2 = LRA.cst (Q.of_int 2) in let _2 = LRA.RealValue.cst (Q.of_int 2) in
let a2 = LRA.add a _2 in let a2 = LRA.add a _2 in
let _3 = LRA.cst (Q.of_int 3) in let _3 = LRA.RealValue.cst (Q.of_int 3) in
let env = run $$ fun env -> let env = run $$ fun env ->
Shuffle.seql [ Shuffle.seql [
(fun () -> (fun () ->
...@@ -132,15 +132,15 @@ let solve3 _ = ...@@ -132,15 +132,15 @@ let solve3 _ =
let solve4 _ = let solve4 _ =
let a,b,c = let a,b,c =
Shuffle.seq3 (fresh Ty.real) ("ar","br","cr") in Shuffle.seq3 (fresh Ty.real) ("ar","br","cr") in
let t1 = LRA.cst (Q.of_int 2) in let t1 = LRA.RealValue.cst (Q.of_int 2) in
let t1 = LRA.add t1 c in let t1 = LRA.add t1 c in
let t1 = LRA.add a t1 in let t1 = LRA.add a t1 in
let t1' = (LRA.cst (Q.of_int 1)) in let t1' = (LRA.RealValue.cst (Q.of_int 1)) in
let t1' = LRA.add b t1' in let t1' = LRA.add b t1' in
let t2 = a in let t2 = a in
let t2' = LRA.cst (Q.of_int 2) in let t2' = LRA.RealValue.cst (Q.of_int 2) in
let t2' = LRA.add t2' b in let t2' = LRA.add t2' b in
let t3' = LRA.cst (Q.of_int (-3)) in let t3' = LRA.RealValue.cst (Q.of_int (-3)) in
let env = run_dec $$ fun env -> let env = run_dec $$ fun env ->
Shuffle.seql [ Shuffle.seql [
(fun () -> (fun () ->
...@@ -161,9 +161,9 @@ let solve5 _ = ...@@ -161,9 +161,9 @@ let solve5 _ =
let c = fresh Ty.real "cr" in let c = fresh Ty.real "cr" in
let t1 = LRA.sub b c in let t1 = LRA.sub b c in
let t1 = LRA.add a t1 in let t1 = LRA.add a t1 in
let t1' = (LRA.cst (Q.of_int 2)) in let t1' = (LRA.RealValue.cst (Q.of_int 2)) in
let t2 = a in let t2 = a in
let t2' = LRA.cst (Q.of_int 2) in let t2' = LRA.RealValue.cst (Q.of_int 2) in
let t3 = LRA.add b c in let t3 = LRA.add b c in
let t3' = LRA.add b b in let t3' = LRA.add b b in
let env = run_dec $$ fun env -> let env = run_dec $$ fun env ->
...@@ -198,9 +198,9 @@ let basic = "LRA.Basic" &: ...@@ -198,9 +198,9 @@ let basic = "LRA.Basic" &:
* let t1 = LRA.sub a b in * let t1 = LRA.sub a b in
* let t1' = LRA.mult a b in * let t1' = LRA.mult a b in
* let t2 = a in * let t2 = a in
* let t2' = LRA.cst (Q.of_int 1) in * let t2' = LRA.RealValue.cst (Q.of_int 1) in
* let t3 = LRA.mult_cst (Q.of_int 2) b in * let t3 = LRA.mult_cst (Q.of_int 2) b in
* let t3' = LRA.cst (Q.of_int 1) in * let t3' = LRA.RealValue.cst (Q.of_int 1) in
* let env = run $$ fun env -> * let env = run $$ fun env ->
* Shuffle.seql [ * Shuffle.seql [
* (fun () -> * (fun () ->
...@@ -225,9 +225,9 @@ let basic = "LRA.Basic" &: ...@@ -225,9 +225,9 @@ let basic = "LRA.Basic" &:
* let t1' = LRA.add b c in * let t1' = LRA.add b c in
* let t1' = LRA.mult t1' a in * let t1' = LRA.mult t1' a in
* let t2 = a in * let t2 = a in
* let t2' = LRA.cst (Q.of_int 2) in * let t2' = LRA.RealValue.cst (Q.of_int 2) in
* let t3 = c in * let t3 = c in
* let t3' = LRA.cst (Q.of_int 1) in * let t3' = LRA.RealValue.cst (Q.of_int 1) in
* let env = run $$ fun env -> * let env = run $$ fun env ->
* Shuffle.seql [ * Shuffle.seql [
* (fun () -> * (fun () ->
......
src_colibri2/theories/LRA/LRA.ml
+ 44
− 290
View file @ cba25d6a
...@@ -18,7 +18,6 @@ ...@@ -18,7 +18,6 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *) (* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************) (*************************************************************************)
(** This module use one domain and two semantic values. *)
open Colibri2_popop_lib open Colibri2_popop_lib
open Colibri2_core open Colibri2_core
open Colibri2_stdlib.Std open Colibri2_stdlib.Std
...@@ -27,17 +26,6 @@ let debug = Debug.register_info_flag ...@@ -27,17 +26,6 @@ let debug = Debug.register_info_flag
~desc:"for the arithmetic theory" ~desc:"for the arithmetic theory"
"LRA" "LRA"
let real = ValueKind.create_key (module struct type t = Q.t let name = "Q" end)
module RealValue = ValueKind.Register(struct
include Q
let key = real
end)
let cst' c = RealValue.index ~basename:(Format.asprintf "%aR" Q.pp c) c
let cst c = RealValue.node (cst' c)
let debug_todo = debug
type bound = Colibrics_lib.Interval.Bound.t = Strict | Large type bound = Colibrics_lib.Interval.Bound.t = Strict | Large
[@@deriving eq,ord,show,hash] [@@deriving eq,ord,show,hash]
module S = struct module S = struct
...@@ -69,194 +57,16 @@ end ...@@ -69,194 +57,16 @@ end
module SE = ThTermKind.Register(S) module SE = ThTermKind.Register(S)
module D = Interval.Convexe
let dom = DomKind.create_key (module struct type t = D.t let name = "ARITH" end)
let dom_poly = DomKind.create_key (module struct type t = Polynome.t let name = "ARITH_POLY" end)
let set_dom d node v =
match D.is_singleton v with
| Some q ->
let cst = cst' q in
Egraph.set_value d node (RealValue.nodevalue cst)
| None ->
(** the pexp must be in the dom *)
Egraph.set_dom d dom node v
(** Polynome *) (** Polynome *)
let propa_dem = Demon.Key.create "Arith.DaemonPropa" let propa_dem = Demon.Key.create "Arith.DaemonPropa"
let print_bag_cl = Colibri2_popop_lib.Bag.pp Pp.comma Node.pp let print_bag_cl = Colibri2_popop_lib.Bag.pp Pp.comma Node.pp
let used_in_poly : Node.t Bag.t Node.HC.t = Node.HC.create (Bag.pp Pp.semi Node.pp) "used_in_poly"
module T = struct
include Polynome
let key = ThTermKind.create_key (module struct type nonrec t = t let name = "SARITH_POLY" end)
end
module ThE = ThTermKind.Register(T)
let set_poly d cl p =
Egraph.set_dom d dom_poly 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_poly used with
| None -> Egraph.set_dom d dom_poly used (Polynome.monome Q.one used)
| Some p ->
Format.eprintf "used=%a p=%a@." Node.pp used Polynome.pp 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_poly 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 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_poly cl norm
let merge d ((p1o,cl1) as a1) ((p2o,cl2) as a2) inv =
assert (not (Egraph.is_equal d cl1 cl2));
assert (not (CCOpt.is_none p1o && CCOpt.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 _ ->
(* 0 = cst <> 0 *)
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 (CCOpt.compare Polynome.compare
(Egraph.get_dom d dom_poly repr)
(Egraph.get_dom d dom_poly other) = 0)
let solve_one d cl p1 =
match Egraph.get_dom d dom_poly 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 _ ->
(* 0 = cst <> 0 *)
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_poly
end
let () = Egraph.register_dom(module Th)
let minus_or_one inv = let minus_or_one inv =
if inv then Q.minus_one else Q.one if inv then Q.minus_one else Q.one
let print_bag_node = Bag.pp Format.(const char ',') Node.pp let print_bag_node = Bag.pp Format.(const char ',') Node.pp
let () = DomKind.register(module struct
include D
let key = dom
let merged i1 i2 =
match i1, i2 with
| None, None -> true
| Some i1, Some i2 -> D.equal i1 i2
| _ -> false
let merge d (i1,cl1) (i2,cl2) _ =
assert (not (Egraph.is_equal d cl1 cl2));
match i1, cl1, i2, cl2 with
| Some i1,_, Some i2,_ ->
begin match D.inter i1 i2 with
| None ->
Egraph.contradiction d
| Some i ->
if not (D.equal i i1) then
Egraph.set_dom d dom cl1 i;
if not (D.equal i i2) then
Egraph.set_dom d dom cl2 i
end
| Some i1, _, _, cl2 | _, cl2, Some i1, _ ->
Egraph.set_dom d dom cl2 i1
| None,_,None,_ -> raise Impossible
end)
module DaemonPropa = struct module DaemonPropa = struct
let key = Demon.Fast.create "LRA.DaemonPropa" let key = Demon.Fast.create "LRA.DaemonPropa"
...@@ -265,36 +75,37 @@ module DaemonPropa = struct ...@@ -265,36 +75,37 @@ module DaemonPropa = struct
let immediate = false let immediate = false
let throttle = 100 let throttle = 100
let gt_zero = D.gt Q.zero let gt_zero = Dom_interval.D.gt Q.zero
let ge_zero = D.ge Q.zero let ge_zero = Dom_interval.D.ge Q.zero
let lt_zero = D.lt Q.zero let lt_zero = Dom_interval.D.lt Q.zero
let le_zero = D.le Q.zero let le_zero = Dom_interval.D.le Q.zero
let get_dom del node = Opt.get_def D.reals (Egraph.get_dom del dom node) let get_dom del node =
Opt.get_def Dom_interval.D.reals (Egraph.get_dom del Dom_interval.dom node)
let get_value del node = let get_value del node =
match Egraph.get_value del real node with match Egraph.get_value del RealValue.key node with
| None -> D.reals | None -> Dom_interval.D.reals
| Some d -> D.singleton d | Some d -> Dom_interval.D.singleton d
let upd del node d d' = let upd del node d d' =
match D.inter d d' with match Dom_interval.D.inter d d' with
| None -> | None ->
Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a" Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
Node.pp node D.pp d D.pp d'; Node.pp node Dom_interval.D.pp d Dom_interval.D.pp d';
Egraph.contradiction del Egraph.contradiction del
| Some d' -> | Some d' ->
if not (D.equal d d') if not (Dom_interval.D.equal d d')
then set_dom del node d' then Dom_interval.set_dom del node d'
let upd_value del node d d' = let upd_value del node d d' =
match D.inter d d' with match Dom_interval.D.inter d d' with
| None -> | None ->
Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a" Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
Node.pp node D.pp d D.pp d'; Node.pp node Dom_interval.D.pp d Dom_interval.D.pp d';
Egraph.contradiction del Egraph.contradiction del
| Some d' -> | Some d' ->
if not (D.equal d d') if not (Dom_interval.D.equal d d')
then set_dom del node d' then Dom_interval.set_dom del node d'
let propagate del s = let propagate del s =
match SE.sem s with match SE.sem s with
...@@ -302,27 +113,27 @@ module DaemonPropa = struct ...@@ -302,27 +113,27 @@ module DaemonPropa = struct
let cl0 = SE.node s in let cl0 = SE.node s in
let d0 = get_value del cl0 in let d0 = get_value del cl0 in
if Q.equal q1 Q.one && Q.equal q2 Q.minus_one && if Q.equal q1 Q.one && Q.equal q2 Q.minus_one &&
D.equal d0 D.zero then Dom_interval.D.equal d0 Dom_interval.D.zero then
Egraph.merge del cl1 cl2 Egraph.merge del cl1 cl2
else else
let d1 = get_value del cl1 in let d1 = get_value del cl1 in
let d2 = get_value del cl2 in let d2 = get_value del cl2 in
let upd_value node d d' = upd_value del node d d' in let upd_value node d d' = upd_value del node d d' in
let qd1 = D.mult_cst q1 d1 in let qd1 = Dom_interval.D.mult_cst q1 d1 in
let qd2 = D.mult_cst q2 d2 in let qd2 = Dom_interval.D.mult_cst q2 d2 in
upd_value cl0 d0 (D.add qd1 qd2); upd_value cl0 d0 (Dom_interval.D.add qd1 qd2);
upd_value cl1 d1 (D.mult_cst (Q.inv q1) (D.minus d0 qd2)); upd_value cl1 d1 (Dom_interval.D.mult_cst (Q.inv q1) (Dom_interval.D.minus d0 qd2));
upd_value cl2 d2 (D.mult_cst (Q.inv q2) (D.minus d0 qd1)) upd_value cl2 d2 (Dom_interval.D.mult_cst (Q.inv q2) (Dom_interval.D.minus d0 qd1))
| S.GZero(node,b) -> begin | S.GZero(node,b) -> begin
let cl0 = SE.node s in let cl0 = SE.node s in
let d = get_value del node in let d = get_value del node in
let dzero_true = if equal_bound b Strict then gt_zero else ge_zero in let dzero_true = if equal_bound b Strict then gt_zero else ge_zero in
let dzero_false = if equal_bound b Strict then le_zero else lt_zero in let dzero_false = if equal_bound b Strict then le_zero else lt_zero in
if D.is_included d dzero_true if Dom_interval.D.is_included d dzero_true
then begin then begin
Boolean.set_true del cl0 Boolean.set_true del cl0
end end
else if D.is_included d dzero_false else if Dom_interval.D.is_included d dzero_false
then then
Boolean.set_false del cl0 Boolean.set_false del cl0
end end
...@@ -340,45 +151,32 @@ module DaemonPropa = struct ...@@ -340,45 +151,32 @@ module DaemonPropa = struct
| S.Add (c1,cl1,c2,cl2) -> | S.Add (c1,cl1,c2,cl2) ->
Egraph.register d cl1; Egraph.register d cl2; Egraph.register d cl1; Egraph.register d cl2;
Demon.Fast.attach d key Demon.Fast.attach d key
[Demon.Create.EventValue(SE.node s, real, s); [Demon.Create.EventValue(SE.node s, RealValue.key, s);
Demon.Create.EventValue(cl1, real, s); Demon.Create.EventValue(cl1, RealValue.key, s);
Demon.Create.EventValue(cl2, real, s); Demon.Create.EventValue(cl2, RealValue.key, s);
]; ];
let cl = (SE.node s) in let cl = (SE.node s) in
let add acc c cl = let add acc c cl =
let cl = Egraph.find d cl in let cl = Egraph.find d cl in
match Egraph.get_dom d dom_poly cl with match Egraph.get_dom d Dom_polynome.dom_poly cl with
| None -> Polynome.add acc (Polynome.monome c cl) | None -> Polynome.add acc (Polynome.monome c cl)
| Some p -> Polynome.x_p_cy acc c p | Some p -> Polynome.x_p_cy acc c p
in in
let p1 = add (add Polynome.zero c1 cl1) c2 cl2 in let p1 = add (add Polynome.zero c1 cl1) c2 cl2 in
Th.solve_one d cl p1 Dom_polynome.solve_one d cl p1
| GZero (node,_) -> | GZero (node,_) ->
Egraph.register d node; Egraph.register d node;
Demon.Fast.attach d key Demon.Fast.attach d key
[Demon.Create.EventValue(SE.node s, Boolean.dom, s); [Demon.Create.EventValue(SE.node s, Boolean.dom, s);
Demon.Create.EventValue(node, real, s)] Demon.Create.EventValue(node, RealValue.key, s)]
end; end;
propagate d s; propagate d s;
end end
module RDaemonPropa = Demon.Fast.Register(DaemonPropa) module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
let assume_poly_equality d n p = let zero = RealValue.cst Q.zero
Debug.dprintf4 debug "assume1: %a = %a" Node.pp n Polynome.pp p; let one = RealValue.cst Q.one
let n = Egraph.find d n in
let add acc cl c =
let cl = Egraph.find d cl in
match Egraph.get_dom d dom_poly cl with
| None -> Polynome.add acc (Polynome.monome c cl)
| Some p -> Polynome.x_p_cy acc c p
in
let p = Polynome.fold add Polynome.zero p in
Debug.dprintf4 debug "assume2: %a = %a" Node.pp n Polynome.pp p;
Th.solve_one d n p
let zero = cst Q.zero
let one = cst Q.one
let index s = SE.index s let index s = SE.index s
let add' q1 cl1 q2 cl2 = let add' q1 cl1 q2 cl2 =
...@@ -408,7 +206,7 @@ let of_poly p = ...@@ -408,7 +206,7 @@ let of_poly p =
| `Some(rq,r) -> `Some(Q.one,SE.node (add' q node rq r)) | `Some(rq,r) -> `Some(Q.one,SE.node (add' q node rq r))
in in
match aux m with match aux m with
| `None -> cst c | `None -> RealValue.cst c
| `Some(rq,r) when Q.equal rq Q.one && Q.equal c Q.zero -> r | `Some(rq,r) when Q.equal rq Q.one && Q.equal c Q.zero -> r
| `Some(rq,r) -> SE.node (add' rq r c one) | `Some(rq,r) -> SE.node (add' rq r c one)
...@@ -416,53 +214,6 @@ let to_poly = function ...@@ -416,53 +214,6 @@ let to_poly = function
| S.Add(q1,cl1,q2,cl2) -> Polynome.of_list Q.one [cl1,q1;cl2,q2] | S.Add(q1,cl1,q2,cl2) -> Polynome.of_list Q.one [cl1,q1;cl2,q2]
| GZero _ -> raise Impossible | GZero _ -> raise Impossible
type hypbound =
| Eq
| Le
| Lt
[@@deriving eq]
let _ = Eq
let _ = Le
let _ = Lt
type hyppoly = {
bound: hypbound ;
poly: Polynome.t ;
}
let pp_hyppoly fmt c =
let bound = function
| Eq -> "="
| Le -> "󠀼≤"
| Lt -> "<"
in
Format.fprintf fmt "0 %s %a"
(bound c.bound)
Polynome.pp c.poly
module ChoLRA = struct
let make_decision node v env =
Debug.dprintf4 Egraph.print_decision
"[LRA] decide %a on %a" D.pp v Node.pp node;
set_dom env node v
let choose_decision node env =
let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
match D.split_heuristic v with
| Singleton _ -> Egraph.DecNo
| Splitted (v1,v2) ->
DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
| NotSplitted ->
DecTodo [make_decision node (D.singleton (D.choose v))]
let choice n = {
Egraph.prio = 1;
choice = choose_decision n;
}
end
(** API *) (** API *)
let index x = SE.node (SE.index x) let index x = SE.node (SE.index x)
...@@ -508,13 +259,13 @@ let converter d (f:Ground.t) = ...@@ -508,13 +259,13 @@ let converter d (f:Ground.t) =
match Ground.sem f with match Ground.sem f with
| { app = {builtin = Dolmen_std.Expr.Base; _ }; tyargs = _; args = _; ty } | { app = {builtin = Dolmen_std.Expr.Base; _ }; tyargs = _; args = _; ty }
when Ground.Ty.equal ty Ground.Ty.real -> when Ground.Ty.equal ty Ground.Ty.real ->
Egraph.register_decision d (ChoLRA.choice res) Egraph.register_decision d (Dom_interval.ChoLRA.choice res)
| { app = {builtin = Expr.Integer s}; tyargs = []; args = []; _ } -> | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; _ } ->
reg (cst (Q.of_string s)) reg (RealValue.cst (Q.of_string s))
| { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; _ } -> | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; _ } ->
reg (cst (Q.of_string_decimal s)) reg (RealValue.cst (Q.of_string_decimal s))
| { app = {builtin = Expr.Rational s}; tyargs = []; args = []; _ } -> | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; _ } ->
reg (cst (Q.of_string_decimal s)) reg (RealValue.cst (Q.of_string_decimal s))
| { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } -> | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
reg (add (of_term a) (of_term b)) reg (add (of_term a) (of_term b))
| { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } -> | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
...@@ -545,11 +296,11 @@ let th_register env = ...@@ -545,11 +296,11 @@ let th_register env =
(module RealValue) (module RealValue)
(fun d value -> (fun d value ->
let v = RealValue.value value in let v = RealValue.value value in
let s = D.singleton v in let s = Dom_interval.D.singleton v in
Egraph.set_dom d dom (RealValue.node value) s; Egraph.set_dom d Dom_interval.dom (RealValue.node value) s;
let cl = RealValue.node value in let cl = RealValue.node value in
let p1 = Polynome.of_list v [] in let p1 = Polynome.of_list v [] in
Th.solve_one d cl p1 Dom_polynome.solve_one d cl p1
) env; ) env;
() ()
...@@ -612,3 +363,6 @@ let () = ...@@ -612,3 +363,6 @@ let () =
!<< (Q.geq !>arg1 !>arg2) !<< (Q.geq !>arg1 !>arg2)
| _ -> None | _ -> None
) )
module RealValue = RealValue
src_colibri2/theories/LRA/LRA.mli
+ 6
− 3
View file @ cba25d6a
...@@ -18,7 +18,6 @@ ...@@ -18,7 +18,6 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *) (* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************) (*************************************************************************)
val cst : Q.t -> Node.t
val add' : Q.t -> Node.t -> Q.t -> Node.t -> Node.t val add' : Q.t -> Node.t -> Q.t -> Node.t -> Node.t
val add : Node.t -> Node.t -> Node.t val add : Node.t -> Node.t -> Node.t
val sub : Node.t -> Node.t -> Node.t val sub : Node.t -> Node.t -> Node.t
...@@ -38,6 +37,10 @@ val le: Node.t -> Node.t -> Node.t ...@@ -38,6 +37,10 @@ val le: Node.t -> Node.t -> Node.t
val gt: Node.t -> Node.t -> Node.t val gt: Node.t -> Node.t -> Node.t
val ge: Node.t -> Node.t -> Node.t val ge: Node.t -> Node.t -> Node.t
module RealValue : ValueKind.Registered with type s = Q.t module RealValue : sig
include ValueKind.Registered with type s = Q.t
val assume_poly_equality: Egraph.t -> Node.t -> Polynome.t -> unit val cst': Q.t -> t
val cst: Q.t -> Node.t
end
src_colibri2/theories/LRA/dom_interval.ml 0 → 100644
+ 93
− 0
View file @ cba25d6a
(*************************************************************************)
(* This file is part of Colibrics. *)
(* *)
(* Copyright (C) 2017 *)
(* 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 intervals for the arithmetic theory"
"LRA.interval"
module D = Interval.Convexe
let dom = DomKind.create_key (module struct type t = D.t let name = "ARITH" end)
let () = DomKind.register(module struct
include D
let key = dom
let merged i1 i2 =
match i1, i2 with
| None, None -> true
| Some i1, Some i2 -> D.equal i1 i2
| _ -> false
let merge d (i1,cl1) (i2,cl2) _ =
assert (not (Egraph.is_equal d cl1 cl2));
match i1, cl1, i2, cl2 with
| Some i1,_, Some i2,_ ->
begin match D.inter i1 i2 with
| None ->
Egraph.contradiction d
| Some i ->
if not (D.equal i i1) then
Egraph.set_dom d dom cl1 i;
if not (D.equal i i2) then
Egraph.set_dom d dom cl2 i
end
| Some i1, _, _, cl2 | _, cl2, Some i1, _ ->
Egraph.set_dom d dom cl2 i1
| None,_,None,_ -> raise Impossible
end)
let set_dom d node v =
match D.is_singleton v with
| Some q ->
let cst = RealValue.cst' q in
Egraph.set_value d node (RealValue.nodevalue cst)
| None ->
(** the pexp must be in the dom *)
Egraph.set_dom d dom node v
module ChoLRA = struct
let make_decision node v env =
Debug.dprintf4 Egraph.print_decision
"[LRA] decide %a on %a" D.pp v Node.pp node;
set_dom env node v
let choose_decision node env =
let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
match D.split_heuristic v with
| Singleton _ -> Egraph.DecNo
| Splitted (v1,v2) ->
DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
| NotSplitted ->
DecTodo [make_decision node (D.singleton (D.choose v))]
let choice n = {
Egraph.prio = 1;
choice = choose_decision n;
}
end
let choice = ChoLRA.choice
src_colibri2/theories/LRA/dom_polynome.ml 0 → 100644
+ 181
− 0
View file @ cba25d6a
(*************************************************************************)
(* This file is part of Colibrics. *)
(* *)
(* Copyright (C) 2017 *)
(* 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"
let dom_poly = DomKind.create_key (module struct type t = Polynome.t let name = "ARITH_POLY" end)
module T = struct
include Polynome
let key = ThTermKind.create_key (module struct type nonrec t = t let name = "SARITH_POLY" end)
end
module ThE = ThTermKind.Register(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_poly 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_poly used with
| None -> Egraph.set_dom d dom_poly used (Polynome.monome Q.one used)
| Some p ->
Format.eprintf "used=%a p=%a@." Node.pp used Polynome.pp 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_poly 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 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_poly cl norm
let merge d ((p1o,cl1) as a1) ((p2o,cl2) as a2) inv =
assert (not (Egraph.is_equal d cl1 cl2));
assert (not (CCOpt.is_none p1o && CCOpt.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 _ ->
(* 0 = cst <> 0 *)
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 (CCOpt.compare Polynome.compare
(Egraph.get_dom d dom_poly repr)
(Egraph.get_dom d dom_poly other) = 0)
let solve_one d cl p1 =
match Egraph.get_dom d dom_poly 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 _ ->
(* 0 = cst <> 0 *)
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_poly
end
let () = Egraph.register_dom(module Th)
let assume_poly_equality d n p =
Debug.dprintf4 debug "assume1: %a = %a" Node.pp n Polynome.pp p;
let n = Egraph.find d n in
let add acc cl c =
let cl = Egraph.find d cl in
match Egraph.get_dom d dom_poly cl with
| None -> Polynome.add acc (Polynome.monome c cl)
| Some p -> Polynome.x_p_cy acc c p
in
let p = Polynome.fold add Polynome.zero p in
Debug.dprintf4 debug "assume2: %a = %a" Node.pp n Polynome.pp p;
Th.solve_one d n p
let solve_one = Th.solve_one
src_colibri2/theories/LRA/dom_polynome.mli 0 → 100644
+ 25
− 0
View file @ cba25d6a
(*************************************************************************)
(* This file is part of Colibrics. *)
(* *)
(* Copyright (C) 2017 *)
(* 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). *)
(*************************************************************************)
val assume_poly_equality: Egraph.t -> Node.t -> Polynome.t -> unit
val dom_poly: Polynome.t DomKind.t
val solve_one: Egraph.t -> Node.t -> Polynome.t -> unit
src_colibri2/theories/LRA/mul.ml
+ 2
− 2
View file @ cba25d6a
let init,attach = let init,attach =
Demon.Fast.register_get_value_daemon Demon.Fast.register_get_value_daemon
~name:"Mul.get_value" ~name:"Mul.get_value"
(module LRA.RealValue) (module RealValue)
(fun d _ q (mul,other) -> (fun d _ q (mul,other) ->
LRA.assume_poly_equality d mul (Polynome.monome q other) Dom_polynome.assume_poly_equality d mul (Polynome.monome q other)
) )
let converter d (f:Ground.t) = let converter d (f:Ground.t) =
......
src_colibri2/theories/LRA/realValue.ml 0 → 100644
+ 35
− 0
View file @ cba25d6a
(*************************************************************************)
(* This file is part of Colibrics. *)
(* *)
(* Copyright (C) 2017 *)
(* 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_core
open Colibri2_stdlib.Std
let real = ValueKind.create_key (module struct type t = Q.t let name = "Q" end)
module RealValue = ValueKind.Register(struct
include Q
let key = real
end)
let cst' c = RealValue.index ~basename:(Format.asprintf "%aR" Q.pp c) c
let cst c = RealValue.node (cst' c)
include RealValue
src_colibri2/theories/LRA/realValue.mli 0 → 100644
+ 24
− 0
View file @ cba25d6a
(*************************************************************************)
(* This file is part of Colibrics. *)
(* *)
(* Copyright (C) 2017 *)
(* 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). *)
(*************************************************************************)
include ValueKind.Registered with type s = Q.t
val cst': Q.t -> t
val cst: Q.t -> Node.t
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