From 3ca38cae1d249eee11e4a514ba1c852a5b30eae8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois@bobot.eu>
Date: Thu, 7 Feb 2013 17:56:41 +0100
Subject: [PATCH] [Solver|Arith] Work but with many hacks problems with the
daemon are registered not delayed but the effect are. They look at only one
place
---
src/arith.ml | 236 +++++++++++++++-------
src/arith.mli | 18 +-
src/inputlang/altergo/popop_of_altergo.ml | 69 +++----
src/solver.ml | 230 +++++++++++++++------
src/solver.mli | 23 ++-
src/uninterp.ml | 18 +-
tests/tests_lib.ml | 10 +-
tests/tests_uf.ml | 4 +-
8 files changed, 411 insertions(+), 197 deletions(-)
diff --git a/src/arith.ml b/src/arith.ml
index cb7c436e8..59945643b 100644
--- a/src/arith.ml
+++ b/src/arith.ml
@@ -19,9 +19,8 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
-
-module E = Egraph_simple
-open Egraph_simple.MTerm
+open Stdlib
+open Solver
let debug = Debug.register_info_flag
~desc:"for the arithmetic theory"
@@ -29,6 +28,8 @@ let debug = Debug.register_info_flag
type t = { cst : Q.t; poly : Q.t Cl.M.t}
+let sem : t sem = create_sem_key ()
+
let cst q = {cst = q; poly = Cl.M.empty}
let monome c x = {cst = Q.zero; poly = Cl.M.singleton x c}
@@ -68,11 +69,10 @@ let x_p_cy p1 c p2 =
m1 m2 in
{cst = f p1.cst p2.cst; poly = poly p1.poly p2.poly}
-module Th = struct
- type repr = t
-
- module Make(X:S with type repr := repr)= struct
- let kind = Other
+module T = struct
+ let key = sem
+ type r = t
+ type t = r
let equal n m = Q.equal n.cst m.cst && Cl.M.equal Q.equal n.poly m.poly
@@ -81,6 +81,18 @@ module Th = struct
Cl.hash k * 101 + Hashtbl.hash v * 107 + acc * 253)
n.poly (Hashtbl.hash n.cst * 27)
+ let compare n m =
+ let c = Q.compare n.cst m.cst in
+ if c <> 0 then c
+ else Cl.M.compare Q.compare n.poly m.poly
+end
+
+module Th = struct
+ include T
+ module M = Map.Make(T)
+ module S = M.Set
+ module H = XHashtbl.Make(T)
+
let print print_cl fmt v =
Format.fprintf fmt "@[";
let print_mono k v fmt =
@@ -90,97 +102,129 @@ module Th = struct
ignore (Cl.M.fold print_mono v.poly fmt);
Format.fprintf fmt "%a@]" Q.pp_print v.cst
- let leaves t = Cl.M.map (fun _ -> ()) t.poly
+ (* let leaves t = Cl.M.map (fun _ -> ()) t.poly *)
- let embed d cl =
- Debug.dprintf debug "[Arith] @[embed cl=%a@]@."
- (UnionFind.print_cl (E.Delayed.hack_env d)) cl;
- match X.extract (E.Delayed.repr d cl) with
+ let embed s cl =
+ match s with
| None -> monome Q.one cl
| Some r -> r
- let add d (v,cl) =
- Cl.S.iter (fun leave ->
- E.Delayed.depend_repr d cl leave) (leaves v)
+ (* let add d (v,cl) = *)
+ (* Cl.S.iter (fun leave -> *)
+ (* E.Delayed.depend_repr d cl leave) (leaves v) *)
- let normalize d x = (** cst = 0 and one empty monome *)
+ let norm x = (** cst = 0 and one empty monome *)
if Q.equal Q.zero x.cst && Cl.M.is_num_elt 1 x.poly then
let cl,k = Cl.M.choose x.poly in
- if Q.equal Q.one k then cl
- else E.Delayed.normalize d (X.make x)
- else E.Delayed.normalize d (X.make x)
-
- let subst d s t =
- let t' = {cst = t.cst; poly = Cl.M.set_diff t.poly s} in
- let t' = Cl.M.fold2_inter
- (fun _ c p poly -> x_p_cy poly c (embed d p))
- t.poly s t' in
- Debug.dprintf debug "[Arith] @[subst t=%a@ t'=%a@]@."
- (X.print (E.Delayed.hack_env d)) t
- (X.print (E.Delayed.hack_env d)) t';
- normalize d t'
-
-
- let solve d (p1,cl1) cl2 =
- let p2 = embed d cl2 in
+ if Q.equal Q.one k then NormalizeTo cl
+ else NormalizeToSem x
+ else NormalizeToSem x
+
+ (* let subst d s t = *)
+ (* let t' = {cst = t.cst; poly = Cl.M.set_diff t.poly s} in *)
+ (* let t' = Cl.M.fold2_inter *)
+ (* (fun _ c p poly -> x_p_cy poly c (embed d p)) *)
+ (* t.poly s t' in *)
+ (* Debug.dprintf debug "[Arith] @[subst t=%a@ t'=%a@]@." *)
+ (* (print Cl.print) t *)
+ (* (print Cl.print) t'; *)
+ (* normalize d t' *)
+
+ let subst_cl p x y =
+ let poly,q = Cl.M.find_remove x p.poly in
+ let poly = Cl.M.change (function
+ | None -> q
+ | Some q' -> none_zero (Q.add (Opt.get q) q')
+ ) y poly in
+ {p with poly}
+
+ let subst_sem p x s =
+ let poly,q = Cl.M.find_remove x p.poly in
+ match q with
+ | None -> p
+ | Some q -> x_p_cy {p with poly} q s
+
+
+ let solve d (p1,cl1) (p2,cl2) =
+ let p2 = embed p2 cl2 in
let p = sub p1 p2 in
if Cl.M.is_empty p.poly
then if Q.equal Q.zero p.cst
- then raise E.SolveSameRepr
- else raise E.Contradiction
+ then raise SolveSameRepr
+ else raise Contradiction
else
let x,q = Cl.M.choose p.poly in
Debug.dprintf debug "[Arith] @[solve p=%a@]@."
- (X.print (E.Delayed.hack_env d)) p;
- let p = {p with poly = Cl.M.remove x p.poly} in
+ (print Cl.print) p;
+ let p' = {p with poly = Cl.M.remove x p.poly} in
assert ( not (Q.equal Q.zero q) );
- let sr = normalize d (mult_cst (Q.inv (Q.neg q)) p) in
- let s = Cl.M.singleton x sr in
- Debug.dprintf debug "[Arith] @[solve q=%a x=%a@, sr=%a@]@."
- Q.pp_print q
- (UnionFind.print_cl (E.Delayed.hack_env d)) x
- (UnionFind.print_cl (E.Delayed.hack_env d)) sr;
- let sp1 = subst d s p1 in
- assert ( let sp2 = subst d s p2 in
- Debug.dprintf debug "[Arith] @[solve sp1=%a@, sp2=%a@]@."
- (UnionFind.print_cl (E.Delayed.hack_env d)) sp1
- (UnionFind.print_cl (E.Delayed.hack_env d)) sp2;
- Cl.equal sp1 sp2 );
- s, sp1
-
- let subst d s t =
- assert (not (Cl.M.is_empty (Cl.M.set_inter t.poly s)));
- subst d s t
- end
+ let sr = norm (mult_cst (Q.inv (Q.neg q)) p') in
+ let sp1 = begin match sr with
+ | NormalizeTo y ->
+ Debug.dprintf debug "[Arith] @[merge q=%a x=%a@, y=%a@]@."
+ Q.pp_print q Cl.print x Cl.print y;
+ Delayed.merge d x y;
+ subst_cl p x y
+ | NormalizeToSem s ->
+ Debug.dprintf debug "[Arith] @[set_sem q=%a x=%a@, s=%a@]@."
+ Q.pp_print q Cl.print x (print Cl.print) s;
+ Delayed.set_sem d sem x s;
+ subst_sem p x s
+ end in
+ (* assert ( let sp2 = subst d s p2 in *)
+ (* Debug.dprintf debug
+ "[Arith] @[solve sp1=%a@, sp2=%a@]@." *)
+ (* Cl.print sp1 Cl.print sp2; *)
+ (* Cl.equal sp1 sp2 ); *)
+ match norm sp1 with
+ | NormalizeTo y -> MergeTo y
+ | NormalizeToSem s -> MergeToSem s
+
+ (* let subst d s t = *)
+ (* assert (not (Cl.M.is_empty (Cl.M.set_inter t.poly s))); *)
+ (* subst d s t *)
+
+ let normalize d t =
+ let t' = Cl.M.fold
+ (fun x _ p ->
+ let x' = Delayed.normalize d x in
+ match Delayed.get_sem d sem x' with
+ | None when Cl.equal x x' -> p
+ | None -> subst_cl p x x'
+ | Some s -> subst_sem p x s)
+ t.poly t in
+ Debug.dprintf debug "[Arith] @[normalize %a@ into %a@]@."
+ (print Cl.print) t
+ (print Cl.print) t';
+ norm t'
+
end
-module M = E.MTerm.Make(Th)
+module E = RegisterSem(Th)
let embed t cl =
- match M.extract (E.repr t cl) with
+ match get_sem t sem cl with
| None -> monome Q.one cl
| Some r -> r
-let basecl t x = (** cst = 0 and one empty monome *)
- if Q.equal Q.zero x.cst && Cl.M.is_num_elt 1 x.poly then
- let cl,k = Cl.M.choose x.poly in
- if Q.equal Q.one k then cl, t
- else E.MTerm.UnionFind.basecl t (M.make x)
- else E.MTerm.UnionFind.basecl t (M.make x)
+let index t x = (** cst = 0 and one empty monome *)
+ match Th.norm x with
+ | NormalizeTo cl -> cl
+ | NormalizeToSem s -> index t sem s
-type env = UnionFind.t
+type env = Solver.t
-let cst t c = basecl t (cst c)
+let cst t c = index t (cst c)
let add t cl1 cl2 =
- basecl t (add (embed t cl1) (embed t cl2))
+ index t (add (embed t cl1) (embed t cl2))
let sub t cl1 cl2 =
- basecl t (sub (embed t cl1) (embed t cl2))
+ index t (sub (embed t cl1) (embed t cl2))
let uninterp_mul env = Uninterp.fun2 env " *"
@@ -189,10 +233,60 @@ let mult t cl1 cl2 =
let m2 = embed t cl2 in
if Cl.M.is_empty m1.poly || Cl.M.is_empty m2.poly then
let cst,m = if Cl.M.is_empty m1.poly then m1.cst, m2 else m2.cst, m1 in
- basecl t (mult_cst cst m)
+ index t (mult_cst cst m)
else
- let f,t = uninterp_mul t in
+ let f = uninterp_mul t in
f t cl1 cl2
let mult_cst t cst cl =
- basecl t (mult_cst cst (embed t cl))
+ index t (mult_cst cst (embed t cl))
+
+
+
+
+ exception SubstNoLeaves
+
+ let rec add_daemon d arg s =
+ Debug.dprintf debug "[Arith] @[if_cl_change %a -> subst %a@]@."
+ Cl.print arg (Th.print Cl.print) s;
+ Delayed.if_cl_change d arg (subst_cl s);
+ Delayed.if_sem_change d arg sem (subst_s s);
+
+ and subst_cl t3 d ~old:t1 t2 =
+ Debug.dprintf debug "[Arith] @[subst_cl %a[%a -> %a]@]@."
+ (Th.print Cl.print) t3 Cl.print t1 Cl.print t2;
+ match (Delayed.is_sem_present d sem t3) with
+ | None -> ()
+ | Some cl3 ->
+ (* let s = Th.subst_cl t3 t1 t2 in *)
+ (* Cl.M.iter (fun k _ -> add_daemon d k s) s.poly; *)
+ (* Delayed.set_sem d sem cl3 s *)
+ match Th.normalize d t3 with
+ | NormalizeTo y -> Delayed.merge d cl3 y
+ | NormalizeToSem s ->
+ Cl.M.iter (fun k _ -> add_daemon d k t3) s.poly;
+ Cl.M.iter (fun k _ -> add_daemon d k s) s.poly;
+ Delayed.set_sem d sem cl3 s
+
+ and subst_s t3 d t1 s =
+ Debug.dprintf debug "[Arith] @[subst_s %a[%a -> %a]@]@."
+ (Th.print Cl.print) t3 Cl.print t1 (Th.print Cl.print) s;
+ match (Delayed.is_sem_present d sem t3) with
+ | None -> ()
+ | Some cl3 ->
+ (* let s = Th.subst_sem t3 t1 s in *)
+ (* Cl.M.iter (fun k _ -> add_daemon d k s) s.poly; *)
+ (* Delayed.set_sem d sem cl3 s *)
+ match Th.normalize d t3 with
+ | NormalizeTo y -> Delayed.merge d cl3 y
+ | NormalizeToSem s ->
+ (** Daemon are immediately added but set_sem is delayed ... *)
+ Cl.M.iter (fun k _ -> add_daemon d k t3) s.poly; (* big hack *)
+ Cl.M.iter (fun k _ -> add_daemon d k s) s.poly;
+ Delayed.set_sem d sem cl3 s
+
+
+ let propagate env =
+ Solver.if_propagate_sem env sem
+ ( fun d cl s ->
+ Cl.M.iter (fun k _ -> add_daemon d k s) s.poly)
diff --git a/src/arith.mli b/src/arith.mli
index 64d906d96..c582f3395 100644
--- a/src/arith.mli
+++ b/src/arith.mli
@@ -19,19 +19,19 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+open Solver
-open Term
+type env = Solver.t
-open Egraph_simple
-open MTerm
+type t
-type env = UnionFind.t
+val cst : env -> Q.t -> Cl.t
+val add : env -> Cl.t -> Cl.t -> Cl.t
+val sub : env -> Cl.t -> Cl.t -> Cl.t
-val cst : env -> Q.t -> cl * env
-val add : env -> cl -> cl -> cl * env
-val sub : env -> cl -> cl -> cl * env
+val mult_cst : env -> Q.t -> Cl.t -> Cl.t
-val mult_cst : env -> Q.t -> cl -> cl * env
+val mult : env -> Cl.t -> Cl.t -> Cl.t
-val mult : env -> cl -> cl -> cl * env
+val propagate : env -> unit
diff --git a/src/inputlang/altergo/popop_of_altergo.ml b/src/inputlang/altergo/popop_of_altergo.ml
index f3716921c..34881e1c0 100644
--- a/src/inputlang/altergo/popop_of_altergo.ml
+++ b/src/inputlang/altergo/popop_of_altergo.ml
@@ -29,17 +29,16 @@ let rec add_lexpr_term env t =
match t.pp_desc with
| PPvar s -> Uninterp.cst env s
| PPapp (s,l) ->
- let f,env = Uninterp.cst env s in
- let env,l = Lists.map_fold_left
- (fun env e -> let e,env = add_lexpr_term env e in env,e) env l in
+ let f = Uninterp.cst env s in
+ let l = List.map (fun e -> add_lexpr_term env e) l in
Uninterp.appl env f l
| PPconst (ConstInt s) ->
Arith.cst env (Q.of_string s)
| PPconst (ConstReal q) ->
Arith.cst env q
| PPinfix (t1,op,t2) ->
- let cl1,env = add_lexpr_term env t1 in
- let cl2,env = add_lexpr_term env t2 in
+ let cl1 = add_lexpr_term env t1 in
+ let cl2 = add_lexpr_term env t2 in
let op = match op with
| PPadd -> Arith.add
| PPsub -> Arith.sub
@@ -47,7 +46,7 @@ let rec add_lexpr_term env t =
| _ -> raise (Not_supported (Loc.extract t.pp_loc)) in
op env cl1 cl2
| PPprefix (PPneg,e) ->
- let cl1, env = add_lexpr_term env e in
+ let cl1 = add_lexpr_term env e in
Arith.mult_cst env (Q.of_int (-1)) cl1
| _ -> raise (Not_supported (Loc.extract t.pp_loc))
@@ -56,50 +55,45 @@ let uninterp_true env = Uninterp.cst env " true"
let rec add_lexpr_axiom _true env t =
match t.pp_desc with
| PPapp (s,l) ->
- let f,env = Uninterp.cst env s in
- let env,l = Lists.map_fold_left
- (fun env e -> let e,env = add_lexpr_term env e in env,e) env l in
- let cl,env = Uninterp.appl env f l in
- let cl,env = Egraph_simple.add env cl in
- let env = Egraph_simple.equal env cl _true in
- env
+ let f = Uninterp.cst env s in
+ let l = List.map (fun e -> add_lexpr_term env e) l in
+ let cl = Uninterp.appl env f l in
+ let cl = Solver.propagate env cl in
+ Solver.merge env cl _true
| PPinfix (t1,PPand,t2) ->
- let env = add_lexpr_axiom _true env t1 in
- let env = add_lexpr_axiom _true env t2 in
- env
+ add_lexpr_axiom _true env t1;
+ add_lexpr_axiom _true env t2
| PPinfix (t1,PPeq,t2) ->
- let cl1,env = add_lexpr_term env t1 in
- let cl1,env = Egraph_simple.add env cl1 in
- let cl2,env = add_lexpr_term env t2 in
- let cl2,env = Egraph_simple.add env cl2 in
- let env = Egraph_simple.equal env cl1 cl2 in
- env
+ let cl1 = add_lexpr_term env t1 in
+ let cl1 = Solver.propagate env cl1 in
+ let cl2 = add_lexpr_term env t2 in
+ let cl2 = Solver.propagate env cl2 in
+ Solver.merge env cl1 cl2
| _ -> raise (Not_supported (Loc.extract t.pp_loc))
let rec add_lexpr_goal _true env t =
match t.pp_desc with
| PPapp (s,l) ->
- let f,env = Uninterp.cst env s in
- let env,l = Lists.map_fold_left
- (fun env e -> let e,env = add_lexpr_term env e in env,e) env l in
- let cl,env = Uninterp.appl env f l in
- let cl,env = Egraph_simple.add env cl in
- Egraph_simple.is_equal env cl _true
+ let f = Uninterp.cst env s in
+ let l = List.map (fun e -> add_lexpr_term env e) l in
+ let cl = Uninterp.appl env f l in
+ let cl = Solver.propagate env cl in
+ Solver.is_equal env cl _true
| PPinfix (t1,PPand,t2) ->
let b1 = add_lexpr_goal _true env t1 in
let b2 = add_lexpr_goal _true env t2 in
b1 && b2
| PPinfix (t1,PPimplies,t2) ->
- let env = add_lexpr_axiom _true env t1 in
+ add_lexpr_axiom _true env t1;
let b2 = add_lexpr_goal _true env t2 in
b2
| PPinfix (t1,PPeq,t2) ->
- let cl1,env = add_lexpr_term env t1 in
- let cl1,env = Egraph_simple.add env cl1 in
- let cl2,env = add_lexpr_term env t2 in
- let cl2,env = Egraph_simple.add env cl2 in
- Egraph_simple.is_equal env cl1 cl2
+ let cl1 = add_lexpr_term env t1 in
+ let cl1 = Solver.propagate env cl1 in
+ let cl2 = add_lexpr_term env t2 in
+ let cl2 = Solver.propagate env cl2 in
+ Solver.is_equal env cl1 cl2
| PPforall (_,_,_,e) | PPforall_named (_,_,_,e) -> add_lexpr_goal _true env e
| _ -> raise (Not_supported (Loc.extract t.pp_loc))
@@ -107,12 +101,15 @@ let rec add_lexpr_goal _true env t =
let rec add_decl _true env = function
| [] -> raise (Not_supported Loc.dummy_position)
- | Axiom(_,_,_,e)::l -> add_decl _true (add_lexpr_axiom _true env e) l
+ | Axiom(_,_,_,e)::l -> add_lexpr_axiom _true env e; add_decl _true env l
| Goal(_,_,e)::_ -> add_lexpr_goal _true env e
| _::l -> add_decl _true env l
let check_goal l =
- let _true,env = uninterp_true Egraph_simple.MTerm.UnionFind.empty in
+ let env = Solver.new_t () in
+ Uninterp.propagate env;
+ Arith.propagate env;
+ let _true = uninterp_true env in
add_decl _true env l
let loc lb = Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
diff --git a/src/solver.ml b/src/solver.ml
index 51c4cc95f..b9d2f8cd1 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -29,6 +29,8 @@ let debug = Debug.register_info_flag
exception BrokenInvariant of string
exception Impossible
+exception Contradiction
+exception SolveSameRepr
module Cl : sig include Datatype val create_cl : unit -> t end = struct
include DInt
@@ -51,6 +53,16 @@ module type Dom' = sig
val key: t dom
end
+type 'a solveResult =
+| NoMerge (** There is no representative for this solve (but not unsat) *)
+| MergeTo of Cl.t
+| MergeToSem of 'a
+
+type 'a normalizeResult =
+| NormalizeTo of Cl.t
+| NormalizeToSem of 'a
+
+
module type Sem' = sig
type delayed
include OrderedHashedType
@@ -60,13 +72,13 @@ module type Sem' = sig
val print: (Format.formatter -> Cl.t -> unit) ->
Format.formatter -> t -> unit
- val normalize: delayed -> t -> Cl.t
- val solve: delayed -> t * Cl.t -> t option * Cl.t -> Cl.t option
+ val normalize: delayed -> t -> t normalizeResult
+ val solve: delayed -> t * Cl.t -> t option * Cl.t -> t solveResult
val key: t sem
end
type ('delayed,'a) dsem_event =
- { dcallback: ('delayed -> Cl.t -> old:'a -> 'a -> unit) }
+ { dcallback: ('delayed -> Cl.t -> 'a -> unit) }
type ('delayed,'a) propa_event =
{ pcallback: ('delayed -> Cl.t -> 'a -> unit) }
@@ -191,6 +203,11 @@ let get_sem : 'a sem -> (module Sem with type t = 'a) = fun k ->
(Obj.magic (sem : (module Sem)) : (module Sem with type t = 'a))
+let print_s (type a) (k : a sem) fmt s =
+ let sem = get_sem k in
+ let module S = (val sem : Sem with type t = a) in
+ S.print Cl.print fmt s
+
module type DomTable = DomTable' with type delayed = delayed_t
module type SemTable = SemTable' with type delayed = delayed_t
@@ -281,6 +298,59 @@ let get_table_sem : t -> 'a sem -> (module SemTable with type dt = 'a)
Cl.M.find_opt cl SemTable.table
+(** {2 For debugging and display} *)
+
+let output_graph filename t =
+ let open Graph in
+ let module G = struct
+ include Imperative.Digraph.Concrete(Cl)
+ let graph_attributes _ = []
+ let default_vertex_attributes _ = [`Shape `Record]
+ let vertex_name cl = string_of_int (Cl.hash cl)
+
+ let print fmt cl =
+ let iter fmt sem =
+ let module Sem =
+ (val sem : SemTable' with type delayed = delayed_t) in
+ try
+ let s = Cl.M.find cl Sem.table in
+ Sem.S.print Cl.print fmt s;
+ let cl' = Sem.S.M.find s Sem.invtable in
+ if Cl.equal cl cl' then Format.pp_print_string fmt "*";
+ with Not_found -> ()
+ in
+ Format.fprintf fmt "{%a | %a}"
+ Cl.print cl
+ (Pp.print_iter1 Simple_vector.iter_initialized
+ (Pp.constant_string " | ") iter) t.sem
+
+ let vertex_attributes cl =
+ let label = Pp.string_of_wnl print cl in
+ [`Label label]
+ let default_edge_attributes _ = []
+ let edge_attributes _ = []
+ let get_subgraph _ = None
+ end in
+ let g = G.create () in
+ Cl.M.iter (fun cl1 cl2 -> G.add_edge g cl1 cl2) t.repr;
+ let cout = open_out filename in
+ let module Dot = Graphviz.Dot(G) in
+ Dot.output_graph cout g
+
+let show_graph = Debug.register_flag
+ ~desc:"Show each step in a gui"
+ "dotgui"
+
+let draw_graph =
+ let c = ref 0 in
+ fun t ->
+ if Debug.test_flag show_graph then
+ let filename = Format.sprintf "debug_graph%i.dot" !c in
+ incr c;
+ Debug.dprintf show_graph "[DotGui] output dot file: %s@." filename;
+ output_graph filename t
+
+
(** {2 Delayed} *)
module Delayed = struct
@@ -297,11 +367,15 @@ module Delayed = struct
let is_normalized t cl = Cl.M.mem cl t.env.repr
let add_pending_merge (t : t) cl cl' =
+ Debug.dprintf debug "[Solver] @[add_pending_merge for %a and %a@]@."
+ Cl.print cl Cl.print cl';
assert (is_normalized t cl);
assert (is_normalized t cl');
Queue.add (Merge (cl,cl')) t.todo
- let add_pending_set_sem (type a) (t : t) (sem : 'a sem) cl (v:'a) =
+ let add_pending_set_sem (type a) (t : t) (sem : a sem) cl (v:a) =
+ Debug.dprintf debug "[Solver] @[add_pending_set_sem for %a and %a@]@."
+ Cl.print cl (print_s sem) v;
assert (is_normalized t cl);
Queue.add (SetSem (sem,cl,v)) t.todo
@@ -322,31 +396,46 @@ module Delayed = struct
(val sem : SemTable' with type delayed = delayed_t) in
try
let s = Cl.M.find cl Sem.table in
- let cl' = Sem.S.normalize t s in
- if Cl.equal cl' cl
- then (* TODO: right place? *)
+ match Sem.S.normalize t s with
+ | NormalizeTo cl' when Cl.equal cl' cl -> (* TODO: right place? *)
+ List.iter (fun {pcallback = f} -> f t cl s) Sem.propagate
+ | NormalizeTo cl' -> add_pending_merge t cl cl';
+ List.iter (fun {pcallback = f} -> f t cl s) Sem.propagate
+ | NormalizeToSem s' when Sem.S.equal s' s ->
List.iter (fun {pcallback = f} -> f t cl s) Sem.propagate
- else add_pending_merge t cl cl'
+ | NormalizeToSem s' -> add_pending_set_sem t Sem.S.key cl s';
+ List.iter (fun {pcallback = f} -> f t cl s') Sem.propagate
with Not_found -> ()
in
Simple_vector.iter_initialized iter t.env.sem;
- Cl.M.find_exn Impossible cl t.env.repr
+ let cl' = Cl.M.find_exn Impossible cl t.env.repr in
+ Debug.dprintf debug "[Solver] normalize %a to %a@."
+ Cl.print cl Cl.print cl';
+ cl'
+
+ let run_sem_event t events cl v =
+ match events with
+ | None -> ()
+ | Some events ->
+ List.iter (fun {dcallback = f} -> f t cl v) events
+
let set_sem_pending (type a) t (sem : a sem) cl v =
let module SemTable =
(val (get_table_sem t.env sem) : SemTable with type dt = a) in
let cl' = SemTable.S.M.find_opt v SemTable.invtable in
+ let new_event, events = Cl.M.find_remove cl SemTable.event in
let module SemTable' : SemTable' with type delayed = delayed_t = struct
(** remove the old semantical value
replace it by the new one *)
include SemTable
- let table =
- let n = Cl.M.remove cl SemTable.table in
- if cl' = None then Cl.M.add cl v SemTable.table else n
+ let table = Cl.M.add cl v SemTable.table
let invtable =
if cl' = None then SemTable.S.M.add v cl invtable else invtable
+ let event = new_event
end in
Simple_vector.set t.env.sem sem (module SemTable');
+ if cl' = None then run_sem_event t events cl v;
match cl' with
| None -> ()
| Some cl' ->
@@ -366,35 +455,41 @@ module Delayed = struct
let choose_repr cl1 cl2 =
(Shuffle.shufflep (cl1,cl2))
- let merge_sem t cl1 cl2 repr_cl =
+ let merge_sem t cl1 cl2 other_cl repr_cl =
assert (Cl.equal repr_cl cl1 || Cl.equal repr_cl cl2);
let iter sem =
let module Sem =
(val sem : SemTable' with type delayed = delayed_t) in
let s1 = Cl.M.find_opt cl1 Sem.table in
let s2 = Cl.M.find_opt cl2 Sem.table in
+ Debug.dprintf debug "[Solver] @[merge sem (%a,%a)@ and (%a,%a)@]@."
+ Cl.print cl1 (Pp.print_option (Sem.S.print Cl.print)) s1
+ Cl.print cl2 (Pp.print_option (Sem.S.print Cl.print)) s2;
begin
match s1,cl1,s2,cl2 with
| Some s1, _ , Some s2, _ when Sem.S.equal s1 s2 ->
let module SemTable' :
SemTable' with type delayed = delayed_t = struct
- (** remove the old semantical value
- replace it by the new one *)
+ (** put the semantical value for the new representative class *)
include Sem
- let table = Cl.M.remove cl1 table
+ let table = Cl.M.remove cl1 table
let table = Cl.M.remove cl2 table
let table = Cl.M.add repr_cl s1 table
+ let cl_inv = Sem.S.M.find_exn Impossible s1 invtable
+ let invtable = if Cl.equal cl_inv other_cl then
+ Sem.S.M.add s1 repr_cl invtable else invtable
end in
Simple_vector.set t.env.sem Sem.S.key (module SemTable')
| None, _, None, _ -> ()
| Some s, cl, None, cl' | None, cl', Some s, cl -> begin
let clr = Sem.S.solve t (s,cl) (None,cl') in
match clr with
- | None -> (** The semantic value stays where it is *) ()
- | Some clr ->
+ | NoMerge -> (** The semantic value stays where it is *) ()
+ | MergeTo clr ->
let r = Cl.M.find_opt clr Sem.table in
(** We remove cl -> s but we keep s -> cl (if s<>r otherwise
its s -> repr_cl) *)
+ let new_event, events = Cl.M.find_remove cl Sem.event in
let module SemTable' :
SemTable' with type delayed = delayed_t = struct
(** remove the old semantical value
@@ -402,16 +497,30 @@ module Delayed = struct
include Sem
let table = Cl.M.remove cl table
let table = Cl.M.add_opt repr_cl r table
+ let event = new_event
end in
Simple_vector.set t.env.sem Sem.S.key (module SemTable');
+ Opt.iter (run_sem_event t events repr_cl) r;
add_pending_merge t repr_cl clr
+ | MergeToSem r ->
+ let module SemTable' :
+ SemTable' with type delayed = delayed_t = struct
+ (** remove the old semantical value
+ replace it by the new one *)
+ include Sem
+ let table = Cl.M.remove cl table
+ let table = Cl.M.add repr_cl r table
+ end in
+ Simple_vector.set t.env.sem Sem.S.key (module SemTable');
+ add_pending_set_sem t Sem.S.key repr_cl r
end
| Some s,cl, s', cl' ->
let clr = Sem.S.solve t (s,cl) (s',cl') in
match clr with
- | None -> (** The semantic values stay where they are *) ()
- | Some clr ->
+ | NoMerge -> (** The semantic values stay where they are *) ()
+ | MergeTo clr ->
let r = Cl.M.find_opt clr Sem.table in
+ let new_event, events = Cl.M.find_remove cl Sem.event in
let module SemTable' :
SemTable' with type delayed = delayed_t = struct
(** remove the old semantical value
@@ -422,11 +531,24 @@ module Delayed = struct
let table = Cl.M.add_opt repr_cl r table
end in
Simple_vector.set t.env.sem Sem.S.key (module SemTable');
+ Opt.iter (run_sem_event t events repr_cl) r;
add_pending_merge t repr_cl clr
+ | MergeToSem r ->
+ let module SemTable' :
+ SemTable' with type delayed = delayed_t = struct
+ (** remove the old semantical value
+ replace it by the new one *)
+ include Sem
+ let table = Cl.M.remove cl table
+ let table = Cl.M.remove cl' table
+ let table = Cl.M.add repr_cl r table
+ end in
+ Simple_vector.set t.env.sem Sem.S.key (module SemTable');
+ add_pending_set_sem t Sem.S.key repr_cl r
end in
Simple_vector.iter_initialized iter t.env.sem
- let merge_dom t cl1 cl2 repr_cl = () (* TODO *)
+ let merge_dom t cl1 cl2 other_cl repr_cl = () (* TODO *)
(** merge two pending actions *)
let merge_pending t cl1 cl2 =
@@ -436,8 +558,8 @@ module Delayed = struct
assert (is_repr t cl1);
assert (is_repr t cl2);
let other_cl, repr_cl = choose_repr cl1 cl2 in
- merge_sem t cl1 cl2 repr_cl;
- merge_dom t cl1 cl2 repr_cl;
+ merge_sem t cl1 cl2 other_cl repr_cl;
+ merge_dom t cl1 cl2 other_cl repr_cl;
t.env.repr <- Cl.M.add other_cl repr_cl t.env.repr;
(** wakeup the daemons *)
let event, other_event = Cl.M.find_remove other_cl t.env.event in
@@ -458,6 +580,7 @@ module Delayed = struct
let set_dom t = assert false
let rec do_pending t =
+ draw_graph t.env;
if Queue.is_empty t.todo
then Debug.dprintf debug "[Solver] @[do_pending Nothing@]@."
else begin
@@ -467,8 +590,8 @@ module Delayed = struct
Cl.print cl1 Cl.print cl2;
merge_pending t cl1 cl2
| SetSem (sem,cl,v) ->
- Debug.dprintf debug "[Solver] @[do_pending SetSem %a@]@."
- Cl.print cl;
+ Debug.dprintf debug "[Solver] @[do_pending SetSem %a %a@]@."
+ Cl.print cl (print_s sem) v;
set_sem_pending t sem cl v
end;
do_pending t
@@ -479,18 +602,34 @@ module Delayed = struct
t.env.event <- Cl.M.add cl events t.env.event
let if_dom_change t cl dom f = assert false
- let if_sem_change t cl sem f = assert false
+ let if_sem_change (type a) t cl (sem : a sem) f =
+ let module SemTable =
+ (val (get_table_sem t.env sem) : SemTable with type dt = a) in
+ let module SemTable' : SemTable' with type delayed = delayed_t = struct
+ (** remove the old semantical value
+ replace it by the new one *)
+ include SemTable
+ let event = Cl.M.change (function
+ | None -> Some [{dcallback = f}]
+ | Some l -> Some ({dcallback = f}::l)) cl event
+ end in
+ Simple_vector.set t.env.sem sem (module SemTable')
let if_propagate_sem t sem f = if_propagate_sem t.env sem f
end
+
let propagate t cl =
+ draw_graph t;
+ Debug.dprintf debug "[Solver] @[propagate %a@]@."
+ Cl.print cl;
let delayed = delayed_of_t t in
let cl = Delayed.normalize delayed cl in
Delayed.do_pending delayed;
Cl.M.find_exn Impossible cl t.repr
let merge t cl1 cl2 =
+ draw_graph t;
let cl1,cl2 = Shuffle.shufflep (cl1,cl2) in
Debug.dprintf debug "[Solver] @[merge %a %a@]@."
Cl.print cl1 Cl.print cl2;
@@ -502,6 +641,7 @@ let merge t cl1 cl2 =
let is_equal t cl1 cl2 =
+ draw_graph t;
let cl1,cl2 = Shuffle.shufflep (cl1,cl2) in
Debug.dprintf debug "[Solver] @[is_equal %a %a@]@."
Cl.print cl1 Cl.print cl2;
@@ -512,41 +652,3 @@ let is_equal t cl1 cl2 =
-(** {2 For debugging and display} *)
-
-let output_graph filename t =
- let open Graph in
- let module G = struct
- include Imperative.Digraph.Concrete(Cl)
- let graph_attributes _ = []
- let default_vertex_attributes _ = [`Shape `Record]
- let vertex_name cl = string_of_int (Cl.hash cl)
-
- let print fmt cl =
- let iter fmt sem =
- let module Sem =
- (val sem : SemTable' with type delayed = delayed_t) in
- try
- let s = Cl.M.find cl Sem.table in
- Sem.S.print Cl.print fmt s;
- let cl' = Sem.S.M.find s Sem.invtable in
- if Cl.equal cl cl' then Format.pp_print_string fmt "*";
- with Not_found -> ()
- in
- Format.fprintf fmt "{%a | {%a}}"
- Cl.print cl
- (Pp.print_iter1 Simple_vector.iter_initialized
- (Pp.constant_string "| ") iter) t.sem
-
- let vertex_attributes cl =
- let label = Pp.string_of_wnl print cl in
- [`Label label]
- let default_edge_attributes _ = []
- let edge_attributes _ = []
- let get_subgraph _ = None
- end in
- let g = G.create () in
- Cl.M.iter (fun cl1 cl2 -> G.add_edge g cl1 cl2) t.repr;
- let cout = open_out filename in
- let module Dot = Graphviz.Dot(G) in
- Dot.output_graph cout g
diff --git a/src/solver.mli b/src/solver.mli
index 8b3905dc9..5505a8101 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -24,6 +24,9 @@ open Stdlib
(** {2 Types } *)
+exception SolveSameRepr
+exception Contradiction
+
(** Classes *)
module Cl : Datatype
@@ -33,7 +36,6 @@ type 'a sem
type 'a dom
(** key of a domain of type 'a *)
-
module Delayed : sig
type t
(** Immediate information *)
@@ -55,10 +57,10 @@ module Delayed : sig
(t -> old:Cl.t -> Cl.t -> unit) -> unit
val if_dom_change :
t -> Cl.t -> 'a dom ->
- (t -> Cl.t -> old:'a -> 'a -> unit) -> unit
+ (t -> Cl.t -> 'a -> unit) -> unit
val if_sem_change :
t -> Cl.t -> 'a sem ->
- (t -> Cl.t -> old:'a -> 'a -> unit) -> unit
+ (t -> Cl.t -> 'a -> unit) -> unit
val if_propagate_sem :
t -> 'a sem ->
(t -> Cl.t -> 'a -> unit) -> unit
@@ -82,6 +84,16 @@ end
module RegisterDom (D:Dom) : sig end
+
+type 'a solveResult =
+| NoMerge (** There is no representative for this solve (but not unsat) *)
+| MergeTo of Cl.t
+| MergeToSem of 'a
+
+type 'a normalizeResult =
+| NormalizeTo of Cl.t
+| NormalizeToSem of 'a
+
module type Sem = sig
include OrderedHashedType
module M : Map.S with type key = t
@@ -90,8 +102,8 @@ module type Sem = sig
val print: (Format.formatter -> Cl.t -> unit) ->
Format.formatter -> t -> unit
- val normalize: Delayed.t -> t -> Cl.t
- val solve: Delayed.t -> t * Cl.t -> t option * Cl.t -> Cl.t option
+ val normalize: Delayed.t -> t -> t normalizeResult
+ val solve: Delayed.t -> t * Cl.t -> t option * Cl.t -> t solveResult
val key: t sem
end
@@ -105,6 +117,7 @@ val index : t -> 'a sem -> 'a -> Cl.t
val propagate: t -> Cl.t -> Cl.t
val merge : t -> Cl.t -> Cl.t -> unit
val is_equal : t -> Cl.t -> Cl.t -> bool
+val get_sem : t -> 'a sem -> Cl.t -> 'a option
val if_propagate_sem :
t -> 'a sem ->
(Delayed.t -> Cl.t -> 'a -> unit) -> unit
diff --git a/src/uninterp.ml b/src/uninterp.ml
index 23486db86..d810e9b48 100644
--- a/src/uninterp.ml
+++ b/src/uninterp.ml
@@ -30,7 +30,7 @@ type t =
| Cst of Strings.Hashcons.t
| App of Cl.t * Cl.t
-let sem = create_sem_key ()
+let sem : t sem = create_sem_key ()
module T = struct
type r = t
@@ -81,15 +81,20 @@ module Th = struct
let add d _ = ()
(* No more classes to merge than the two given class themselves *)
- let solve _d _ _ = None
+ let solve _d _ _ = NoMerge
let norm d s =
Delayed.normalize d (Delayed.index d sem s)
let normalize d s =
match s with
- | Cst _ -> norm d s
- | App(f,g) -> norm d (App(Delayed.normalize d f, Delayed.normalize d g))
+ | Cst _ ->
+ NormalizeToSem s
+ | App(f,g) ->
+ let s' = (App(Delayed.normalize d f, Delayed.normalize d g)) in
+ Debug.dprintf debug "[Uninterp] @[normalize %a to %a@]@."
+ (print Cl.print) s (print Cl.print) s';
+ NormalizeToSem s'
end
module Registered = RegisterSem(Th)
@@ -134,6 +139,9 @@ module Registered = RegisterSem(Th)
Delayed.if_cl_change d arg (subst s)
and subst t3 d ~old:t1 t2 =
+ Debug.dprintf debug "[Uninterp] @[subst %a[%a -> %a]@]@."
+ (Th.print Cl.print) t3 Cl.print t1 Cl.print t2;
+
Debug.dprintf debug "[Uninterp] @[subst %a[%a -> %a]@]@."
(Th.print Cl.print) t3 Cl.print t1 Cl.print t2;
match (Delayed.is_sem_present d sem t3), t3 with
@@ -143,7 +151,7 @@ module Registered = RegisterSem(Th)
assert (
if not ( Cl.equal t1 f || Cl.equal t1 g) then raise SubstNoLeaves
else true);
- let replace arg = if Cl.equal arg t1 then t2 else arg in
+ let replace arg = Delayed.normalize d arg in
let f = replace f in
let g = replace g in
let s = App (f,g) in
diff --git a/tests/tests_lib.ml b/tests/tests_lib.ml
index be92fa9d9..48a62c2a2 100644
--- a/tests/tests_lib.ml
+++ b/tests/tests_lib.ml
@@ -11,13 +11,13 @@ let test_split s =
s >::: begin
let l = Popop_of_altergo.read_split s in
List.map (fun (res,loc,d) ->
- (Pp.string_of Loc.gen_report_position loc) >::
- fun () ->
+ TestCase (fun () ->
+ let s = Pp.string_of_wnl Loc.gen_report_position loc in
let b = (Popop_of_altergo.check_goal d) in
match res with
- | "Valid" -> assert_bool "" b
- | "Unknown" -> assert_bool "" (not b)
- | _ -> invalid_arg "Unknown status"
+ | "Valid" -> assert_bool s b
+ | "Unknown" -> assert_bool s (not b)
+ | _ -> invalid_arg "Unknown status")
) l
end
diff --git a/tests/tests_uf.ml b/tests/tests_uf.ml
index ad37332d3..0ce690149 100644
--- a/tests/tests_uf.ml
+++ b/tests/tests_uf.ml
@@ -185,10 +185,10 @@ let altergo = "altergo tests" >::: [altergo1; altergo2]
let files = ["tests/tests_altergo_qualif.split"]
-(* let altergo2 = TestList (List.map Tests_lib.test_split files) *)
+let altergo2 = TestList (List.map Tests_lib.test_split files)
-let tests = TestList [basic;congru1;congru2;altergo;(* altergo2 *)]
+let tests = TestList [basic;congru1;congru2;altergo;altergo2]
end
--
GitLab