From 6af6d2113afeb383b4b1b1c088413e97896c43d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 2 Jan 2014 11:28:45 +0100
Subject: [PATCH] clsem in place remains to remove invtable
---
Makefile | 2 +-
src/arith.ml | 47 ++--
src/arith.mli | 1 -
src/bool.ml | 65 ++---
src/bool.mli | 6 -
src/conflict.ml | 51 +---
src/conflict.mli | 9 +-
src/demon.ml | 1 +
src/equality.ml | 146 ++---------
src/equality.mli | 13 -
src/explanation.ml | 10 -
src/explanation.mli | 11 -
src/inputlang/altergo/popop_of_altergo.mli | 2 -
src/solver.ml | 279 ++++++++-------------
src/solver.mli | 16 +-
src/types.ml | 200 +++++++++++++--
src/types.mli | 74 ++++--
src/uninterp.ml | 50 ++--
src/util/hashcons.ml | 85 ++++++-
src/util/hashcons.mli | 29 ++-
src/util/strings.ml | 38 +--
src/util/strings.mli | 2 +
src/util/util.ml | 3 +
src/util/util.mli | 3 +
src/variable.ml | 4 +-
src/variable.mli | 1 -
26 files changed, 588 insertions(+), 560 deletions(-)
diff --git a/Makefile b/Makefile
index 45201d9d0..e23354964 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,7 @@
PACKAGES=oUnit zarith ocamlgraph cryptokit #-package lablgtk2
# I don't understand warning 18
-OPTIONS=-tag annot -no-sanitize -tag debug -use-ocamlfind -cflags -w,+a-4-9-18-41-44-40 -cflags -warn-error,+5+10+8+12+20+11 -cflag -bin-annot -j 8
+OPTIONS=-tag annot -no-sanitize -tag debug -use-ocamlfind -cflags -w,+a-4-9-18-41-44-40-45-42 -cflags -warn-error,+5+10+8+12+20+11 -cflag -bin-annot -j 8
#OPTIONS += -cflags -warn-error,+a
DIRECTORIES=src src/util src/inputlang/altergo src/inputlang/dimacs_cnf src/inputlang/smtlib2 tests src/cmd fuzz
OCAMLBUILD=ocamlbuild \
diff --git a/src/arith.ml b/src/arith.ml
index 0bf1ca2dd..8e765e439 100644
--- a/src/arith.ml
+++ b/src/arith.ml
@@ -596,7 +596,7 @@ module P = struct
let x_p_cy = x_p_cy
end
-module E = RegisterSem(Th)
+module ThE = RegisterSem(Th)
module D = RegisterDom(struct include Th let key = dom end)
let embed t cl =
@@ -615,7 +615,7 @@ module DaemonPropa = struct
let immediate = true
let wakeup d v ev =
- match Delayed.get_cl_sem d sem v with
+ match Delayed.get_cl_sem d sem v real with
| None -> assert false
| Some own ->
match Delayed.get_dom d dom own with
@@ -789,7 +789,7 @@ module DaemonMultPropa = struct
let immediate = false
let wakeup d v _ev =
- match Delayed.get_cl_sem d mul_sem v with
+ match Delayed.get_cl_sem d mul_sem v real with
| None -> assert false
| Some own ->
Debug.dprintf4 debug "[Uninterp] @[wakeup own %a v:%a@]@\n"
@@ -852,7 +852,7 @@ end
module RDaemonMultInit = Demon.Key.Register(DaemonMultInit)
-let zero = Cl.create "0" real
+let zero = ThE.cl (ThE.index poly_zero real)
let propagate env =
RDaemonPropa.init env;
@@ -864,8 +864,6 @@ let propagate env =
Demon.Key.attach env
DaemonMultInit.key () [Demon.Create.EventPropaSem(mul_sem,())];
Delayed.propagate env zero;
- Delayed.set_sem env Explanation.pexpfact
- sem zero poly_zero;
Delayed.set_dom env (Solver.Delayed.mk_pexp env Explanation.expfact ())
dom zero poly_zero
@@ -995,7 +993,6 @@ module GenEquality = struct
(* let p,deps = get_rlist_conpoly_deps t cl r1 deps in *)
(* assert (is_zero p.exp); *)
(* Explanation.Deps.add_unknown_con deps conpoly p); *)
- sem = get_sem;
dodec = true (** TODO *);
}
@@ -1034,7 +1031,8 @@ module ConPoly = struct
let _,vn = Th.normalize d v in
if not (Cl.M.is_empty vn.poly)
then
- let c = (Equality.Sem(sem,v,zero,false)) in
+ let cl = ThE.cl (ThE.index v real) in
+ let c = Equality.Eq(cl,zero,false) in
f.fold_decisions acc Equality.choequal c ()
else acc) acc v
method conflict_add d =
@@ -1076,10 +1074,16 @@ module ConPoly = struct
else Some (new finalized s)
- let same_sem t age _sem (_,pexp2) pexp1 cl1 cl2 =
+ let same_sem (type a) t age (sem':a sem) (v:a) pexp1 cl1 cl2 =
+ let r2 =
+ match Sem.Eq.eq_type sem sem' with
+ | None -> raise Impossible (* understand why that happend *)
+ | Some Eqtype.Eq ->
+ let p2 = x_p_cy (monome Q.one cl2) Q.minus_one v in
+ Some {imp = p2; exp = p2}
+ in
let r1 = get_pexp_conpoly t pexp1 in
- let r2 = get_pexp_conpoly t pexp2 in
- let p = match r1, r2 with
+ let p = match r1,r2 with
| Some p1, Some p2 ->
x_p_cy_conpoly p2 Q.minus_one p1
| _ -> dist_conpoly cl1 cl2 in
@@ -1094,17 +1098,6 @@ module ConPoly = struct
then GRequested (dist_conpoly cl rcl)
else GRequested {imp = poly_zero; exp = dist cl rcl}
- let propasem :
- type a. ComputeConflict.t -> age -> a sem -> a -> Cl.t -> t rescon =
- fun t age sem' v cl ->
- match Sem.Eq.eq_type sem sem' with
- | None -> raise Impossible
- | Some Eqtype.Eq ->
- let p = x_p_cy (monome Q.one cl) Q.minus_one v in
- if ComputeConflict.before_first_dec t age
- then GRequested {imp = p; exp = p}
- else GRequested {imp = poly_zero; exp = p}
-
end
module EConPoly = Conflict.RegisterCon(ConPoly)
@@ -1214,13 +1207,8 @@ module ExpEquality = struct
x_p_cy_conpoly p q (get_rlist_conpoly t age modcl cl)
| CombiS(q,v,n) ->
let n = analyse_combi t age n in
- let cl,pexp = get_sem t sem v in
- let pexp = match get_pexp_conpoly t pexp with
- | None -> mk_conpoly (x_p_cy (monome Q.one cl) Q.minus_one v)
- | Some p ->
- assert (Th.equal (x_p_cy (monome Q.one cl) Q.minus_one v) p.exp);
- p
- in
+ let cl = ThE.cl (ThE.index v real) in
+ let pexp = mk_conpoly (x_p_cy (monome Q.one cl) Q.minus_one v) in
x_p_cy_conpoly n q pexp
| CombiRepr(q,cl,n) ->
let n = analyse_combi t age n in
@@ -1299,7 +1287,6 @@ module ExpMulSubst = struct
| Some Eqtype.Eq -> GRequested () in
begin match exp with
| Mul(f,g) as v ->
- get_con () t (get_pexp t (snd (get_sem t mul_sem v)) confact);
get_cons ()
(ComputeConflict.get_equal t age f (get_repr_at t age f));
get_cons ()
diff --git a/src/arith.mli b/src/arith.mli
index 189bc7f36..600c31ffc 100644
--- a/src/arith.mli
+++ b/src/arith.mli
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
open Types
-open Solver
val real: Ty.t
val real_ctr: Ty.Constr.t
diff --git a/src/bool.ml b/src/bool.ml
index 918e1f395..453a7efe9 100644
--- a/src/bool.ml
+++ b/src/bool.ml
@@ -32,8 +32,8 @@ let debug = Debug.register_info_flag
let ty_ctr = Ty.Constr.create "Bool"
let ty = Ty.ctr ty_ctr
let dom : bool dom = Conflict.dom_bool
-let cl_true = Cl.create "⊤" ty
-let cl_false = Cl.create "⊥" ty
+let cl_true = Cl.fresh "⊤" ty
+let cl_false = Cl.fresh "⊥" ty
let union_disjoint m1 m2 =
Cl.M.union (fun _ b1 b2 -> assert (b1 == b2); Some b1) m1 m2
@@ -352,7 +352,7 @@ module DaemonPropa = struct
| Events.Fired.EventDom(_ownr,dom',All v) ->
assert( Dom.equal dom dom' );
(** use this own because the other is the representant *)
- let own = Opt.get (Delayed.get_cl_sem d sem v) in
+ let own = ThE.cl (ThE.index v ty) in
ignore (wakeup_own ~first:false d v own)
| _ -> raise UnwaitedEvent
@@ -533,13 +533,6 @@ let mk_conequal:
(ComputeConflict.t -> Cl.t -> Cl.t -> clause_conflict rescon) ref =
ref (fun _ _ -> assert false)
-type mk_conequal_sem =
- {mutable mk_conequal_sem:
- 'a. ComputeConflict.t -> 'a sem -> 'a -> Cl.t -> clause_conflict rescon}
-let mk_conequal_sem: mk_conequal_sem =
- { mk_conequal_sem = (fun _ _ _ -> assert false) }
-
-
let concat s1 s2 =
Cl.M.union (fun _ b1 b2 -> assert (DBool.equal b1 b2); Some b1) s1 s2
@@ -570,9 +563,9 @@ let get_pexp t s pexp =
get_con s t (ComputeConflict.get_pexp t pexp conclause)
-let get_sem t v s =
- let _, pexp = ComputeConflict.get_sem t sem v in
- get_pexp t s pexp
+let check_sem v cl =
+ let own = ThE.cl (ThE.index v ty) in
+ Cl.equal cl own
(** **)
module ExpMerge = struct
@@ -689,24 +682,24 @@ module ExpProp = struct
raise Impossible
| ExpBCP (v,own,propa,kind,_) ->
let s = Cl.M.empty in
- let s = get_sem t v s in
+ assert (check_sem v own);
let s = if kind == BCPOwnKnown then get_dom t age own s else s in
fold (fun s (cl,_) ->
if kind != BCPLeavesKnown && (Cl.equal cl propa) then s
else get_dom t age cl s) s v
- | ExpUp (v,_,leaf) ->
+ | ExpUp (v,own,leaf) ->
let s = Cl.M.empty in
- let s = get_sem t v s in
+ assert (check_sem v own);
let s = get_dom t age leaf s in
s
| ExpDown (v,own,_,_) ->
let s = Cl.M.empty in
- let s = get_sem t v s in
+ assert (check_sem v own);
let s = get_dom t age own s in
s
| ExpNot ((v,clfrom,clto),_)->
let s = Cl.M.empty in
- let s = get_sem t v s in
+ assert (check_sem v clto || check_sem v clfrom);
let s = get_dom t age clfrom s in
fold (fun s (cl,_) ->
if (Cl.equal cl clfrom) ||
@@ -802,9 +795,8 @@ module ConClause = struct
Some (new finalized s)
- let same_sem t _age _sem (_,pexp1) pexp2 _cl1 _cl2 =
+ let same_sem t _age _sem _v pexp2 _cl1 _cl2 =
let s = Cl.M.empty in
- let s = get_con s t (ComputeConflict.get_pexp t pexp1 conclause) in
let s = get_con s t (ComputeConflict.get_pexp t pexp2 conclause) in
GRequested s
@@ -828,26 +820,19 @@ module ConClause = struct
| _ ->
!mk_conequal t clo rcl
- let propasem t age sem v cl =
- if ComputeConflict.before_first_dec t age
- then GRequested Cl.M.empty
- else
- (** TODO ty bool if sem is bool? *)
- mk_conequal_sem.mk_conequal_sem t sem v cl
-
- let propadom:
- type a. ComputeConflict.t ->
- Explanation.Age.t -> a dom -> Cl.t -> a option -> t rescon =
- fun t age dom' cl bval ->
- if ComputeConflict.before_first_dec t age
- then GRequested Cl.M.empty
- else
- match Dom.Eq.coerce_type dom dom' with
- | Eqtype.Eq ->
- if Cl.equal cl cl_true || Cl.equal cl cl_false then
- GRequested Cl.M.empty
- else
- GRequested (Cl.M.singleton cl (Opt.get bval))
+ (* let propadom: *)
+ (* type a. ComputeConflict.t -> *)
+ (* Explanation.Age.t -> a dom -> Cl.t -> a option -> t rescon = *)
+ (* fun t age dom' cl bval -> *)
+ (* if ComputeConflict.before_first_dec t age *)
+ (* then GRequested Cl.M.empty *)
+ (* else *)
+ (* match Dom.Eq.coerce_type dom dom' with *)
+ (* | Eqtype.Eq -> *)
+ (* if Cl.equal cl cl_true || Cl.equal cl cl_false then *)
+ (* GRequested Cl.M.empty *)
+ (* else *)
+ (* GRequested (Cl.M.singleton cl (Opt.get bval)) *)
end
module EC = Conflict.RegisterCon(ConClause)
diff --git a/src/bool.mli b/src/bool.mli
index bef16b84c..163c363c5 100644
--- a/src/bool.mli
+++ b/src/bool.mli
@@ -78,9 +78,3 @@ val mk_clause: Solver.Delayed.t -> clause_conflict -> Cl.t
val mk_conequal:
(Conflict.ComputeConflict.t ->
Cl.t -> Cl.t -> clause_conflict Conflict.rescon) ref
-
-type mk_conequal_sem =
- {mutable mk_conequal_sem:
- 'a. Conflict.ComputeConflict.t -> 'a sem -> 'a -> Cl.t ->
- clause_conflict Conflict.rescon}
-val mk_conequal_sem: mk_conequal_sem
diff --git a/src/conflict.ml b/src/conflict.ml
index d4486c603..34ac4a06e 100644
--- a/src/conflict.ml
+++ b/src/conflict.ml
@@ -29,7 +29,6 @@ exception DontKnowThisDec of Dom.K.t * Cl.t
exception DomNeverSet
exception ClNotEqual
-exception SemNeverSet
let debug = Debug.register_info_flag
~desc:"for@ the@ main@ part@ of@ conflicts."
@@ -44,29 +43,26 @@ let return : type a b. a con -> b con -> b -> a rescon = fun con con' v ->
| Some Eqtype.Eq -> GRequested v
| None -> GOther(con',v)
-exception NotMarkedAge
-
type explearnt =
| ExpLearnt: Tags.t -> explearnt
let explearnt : explearnt exp = Exp.create_key "Explanation.learnt_exp"
let dom_bool : bool dom = Dom.create_key "bool"
-type tofind =
-| FDom : Cl.t * 'a dom -> tofind
-
exception NotMarkedExp
+(*
module type SemH = sig
type k
type v
- module S : Solver.Sem with type t = k
+ module S : Types.Sem with type t = k
val h : v S.H.t
end
module SemH = Sem.MkVector(struct
type ('a,'b) t = (module SemH with type k = 'a and type v = 'b)
end)
+*)
(** *)
let hash_chogen = ref (fun _ -> assert false)
@@ -243,11 +239,9 @@ module type Con' = sig
val key: t con
val same_sem:
- con_iter -> age -> 'a sem -> Cl.t * pexp ->
+ con_iter -> age -> 'a sem -> 'a ->
pexp -> Cl.t -> Cl.t -> t rescon
- val propasem: con_iter -> Age.t -> 'a sem -> 'a -> Cl.t -> t rescon
-
val propacl : con_iter -> Age.t -> Cl.t -> Cl.t -> t rescon
val finalize: con_iter -> t Bag.t -> finalized option
@@ -355,9 +349,6 @@ let print_modif fmt = function
| Cl (cl1,cl2) -> Format.fprintf fmt "Cl %a -> %a" Cl.print cl1 Cl.print cl2
| Dom (cl,dom,_,cl0) -> Format.fprintf fmt "Dom %a for %a(%a)"
Dom.print dom Cl.print cl0 Cl.print cl;
- | Sem (cl0,sem,s) ->
- Format.fprintf fmt "Sem %a for %a with value %a"
- Sem.print sem Cl.print cl0 (Solver.print_sem sem) s;
| Dec _ -> Format.fprintf fmt "Dec"
| DomL (cl,dom,v,_,_,cl0) ->
Format.fprintf fmt "DomL %a for %a(%a) with value %a"
@@ -380,14 +371,9 @@ type explimit =
(** At the limit the first cl is represented by this cl *)
| LDom: 'a dom * Explanation.mod_dom -> explimit
(** At the limit this class have this value for this dom *)
- | LSem: 'a sem * 'a * Cl.t -> explimit
- (** Similar to LCl. At the limit this cl is the representant and
- before the limit this sem have been associated to it *)
let print_explimit fmt = function
| LCl (cl,rcl) -> Format.fprintf fmt "LCl(%a,%a)" Cl.print cl Cl.print rcl
- | LSem (sem,v,cl) -> Format.fprintf fmt "LSem(%a,%a,%a)"
- Sem.print sem (Solver.print_sem sem) v Cl.print cl
| LDom (dom,moddom) ->
Format.fprintf fmt "LDom(%a,%a)" Dom.print dom
Explanation.print_mod_dom moddom
@@ -461,15 +447,6 @@ module ComputeConflict = struct
{eto=cln;epexp=pexp;einv=false}::l
| GEAAfterDec l -> l
- let get_sem (type a) t (sem : a sem) v =
- match Solver.get_sem_first t.csolver_unsat sem v with
- | None -> raise SemNeverSet
- | Some (cl,age,pexp) when
- Age.compare t.ctrail.last_dec age <= 0 -> (cl,pexp)
- | Some (cl,age,pexp) ->
- let pexp = Explanation.mk_pexp_direct ~age explimit (LSem (sem,v,cl)) in
- (cl,pexp)
-
let rec get_repr_at t age cl =
try
let (agemerge,cl') = Cl.M.find cl t.ctrail.clhist in
@@ -1176,11 +1153,9 @@ module type Con = sig
val key: t con
val same_sem:
- ComputeConflict.t -> age -> 'a sem -> Cl.t * pexp ->
+ ComputeConflict.t -> age -> 'a sem -> 'a ->
pexp -> Cl.t -> Cl.t -> t rescon
- val propasem: con_iter -> Age.t -> 'a sem -> 'a -> Cl.t -> t rescon
-
val propacl : con_iter -> Age.t -> Cl.t -> Cl.t -> t rescon
val finalize: ComputeConflict.iter -> t Bag.t -> finalized option
@@ -1345,17 +1320,15 @@ module ConFact = struct
let finalize _ = assert false (** catched before *)
- let same_sem t age _ (_,pexp1) pexp2 _ _ =
+ let same_sem t age _ _ pexp2 _ _ =
let get_con () t = function
| GRequested () -> ()
| GOther (con,c) -> ComputeConflict.unknown_con t con c
in
- get_con () t (ComputeConflict.get_pexp t pexp1 confact);
get_con () t (ComputeConflict.get_pexp t pexp2 confact);
GRequested ()
let propacl _ _ _ _ = raise Impossible
- let propasem _ _ _ _ _ = raise Impossible
let propadom _ _ dom cl v =
Debug.dprintf6 debug
"[Conflict] @[Error: Ask ConFact for the limit for %a with %a of %a @]@\n"
@@ -1399,9 +1372,6 @@ module ExpLimit = struct
| LCl (cl,rcl) ->
let module C = (val (get_con con)) in
C.propacl t age cl rcl
- | LSem (sem,v,cl) ->
- let module C = (val (get_con con)) in
- C.propasem t age sem v cl
| LDom (dom,{modcl;modage;modpexp}) ->
let f (type b) (k : b exp) (exp: b) =
let module S = (val (get_exp k) : Exp' with type t = b) in
@@ -1439,11 +1409,10 @@ module ExpSameSem = struct
*)
let analyse (type b) t age (con : b con) = function
| Solver.ExpSameSem(pexp,cl1,cl2,sem,v) ->
- let c = get_con con in
- let module C = (val c : Con' with type t = b) in
- let (cl0,_) as c1 = ComputeConflict.get_sem t sem v in
- assert (Cl.equal cl0 cl2);
- C.same_sem t age sem c1 pexp cl1 cl2
+ assert (Ty.equal (Cl.ty cl1) (Cl.ty cl2));
+ assert (Cl.equal (Cl.index sem v (Cl.ty cl2)) cl2);
+ let module C = (val get_con con) in
+ C.same_sem t age sem v pexp cl1 cl2
(** not used for dom *)
let expdom _ _ _ _ _ _ = raise Impossible
diff --git a/src/conflict.mli b/src/conflict.mli
index d3706dade..c44432a9b 100644
--- a/src/conflict.mli
+++ b/src/conflict.mli
@@ -74,8 +74,6 @@ module ComputeConflict: sig
(** get the list of merge that make the too classes equal. *)
val get_repr_at: t -> age -> Cl.t -> Cl.t
(** get the repr of the class at this age . *)
- val get_sem : t -> 'b sem -> 'b -> Cl.t * pexp
- (** get the explication why the sem have been linked for the first time *)
val get_dom : t -> age -> Cl.t -> 'b dom -> mod_dom list
(** get the explications for the domain of this class at the given age *)
@@ -188,11 +186,9 @@ module type Con = sig
(** Particular conflict computation *)
val same_sem:
- ComputeConflict.t -> age -> 'a sem -> Cl.t * pexp ->
+ ComputeConflict.t -> age -> 'a sem -> 'a ->
pexp -> Cl.t -> Cl.t -> t rescon
- val propasem: ComputeConflict.t -> Age.t -> 'a sem -> 'a -> Cl.t -> t rescon
-
val propacl : ComputeConflict.t -> Age.t -> Cl.t -> Cl.t -> t rescon
(* cl1 -> cl2 repr *)
@@ -264,9 +260,6 @@ type explimit =
(** At the limit the first cl is represented by this cl *)
| LDom: 'a dom * Explanation.mod_dom -> explimit
(** At the limit this class have this value for this dom *)
- | LSem: 'a sem * 'a * Cl.t -> explimit
- (** Similar to LCl. At the limit this cl is the representant and
- before the limit this sem have been associated to it *)
val is_explimit : pexp -> explimit option
diff --git a/src/demon.ml b/src/demon.ml
index 27616b7ba..4372e3001 100644
--- a/src/demon.ml
+++ b/src/demon.ml
@@ -381,6 +381,7 @@ module Fast = struct
Dem.print D.key.dk_id Solver.Events.Fired.print event
D.Data.print (Solver.Events.Fired.get_data event);
D.wakeup d event;
+ Debug.dprintf0 debug "[Demon] @[Done@]@\n";
if not D.immediate then Solver.Delayed.flush d;
run_one () in
try
diff --git a/src/equality.ml b/src/equality.ml
index 1430f76ef..52bd53f93 100644
--- a/src/equality.ml
+++ b/src/equality.ml
@@ -123,8 +123,11 @@ module Th = struct
end
-module Registered = RegisterSem(Th)
+module ThE = RegisterSem(Th)
+let check_sem v cl =
+ let own = ThE.cl (ThE.index v Bool.ty) in
+ Cl.equal cl own
(** API *)
@@ -219,7 +222,6 @@ let norm_set d own v =
(** Conflict *)
type eqconflict =
| Eq : Cl.t * Cl.t * bool -> eqconflict
- | Sem: 'a sem * 'a * Cl.t * bool -> eqconflict
module EqConflict = struct
@@ -236,23 +238,11 @@ module EqConflict = struct
let print fmt = function
| Eq(cl1,cl2,b) ->
Format.fprintf fmt "%a%a%a" Cl.print cl1 print_equal b Cl.print cl2
- | Sem(sem,v,cl,b) ->
- Format.fprintf fmt "%a:%a%a%a"
- Sem.print sem (Solver.print_sem sem) v print_equal b Cl.print cl
let equal e1 e2 =
match e1, e2 with
| Eq(cla1,clb1,b1), Eq(cla2,clb2,b2) ->
Cl.equal cla1 cla2 && Cl.equal clb1 clb2 && DBool.equal b1 b2
- | Sem(sem1,v1,c1,b1), Sem(sem2,v2,c2,b2) ->
- Cl.equal c1 c2 && DBool.equal b1 b2 &&
- begin match Sem.Eq.eq_type sem1 sem2 with
- | None -> false
- | Some Eqtype.Eq ->
- let module Sem = (val Solver.get_sem sem1) in
- Sem.equal v1 v2
- end
- | _ -> false
let compare e1 e2 =
match e1, e2 with
@@ -262,31 +252,11 @@ module EqConflict = struct
let c = Cl.compare clb1 clb2 in
if c != 0 then c else
DBool.compare b1 b2
- | Sem(sem1,v1,c1,b1), Sem(sem2,v2,c2,b2) ->
- let c = Cl.compare c1 c2 in
- if c != 0 then c
- else
- let c = DBool.compare b1 b2 in
- if c != 0 then c
- else
- begin match Sem.Eq.eq_type sem1 sem2 with
- | None -> Sem.compare sem1 sem2
- | Some Eqtype.Eq ->
- let module Sem = (val Solver.get_sem sem1) in
- Sem.compare v1 v2
- end
- | Eq _, _ -> 1
- | _, Eq _ -> -1
let hash e1 =
match e1 with
| Eq(cla1,clb1,b) ->
Hashcons.combine2 (Cl.hash cla1) (Cl.hash clb1) (DBool.hash b)
- | Sem(sem1,v1,c1,b) ->
- Hashcons.combine3
- (Cl.hash c1) (DBool.hash b) (Sem.hash sem1)
- (let module Sem = (val Solver.get_sem sem1) in
- Sem.hash v1)
end)
include K
@@ -296,9 +266,6 @@ module EqConflict = struct
then Eq(cl1,cl2,b)
else Eq(cl2,cl1,b)
- let mk_sem sem v cl = Sem(sem,v,cl,true)
-
-
end
let choequal : (EqConflict.t,unit) Explanation.cho =
@@ -335,10 +302,6 @@ module ConDefaultEq = struct
match v with
| Eq(cl1,cl2,b) ->
f cl1 cl2 b
- | Sem(sem,v,cl,b) ->
- match Delayed.get_cl_sem d sem v with
- | Some own -> f own cl b
- | _ -> ToDecide
in
try
EqConflict.S.fold_left fold False eqs
@@ -353,11 +316,7 @@ module ConDefaultEq = struct
match v with
| Eq(cl1,cl2,b) ->
return cl1 cl2 (Eq(cl1,cl2,not b))
- | Sem(sem,v,cl,b) ->
- let c = (Sem(sem,v,cl,not b)) in
- match Delayed.get_cl_sem d sem v with
- | Some own -> return own cl c
- | _ -> f.fold_decisions acc choequal c () in
+ in
EqConflict.S.fold_left fold acc eqs
method conflict_add d =
let fold acc v =
@@ -368,9 +327,6 @@ module ConDefaultEq = struct
match v with
| Eq(cl1,cl2,b) ->
f cl1 cl2 b
- | Sem(sem,v,cl,b) ->
- let cl' = Delayed.index d sem v (Cl.ty cl) in
- f cl' cl b
in
EqConflict.S.fold_left fold Cl.M.empty eqs
end
@@ -389,9 +345,8 @@ module ConDefaultEq = struct
let get_cons t _age s rlist = fold_rescon_list t get_con key s rlist
- let same_sem t age _sem (_,pexp1) pexp2 _cl1 _cl2 =
+ let same_sem t age _sem _v pexp2 _cl1 _cl2 =
let s = Bag.empty in
- let s = get_con s t (ComputeConflict.get_pexp t pexp1 key) in
let s = get_con s t (ComputeConflict.get_pexp t pexp2 key) in
GRequested s
@@ -403,15 +358,6 @@ module ConDefaultEq = struct
ComputeConflict.set_dec_cho t choequal v;
GRequested(Bag.elt v)
- (** For the extension *)
- let propasem t age sem v cl =
- if ComputeConflict.before_first_dec t age
- then GRequested Bag.empty
- else
- let v = mk_sem sem v cl in
- ComputeConflict.set_dec_cho t choequal v;
- GRequested(Bag.elt v)
-
end
module EConDefaultEq = Conflict.RegisterCon(ConDefaultEq)
@@ -420,12 +366,7 @@ let () =
Bool.mk_conequal := (fun t cl1 cl2 ->
let v = EqConflict.mk_eq cl1 cl2 true in
Conflict.ComputeConflict.set_dec_cho t choequal v;
- Conflict.GOther(ConDefaultEq.key,Bag.elt v));
- Bool.mk_conequal_sem.Bool.mk_conequal_sem <-
- (fun t sem v cl ->
- let v = EqConflict.mk_sem sem v cl in
- Conflict.ComputeConflict.set_dec_cho t choequal v;
- Conflict.GOther(ConDefaultEq.key,Bag.elt v))
+ Conflict.GOther(ConDefaultEq.key,Bag.elt v))
module ChoEquals = struct
open Conflict
@@ -441,8 +382,8 @@ module ChoEquals = struct
let key = Explanation.Cho.create_key "Equals.cho"
let choose_decision d v =
- match Delayed.get_cl_sem d sem v with
- | None -> DecNo
+ match Delayed.get_cl_sem d sem v Bool.ty with
+ | None -> assert false
| Some own ->
Debug.dprintf4 debug "[Equality] @[dec on %a for %a@]@\n"
Cl.print own Th.print v;
@@ -491,11 +432,6 @@ module ChoEqual = struct
match v with
| Eq(cl1,cl2,_) ->
f cl1 cl2
- | Sem(sem,v,cl,_) ->
- match Delayed.get_cl_sem d sem v with
- | Some own -> f cl own
- | _ -> DecTodo ()
-
let make_decision d dec v () =
Debug.dprintf2 Conflict.print_decision
@@ -505,9 +441,7 @@ module ChoEqual = struct
match v with
| Eq(cl1,cl2,b) ->
cl1,cl2, b
- | Sem(sem,v,cl,b) ->
- let cl' = Delayed.index d sem v (Cl.ty cl) in
- cl',cl, b in
+ in
if b then begin
Delayed.propagate d cl1;
Delayed.propagate d cl2;
@@ -586,10 +520,6 @@ type special_equality = {
Conflict.ComputeConflict.t -> Explanation.Deps.t -> Explanation.Age.t ->
Cl.t -> Conflict.rlist ->
Explanation.Deps.t;
- sem: 'a.
- Conflict.ComputeConflict.t -> Explanation.Deps.t -> Explanation.Age.t ->
- 'a sem -> 'a -> Explanation.pexp ->
- Explanation.Deps.t;
dodec: bool;
}
@@ -640,7 +570,6 @@ module GenEquality = struct
repr = (fun t deps age _ r1 ->
let b,deps = get_cons t (Bag.empty,deps) r1 in
Explanation.Deps.add_unknown_con deps ConDefaultEq.key b);
- sem = get_sem;
dodec;
}
@@ -671,28 +600,8 @@ module GenEquality = struct
assert (deps0 == ComputeConflict.get_current_deps t);
deps
*)
- let sem t deps age sem v rl1 ty =
- let deps0 = ComputeConflict.get_current_deps t in
- let deps = (find_expspecial ty).sem t deps age sem v rl1 in
- assert (deps0 == ComputeConflict.get_current_deps t);
- deps
let dodec ty = (find_expspecial ty).dodec
-
- let get_con = Conflict.fold_requested_deps
- (fun (b1,deps) _ b2 -> Bag.concat b1 b2, deps)
- let get_cons t age = fold_rescon_list_deps t get_con ConDefaultEq.key
- let get_sem t deps age _ _ r =
- let accdeps = Bag.empty,deps in
- let b,deps = get_cons t age accdeps r in
- Explanation.Deps.add_unknown_con deps ConDefaultEq.key b
-
- let sem_def t deps age rl1 =
- let deps0 = ComputeConflict.get_current_deps t in
- let deps = get_sem t deps age () () rl1 in
- assert (deps0 == ComputeConflict.get_current_deps t);
- deps
-
end
let register_sort_con ty ~dodec con = register_sort ty
@@ -714,7 +623,7 @@ module DaemonPropa = struct
let immediate = false
let wakeup d v _ev =
- norm_dom d (Opt.get (Delayed.get_cl_sem d sem v)) v
+ norm_dom d (Opt.get (Delayed.get_cl_sem d sem v Bool.ty)) v
end
@@ -986,13 +895,11 @@ module ExpSubst = struct
| SubstUpTrue (v,e1,e2,_) -> (** two are equals *)
let ty = Th.get_ty v in
let s = Cl.M.empty in
- let s = Bool.get_pexp t s (snd (get_sem t sem v)) in
GenEquality.equality t age e1 e2 ty;
return con conclause s
| SubstUpFalse (v,_) ->
let ty = Th.get_ty v in
let s = Cl.M.empty in
- let s = Bool.get_pexp t s (snd (get_sem t sem v)) in
let l = Cl.S.fold_left
(fun acc cl -> (cl,ComputeConflict.get_dom t age cl dom)::acc) [] v in
begin match l with
@@ -1015,13 +922,13 @@ module ExpSubst = struct
end
| SubstDownTrue (v,own) ->
let ty = Th.get_ty v in
- let s = Bool.get_pexp t Cl.M.empty (snd (get_sem t sem v)) in
- let s = Bool.get_dom t age own s in
+ assert (check_sem v own);
+ let s = Bool.get_dom t age own Cl.M.empty in
return con conclause s
| SubstDownFalse (v,own,i) ->
let ty = Th.get_ty v in
- let s = Bool.get_pexp t Cl.M.empty (snd (get_sem t sem v)) in
- let s = Bool.get_dom t age own s in
+ assert (check_sem v own);
+ let s = Bool.get_dom t age own Cl.M.empty in
unknown_con t conclause s;
return_dis con i
| SubstDownDec (pexp,i) ->
@@ -1103,7 +1010,7 @@ module ITE = struct
end
open ITE
-module EITE = Solver.RegisterSem(ITE)
+module EITE = Types.RegisterSem(ITE)
let ite env cond then_ else_ =
let ty1 = Cl.ty then_ in
@@ -1115,11 +1022,10 @@ let expite : (ITE.t * bool) Explanation.exp =
Explanation.Exp.create_key "Ite.exp"
module DaemonPropaITE = struct
- type d = ITE.t
+ type d = EITE.t
let key = Demon.Fast.create "ITE.propa"
- module Key = DUnit
- module Data = ITE
+ module Data = EITE
let simplify d own b v =
let branch = if b then v.then_ else v.else_ in
@@ -1130,15 +1036,14 @@ module DaemonPropaITE = struct
let immediate = false
let throttle = 100
let wakeup d = function
- | Events.Fired.EventDom(cond,dom,v) ->
+ | Events.Fired.EventDom(cond,dom,clsem) ->
assert (Dom.equal dom Bool.dom);
+ let v = EITE.sem clsem in
assert (Delayed.is_equal d cond v.cond);
- begin match Delayed.get_cl_sem d ITE.key v with
+ let own = EITE.cl clsem in
+ begin match Bool.is d v.cond with
| None -> assert false
- | Some own ->
- match Bool.is d v.cond with
- | None -> assert false
- | Some b -> simplify d own b v
+ | Some b -> simplify d own b v
end
| _ -> raise UnwaitedEvent
@@ -1163,9 +1068,11 @@ module DaemonInitITE = struct
| Some b ->
DaemonPropaITE.simplify d own b v
| None ->
+ let clsem = EITE.index v (Cl.ty own) in
+ assert (Cl.equal (EITE.cl clsem) own);
Delayed.propagate d v.cond;
Delayed.ask_decision d (Explanation.GCho(Bool.chobool,v.cond));
- let events = [Demon.Create.EventDom(v.cond,Bool.dom,v)] in
+ let events = [Demon.Create.EventDom(v.cond,Bool.dom,clsem)] in
Demon.Fast.attach d DaemonPropaITE.key events
end
| _ -> raise UnwaitedEvent
@@ -1192,7 +1099,6 @@ module ExpITE = struct
Explanation.age -> a Explanation.con -> t -> a Conflict.rescon =
fun t age con (ite,_) ->
let s = Cl.M.empty in
- let s = Bool.get_pexp t s (snd (ComputeConflict.get_sem t ITE.key ite)) in
let s = Bool.get_dom t age ite.cond s in
return con conclause s
diff --git a/src/equality.mli b/src/equality.mli
index 68a2b8e0b..cb3ca3d57 100644
--- a/src/equality.mli
+++ b/src/equality.mli
@@ -19,9 +19,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
-open Stdlib
open Types
-open Solver
val equality : Solver.d -> Cl.t list -> Cl.t
val disequality : Solver.d -> Cl.t list -> Cl.t
@@ -34,7 +32,6 @@ val ite : Solver.d -> Cl.t -> Cl.t -> Cl.t -> Cl.t
val propagate : Solver.d -> unit
open Explanation
-open Conflict
type special_equality = {
equality:
@@ -53,10 +50,6 @@ type special_equality = {
Conflict.ComputeConflict.t -> Explanation.Deps.t -> Explanation.Age.t ->
Cl.t -> Conflict.rlist ->
Explanation.Deps.t;
- sem: 'a.
- Conflict.ComputeConflict.t -> Explanation.Deps.t -> Explanation.Age.t ->
- 'a sem -> 'a -> Explanation.pexp ->
- Explanation.Deps.t;
dodec: bool;
}
@@ -67,15 +60,9 @@ module GenEquality: sig
val equality: Conflict.ComputeConflict.t ->
Explanation.Age.t -> Types.Cl.t -> Types.Cl.t -> Ty.t -> unit
- val sem:
- Conflict.ComputeConflict.t -> Explanation.Deps.t -> Explanation.Age.t ->
- 'a sem -> 'a -> Explanation.pexp -> Ty.t ->
- Explanation.Deps.t
-
end
type eqconflict =
| Eq : Cl.t * Cl.t * bool -> eqconflict
- | Sem: 'a sem * 'a * Cl.t * bool -> eqconflict
val choequal : (eqconflict, unit) Explanation.cho
diff --git a/src/explanation.ml b/src/explanation.ml
index 5b9c4efb7..c3fda5dfa 100644
--- a/src/explanation.ml
+++ b/src/explanation.ml
@@ -218,7 +218,6 @@ type modif =
| Cl : Cl.t * Cl.t -> modif (** Just for taking an age *)
| Dom: Cl.t * 'a dom * pexp * Cl.t -> modif
| DomL: Cl.t * 'a dom * 'a option * Age.t * pexp * Cl.t -> modif
-| Sem: Cl.t * 'a sem * 'a -> modif (** Just for taking an age *)
| Dec: dec -> modif
let print_modif_ref = ref (fun _ _ -> assert false)
@@ -400,15 +399,6 @@ let add_pexp_dom t pexp dom ~cl ~cl0 _ =
let expfact : unit exp = Exp.create_key "Explanation.fact"
let pexpfact = Pexp(Age.bef,expfact,(),Tags.empty,Concache.mk ())
-let add_pexp_sem t pexp _sem _v _cl =
- (* let modif = Sem(cl,sem,v) in *)
- push (* modif *) t;
- Debug.dprintf2 debug "[Trail] @[change sem %a@]@\n"
- (* print_modif modif *) Age.print t.age;
- if pexp == pexpfact (** because it depend of nothing *)
- then Age.min
- else t.age
-
type invclhist = Cl.t Age.M.t Cl.H.t
let print_invclhist fmt h =
diff --git a/src/explanation.mli b/src/explanation.mli
index c288ea063..12fbba992 100644
--- a/src/explanation.mli
+++ b/src/explanation.mli
@@ -83,11 +83,6 @@ type modif =
| DomL: Cl.t * 'a dom * 'a option * Age.t * pexp * Cl.t -> modif
(** same as before but the first time in this level *)
-| Sem: Cl.t * 'a sem * 'a -> modif
- (** Cl(cl,sem,v,pexp) explication why (sem,v) is binded to this cl
- perhaps not the representative of its eq class
- *)
-
| Dec: dec -> modif
(** new level decision *)
@@ -161,12 +156,6 @@ val add_pexp_dom:
t -> pexp -> 'b dom -> cl:Cl.t -> cl0:Cl.t -> 'b option -> unit
(** The value must be the old value *)
-val add_pexp_sem:
- t -> pexp -> 'b sem -> 'b -> Cl.t -> Age.t
-(** cl the representative cl0 the class *)
-
-
-
val trail: t -> modif list
val last_dec: t -> Age.t
val nbdec: t -> int
diff --git a/src/inputlang/altergo/popop_of_altergo.mli b/src/inputlang/altergo/popop_of_altergo.mli
index 45d8b8d69..9005ccdcf 100644
--- a/src/inputlang/altergo/popop_of_altergo.mli
+++ b/src/inputlang/altergo/popop_of_altergo.mli
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-open Why_ptree
-
exception Not_supported of Loc.position
val read_file: string -> Why_ptree.file
diff --git a/src/solver.ml b/src/solver.ml
index 512d51e0e..2d5319a69 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -148,12 +148,6 @@ module type Dom' = sig
val key: t dom
end
-module type Sem' = sig
- type delayed
- include Stdlib.Datatype
- val key: t sem
-end
-
type _ enqueue =
| EnqRun: 'r -> 'r enqueue
@@ -188,8 +182,7 @@ end
module type SemTable' = sig
type delayed
- module S : Sem' with type delayed := delayed
- val invtable : (Cl.t * age * pexp) S.M.t
+ module S : Sem
(** class where propa of this sem must be done *)
val events : Events.Wait.t list Cl.M.t
(** propa of new semantic value *)
@@ -221,7 +214,6 @@ type t = {
mutable event : Events.Wait.t Bag.t Cl.M.t;
mutable event_propa : Events.Wait.t list Cl.M.t;
mutable event_any_propa : Events.Wait.t list;
- mutable when_propa : (delayed_t -> Cl.t -> unit) list Cl.M.t;
(** extensible "number of fields" *)
dom : delayed_t VDomTable.t;
sem : delayed_t VSemTable.t;
@@ -286,7 +278,6 @@ let new_t () = {
event = Cl.M.empty;
event_propa = Cl.M.empty;
event_any_propa = [];
- when_propa = Cl.M.empty;
dom = VDomTable.create 5;
sem = VSemTable.create 5;
envs = Env.VectorH.create 5;
@@ -301,7 +292,6 @@ let new_handler t =
event = t.event;
event_propa = t.event_propa;
event_any_propa = t.event_any_propa;
- when_propa = t.when_propa;
dom = VDomTable.copy t.dom;
sem = VSemTable.copy t.sem;
envs = Env.VectorH.copy t.envs;
@@ -311,24 +301,18 @@ let new_handler t =
(** {2 Dom and Sem} *)
module type Dom = Dom' with type delayed := delayed_t
-module type Sem = Sem' with type delayed := delayed_t
module type Dem = Dem' with type delayed := delayed_t
module VDom = Dom.MkVector
(struct type ('a,'unedeed) t =
(module Dom with type t = 'a)
end)
-module VSem = Sem.MkVector
- (struct type ('a,'unedeed) t =
- (module Sem with type t = 'a)
- end)
module VDem = Dem.MkVector
(struct type ('k,'d,'unedeed) t =
(module Dem with type event = 'k and type runable = 'd) end)
let defined_dom : unit VDom.t = VDom.create 8
-let defined_sem : unit VSem.t = VSem.create 8
let defined_dem : unit VDem.t = VDem.create 8
module RegisterDom (D:Dom) = struct
@@ -342,16 +326,6 @@ module RegisterDom (D:Dom) = struct
end
-module RegisterSem (D:Sem) = struct
-
- let () =
- VSem.inc_size D.key defined_sem;
- assert (if not (VSem.is_uninitialized defined_sem D.key)
- then raise AlreadyRegisteredKey else true);
- let sem = (module D: Sem with type t = D.t) in
- VSem.set defined_sem D.key sem
-
-end
module RegisterDem (D:Dem) = struct
@@ -370,11 +344,6 @@ let get_dom k =
then raise UnregisteredKey else true);
VDom.get defined_dom k
-let get_sem k =
- assert (if VSem.is_uninitialized defined_sem k
- then raise UnregisteredKey else true);
- VSem.get defined_sem k
-
let get_dem k =
assert (if VDem.is_uninitialized defined_dem k
then raise UnregisteredKey else true);
@@ -521,15 +490,13 @@ let get_table_dom : t -> 'a dom -> (module DomTable with type D.t = 'a)
let get_table_sem : t -> 'a sem -> (module SemTable with type S.t = 'a)
= fun (type a) t k ->
- assert (if VSem.is_uninitialized defined_sem k
- then raise UnregisteredKey else true);
+ assert (if sem_uninitialized k then raise UnregisteredKey else true);
VSemTable.inc_size k t.sem;
if VSemTable.is_uninitialized t.sem k then
let sem = get_sem k in
let module SemTable = struct
type delayed = delayed_t
module S = (val sem : Sem with type t = a)
- let invtable = S.M.empty
let events = Cl.M.empty
let propa_events = []
end in
@@ -543,35 +510,36 @@ exception UninitializedEnv of Env.K.t
exception NotNormalized
-let rec find t cl =
- let cl' = Cl.M.find_exn NotNormalized cl t.repr in
- if Cl.equal cl cl' then cl else
- let r = find t cl' in
- t.repr <- Cl.M.add cl r t.repr;
- r
+(** Just used for being able to qualify these function on t *)
+module T = struct
+ let rec find t cl =
+ let cl' = Cl.M.find_exn NotNormalized cl t.repr in
+ if Cl.equal cl cl' then cl else
+ let r = find t cl' in
+ t.repr <- Cl.M.add cl r t.repr;
+ r
-let find_def t cl =
- let cl' = Cl.M.find_def cl cl t.repr in
- if Cl.equal cl cl' then cl else
- let r = find t cl' in
- t.repr <- Cl.M.add cl r t.repr;
- r
-
-let is_repr t cl =
- try Cl.equal (Cl.M.find cl t.repr) cl
- with Not_found -> true
+ let find_def t cl =
+ let cl' = Cl.M.find_def cl cl t.repr in
+ if Cl.equal cl cl' then cl else
+ let r = find t cl' in
+ t.repr <- Cl.M.add cl r t.repr;
+ r
-let is_equal t cl1 cl2 =
- let cl1 = find_def t cl1 in
- let cl2 = find_def t cl2 in
- Cl.equal cl1 cl2
+ let is_repr t cl =
+ try Cl.equal (Cl.M.find cl t.repr) cl
+ with Not_found -> true
+ let is_equal t cl1 cl2 =
+ let cl1 = find_def t cl1 in
+ let cl2 = find_def t cl2 in
+ Cl.equal cl1 cl2
+end
+open T
-let get_cl_sem (type a) t (sem : a sem) s =
- let module SemTable =
- (val (get_table_sem t sem) : SemTable with type S.t = a) in
- Opt.map (fun (cl,_,_) -> cl)
- (SemTable.S.M.find_opt s SemTable.invtable)
+let get_cl_sem (type a) t (sem : a sem) s ty =
+ let cl = Cl.index sem s ty in
+ Some cl
let get_direct_dom (type a) t (dom : a dom) cl =
let module DomTable =
@@ -582,12 +550,6 @@ let get_dom t dom cl =
let cl = find_def t cl in
get_direct_dom t dom cl
-
-let add_when_propa t cl todo =
- t.when_propa <-
- Cl.M.add_change Lists.singleton Lists.add cl todo t.when_propa
-
-
(** {2 For debugging and display} *)
let _print_env fmt t =
let printd (type a) _ fmt domtable =
@@ -612,24 +574,6 @@ let output_graph filename t =
let default_vertex_attributes _ = [`Shape `Record]
let vertex_name cl = string_of_int (Cl.hash cl)
- let table = Cl.H.create 10
-
- let iter_sem =
- fun (type a) sem ->
- let module Sem =
- (val sem : SemTable' with type delayed = delayed_t
- and type S.t = a) in
- let iter s (cl,_,_) =
- let mssg = Pp.sprintf_wnl "| {%a | %a} "
- Types.Sem.print Sem.S.key Sem.S.print s in
- let mssg' = (Cl.H.find_def table "" cl) in
- let mssg = mssg' ^ mssg in
- Cl.H.replace table cl mssg
- in
- Sem.S.M.iter iter Sem.invtable
-
- let () = VSemTable.iter_initialized {VSemTable.iter = iter_sem} t.sem
-
let print fmt cl =
let iter_dom (type a) _ fmt dom =
let module Dom =
@@ -645,10 +589,18 @@ let output_graph filename t =
if is_repr t cl
then Format.fprintf fmt ": %a" Ty.print (Cl.ty cl)
in
- Format.fprintf fmt "{%a %a %s %a}" (* "{%a | %a | %a}" *)
+ let print_sem fmt cl =
+ match Only_for_solver.sem_of_cl cl with
+ | Only_for_solver.Fresh -> ()
+ | Only_for_solver.Sem(sem,v) ->
+ let module S = (val get_sem sem) in
+ Format.fprintf fmt "| {%a | %a}"
+ Sem.print sem S.print v
+ in
+ Format.fprintf fmt "{%a %a %a %a}" (* "{%a | %a | %a}" *)
Cl.print cl
print_ty cl
- (Cl.H.find_def table "" cl)
+ print_sem cl
(if is_repr t cl
then VDomTable.print Pp.nothing Pp.nothing
{VDomTable.printk=Pp.nothing}
@@ -690,6 +642,7 @@ let draw_graph =
(** {2 Delayed} *)
module Delayed = struct
+ open T
type t = delayed_t
let find t cl =
@@ -704,9 +657,9 @@ module Delayed = struct
assert (t.env.current_delayed == t);
is_repr t.env cl
- let is_repr_of t cl1 cl2 =
- try Cl.equal (find t cl2) cl1
- with NotNormalized -> Cl.equal cl2 cl1
+ (* let is_repr_of t cl1 cl2 = *)
+ (* try Cl.equal (find t cl2) cl1 *)
+ (* with NotNormalized -> Cl.equal cl2 cl1 *)
let is_equal t cl1 cl2 =
assert (t.env.current_delayed == t);
@@ -715,7 +668,7 @@ module Delayed = struct
let is_propagated t cl = Cl.M.mem cl t.env.repr
- let get_cl_sem t sem s = get_cl_sem t.env sem s
+ let get_cl_sem t sem s ty = get_cl_sem t.env sem s ty
let add_pending_merge (t : t) pexp cl cl' =
Debug.dprintf4 debug "[Solver] @[add_pending_merge for %a and %a@]@\n"
@@ -806,44 +759,16 @@ module Delayed = struct
include SemTable
let propa_events = event::propa_events
end in
- (** propagate the sematic value that are already propagated *)
- VSemTable.set t.env.sem sem (module SemTable');
- SemTable'.S.M.iter (fun s (cl,_,_) ->
- let wakeup t cl =
- wakeup_event Events.Fired.translate_propasem t (cl,sem,s) event
- in
- if is_propagated t cl
- then wakeup t cl
- else add_when_propa t.env cl wakeup
- )
- SemTable'.invtable
+ VSemTable.set t.env.sem sem (module SemTable')
let index_t (type a) t (sem : a sem) s ty =
- let module SemTable = (val (get_table_sem t sem)) in
- try
- let cl,_,_ = SemTable.S.M.find s SemTable.invtable in
- assert (Ty.equal (Cl.ty cl) ty);
- cl
- with Not_found ->
- let cl = Cl.create "" ty in
- let age = add_pexp_sem t.trail pexpfact sem s cl in
- let module SemTable = struct
- include SemTable
- let invtable = SemTable.S.M.add s (cl,age,pexpfact) SemTable.invtable
- end in
- Debug.dprintf4 debug_create "[Solver] @[index %a into %a@]@\n"
- SemTable.S.print s Cl.print cl;
- VSemTable.set t.sem sem
- (module SemTable);
- (** propasem *)
- begin if SemTable.propa_events != [] then
- let wakeup t cl =
- wakeup_events_list Events.Fired.translate_propasem
- t (Some SemTable.propa_events) (cl,sem,s);
- in
- add_when_propa t cl wakeup
- end;
- cl
+ let cl = Cl.index sem s ty in
+ begin if Debug.test_flag debug_create && not (Cl.M.mem cl t.repr) then
+ let module Sem = (val get_sem sem) in
+ Debug.dprintf4 debug_create "[Solver] @[index %a into %a@]@\n"
+ Sem.print s Cl.print cl
+ end;
+ cl
let index t sem s =
assert (t.env.current_delayed == t);
@@ -853,7 +778,7 @@ module Delayed = struct
(type k) (type d) d cl (dem:(k,d) dem) : k Enum.t =
Enum.from_list
~filter:(function
- | Events.Wait.Event(dem',event) ->
+ | Events.Wait.Event(dem',_) ->
Dem.equal dem dem'
)
~map:(function
@@ -867,7 +792,7 @@ module Delayed = struct
(type k) (type d) d cl (dem:(k,d) dem) : k Enum.t =
Enum.from_bag
~filter:(function
- | Events.Wait.Event(dem',event) ->
+ | Events.Wait.Event(dem',_) ->
Dem.equal dem dem'
)
~map:(function
@@ -881,57 +806,66 @@ module Delayed = struct
(** *)
+ let check_no_dom t cl =
+ let foldi (type a) acc _dom domtable =
+ acc &&
+ let module DomTable =
+ (val domtable : DomTable' with type D.t = a
+ and type delayed = delayed_t) in
+ not (Cl.M.mem cl DomTable.table)
+ in
+ VDomTable.fold_initializedi {VDomTable.foldi} true t.env.dom
+
let propagate t cl =
assert (t.env.current_delayed == t);
if not (is_propagated t cl) then begin
Debug.dprintf2 debug "[Solver] propagate %a@\n" Cl.print cl;
+ assert ( check_no_dom t cl );
t.env.repr <- Cl.M.add cl cl t.env.repr;
+ (** propa_cl *)
let new_events, cl_events = Cl.M.find_remove cl t.env.event_propa in
t.env.event_propa <- new_events;
wakeup_events_list Events.Fired.translate_propacl t cl_events cl;
+ (** propa *)
wakeup_events_list Events.Fired.translate_propa
t (Some t.env.event_any_propa) cl;
- let when_propa, todos = Cl.M.find_remove cl t.env.when_propa in
- begin match todos with
- | None -> ()
- | Some todos ->
- t.env.when_propa <- when_propa;
- List.iter (fun f -> f t cl) todos
- end;
+ (** propa_sem *)
+ match Only_for_solver.sem_of_cl cl with
+ | Only_for_solver.Fresh -> ()
+ | Only_for_solver.Sem(sem,s) ->
+ let module SemTable = (val get_table_sem t.env sem) in
+ wakeup_events_list Events.Fired.translate_propasem
+ t (Some SemTable.propa_events) (cl,sem,s)
end
let set_sem_pending (type a) t pexp (sem : a sem) cl0 v =
let cl = find t cl0 in
- let module SemTable = (val (get_table_sem t.env sem)) in
- let clo' = SemTable.S.M.find_opt v SemTable.invtable in
- match clo' with
- | Some (cl',_,_) when is_repr_of t cl cl' ->
- (** if cl is the representant of cl' then we have nothing to do *)
- ()
- | _ ->
- begin match clo' with
- | None ->
- let age = add_pexp_sem t.env.trail pexp sem v cl0 in
- let module SemTable' = struct
- include SemTable
- let invtable =
- SemTable.S.M.add v (cl0,age,pexp) invtable
- end in
- VSemTable.set t.env.sem sem (module SemTable');
- wakeup_events_list Events.Fired.translate_propasem
- t (Some SemTable.propa_events) (cl,sem,v)
- | Some (cl',_,_) ->
- assert (is_repr t cl);
- (** come from invtable, can be just indexed *)
+ let cl0' = Cl.index sem v (Cl.ty cl0) in
+ begin
+ if not (is_propagated t cl0') then begin
+ propagate t cl0';
+ t.env.repr <- Cl.M.add cl0' cl t.env.repr;
+ add_pexp_cl t.env.trail pexp ~inv:false
+ ~other_cl:cl0' ~other_cl0:cl0'
+ ~repr_cl:cl ~repr_cl0:cl0;
+ (** wakeup the daemons propagate_cl *)
+ let event, other_event = Cl.M.find_remove cl0' t.env.event in
+ wakeup_events_bag Events.Fired.translate_change t other_event cl0';
+ t.env.event <- event
+ end
+ (** cl' is already propagated *)
+ else if Cl.equal cl (find t cl0') then
+ (** if cl is the representant of cl' then we have nothing to do *)
+ ()
+ else
+ (** merge cl and cl0' *)
let pexp' = mk_pexp t.env.trail exp_same_sem
- (ExpSameSem(pexp,cl0,cl',sem,v)) in
- propagate t cl';
- if not (Cl.equal cl (find t cl'))
- then
- add_pending_merge t pexp' cl0 cl'
- end;
- let cl_events = Cl.M.find_opt cl SemTable.events in
- wakeup_events_list Events.Fired.translate_sem t cl_events (cl,sem,v)
+ (ExpSameSem(pexp,cl0,cl0',sem,v)) in
+ add_pending_merge t pexp' cl0 cl0'
+ end;
+ let module SemTable = (val get_table_sem t.env sem) in
+ let cl_events = Cl.M.find_opt cl SemTable.events in
+ wakeup_events_list Events.Fired.translate_sem t cl_events (cl,sem,v)
let set_dom_pending (type a) t pexp (dom : a dom) cl0 new_v =
Debug.incr stats_set_dom;
@@ -1150,7 +1084,9 @@ module Delayed = struct
let merge t pexp cl1_0 cl2_0 =
assert (t.env.current_delayed == t);
- if not (Cl.equal (find t cl1_0) (find t cl2_0)) then
+ if not (Cl.equal
+ (find t cl1_0)
+ (find t cl2_0)) then
add_pending_merge t pexp cl1_0 cl2_0
let set_sem d pexp sem cl v =
@@ -1353,10 +1289,6 @@ let get_trail t =
let current_age t = Explanation.current_age t.trail
let current_nbdec t = Explanation.nbdec t.trail
-let get_sem_first (type a) t (sem : a sem) s =
- let module SemTable = (val (get_table_sem t sem)) in
- SemTable.S.M.find_opt s SemTable.invtable
-
let get_direct_dom t dom cl =
assert (t.current_delayed == dumb_delayed ||
t.current_delayed == unsat_delayed);
@@ -1379,7 +1311,7 @@ module type Ro = sig
val is_repr : t -> Cl.t -> bool
- val get_cl_sem : t -> 'a sem -> 'a -> Cl.t option
+ val get_cl_sem : t -> 'a sem -> 'a -> Ty.t -> Cl.t option
(** return the first class associated to this sem
in the current context. Return None if it has never been binded
*)
@@ -1419,13 +1351,6 @@ let check_initialization () =
Dom.print dom;
end};
- Sem.iter {Sem.iter = fun sem ->
- if VSem.is_uninitialized defined_sem sem then begin
- Format.eprintf
- "[Warning] The set of values %a is not registered@." Sem.print sem;
- well_initialized := false;
- end};
-
Dem.iter {Dem.iter = fun dem ->
if VDem.is_uninitialized defined_dem dem then begin
Format.eprintf
diff --git a/src/solver.mli b/src/solver.mli
index 34d443290..237674b18 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -83,16 +83,16 @@ module type Ro = sig
val is_equal : t -> Cl.t -> Cl.t -> bool
val find_def : t -> Cl.t -> Cl.t
-
- (** {4 The classes must have been marked has propagated} *)
val get_dom : t -> 'a dom -> Cl.t -> 'a option
(** dom of the representative class *)
+ (** {4 The classes must have been marked has propagated} *)
+
val find : t -> Cl.t -> Cl.t
val is_repr : t -> Cl.t -> bool
- val get_cl_sem : t -> 'a sem -> 'a -> Cl.t option
+ val get_cl_sem : t -> 'a sem -> 'a -> Ty.t -> Cl.t option
(** return the first class associated to this sem
in the current context. Return None if it has never been binded
*)
@@ -186,15 +186,6 @@ end
module RegisterDom (D:Dom) : sig end
-module type Sem = sig
- include Datatype
-
- val key: t sem
-end
-
-module RegisterSem (D:Sem) : sig end
-
-val get_sem: 'a sem -> (module Sem with type t = 'a)
val register_env: 'a Pp.printer -> 'a env -> unit
val print_env: 'a env -> 'a Pp.printer
@@ -271,7 +262,6 @@ val current_age : t -> Explanation.Age.t
val current_nbdec : t -> int
(** for conflict *)
-val get_sem_first : t -> 'a sem -> 'a -> (Cl.t * age * pexp) option
val get_direct_dom : t -> 'a dom -> Cl.t -> 'a option
(** dom of the class directly (the last time modified) *)
diff --git a/src/types.ml b/src/types.ml
index 9e76addad..b2ab265a9 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -65,21 +65,6 @@ module Ty = struct
end
-module Cl = struct
- include Strings.Fresh(struct end)
-
- let ty_of_cl = Simple_vector.create 100
- let create debug ty =
- let cl = create debug in
- Simple_vector.inc_size ((cl :> int) + 1) ty_of_cl;
- Simple_vector.set ty_of_cl (cl :> int) ty;
- cl
-
- let ty (cl : t) = Simple_vector.get ty_of_cl (cl :> int)
-
-end
-
-
module type Key = sig
module K: Datatype
@@ -88,6 +73,7 @@ module type Key = sig
val compare: 'a k -> 'b k -> int
val equal: 'a k -> 'b k -> bool
val hash : 'a k -> int
+ val tag: 'a k -> int
type iter = {iter : 'a. 'a k -> unit}
val iter : iter -> unit
@@ -109,7 +95,7 @@ module type Key = sig
module M : Intmap_hetero.R1 with type 'a key = 'a k
end
-module Make_key(X:sig end) : Key = struct
+module Make_key(X:sig end): Key = struct
module K = Strings.Fresh(struct end)
type 'a k = K.t (* >= 0 *)
@@ -117,6 +103,7 @@ module Make_key(X:sig end) : Key = struct
let compare x y = K.compare x y
let equal x y = K.equal x y
let hash x = K.hash x
+ let tag (x:K.t) = (x:>int)
type iter = {iter : 'a. 'a k -> unit}
let iter f = K.iter f.iter
@@ -143,6 +130,161 @@ module Sem = Make_key(struct end)
type 'a dom = 'a Dom.k
type 'a sem = 'a Sem.k
+module type Sem = sig
+ include Stdlib.Datatype
+ val key: t sem
+end
+
+
+module VSem = Sem.MkVector
+ (struct type ('a,'unedeed) t =
+ (module Sem with type t = 'a)
+ end)
+
+let defined_sem : unit VSem.t = VSem.create 8
+let sem_uninitialized sem = VSem.is_uninitialized defined_sem sem
+let get_sem k =
+ assert (if sem_uninitialized k then raise UnregisteredKey else true);
+ VSem.get defined_sem k
+
+module Cl = struct
+ type 'a r =
+ | Fresh: int * Ty.t -> [>`Fresh] r
+ | Sem : int * Ty.t * 'a sem * 'a -> [>`Sem] r
+
+ type t' = [ `Fresh | `Sem] r
+
+ let tag: t' -> int = function
+ | Fresh(tag,_) -> tag
+ | Sem(tag,_,_,_) -> tag
+
+ let names = Simple_vector.create 100
+ let used_names : (* next id to use *) int DStr.H.t = DStr.H.create 100
+
+ (** remove the empty string *)
+ let () = DStr.H.add used_names "" 0
+
+ let print fmt x =
+ Format.pp_print_char fmt '@';
+ Format.pp_print_string fmt (Simple_vector.get names (tag x))
+
+ module T = Stdlib.MakeMSH(struct
+ type t = t' let tag = tag
+ let print = print
+ end)
+
+ include T
+
+ let next_tag, incr_tag = Util.get_counter ()
+
+ let fresh s ty : t =
+ let i = next_tag () in
+ incr_tag ();
+ let s = Strings.find_new_name used_names s in
+ Simple_vector.inc_size (i+1) names;
+ Simple_vector.set names i s;
+ Fresh(i,ty)
+
+ let rename cl s =
+ let s = Strings.find_new_name used_names s in
+ Simple_vector.set names (tag cl) s
+
+ let ty = function | Fresh (_,ty) | Sem(_,ty,_,_) -> ty
+
+ module SemIndex = Sem.MkVector
+ (struct type ('a,'unedeed) t = 'a -> Ty.t -> t' end)
+
+ let semindex : unit SemIndex.t = SemIndex.create 8
+
+ let index sem v ty =
+ assert (if sem_uninitialized sem then raise UnregisteredKey else true);
+ (SemIndex.get semindex sem) v ty
+
+end
+
+module RegisterSem (D:Sem) = struct
+
+ module HC = Hashcons.MakeTag(struct
+ open Cl
+ type t = [`Sem] Cl.r
+
+ let next_tag = Cl.next_tag
+ let incr_tag = Cl.incr_tag
+
+ let equal: t -> t -> bool = fun a b ->
+ match a, b with
+ | Sem(_,tya,sema,va), Sem(_,tyb,semb,vb) ->
+ match Sem.Eq.coerce_type sema D.key,
+ Sem.Eq.coerce_type semb D.key with
+ | Eqtype.Eq, Eqtype.Eq ->
+ Ty.equal tya tyb && D.equal va vb
+
+ let hash: t -> int = fun a ->
+ match a with
+ | Sem(_,tya,sema,va) ->
+ match Sem.Eq.coerce_type sema D.key with
+ | Eqtype.Eq ->
+ Hashcons.combine (Ty.hash tya) (D.hash va)
+
+ let set_tag: int -> t -> t = fun tag x ->
+ match x with
+ | Sem(_,ty,sem,v) -> Sem(tag,ty,sem,v)
+
+ let tag: t -> int = function
+ | Sem(tag,_,_,_) -> tag
+
+ let print fmt x =
+ Format.pp_print_char fmt '@';
+ Format.pp_print_string fmt (Simple_vector.get names (tag x))
+ end)
+
+ include HC
+
+ let tag: t -> int = function
+ | Cl.Sem(tag,_,_,_) -> tag
+
+ let index v ty =
+ let cl =
+ HC.hashcons3
+ (fun tag sem v ty -> Cl.Sem(tag,ty,sem,v))
+ D.key v ty in
+ let i = tag cl in
+ Simple_vector.inc_size (i+1) Cl.names;
+ begin
+ if Simple_vector.is_uninitialized Cl.names i then
+ let s = Strings.find_new_name Cl.used_names ""
+ (** TODO use Sem.print or Sem.print_debug *) in
+ Simple_vector.set Cl.names i s
+ end;
+ cl
+
+ (** Just used for checking the typability *)
+ let _cl : t -> Cl.t = function
+ | Cl.Sem(tag,ty,sem,v) -> Cl.Sem(tag,ty,sem,v)
+
+ (** IF the previous function is typable this one is correct:
+ I'm not able to defined is without obj.magic
+ *)
+ let cl : t -> Cl.t = Obj.magic
+
+ let sem : t -> D.t = function
+ | Cl.Sem(_,_,sem,v) ->
+ match Sem.Eq.coerce_type sem D.key with
+ | Eqtype.Eq -> v
+
+ let ty : t -> Ty.t = function
+ | Cl.Sem(_,ty,_,_) -> ty
+
+ let () =
+ VSem.inc_size D.key defined_sem;
+ assert (if not (VSem.is_uninitialized defined_sem D.key)
+ then raise AlreadyRegisteredKey else true);
+ let sem = (module D: Sem with type t = D.t) in
+ VSem.set defined_sem D.key sem;
+ Cl.SemIndex.set Cl.semindex D.key (fun v ty -> cl (index v ty))
+
+end
+
module Env = Make_key(struct end)
type 'a env = 'a Env.k
@@ -185,8 +327,6 @@ module Dem = Make_key2(struct end)
type ('k,'d) dem = ('k,'d) Dem.k
-
-
module Print = struct (** Cutting the knot for printer *)
type psem = { mutable psem : 'a. ('a sem -> 'a Pp.printer)}
@@ -210,3 +350,27 @@ module Print = struct (** Cutting the knot for printer *)
end
+
+module Only_for_solver = struct
+ type sem_of_cl =
+ | Fresh: sem_of_cl
+ | Sem: 'a sem * 'a -> sem_of_cl
+
+ let sem_of_cl = function
+ | Cl.Fresh _ -> Fresh
+ | Cl.Sem (_,_,sem,v) -> Sem(sem,v)
+end
+
+
+let check_initialization () =
+ let well_initialized = ref true in
+
+ Sem.iter {Sem.iter = fun sem ->
+ if VSem.is_uninitialized defined_sem sem then begin
+ Format.eprintf
+ "[Warning] The set of values %a is not registered@." Sem.print sem;
+ well_initialized := false;
+ end};
+
+ !well_initialized
+
diff --git a/src/types.mli b/src/types.mli
index a9343f9dd..0e2aeef8c 100644
--- a/src/types.mli
+++ b/src/types.mli
@@ -49,20 +49,6 @@ module Ty : sig
end
-(** Classes *)
-module Cl : sig
- type t = private int
- include Datatype with type t := t
-
- val create: string -> Ty.t -> t
- (** the string is used as the prefix for the debug output *)
-
- val rename: t -> string -> unit
- (** to use with care *)
-
- val ty: t -> Ty.t
-end
-
(** the key shouldn't be used before its registration and shouldn't be
registered again *)
exception UnregisteredKey
@@ -77,6 +63,7 @@ module type Key = sig
val compare: 'a k -> 'b k -> int
val equal: 'a k -> 'b k -> bool
val hash : 'a k -> int
+ val tag: 'a k -> int
type iter = {iter : 'a. 'a k -> unit}
val iter : iter -> unit
@@ -108,9 +95,53 @@ module Dom: Key
type 'a dom = 'a Dom.k
type 'a sem = 'a Sem.k
+module type Sem = sig
+ include Datatype
+
+ val key: t sem
+end
+
+val get_sem: 'a sem -> (module Sem with type t = 'a)
+val sem_uninitialized: 'a sem -> bool
+
module Env: Key
type 'a env = 'a Env.k
+(** Classes *)
+module Cl : sig
+ include Datatype
+
+ val fresh: string -> Ty.t -> t
+ (** the string is used as the prefix for the debug output *)
+
+ val rename: t -> string -> unit
+ (** to use with care *)
+
+ val ty: t -> Ty.t
+
+ val index: 'a sem -> 'a -> Ty.t -> t
+ (** Return the corresponding cl from a semantical value *)
+
+end
+
+module RegisterSem (D:Sem) : sig
+ (** clsem *)
+ include Datatype
+
+ val index: D.t -> Ty.t -> t
+ (** Return a clsem from a semantical value *)
+
+ val cl: t -> Cl.t
+ (** Return a class from a clsem *)
+
+ val ty: t -> Ty.t
+ (** Return the type from a clsem *)
+
+ val sem: t -> D.t
+ (** Return the sem from a clsem *)
+
+end
+
module type Key2 = sig
module K: Datatype
type ('k,'d) k = private K.t
@@ -156,3 +187,18 @@ module Print : sig (** Cutting the knot for printer *)
end
+
+val check_initialization: unit -> bool
+(** Check if the initialization of all the dom, sem and dem have been done *)
+
+(** Only for Solver *)
+module Only_for_solver: sig
+ type sem_of_cl =
+ | Fresh: sem_of_cl
+ | Sem: 'a sem * 'a -> sem_of_cl
+
+ val sem_of_cl:
+ Cl.t -> sem_of_cl
+ (** give the sem associated with a cl, make sens only for not merged
+ class. So only the module solver can use it *)
+end
diff --git a/src/uninterp.ml b/src/uninterp.ml
index 0675176f2..857a27839 100644
--- a/src/uninterp.ml
+++ b/src/uninterp.ml
@@ -70,7 +70,7 @@ module Th = struct
end
-module Registered = RegisterSem(Th)
+module ThE = RegisterSem(Th)
let funty_ctr = Ty.Constr.create "Fun"
let funty = Ty.ctr funty_ctr
@@ -100,7 +100,7 @@ let result_to_dec = Cl.H.create 20
let fresh_fun _env ~result ~arity name =
assert (arity > 0);
- let cl = Cl.create name funty in
+ let cl = Cl.fresh name funty in
let result_info = Ty.H.find_def result_of_sort None result in
Cl.H.add result_to_dec cl (result,arity,result_info);
cl
@@ -133,16 +133,16 @@ let fun5 t ty s =
(fun t x1 x2 x3 x4 x5 -> app_fun t f [x1;x2;x3;x4;x5])
-type expsubst = Th.t
+type expsubst = ThE.t
let expsubst : expsubst Explanation.exp =
Explanation.Exp.create_key "Uninterp"
module DaemonPropa = struct
- type k = Th.t
+ type k = ThE.t
type d = unit
let key = Demon.Key.create "Uninterp.DaemonPropa"
- module Key = Th
+ module Key = ThE
module Data = DUnit
let is_unborn d v =
@@ -158,17 +158,17 @@ module DaemonPropa = struct
[EventChange(f,()); EventChange(g,())]
let immediate = true (** can be false *)
- let wakeup d (App(f,g) as v) _ev =
- match Delayed.get_cl_sem d sem v with
- | None -> assert false
- | Some own ->
+ let wakeup d (clsem:k) _ev =
+ match ThE.sem clsem with
+ | App(f,g) as v ->
Debug.dprintf4 debug "[Uninterp] @[wakeup own %a v:%a@]@\n"
- Cl.print own Th.print v;
+ Cl.print (ThE.cl clsem) Th.print v;
let v' = App(Delayed.find d f, Delayed.find d g) in
assert (not (Th.equal v v'));
- let pexp = Delayed.mk_pexp d expsubst v in
- Delayed.set_sem d pexp sem own v';
- Demon.AliveRedirected v'
+ let pexp = Delayed.mk_pexp d expsubst clsem in
+ Delayed.set_sem d pexp sem (ThE.cl clsem) v';
+ let clsem' = ThE.index v' (ThE.ty clsem) in
+ Demon.AliveRedirected clsem'
end
module RDaemonPropa = Demon.Key.Register(DaemonPropa)
@@ -189,17 +189,19 @@ module DaemonInit = struct
begin match Sem.Eq.coerce_type sem sem' with
| Eqtype.Eq ->
Debug.dprintf2 debug "[Uninterp] @[init %a@]@\n" Th.print v;
- if DaemonPropa.is_unborn d v then
+ let clsem = ThE.index v (Cl.ty own) in
+ assert (Cl.equal own (ThE.cl clsem));
+ if DaemonPropa.is_unborn d clsem then
match v with
| App(f,g) ->
Delayed.propagate d f; Delayed.propagate d g;
let f' = Delayed.find d f in
let g' = Delayed.find d g in
if Cl.equal f' f && Cl.equal g' g then
- DaemonPropa.attach d f g (v : t)
+ DaemonPropa.attach d f g clsem
else
let v' = App(f',g') in
- let pexp = Delayed.mk_pexp d expsubst v in
+ let pexp = Delayed.mk_pexp d expsubst clsem in
Delayed.set_sem d pexp sem own v'
end
| _ -> raise UnwaitedEvent
@@ -225,8 +227,10 @@ module ExpSubst = struct
type t = expsubst
- let print fmt (App(f,g)) =
- Format.fprintf fmt "Subst(%a,%a)" Cl.print f Cl.print g
+ let print fmt clsem =
+ match ThE.sem clsem with
+ | App(f,g) ->
+ Format.fprintf fmt "Subst(%a,%a)" Cl.print f Cl.print g
(*
let iterexp t age = function
@@ -238,18 +242,12 @@ module ExpSubst = struct
let analyse :
type a. Conflict.ComputeConflict.t ->
Explanation.age -> a Explanation.con -> t -> a Conflict.rescon =
- fun t age con exp ->
- begin match exp with
+ fun t age con clsem ->
+ begin match ThE.sem clsem with
| App(f,g) as v ->
let fty = Cl.ty f in
let gty = Cl.ty g in
let deps = Deps.empty in
- let own,pexp = get_sem t sem v in
- let ty = Cl.ty own in
- let deps =
- (** TODO separate the first Merge(UF) from the others(GenEquality)? *)
- Equality.GenEquality.sem t deps age sem v pexp ty in
- add_deps t deps;
Equality.GenEquality.equality t age f (get_repr_at t age f) fty;
Equality.GenEquality.equality t age g (get_repr_at t age g) gty
end;
diff --git a/src/util/hashcons.ml b/src/util/hashcons.ml
index f8fe6565f..7175b6596 100644
--- a/src/util/hashcons.ml
+++ b/src/util/hashcons.ml
@@ -27,24 +27,40 @@ module type S =
sig
include Datatype
val hashcons : t -> t
+ val hashcons0: (int -> t) -> t
+ val hashcons1: (int -> 'a -> t) -> 'a -> t
+ val hashcons2: (int -> 'a -> 'b -> t) -> 'a -> 'b -> t
+ val hashcons3: (int -> 'a -> 'b -> 'c -> t) -> 'a -> 'b -> 'c -> t
val iter : (t -> unit) -> unit
- val stats : unit -> int * int * int * int * int * int
+ type cat
+ val stats : cat -> int * int * int * int * int * int
+ val fresh_tag: unit -> int
end
-module Make(H : HashedType) : (S with type t = H.t) =
+
+module MakeTag(H : sig include HashedType
+ val next_tag: unit -> int
+ val incr_tag: unit -> unit
+ end) :
+ (S with type t = H.t and type cat := unit) =
struct
module WH = Weak.Make (H)
- let next_tag = ref 0
+ let fresh_tag () = let tag = H.next_tag () in H.incr_tag (); tag
let htable = WH.create 5003
- let hashcons d =
- let d = H.set_tag !next_tag d in
+ let hashcons' d =
let o = WH.merge htable d in
- if o == d then incr next_tag;
+ if o == d then H.incr_tag ();
o
+ let hashcons d = hashcons' (H.set_tag (H.next_tag ()) d)
+ let hashcons0 f = hashcons' (f (H.next_tag ()))
+ let hashcons1 f a = hashcons' (f (H.next_tag ()) a)
+ let hashcons2 f a b = hashcons' (f (H.next_tag ()) a b)
+ let hashcons3 f a b c = hashcons' (f (H.next_tag ()) a b c)
+
let iter f = WH.iter f htable
let stats () = WH.stats htable
@@ -61,6 +77,63 @@ struct
end
+module Make(H : HashedType) :
+ (S with type t = H.t and type cat := unit) =
+ MakeTag(struct
+ include H
+ let next_tag, incr_tag = Util.get_counter ()
+ end)
+
+module MakeCat(H : sig include HashedType val category: t -> int end) :
+ (sig include S with type t = H.t and type cat := int
+ val new_category: int -> unit
+ val iter_cat: (t -> unit) -> int -> unit
+ end) =
+struct
+ module WH = Weak.Make (H)
+
+ let next_tag = ref 0
+ let fresh_tag () = let tag = !next_tag in incr next_tag; tag
+
+ let htable: WH.t Simple_vector.t = Simple_vector.create 10
+
+ let new_category cat =
+ Simple_vector.inc_size cat htable;
+ assert (Simple_vector.is_uninitialized htable cat);
+ Simple_vector.set htable cat (WH.create 64)
+
+ let hashcons' d =
+ let o = WH.merge (Simple_vector.get htable (H.category d)) d in
+ if o == d then incr next_tag;
+ o
+
+ let hashcons d = hashcons' (H.set_tag !next_tag d)
+ let hashcons0 f = hashcons' (f !next_tag)
+ let hashcons1 f a = hashcons' (f !next_tag a)
+ let hashcons2 f a b = hashcons' (f !next_tag a b)
+ let hashcons3 f a b c = hashcons' (f !next_tag a b c)
+
+ let iter f =
+ Simple_vector.iter_initialized (fun h -> WH.iter f h) htable
+
+ let iter_cat f cat =
+ WH.iter f (Simple_vector.get htable cat)
+
+ let stats cat = WH.stats (Simple_vector.get htable cat)
+
+ module T = struct
+ type t = H.t
+ let hash = H.tag
+ let equal ts1 ts2 = ts1 == ts2
+ let compare ts1 ts2 = Pervasives.compare (H.tag ts1) (H.tag ts2)
+ let print = H.print
+ end
+
+ include MkDatatype(T)
+
+end
+
+
let combine acc n = n * 65599 + acc
let combine2 acc n1 n2 = combine acc (combine n1 n2)
let combine3 acc n1 n2 n3 = combine acc (combine n1 (combine n2 n3))
diff --git a/src/util/hashcons.mli b/src/util/hashcons.mli
index 321b8b42c..5034ee5bb 100644
--- a/src/util/hashcons.mli
+++ b/src/util/hashcons.mli
@@ -43,17 +43,42 @@ module type S =
in the table and returns it.
*)
+ (** Versions where you don't create a value before modifying it *)
+ val hashcons0: (int -> t) -> t
+ val hashcons1: (int -> 'a -> t) -> 'a -> t
+ val hashcons2: (int -> 'a -> 'b -> t) -> 'a -> 'b -> t
+ val hashcons3: (int -> 'a -> 'b -> 'c -> t) -> 'a -> 'b -> 'c -> t
+
val iter : (t -> unit) -> unit
(** [iter f] iterates [f] over all elements of the table . *)
- val stats : unit -> int * int * int * int * int * int
+
+ type cat
+ val stats : cat -> int * int * int * int * int * int
(** Return statistics on the table. The numbers are, in order:
table length, number of entries, sum of bucket lengths,
smallest bucket length, median bucket length, biggest
bucket length. *)
+
+ val fresh_tag: unit -> int
+ (** get a fresh tag *)
end
-module Make(H : HashedType) : (S with type t = H.t)
+module Make(H : HashedType) : (S with type t = H.t
+ and type cat := unit)
+
+module MakeCat(H : sig include HashedType val category: t -> int end) :
+ (sig
+ include S with type t = H.t and type cat := int
+ val new_category: int -> unit
+ val iter_cat: (t -> unit) -> int -> unit
+ end)
+
+module MakeTag(H : sig include HashedType
+ val next_tag: unit -> int
+ val incr_tag: unit -> unit
+ end) :
+ (S with type t = H.t and type cat := unit)
(* helpers *)
diff --git a/src/util/strings.ml b/src/util/strings.ml
index bb0d41aac..9be4e27f4 100644
--- a/src/util/strings.ml
+++ b/src/util/strings.ml
@@ -85,6 +85,24 @@ module type Fresh = sig
val rename: t -> string -> unit
end
+
+let find_new_name used_names s =
+ let rec aux used_names s n =
+ let sid = s^(string_of_int n) in
+ if DStr.H.mem used_names sid then
+ aux used_names s (n+1)
+ else sid,(n+1) in
+ try
+ let n = DStr.H.find used_names s in
+ let s',n = aux used_names s n in
+ DStr.H.replace used_names s n;
+ DStr.H.add used_names s' 2;
+ s'
+ with Not_found ->
+ DStr.H.add used_names s 2;
+ s
+
+
module Fresh (X : sig end) = struct
include DInt
let names = Simple_vector.create 100
@@ -94,28 +112,12 @@ module Fresh (X : sig end) = struct
Format.pp_print_char fmt '@';
Format.pp_print_string fmt (Simple_vector.get names (x:>int))
- let find_new_name s =
- let rec aux s n =
- let sid = s^(string_of_int n) in
- if DStr.H.mem used_names sid then
- aux s (n+1)
- else sid,(n+1) in
- try
- let n = DStr.H.find used_names s in
- let s',n = aux s n in
- DStr.H.replace used_names s n;
- DStr.H.add used_names s' 2;
- s'
- with Not_found ->
- DStr.H.add used_names s 2;
- s
-
let c = ref (-1)
let create s =
incr c;
let i = !c in
- let s = find_new_name s in
+ let s = find_new_name used_names s in
Simple_vector.inc_size (i+1) names;
Simple_vector.set names i s;
i
@@ -129,6 +131,6 @@ module Fresh (X : sig end) = struct
let hint_size () = !c + 1
let rename i s =
- let s = find_new_name s in
+ let s = find_new_name used_names s in
Simple_vector.set names i s
end
diff --git a/src/util/strings.mli b/src/util/strings.mli
index cf686a071..c111433ef 100644
--- a/src/util/strings.mli
+++ b/src/util/strings.mli
@@ -45,3 +45,5 @@ module type Fresh = sig
end
module Fresh (X : sig end) : Fresh
+
+val find_new_name: int Stdlib.DStr.H.t -> string -> string
diff --git a/src/util/util.ml b/src/util/util.ml
index 50aa37ec7..513f3b6c5 100644
--- a/src/util/util.ml
+++ b/src/util/util.ml
@@ -40,3 +40,6 @@ let any_fn pr _ t = pr t && raise FoldSkip
let ttrue _ = true
let ffalse _ = false
+let get_counter () =
+ let r = ref 0 in
+ (fun () -> !r), (fun () -> incr r)
diff --git a/src/util/util.mli b/src/util/util.mli
index 192406563..141b4581c 100644
--- a/src/util/util.mli
+++ b/src/util/util.mli
@@ -41,3 +41,6 @@ val ffalse : 'a -> bool
val ttrue : 'a -> bool
(** [ttrue] constant function [true] *)
+
+val get_counter: unit -> (unit -> int) * (unit -> unit)
+(** a strictly increasing counter (next_tag,incr_tag) *)
diff --git a/src/variable.ml b/src/variable.ml
index c87d4bb13..7e338f61b 100644
--- a/src/variable.ml
+++ b/src/variable.ml
@@ -56,7 +56,7 @@ let cst =
assert (Ty.equal (Cl.ty cl) ty);
cl
with Not_found ->
- let cl = Cl.create s ty in
+ let cl = Cl.fresh s ty in
DStr.H.add h s cl;
cl
@@ -68,7 +68,7 @@ let register_sort ~dec ty =
let fresh t ty s =
- let cl = Cl.create s ty in
+ let cl = Cl.fresh s ty in
(try add_dec ~dec:(Ty.H.find dec_of_sort ty) t cl;
with Not_found -> ());
cl
diff --git a/src/variable.mli b/src/variable.mli
index 977b49483..ac794884f 100644
--- a/src/variable.mli
+++ b/src/variable.mli
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
open Types
-open Solver
type make_dec = Cl.t -> Explanation.chogen
--
GitLab