diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index cd1b22a0d2dc46dffc00725c8756ca26d5cef7f9..075dc5144a633b42a38326751dd0a4ba34656ec1 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -42,7 +42,7 @@ open Expr
let solve0a _ =
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 env = run $$ fun env ->
register env a1; register env _1;
@@ -52,9 +52,9 @@ let solve0a _ =
(* let solve0b _ =
* let a = fresh Term._Real "ar" in
- * let _1 = LRA.cst Q.one in
- * let _2 = LRA.cst Q.two in
- * let _4 = LRA.cst (Q.of_int 4) in
+ * let _1 = LRA.RealValue.cst Q.one in
+ * let _2 = LRA.RealValue.cst Q.two in
+ * let _4 = LRA.RealValue.cst (Q.of_int 4) in
* let a1 = LRA.add a _1 in
* let _2a2 = LRA.add' Q.two a Q.one _2 in
* let env = run $$ fun env ->
@@ -66,7 +66,7 @@ let solve0a _ =
let solve0c _ =
let a = fresh Ty.real "ar" 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 b1 = LRA.add b _1 in
let env = run_dec $$ fun env ->
@@ -77,10 +77,10 @@ let solve0c _ =
let solve1 _ =
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 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 b2 = LRA.add b _2 in
let env = run_dec $$ fun env ->
@@ -91,10 +91,10 @@ let solve1 _ =
let solve2 _ =
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 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 b2 = LRA.add b _2 in
let env = run_dec $$ fun env ->
@@ -105,11 +105,11 @@ let solve2 _ =
let solve3 _ =
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 _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 _3 = LRA.cst (Q.of_int 3) in
+ let _3 = LRA.RealValue.cst (Q.of_int 3) in
let env = run $$ fun env ->
Shuffle.seql [
(fun () ->
@@ -132,15 +132,15 @@ let solve3 _ =
let solve4 _ =
let a,b,c =
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 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 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 t3' = LRA.cst (Q.of_int (-3)) in
+ let t3' = LRA.RealValue.cst (Q.of_int (-3)) in
let env = run_dec $$ fun env ->
Shuffle.seql [
(fun () ->
@@ -161,9 +161,9 @@ let solve5 _ =
let c = fresh Ty.real "cr" in
let t1 = LRA.sub b c 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' = 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 b in
let env = run_dec $$ fun env ->
@@ -198,9 +198,9 @@ let basic = "LRA.Basic" &:
* let t1 = LRA.sub a b in
* let t1' = LRA.mult a b 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.cst (Q.of_int 1) in
+ * let t3' = LRA.RealValue.cst (Q.of_int 1) in
* let env = run $$ fun env ->
* Shuffle.seql [
* (fun () ->
@@ -225,9 +225,9 @@ let basic = "LRA.Basic" &:
* let t1' = LRA.add b c in
* let t1' = LRA.mult t1' 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' = LRA.cst (Q.of_int 1) in
+ * let t3' = LRA.RealValue.cst (Q.of_int 1) in
* let env = run $$ fun env ->
* Shuffle.seql [
* (fun () ->
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 9a3ad7370db5d7408050149cbc1f7b14da2443b3..9a070bd559af4b39294da13fe1edc2b8575fc684 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -18,7 +18,6 @@
(* 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_core
open Colibri2_stdlib.Std
@@ -27,17 +26,6 @@ let debug = Debug.register_info_flag
~desc:"for the arithmetic theory"
"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
[@@deriving eq,ord,show,hash]
module S = struct
@@ -69,194 +57,16 @@ end
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 *)
let propa_dem = Demon.Key.create "Arith.DaemonPropa"
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 =
if inv then Q.minus_one else Q.one
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
let key = Demon.Fast.create "LRA.DaemonPropa"
@@ -265,36 +75,37 @@ module DaemonPropa = struct
let immediate = false
let throttle = 100
- let gt_zero = D.gt Q.zero
- let ge_zero = D.ge Q.zero
- let lt_zero = D.lt Q.zero
- let le_zero = D.le Q.zero
+ let gt_zero = Dom_interval.D.gt Q.zero
+ let ge_zero = Dom_interval.D.ge Q.zero
+ let lt_zero = Dom_interval.D.lt 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 =
- match Egraph.get_value del real node with
- | None -> D.reals
- | Some d -> D.singleton d
+ match Egraph.get_value del RealValue.key node with
+ | None -> Dom_interval.D.reals
+ | Some d -> Dom_interval.D.singleton d
let upd del node d d' =
- match D.inter d d' with
+ match Dom_interval.D.inter d d' with
| None ->
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
| Some d' ->
- if not (D.equal d d')
- then set_dom del node d'
+ if not (Dom_interval.D.equal d d')
+ then Dom_interval.set_dom del node d'
let upd_value del node d d' =
- match D.inter d d' with
+ match Dom_interval.D.inter d d' with
| None ->
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
| Some d' ->
- if not (D.equal d d')
- then set_dom del node d'
+ if not (Dom_interval.D.equal d d')
+ then Dom_interval.set_dom del node d'
let propagate del s =
match SE.sem s with
@@ -302,27 +113,27 @@ module DaemonPropa = struct
let cl0 = SE.node s in
let d0 = get_value del cl0 in
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
else
let d1 = get_value del cl1 in
let d2 = get_value del cl2 in
let upd_value node d d' = upd_value del node d d' in
- let qd1 = D.mult_cst q1 d1 in
- let qd2 = D.mult_cst q2 d2 in
- upd_value cl0 d0 (D.add qd1 qd2);
- upd_value cl1 d1 (D.mult_cst (Q.inv q1) (D.minus d0 qd2));
- upd_value cl2 d2 (D.mult_cst (Q.inv q2) (D.minus d0 qd1))
+ let qd1 = Dom_interval.D.mult_cst q1 d1 in
+ let qd2 = Dom_interval.D.mult_cst q2 d2 in
+ upd_value cl0 d0 (Dom_interval.D.add qd1 qd2);
+ upd_value cl1 d1 (Dom_interval.D.mult_cst (Q.inv q1) (Dom_interval.D.minus d0 qd2));
+ upd_value cl2 d2 (Dom_interval.D.mult_cst (Q.inv q2) (Dom_interval.D.minus d0 qd1))
| S.GZero(node,b) -> begin
let cl0 = SE.node s 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_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
Boolean.set_true del cl0
end
- else if D.is_included d dzero_false
+ else if Dom_interval.D.is_included d dzero_false
then
Boolean.set_false del cl0
end
@@ -340,45 +151,32 @@ module DaemonPropa = struct
| S.Add (c1,cl1,c2,cl2) ->
Egraph.register d cl1; Egraph.register d cl2;
Demon.Fast.attach d key
- [Demon.Create.EventValue(SE.node s, real, s);
- Demon.Create.EventValue(cl1, real, s);
- Demon.Create.EventValue(cl2, real, s);
+ [Demon.Create.EventValue(SE.node s, RealValue.key, s);
+ Demon.Create.EventValue(cl1, RealValue.key, s);
+ Demon.Create.EventValue(cl2, RealValue.key, s);
];
let cl = (SE.node s) in
let add acc c cl =
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)
| Some p -> Polynome.x_p_cy acc c p
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,_) ->
Egraph.register d node;
Demon.Fast.attach d key
[Demon.Create.EventValue(SE.node s, Boolean.dom, s);
- Demon.Create.EventValue(node, real, s)]
+ Demon.Create.EventValue(node, RealValue.key, s)]
end;
propagate d s;
end
module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
-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 zero = cst Q.zero
-let one = cst Q.one
+let zero = RealValue.cst Q.zero
+let one = RealValue.cst Q.one
let index s = SE.index s
let add' q1 cl1 q2 cl2 =
@@ -408,7 +206,7 @@ let of_poly p =
| `Some(rq,r) -> `Some(Q.one,SE.node (add' q node rq r))
in
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) -> SE.node (add' rq r c one)
@@ -416,53 +214,6 @@ let to_poly = function
| S.Add(q1,cl1,q2,cl2) -> Polynome.of_list Q.one [cl1,q1;cl2,q2]
| 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 *)
let index x = SE.node (SE.index x)
@@ -508,13 +259,13 @@ let converter d (f:Ground.t) =
match Ground.sem f with
| { app = {builtin = Dolmen_std.Expr.Base; _ }; tyargs = _; args = _; ty }
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 = []; _ } ->
- reg (cst (Q.of_string s))
+ reg (RealValue.cst (Q.of_string s))
| { 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 = []; _ } ->
- reg (cst (Q.of_string_decimal s))
+ reg (RealValue.cst (Q.of_string_decimal s))
| { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
reg (add (of_term a) (of_term b))
| { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
@@ -545,11 +296,11 @@ let th_register env =
(module RealValue)
(fun d value ->
let v = RealValue.value value in
- let s = D.singleton v in
- Egraph.set_dom d dom (RealValue.node value) s;
+ let s = Dom_interval.D.singleton v in
+ Egraph.set_dom d Dom_interval.dom (RealValue.node value) s;
let cl = RealValue.node value in
let p1 = Polynome.of_list v [] in
- Th.solve_one d cl p1
+ Dom_polynome.solve_one d cl p1
) env;
()
@@ -612,3 +363,6 @@ let () =
!<< (Q.geq !>arg1 !>arg2)
| _ -> None
)
+
+
+module RealValue = RealValue
diff --git a/src_colibri2/theories/LRA/LRA.mli b/src_colibri2/theories/LRA/LRA.mli
index b4dabc9d1b5f979182d5f50bc6e5152077772971..268e693d7941e925b64f4c696478813a60a5204c 100644
--- a/src_colibri2/theories/LRA/LRA.mli
+++ b/src_colibri2/theories/LRA/LRA.mli
@@ -18,7 +18,6 @@
(* 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 : 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
val gt: 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
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
new file mode 100644
index 0000000000000000000000000000000000000000..dfa402a5030a302407b2b9286c4c8baa15a7c249
--- /dev/null
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -0,0 +1,93 @@
+(*************************************************************************)
+(* 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
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4083cfc661b3ec14c7799e83cf17c2c24512e3ad
--- /dev/null
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -0,0 +1,181 @@
+(*************************************************************************)
+(* 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
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9e4c64f2cc42a974bb7f99a215f620b1331ceb44
--- /dev/null
+++ b/src_colibri2/theories/LRA/dom_polynome.mli
@@ -0,0 +1,25 @@
+(*************************************************************************)
+(* 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
diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml
index de0ec118be79eeaa851f03804f9ee9a804e06e18..cbb9a2d40bcadac0c6d9da0f467546ec6e4ba619 100644
--- a/src_colibri2/theories/LRA/mul.ml
+++ b/src_colibri2/theories/LRA/mul.ml
@@ -1,9 +1,9 @@
let init,attach =
Demon.Fast.register_get_value_daemon
~name:"Mul.get_value"
- (module LRA.RealValue)
+ (module RealValue)
(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) =
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8d770278d458b1ddee263bd2bc9105bd81c400dc
--- /dev/null
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -0,0 +1,35 @@
+(*************************************************************************)
+(* 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
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0988142fd014c76dc1e498019f27f3f9ea317398
--- /dev/null
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -0,0 +1,24 @@
+(*************************************************************************)
+(* 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