diff --git a/src/bool.ml b/src/bool.ml
index 544df1b495a3261045c3e5b2be03fef7b11b4d6f..85a9c589d1cebc836297804d757e734935184944 100644
--- a/src/bool.ml
+++ b/src/bool.ml
@@ -35,6 +35,9 @@ let dom : bool dom = Conflict.dom_bool
let cl_true = Cl.create "⊤" ty
let cl_false = Cl.create "⊥" ty
+let union_disjoint m1 m2 =
+ Cl.M.union (fun _ b1 b2 -> assert (b1 == b2); Some b1) m1 m2
+
let index t sem v = Delayed.index t sem v ty
let with_other = ref false
@@ -445,15 +448,21 @@ let _or_and b env l =
let _or = _or_and false
let _and = _or_and true
+let mk_clause env m =
+ if Cl.M.is_empty m then cl_false
+ else let len = Cl.M.cardinal m in
+ if len = 1 then
+ let cl,b = Cl.M.choose m in
+ if b then _not env cl else cl
+ else
+ index env sem {topnot=false;
+ lits = IArray.of_iter len
+ (fun iter -> Cl.M.iter (fun cl b -> iter (cl,b)) m)}
let _false _ = cl_false
let set_true env pexp cl = set_bool env pexp cl true
-let () =
- Conflict.set_true := set_true;
- Conflict.is_false := is_false
-
let set_false env pexp cl = set_bool env pexp cl false
let chobool = Explanation.Cho.create_key "Bool.cho"
@@ -484,7 +493,7 @@ module ChoBool = struct
match Explanation.Con.Eq.eq_type conclause con with
| None -> GOther (conclause,s)
| Some Eqtype.Eq -> GRequested s in
- ComputeConflict.set_dec_cho t dom cl chobool cl;
+ ComputeConflict.set_dec_cho t chobool cl;
return (Cl.M.singleton cl b)
@@ -523,11 +532,19 @@ end
module EChoClause = Conflict.RegisterCho(ChoClause)
open Conflict
-let mk_permanent_equality: (Cl.t * Cl.t -> Cl.t) ref =
- ref (fun _ -> assert false)
-
type clause_conflict = bool Types.Cl.M.t
+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 get_con = Conflict.fold_requested (fun acc _ s ->
Cl.M.union
(fun _ b1 b2 -> assert (DBool.equal b1 b2); Some b1) s acc)
@@ -672,6 +689,7 @@ end
module EP = Conflict.RegisterExp(ExpProp)
module ConClause = struct
+ open Conflict
type t = bool Cl.M.t
@@ -684,64 +702,39 @@ module ConClause = struct
let key = conclause
- class finalized_one cl : Conflict.finalized = object
- method print fmt = Cl.print fmt cl
- method test d =
- match is d cl with
- | None -> ToDecide(Explanation.GCho(chobool,cl))
- | Some true -> True
- | Some false -> False
- method conflict_add _ = cl
- end
-
- exception Found of Conflict.testconflict
class finalized v : Conflict.finalized = object
- method print fmt = Th.print fmt v
+ method print fmt =
+ Pp.print_iter2 Cl.M.iter Pp.semi Pp.comma Cl.print DBool.print fmt v
method test d =
- match isnot v with
- | Some cl ->
- begin match is d cl with
- | None ->
- let chogen = Explanation.GCho(choclause,v) in
- ToDecide(chogen)
- | Some true -> False
- | Some false -> True
- end
- | None ->
- try
- iter (fun (cl,sign) ->
- match is d cl with
- | None ->
- let chogen = Explanation.GCho(choclause,v) in
- raise (Found (ToDecide(chogen)))
- | Some b ->
- Debug.dprintf4 debug "finalize: %a = %b dom %b@."
- Cl.print cl sign b;
- if mulbool b sign then
- raise (Found True)) v;
- False
- with Found x -> x
- method conflict_add d =
- index d sem v
+ try
+ Cl.M.fold_left (fun acc cl sign ->
+ match is d cl with
+ | None -> ToDecide
+ | Some b ->
+ Debug.dprintf4 debug "finalize: %a = %b dom %b@."
+ Cl.print cl sign b;
+ if mulbool b sign
+ then raise Exit
+ else acc) False v
+ with Exit -> True
+ method decide :
+ 'a. 'a Conflict.fold_decisions -> Solver.Delayed.t -> 'a -> 'a =
+ fun f d acc ->
+ Cl.M.fold_left (fun acc cl b ->
+ match is d cl with
+ | None ->
+ f.fold_decisions acc chobool cl (not b)
+ | Some _ -> acc) acc v
+ method conflict_add _ = v
end
- let finalize t sl =
- let union = Cl.M.union (fun _ b1 b2 -> assert (b1 == b2); Some b1) in
- let s = List.fold_left union Cl.M.empty sl in
- Cl.M.iter (fun cl _ -> Conflict.ComputeConflict.dep_dec t dom cl) s;
+ let finalize _ sl =
+ let s = Bag.fold_left union_disjoint Cl.M.empty sl in
Debug.dprintf2 Conflict.print_conflicts "[Bool] @[conflict: %a@]@." print s;
match Cl.M.cardinal s with
| 0 -> None
- | 1 ->
- let cl,b = (Cl.M.choose s) in
- if b
- then Some (new finalized ({topnot = true;
- lits = IArray.of_list [cl,false]} ))
- else Some (new finalized_one cl)
- | l ->
- let lits = IArray.of_iter l
- (fun f -> Cl.M.iter (fun cl b -> f (cl,b)) s) in
- Some (new finalized {topnot = false; lits})
+ | _ ->
+ Some (new finalized s)
let same_sem t age _sem c1 c2 _cl1 _cl2 =
@@ -753,42 +746,34 @@ module ConClause = struct
let propacl t _age clo rcl =
match clo, rcl with
| (_true, cl) when Cl.equal _true cl_true ->
- ComputeConflict.set_dec_cho t dom cl chobool cl;
+ ComputeConflict.set_dec_cho t chobool cl;
GRequested (Cl.M.singleton cl true)
| (cl, _true) when Cl.equal _true cl_true ->
- ComputeConflict.set_dec_cho t dom cl chobool cl;
+ ComputeConflict.set_dec_cho t chobool cl;
GRequested (Cl.M.singleton cl true)
| (_false, cl) when Cl.equal _false cl_false ->
- ComputeConflict.set_dec_cho t dom cl chobool cl;
+ ComputeConflict.set_dec_cho t chobool cl;
GRequested (Cl.M.singleton cl false)
| (cl, _false) when Cl.equal _false cl_false ->
- ComputeConflict.set_dec_cho t dom cl chobool cl;
+ ComputeConflict.set_dec_cho t chobool cl;
GRequested (Cl.M.singleton cl false)
| _ ->
- let eq = !mk_permanent_equality (clo,rcl) in
- ComputeConflict.set_dec_cho t dom eq chobool eq;
- GRequested (Cl.M.singleton eq true)
+ !mk_conequal t clo rcl
let propasem t _age sem v cl =
(** TODO ty bool if sem is bool? *)
- let eq = !mk_permanent_equality (cl,new_permanent sem v (Cl.ty cl)) in
- ComputeConflict.set_dec_cho t dom eq chobool eq;
- GRequested (Cl.M.singleton eq true)
+ mk_conequal_sem.mk_conequal_sem t sem v cl
let propadom:
type a. ComputeConflict.t ->
Explanation.Age.t -> a dom -> Cl.t -> a -> t rescon =
- fun t age dom' cl bval ->
+ fun _ _ dom' cl bval ->
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
- begin
- ComputeConflict.set_dec_age t dom cl age;
- GRequested (Cl.M.singleton cl bval)
- end
-
+ GRequested (Cl.M.singleton cl bval)
end
module EC = Conflict.RegisterCon(ConClause)
diff --git a/src/bool.mli b/src/bool.mli
index 406aef5d09c81f591fbef9491624a0066df170ca..e1ac11403f961722ae904089e1249db1e3b5100b 100644
--- a/src/bool.mli
+++ b/src/bool.mli
@@ -57,9 +57,6 @@ val make_dec: Variable.make_dec
val ty: Ty.t
val ty_ctr: Ty.Constr.t
-(** For equality *)
-val mk_permanent_equality : (Cl.t * Cl.t -> Cl.t) ref
-
(** For conflict *)
type clause_conflict = bool Types.Cl.M.t
@@ -72,3 +69,18 @@ val get_dom:
Conflict.ComputeConflict.t ->
Explanation.age ->
Types.Cl.t -> clause_conflict -> clause_conflict
+
+val union_disjoint: clause_conflict -> clause_conflict -> clause_conflict
+
+val mk_clause: Solver.Delayed.t -> clause_conflict -> Cl.t
+
+(** For equality *)
+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 3911da49426ed6f4c66e37f89ed53412ed9bc50f..6a29641585103aa78fad79ec89a4b409450217cf 100644
--- a/src/conflict.ml
+++ b/src/conflict.ml
@@ -26,7 +26,6 @@ open Explanation
exception DontKnowThisCon
exception DontKnowThisDec of Dom.K.t * Cl.t
-exception SemChoUsedMoreThanOnce
let debug = Debug.register_info_flag
~desc:"for@ the@ main@ part@ of@ conflicts."
@@ -48,10 +47,6 @@ type explearnt =
let explearnt : explearnt exp = Exp.create_key "Explanation.learnt_exp"
let dom_bool : bool dom = Dom.create_key "bool"
-let set_true =
- ref (fun _ _ _ -> assert false : Solver.Delayed.t -> pexp -> Cl.t -> unit)
-let is_false =
- ref (fun _ _ -> assert false : Solver.Delayed.t -> Cl.t -> bool)
type tofind =
| FDom : Cl.t * 'a dom -> tofind
@@ -317,7 +312,6 @@ let rec get_repr_at age cl = function
| CRepr | CMerge _ -> cl
(** Con_iter *)
-
type con_iter = {
csolver : Solver.t;
cneeded : rlist needed;
@@ -325,7 +319,6 @@ type con_iter = {
mutable cdeps : Explanation.Deps.t;
ctrail : Explanation.t;
cseen : Explanation.concache Simple_vector.t; (** to clear at the end *)
- cchoage: Age.t ChoH.t;
cdomcho: chogen Cl.H.t Dom.Vector.t;
cdomage: Age.t Cl.H.t Dom.Vector.t;
}
@@ -338,7 +331,6 @@ let create_con_iter solver needed t =
cdeps = Deps.empty;
ctrail = t;
cseen = Simple_vector.create 0;
- cchoage = ChoH.create 10;
cdomcho = Dom.Vector.create (Dom.hint_size ());
cdomage = Dom.Vector.create (Dom.hint_size ());
} in
@@ -362,10 +354,6 @@ let mk_confact (type a) (con : a con) : a rescon =
let return_nothing con = return con confact ()
-type con_age = { t : con_iter;
- mutable max_1 : age; mutable max_2 : age; (* max_1 > max_2 *)
- mutable decs: chogen list}
-
type exp_iter = {
older : tofind list array;
mutable tage : age;
@@ -387,14 +375,20 @@ let print_dom_can_be_at_current fmt v =
type testconflict =
- | True (* true in this context *)
| False (* false in this context *)
- | ToDecide of chogen (* Can be decided *)
+ | True (* true in this context *)
+ | ToDecide (* can be decided *)
+
+
+type 'a fold_decisions =
+ {fold_decisions : 'k 'd. ('a -> ('k,'d) cho -> 'k -> 'd -> 'a) }
class type finalized = object
method print: Format.formatter -> unit
- method conflict_add: Solver.Delayed.t -> Cl.t
+ method conflict_add: Solver.Delayed.t -> bool Cl.M.t
method test: Solver.Delayed.t -> testconflict
+ method decide: 'a. 'a fold_decisions -> Solver.Delayed.t -> 'a -> 'a
+ (** to call only when test is [Todecide] *)
end
let print_finalized fmt fin = fin#print fmt
@@ -418,7 +412,7 @@ module type Con' = sig
val propacl : con_iter -> Age.t -> Cl.t -> Cl.t -> t rescon
- val finalize: con_age -> t list -> finalized option
+ val finalize: con_iter -> t Bag.t -> finalized option
end
@@ -633,16 +627,11 @@ module ComputeConflict = struct
r
(** add because we will have multiple value *)
- let set_dec_cho t dom cl cho k =
- Cl.H.add (Dom.Vector.get t.cdomcho dom) cl (GCho(cho,k))
- let set_dec_age t dom cl age =
- Cl.H.add (Dom.Vector.get t.cdomage dom) cl age
+ let set_dec_cho t cho k =
+ t.cdeps <- Deps.add_chogen t.cdeps (GCho(cho,k))
- let set_cho_sem_age t chogen age =
- ChoH.change (function
- | None -> Some age
- | Some age' when Age.equal age age' -> Some age'
- | _ -> raise SemChoUsedMoreThanOnce) t.cchoage chogen
+ let set_dec_cho_cond t dom cl cho k =
+ Cl.H.add (Dom.Vector.get t.cdomcho dom) cl (GCho(cho,k))
let compute_con_iter solver t needed pexp =
let state = create_con_iter solver needed t in
@@ -655,89 +644,56 @@ module ComputeConflict = struct
Simple_vector.iter_initialized Concache.clear state.cseen;
state
- type iter = con_age
+ type iter = con_iter
let dep_dec (type a) iter (dom: a dom) cl : unit =
let lchogen =
- Cl.H.find_all (Dom.Vector.get iter.t.cdomcho dom) cl in
+ Cl.H.find_all (Dom.Vector.get iter.cdomcho dom) cl in
let lchoage =
- Cl.H.find_all (Dom.Vector.get iter.t.cdomage dom) cl in
+ Cl.H.find_all (Dom.Vector.get iter.cdomage dom) cl in
if lchogen == [] && lchoage == [] then
raise (DontKnowThisDec (((dom : a Dom.k) :> Dom.K.t),cl));
- let max_age age =
- if Age.compare age iter.max_1 > 0 then begin
- iter.max_1 <- age;
- iter.max_2 <- iter.max_1 end
- else if Age.compare age iter.max_1 = 0 then
- ()
- else if Age.compare age iter.max_2 > 0 then begin
- iter.max_2 <- age;
- end
- in
- let iter_chogen chogen =
- iter.decs <- chogen::iter.decs;
- try
- let age = ChoH.find iter.t.cchoage chogen in
- max_age age
- with Not_found -> (* An additional chogen not the original one *) ()
- in
- List.iter iter_chogen lchogen;
- List.iter max_age lchoage
+ iter.cdeps <- List.fold_left Deps.add_chogen iter.cdeps lchogen
- type cons_learnt = Cl.t IArray.t
- let cons_learnt : cons_learnt sem = Sem.create_key "Core.cons_learnt"
+ class wrapp ctags (l:finalized list) : finalized = object
+ method print fmt = (Pp.print_list Pp.semi (fun fmt c -> c#print fmt)) fmt l
+ method test d =
+ try
+ List.fold_left (fun acc c ->
+ match c#test d with
+ | False -> acc
+ | True -> raise Exit
+ | ToDecide -> ToDecide) False l
+ with Exit -> True
+
+ method decide:
+ 'a. 'a fold_decisions -> Solver.Delayed.t -> 'a -> 'a =
+ fun f d acc ->
+ List.fold_left (fun acc (c:finalized) -> c#decide f d acc) acc l
- class wrapp ctags (c:finalized) = object
- method print = c#print
- method test = c#test
method conflict_add d =
- let cl = c#conflict_add d in
- (** What is learnt is a general consequence *)
- let pexp = Solver.Delayed.mk_pexp ~age:Age.min
- d explearnt (ExpLearnt ctags) in
- Solver.Delayed.propagate d cl;
- (!set_true) d pexp cl;
- cl
+ List.fold_left
+ (fun acc c -> Cl.M.union (fun _ b1 b2 -> assert (b1 == b2); Some b1)
+ (c#conflict_add d) acc) Cl.M.empty l
end
- let finalize t =
- let state = { t = t; max_1 = Age.min; max_2 = Age.min;
- decs = []} in
+ let finalize state =
let fold (type b) acc con l =
if Con.equal con confact then acc
else
let con = get_con con in
let module C = (val con : Con' with type t = b) in
- match C.finalize state (Bag.elements l) with
+ match C.finalize state l with
| None -> acc
| Some mcl -> mcl::acc
in
let acc =
- Conunknown.fold {Conunknown.fold} [] (Deps.cunknown t.cdeps) in
- let tags = Deps.tags t.cdeps in
+ Conunknown.fold {Conunknown.fold} [] (Deps.cunknown state.cdeps) in
+ let tags = Deps.tags state.cdeps in
+ let decs = Deps.decs state.cdeps in
match acc with
- | [] -> None,tags, state.decs
- | [mcl] ->
- assert (Age.compare state.max_1 state.max_2 >= 0);
- let age = state.max_2 in
- Some (new wrapp tags mcl), tags, state.decs
- | l ->
- assert false
-(* assert (Age.compare state.max_1 state.max_2 >= 0);
- let age = state.max_2 in
- let new_finalized_list = new_finalized_list () in
- let mk d =
- let finl = List.map (fun mcl -> mcl d) l in
- let cll = List.map (fun fin -> fin.fin_cl) finl in
- let cl = Solver.Delayed.index d cons_learnt (IArray.of_list cll) in
- let pexp = Solver.Delayed.mk_pexp ~age:Age.min
- d explearnt (ExpLearnt t.ctags) in
- Solver.Delayed.propagate d cl;
- (!set_true) d pexp cl;
- {fin_cl = cl;
- fin_dec = GCho(cholearnt, new_finalized_list finl)}
- in
- Some (mk,age), t.ctags, state.decs*)
+ | [] -> None,tags, decs
+ | l -> Some (new wrapp tags l), tags, decs
end
@@ -1208,7 +1164,7 @@ module type Con = sig
val propacl : con_iter -> Age.t -> Cl.t -> Cl.t -> t rescon
- val finalize: ComputeConflict.iter -> t list -> finalized option
+ val finalize: ComputeConflict.iter -> t Bag.t -> finalized option
end
@@ -1301,6 +1257,9 @@ let choose_decision (type k) (type d) d (cho : (k,d) cho) k =
| DecTodo v ->
DecTodo (fun d dec -> Cho.make_decision d dec k v)
+let make_decision (type k) (type d) d (cho : (k,d) cho) k v dec =
+ let module Cho = (val (get_cho cho)) in
+ Cho.make_decision d dec k v
let print_pcho fmt = function
| Pcho(dec,cho,k,d) ->
@@ -1329,8 +1288,6 @@ module ExpCho = struct
let analyse (type a) t _ (con: a con) (Pcho(dec,cho,k,v)) =
let f (type k) (type d) t con (cho : (k,d) cho) k v =
- let age = Explanation.age_of_dec dec in
- ComputeConflict.set_cho_sem_age t (GCho(cho,k)) age;
let module C = (val get_cho cho) in
C.analyse t con k v in
f t con cho k v
@@ -1504,188 +1461,6 @@ end
module EExpLearnt = RegisterExp(ExpLearnt)
-module SemLearnt = struct
- module T = struct
- type t = Cl.t IArray.t
-
- let equal l1 l2 = IArray.equal Cl.equal l1 l2
- let hash l1 = IArray.hash Cl.hash l1
- let compare l1 l2 = IArray.compare Cl.compare l1 l2
- let print fmt t1 = (Pp.print_iter1 IArray.iter Pp.comma Cl.print) fmt t1
-
- end
- include T
- module M = Map.Make(T)
- module S = M.Set
- module H = XHashtbl.Make(T)
-
- let key = ComputeConflict.cons_learnt
-
-end
-
-module ESemLearnt = Solver.RegisterSem(SemLearnt)
-
-type expprop = SemLearnt.t * Cl.t (* own *) * Cl.t (* propa *)
-let expprop : expprop Explanation.exp =
- Explanation.Exp.create_key "Bool.prop"
-
-module DaemonLearnt = struct
- type k = SemLearnt.t
- type d = int * int
- let key = Dem.create_key "Core.DemLearnt"
-
- module Key = SemLearnt
- module Data = struct
- type t = d
-
- let print fmt (p1,p2) =
- Format.fprintf fmt "watch:%i next:%i" p1 p2
- end
-
- let immediate = false
-
- open Solver
-
- let wakeup d v ev =
- let propa_cl cl =
- let pexp : pexp = assert false in
- (!set_true) d pexp cl;
- raise Exit
- in
- let rec find_next cl_watched dir pos =
- assert (dir == 1 || dir == -1);
- if (dir == 1 && pos == IArray.length v) ||
- (dir == -1 && pos == -1)
- then
- propa_cl cl_watched
- else
- let cl = IArray.get v pos in
- if not (Delayed.is_propagated d cl)
- then pos
- else
- match Delayed.get_dom d dom_bool cl with
- | None -> pos
- | Some true -> raise Exit
- | Some false -> find_next cl_watched dir (dir+pos)
- in
- let rec find_watch dir pos =
- assert (dir == 1 || dir == -1);
- let cl = IArray.get v pos in
- Delayed.propagate d cl;
- if (dir == 1 && pos == IArray.length v - 1) ||
- (dir == -1 && pos == 0)
- then
- propa_cl cl
- else
- match Delayed.get_dom d dom_bool cl with
- | None -> cl,pos
- | Some true -> raise Exit
- | Some false -> find_watch dir (dir+pos)
- in
- try
- List.iter (function
- | Events.Fired.EventDom(cl,dom,(watched,next))
- when Dom.equal dom dom_bool ->
- let dir = if watched < 0 then -1 else 1 in
- begin match Delayed.get_dom d dom_bool cl with
- | None -> raise Impossible
- | Some true -> raise Exit
- | Some false ->
- let clwatched, watched = find_watch dir next in
- let next = find_next clwatched dir (watched+dir) in
- Delayed.attach_events d key v
- [Events.Create.EventDom(clwatched,dom_bool,(dir*watched,next))]
- end
- | _ -> raise UnwaitedEvent)
- ev;
- Solver.AliveReattached
- with Exit ->
- Solver.AliveStopped
-end
-
-module EDaemonLearnt = Solver.RegisterDem(DaemonLearnt)
-
-module ChoLearnt = struct
-
- module Key = MakeMSH(struct
- type t = chogen list * int
- let tag = snd
- let print fmt (_,i) = Format.fprintf fmt "Learnt(%i)" i
- end)
-
- module Data = struct
- type t = Solver.Delayed.t -> dec -> unit
- let print fmt _ = Format.fprintf fmt "ChoLearnt"
- end
-
- let choose_decision d (finl,_) =
- let rec fin_dec d = function
- | [] -> DecNo
- | GCho(cho,k)::l ->
- match choose_decision d cho k with
- | DecNo -> fin_dec d l
- | DecTodo _ as td -> td in
- fin_dec d finl
-
- let make_decision d dec _ f = f d dec
-
- let analyse _ _ _ _ = assert false
-
- let key = cholearnt
-
-end
-
-module EChoLearnt = RegisterCho(ChoLearnt)
-
-module ExpProp = struct
- type t = expprop
-
- let print fmt = function
- | (v,own,cl) ->
- Format.fprintf fmt "Bcp(%a,%a = %a)"
- SemLearnt.print v Cl.print own Cl.print cl
-
- let sem = ComputeConflict.cons_learnt
-
- let iterexp t age = function
- | (v,_,propa) ->
- IterExp.need_sem t age sem v;
- IArray.iter (fun cl ->
- if not (Cl.equal cl propa) then
- IterExp.need_dom t age cl dom_bool) v
-
- let analyse :
- type a. ComputeConflict.t ->
- Explanation.age -> a Explanation.con -> t -> a rescon =
- fun t age con exp ->
- let get_con acc t = function
- | GRequested s ->
- Cl.M.union (fun _ b1 b2 -> assert (b1 == b2); Some b1) s acc
- | GOther (con,c) -> ComputeConflict.unknown_con t con c; acc in
- let get_rlist acc rl = fold_rescon_list t get_con age conclause acc rl in
- let s =
- match exp with
- | (v,_,propa) ->
- let s = Cl.M.empty in
- let s = get_rlist s (ComputeConflict.get_sem t sem v) in
- IArray.fold (fun s cl ->
- if (Cl.equal cl propa) then s else
- let rlist,pexp = ComputeConflict.get_dom t age cl dom_bool in
- let s = get_con s t (ComputeConflict.get_pexp t pexp conclause) in
- get_rlist s rlist
- ) s v
- in
- match Explanation.Con.Eq.eq_type conclause con with
- | None -> GOther (conclause,s)
- | Some Eqtype.Eq -> GRequested s
-
-
- let key = expprop
-
-end
-
-module EP = RegisterExp(ExpProp)
-
let check_initialization () =
let well_initialized = ref true in
diff --git a/src/conflict.mli b/src/conflict.mli
index 129e9fbac7dfef18cb3d910d34b25e5ac15ac157..0f6ffaa86b5a7ec50984e0a690c37097f5d64694 100644
--- a/src/conflict.mli
+++ b/src/conflict.mli
@@ -88,8 +88,9 @@ module ComputeConflict: sig
val unknown_con: t -> 'b con -> 'b -> unit
(** same as [Deps.add_unknown_con Deps.empty con a] followed by add_deps *)
- val set_dec_cho : t -> 'a dom -> Cl.t -> ('k,'d) cho -> 'k -> unit
- val set_dec_age : t -> 'a dom -> Cl.t -> Age.t -> unit
+
+ val set_dec_cho : t -> ('k,'d) cho -> 'k -> unit
+ val set_dec_cho_cond : t -> 'a dom -> Cl.t -> ('k,'d) cho -> 'k -> unit
type iter
val dep_dec: iter -> 'a dom -> Cl.t -> unit
@@ -137,14 +138,19 @@ end
module RegisterExp(E:Exp) : sig end
type testconflict =
- | True (* true in this context *)
| False (* false in this context *)
- | ToDecide of chogen (* Can be decided *)
+ | True (* true in this context *)
+ | ToDecide (* can be decided *)
+
+type 'a fold_decisions =
+ {fold_decisions : 'k 'd. ('a -> ('k,'d) cho -> 'k -> 'd -> 'a) }
class type finalized = object
method print: Format.formatter -> unit
- method conflict_add: Solver.Delayed.t -> Cl.t
+ method conflict_add: Solver.Delayed.t -> bool Cl.M.t
method test: Solver.Delayed.t -> testconflict
+ method decide: 'a. 'a fold_decisions -> Solver.Delayed.t -> 'a -> 'a
+ (** to call only when test is [Todecide] *)
end
val print_finalized: finalized Pp.printer
@@ -170,7 +176,7 @@ module type Con = sig
(* cl1 -> cl2 repr *)
(** Finalization and propagation of the conflict *)
- val finalize: ComputeConflict.iter -> t list -> finalized option
+ val finalize: ComputeConflict.iter -> t Bag.t -> finalized option
(** None if the conflict is empty (always satisfied constraint)
TODO better doc we produce the conflcit ro the explication?
*)
@@ -211,7 +217,7 @@ module RegisterCho(C:Cho) : sig end
val analyse:
Solver.t -> pexp -> (* 'a must be a conflict *)
- finalized option * tags * chogen list
+ finalized option * tags * chogen Bag.t
(* maximum age not in conflict *)
val choose_decision:
@@ -219,6 +225,9 @@ val choose_decision:
(Solver.Delayed.t -> dec -> unit) decdone
+val make_decision:
+ Solver.Delayed.t -> ('k,'d) cho -> 'k -> 'd -> dec -> unit
+
val print_pexp: pexp Pp.printer
val print_chogen: Explanation.chogen Pp.printer
@@ -241,8 +250,6 @@ val is_explimit : pexp -> explimit option
(** Stuff common to Boolean *)
val dom_bool: bool dom
-val set_true: (Solver.Delayed.t -> pexp -> Cl.t -> unit) ref
-val is_false: (Solver.Delayed.t -> Cl.t -> bool) ref
val conclause: bool Cl.M.t Explanation.con
val print_conflicts: Debug.flag
@@ -250,3 +257,8 @@ val print_decision: Debug.flag
(** Helpers for scheduler *)
module ChoGenH : Exthtbl.Hashtbl.S with type key = chogen
+
+type explearnt =
+| ExpLearnt: Tags.t -> explearnt
+
+val explearnt : explearnt exp
diff --git a/src/equality.ml b/src/equality.ml
index 615baecd1a088a8990ccd64e6e58234c17bdd1b6..229f3cd6460e72912add3de580d0329e38f5b4b7 100644
--- a/src/equality.ml
+++ b/src/equality.ml
@@ -135,6 +135,30 @@ end
module Registered = RegisterSem(Th)
+
+(** API *)
+
+let equality t cll =
+ try
+ let fold acc e = Cl.S.add_new Exit e acc in
+ let s = List.fold_left fold Cl.S.empty cll in
+ Delayed.index t sem s Bool.ty
+ with Exit ->
+ Bool._true t
+
+let disequality t cll = Bool._not t (equality t cll)
+
+let is_equal t cl1 cl2 = Cl.equal (Delayed.find t cl1) (Delayed.find t cl2)
+let is_disequal t cl1 cl2 =
+ let dom1 = Delayed.get_dom t dom cl1 in
+ let dom2 = Delayed.get_dom t dom cl2 in
+ match dom1, dom2 with
+ | Some s1, Some s2 -> not (Dis.disjoint s1 s2)
+ | _ -> false
+
+
+
+
let new_tag =
let c = ref (-1) in
fun () -> incr c;
@@ -207,9 +231,197 @@ let norm_set d own v =
Bool.set_true d pexp own;
None
-let choequal = Explanation.Cho.create_key "Equal.cho"
+(** Conflict *)
+module EqConflict = struct
+
+ type eqconflict =
+ | Eq : Cl.t * Cl.t * bool -> eqconflict
+ | Sem: 'a sem * 'a * Cl.t -> eqconflict
+
+ module K = Stdlib.MkDatatype(struct
+
+ type t = eqconflict
+
+ let print fmt = function
+ | Eq(cl1,cl2,b) ->
+ if b then
+ Format.fprintf fmt "%a==%a" Cl.print cl1 Cl.print cl2
+ else
+ Format.fprintf fmt "%a!=%a" Cl.print cl1 Cl.print cl2
+ | Sem(sem,v,cl) ->
+ Format.fprintf fmt "%a:%a=%a"
+ Sem.print sem (Solver.print_sem sem) v 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), Sem(sem2,v2,c2) ->
+ Cl.equal c1 c2 &&
+ 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
+ | Eq(cla1,clb1,b1), Eq(cla2,clb2,b2) ->
+ let c = Cl.compare cla1 cla2 in
+ if c != 0 then c else
+ let c = Cl.compare clb1 clb2 in
+ if c != 0 then c else
+ DBool.compare b1 b2
+ | Sem(sem1,v1,c1), Sem(sem2,v2,c2) ->
+ let c = Cl.compare c1 c2 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
-module ChoEqual = struct
+ 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) ->
+ Hashcons.combine2
+ (Cl.hash c1) (Sem.hash sem1)
+ (let module Sem = (val Solver.get_sem sem1) in
+ Sem.hash v1)
+ end)
+
+ include K
+
+ let mk_eq cl1 cl2 b =
+ if Cl.compare cl1 cl2 <= 0
+ then Eq(cl1,cl2,b)
+ else Eq(cl2,cl1,b)
+
+ let mk_sem sem v cl = Sem(sem,v,cl)
+
+
+end
+
+let choequal : (EqConflict.t,unit) Explanation.cho =
+ Explanation.Cho.create_key "Equal.cho"
+
+(** Default equality/disequality conflict *)
+module ConDefaultEq = struct
+ open Conflict
+ open EqConflict
+
+ type t = EqConflict.t Bag.t
+
+ let print fmt b =
+ Bag.print Pp.semi EqConflict.print fmt b
+
+ let key = Explanation.Con.create_key "Equality.gen"
+
+ let print_eqs fmt eqs =
+ Pp.print_iter1 EqConflict.S.iter Pp.semi EqConflict.print fmt eqs
+
+ class finalized eqs : Conflict.finalized = object
+ method print fmt = print_eqs fmt eqs
+ method test d =
+ let fold acc = function
+ | Eq(cl1,cl2,b) ->
+ let cl1 = Delayed.find d cl1 in
+ let cl2 = Delayed.find d cl2 in
+ let return b =
+ if b then raise Exit (** true *) else acc (** false *) in
+ if Cl.equal cl1 cl2 then return (not b)
+ else if is_disequal d cl1 cl2 then
+ return b
+ else ToDecide
+ | Sem(sem,v,cl) ->
+ match Delayed.is_sem_present d sem v with
+ | Some own when Cl.equal (Delayed.find d cl) own -> acc (** false *)
+ | _ -> ToDecide in
+ try
+ EqConflict.S.fold_left fold False eqs
+ with Exit -> True
+ method decide :
+ 'a. 'a Conflict.fold_decisions -> Solver.Delayed.t -> 'a -> 'a =
+ fun f d acc ->
+ let fold acc = function
+ | Eq(cl1,cl2,_) as c ->
+ let cl1 = Delayed.find d cl1 in
+ let cl2 = Delayed.find d cl2 in
+ if Cl.equal cl1 cl2 || is_disequal d cl1 cl2 then acc
+ else f.fold_decisions acc choequal c ()
+ | Sem(sem,v,cl) as c ->
+ match Delayed.is_sem_present d sem v with
+ | Some own when Cl.equal (Delayed.find d cl) own -> acc
+ | _ -> f.fold_decisions acc choequal c () in
+ EqConflict.S.fold_left fold acc eqs
+ method conflict_add d =
+ let fold acc = function
+ | Eq(cl1,cl2,b) ->
+ let eq = equality d [cl1;cl2] in
+ Cl.M.add eq b acc
+ | Sem(sem,v,cl) ->
+ let cl' = Delayed.index d sem v (Cl.ty cl) in
+ let eq = equality d [cl;cl'] in
+ Cl.M.add eq true acc in
+ EqConflict.S.fold_left fold Cl.M.empty eqs
+ end
+
+ let finalize _ l =
+ let m =
+ Bag.fold_left (fun acc b ->
+ Bag.fold_left (fun acc e -> EqConflict.S.add e acc) acc b)
+ EqConflict.S.empty l in
+ Debug.dprintf2 Conflict.print_conflicts "[Equality] @[conflict: %a@]@."
+ print_eqs m;
+ if EqConflict.S.is_empty m then None
+ else Some (new finalized m)
+
+ let get_con = Conflict.fold_requested (fun b1 _ b2 -> Bag.concat b1 b2)
+ let get_cons t age = fold_rescon_list t get_con age key
+
+ let same_sem t age _sem c1 c2 _cl1 _cl2 =
+ let b = get_cons t age Bag.empty c1 in
+ let b = get_con b t c2 in
+ GRequested b
+
+ let propacl t _ cl rcl =
+ let v = mk_eq cl rcl true in
+ ComputeConflict.set_dec_cho t choequal v;
+ GRequested(Bag.elt v)
+
+ (** For the extension *)
+ let propasem t _ sem v cl =
+ let v = mk_sem sem v cl in
+ ComputeConflict.set_dec_cho t choequal v;
+ GRequested(Bag.elt v)
+
+ (** used only for equality *)
+ let propadom _ _ _ _ _ = raise Impossible
+
+end
+
+module EConDefaultEq = Conflict.RegisterCon(ConDefaultEq)
+
+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))
+
+module ChoEquals = struct
open Conflict
module Key = Th
@@ -220,11 +432,7 @@ module ChoEqual = struct
Cl.print cl1 Cl.print cl2
end
-
- let mk_permanent_equality (cl1,cl2) =
- assert (not (Cl.equal cl1 cl2));
- let s = Cl.S.add cl1 (Cl.S.singleton cl2) in
- Solver.new_permanent sem s Bool.ty
+ let key = Explanation.Cho.create_key "Equals.cho"
let choose_decision d v0 =
match Delayed.is_sem_present d sem v0 with
@@ -246,29 +454,61 @@ module ChoEqual = struct
let make_decision d dec v (cl1,cl2) =
Debug.dprintf4 Conflict.print_decision
"[Equality] @[decide on merge of %a and %a@]@." Cl.print cl1 Cl.print cl2;
- let pexp = Explanation.mk_pcho dec choequal v (cl1,cl2) in
+ let pexp = Explanation.mk_pcho dec key v (cl1,cl2) in
Delayed.merge d pexp cl1 cl2
- let analyse (type a) t (con: a Explanation.con) v p =
- let return (s:bool Types.Cl.M.t) : a rescon =
- match Explanation.Con.Eq.eq_type conclause con with
- | None -> GOther (conclause,s)
- | Some Eqtype.Eq -> GRequested s in
- let cl = mk_permanent_equality p in
- ComputeConflict.set_dec_cho t Bool.dom cl choequal v;
- ComputeConflict.set_dec_cho t Bool.dom cl Bool.chobool cl;
- return (Cl.M.singleton cl true)
+ let analyse (type a) t (con: a Explanation.con) v (cl1,cl2) =
+ ComputeConflict.set_dec_cho t key v;
+ return con ConDefaultEq.key (Bag.elt (EqConflict.mk_eq cl1 cl2 true))
+
+end
+
+module EChoEquals = Conflict.RegisterCho(ChoEquals)
+
+module ChoEqual = struct
+ open Conflict
+
+ module Key = EqConflict
+ module Data = DUnit
let key = choequal
+ let choose_decision d = function
+ | EqConflict.Eq(cl1,cl2,_) ->
+ let cl1 = Delayed.find d cl1 in
+ let cl2 = Delayed.find d cl2 in
+ if Cl.equal cl1 cl2 || is_disequal d cl1 cl2 then DecNo
+ else DecTodo ()
+ | EqConflict.Sem(sem,v,cl) ->
+ match Delayed.is_sem_present d sem v with
+ | Some own when Cl.equal (Delayed.find d cl) own -> DecNo
+ | _ -> DecTodo ()
+
+
+ let make_decision d dec v () =
+ Debug.dprintf2 Conflict.print_decision
+ "[Equality] @[decide on %a@]@." EqConflict.print v;
+ let pexp = Explanation.mk_pcho dec key v () in
+ match v with
+ | EqConflict.Eq(cl1,cl2,true) ->
+ Delayed.merge d pexp cl1 cl2
+ | EqConflict.Eq(cl1,cl2,false) ->
+ let _dis, stag = new_tag () in
+ let set_dom cl = Delayed.set_dom_merge d pexp dom cl (Some (stag ())) in
+ set_dom cl1; set_dom cl2
+ | EqConflict.Sem(sem,v,cl) ->
+ let cl' = Delayed.index d sem v (Cl.ty cl) in
+ Delayed.merge d pexp cl' cl
+
+ let analyse (type a) t (con: a Explanation.con) v () =
+ ComputeConflict.set_dec_cho t choequal v;
+ return con ConDefaultEq.key (Bag.elt v)
+
end
module EChoEqual = Conflict.RegisterCho(ChoEqual)
-let mk_permanent_equality = ChoEqual.mk_permanent_equality
-let () = Bool.mk_permanent_equality := ChoEqual.mk_permanent_equality
-
let norm_dom d own v0 =
match norm_set d own v0 with
| None -> AliveStopped
@@ -308,45 +548,6 @@ let norm_dom d own v0 =
AliveReattached
-(** Default equality/disequality conflict *)
-module ConDefaultEq = struct
- open Conflict
-
- type t = unit
-
- let print _ _ = ()
-
- let key = Explanation.Con.create_key "Equality.gen"
-
- let finalize _ _ = raise Impossible
-
- let get_con = Conflict.fold_requested (fun () _ () -> ())
- let get_cons t age = fold_rescon_list t get_con age key
-
- let same_sem t age _sem c1 c2 _cl1 _cl2 =
- get_cons t age () c1;
- get_con () t c2;
- GRequested ()
-
- let propacl t _ cl rcl =
- let eq = mk_permanent_equality (cl,rcl) in
- ComputeConflict.set_dec_cho t Bool.dom eq Bool.chobool eq;
- GOther(conclause,(Cl.M.singleton eq true))
-
- (** For the extension *)
- let propasem t _ sem v cl =
- let eq =
- mk_permanent_equality (cl,new_permanent sem v (Cl.ty cl)) in
- ComputeConflict.set_dec_cho t Bool.dom eq Bool.chobool eq;
- GOther(conclause,(Cl.M.singleton eq true))
-
- (** used only for equality *)
- let propadom _ _ _ _ _ = raise Impossible
-
-end
-
-module EConDefaultEq = Conflict.RegisterCon(ConDefaultEq)
-
(** Register equality/disequality exp for types *)
type special_equality = {
@@ -383,36 +584,41 @@ module GenEquality = struct
open Conflict
let equality t age r1 r2 =
- ConDefaultEq.get_cons t age () r1;
- ConDefaultEq.get_cons t age () r2
+ let b = Bag.empty in
+ let b = ConDefaultEq.get_cons t age b r1 in
+ let b = ConDefaultEq.get_cons t age b r2 in
+ ComputeConflict.unknown_con t ConDefaultEq.key b
let expspecial ~dodec f con =
let get_con = Conflict.fold_requested_deps f in
let get_cons t age = fold_rescon_list_deps t get_con age con in
let get_sem t deps age _ _ r =
- let accdeps = (),deps in
- let (),deps = get_cons t age accdeps r in
- deps in
+ 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
+ in
{ equality; disequality = equality;
merged = (fun t deps age pexp _ r1 _ r2 ->
let rs,deps' =
ComputeConflict.get_pexp_deps t pexp con in
let deps = Deps.concat deps deps' in
- let accdeps = (),deps in
+ let accdeps = Bag.empty,deps in
let accdeps = get_con accdeps t rs in
let accdeps = get_cons t age accdeps r1 in
- let (),deps = get_cons t age accdeps r2 in
- deps);
+ let b,deps = get_cons t age accdeps r2 in
+ Explanation.Deps.add_unknown_con deps ConDefaultEq.key b);
repr = (fun t deps age _ r1 ->
- let accdeps = (),deps in
- let (),deps = get_cons t age accdeps r1 in
- deps);
+ let accdeps = Bag.empty,deps in
+ let b,deps = get_cons t age accdeps r1 in
+ Explanation.Deps.add_unknown_con deps ConDefaultEq.key b);
sem = get_sem;
dodec;
}
let def_expspecial =
- expspecial ~dodec:true (fun accdeps _ () -> accdeps) ConDefaultEq.key
+ expspecial ~dodec:true
+ (fun (b1,deps) _ b2 -> Bag.concat b1 b2, deps)
+ ConDefaultEq.key
let find_expspecial ty =
Ty.H.find_def expspecial_of_sort def_expspecial ty
@@ -444,12 +650,13 @@ module GenEquality = struct
let dodec ty = (find_expspecial ty).dodec
- let get_con = Conflict.fold_requested_deps (fun accdeps _ () -> accdeps)
+ 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 age ConDefaultEq.key
let get_sem t deps age _ _ r =
- let accdeps = (),deps in
- let (),deps = get_cons t age accdeps r in
- deps
+ 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
@@ -461,7 +668,7 @@ end
let register_sort_con ty ~dodec con = register_sort ty
(GenEquality.expspecial ~dodec
- (fun ((),deps) _ x -> (),Explanation.Deps.add_unknown_con deps con x)
+ (fun (b,deps) _ x -> b,Explanation.Deps.add_unknown_con deps con x)
con)
let () = register_sort_con Bool.ty ~dodec:false Conflict.conclause
@@ -511,7 +718,7 @@ module DaemonInit = struct
if GenEquality.dodec (Th.get_ty v) then begin
Debug.dprintf4 debug "[Equality] @[ask_dec on %a for %a@]@."
Cl.print own Th.print v;
- Delayed.ask_decision d (Explanation.GCho(choequal,v));
+ Delayed.ask_decision d (Explanation.GCho(ChoEquals.key,v));
end
| _ -> ()
end
@@ -619,12 +826,13 @@ module ExpMerge = struct
return con conclause (Cl.M.singleton cl true)
*)
| Some cl1, Some cl2 ->
- let eq = mk_permanent_equality (cl1,cl2) in
- ComputeConflict.set_dec_cho t Bool.dom eq Bool.chobool eq;
- return con conclause (Cl.M.add eq false clauses)
+ let v = EqConflict.mk_eq cl1 cl2 false in
+ ComputeConflict.set_dec_cho t ChoEqual.key v;
+ ComputeConflict.unknown_con t ConDefaultEq.key (Bag.elt v);
+ return con conclause clauses
| None, None ->
(** The conflict comes from a propagation bool -> equality *)
- return con conclause Cl.M.empty
+ return con conclause clauses
| _ -> raise Impossible (** the tag can't come from two different place *)
let analyse :
@@ -784,25 +992,6 @@ end
module EExpSubst = Conflict.RegisterExp(ExpSubst)
-(** API *)
-
-let equality t cll =
- try
- let fold acc e = Cl.S.add_new Exit e acc in
- let s = List.fold_left fold Cl.S.empty cll in
- Delayed.index t sem s Bool.ty
- with Exit ->
- Bool._true t
-
-let disequality t cll = Bool._not t (equality t cll)
-
-let is_equal t cl1 cl2 = Cl.equal (Delayed.find t cl1) (Delayed.find t cl2)
-let is_disequal t cl1 cl2 =
- let dom1 = Delayed.get_dom t dom cl1 in
- let dom2 = Delayed.get_dom t dom cl2 in
- match dom1, dom2 with
- | Some s1, Some s2 -> not (Dis.disjoint s1 s2)
- | _ -> false
(** ITE *)
module TITE = struct
diff --git a/src/equality.mli b/src/equality.mli
index 3cf68dc4a97419494fc50888fb3cf30eb8e2290c..5eef234f419714c2c1af7829e3a99f887c70ac53 100644
--- a/src/equality.mli
+++ b/src/equality.mli
@@ -33,8 +33,6 @@ val ite : Solver.d -> Cl.t -> Cl.t -> Cl.t -> Cl.t
val propagate : Solver.d -> unit
-val mk_permanent_equality: Cl.t * Cl.t -> Cl.t
-
open Explanation
open Conflict
diff --git a/src/explanation.ml b/src/explanation.ml
index f5af86453270b152ffec7fe8f5c36fa6696a7fee..a5444f59da7e86d8e0e4f5e715c000e52a2da126 100644
--- a/src/explanation.ml
+++ b/src/explanation.ml
@@ -96,15 +96,18 @@ module Deps = struct
type t = {
cunknown : conunknown;
ctags : tags;
+ decs : chogen Bag.t;
}
let tags t = t.ctags
let cunknown t = t.cunknown
+ let decs t = t.decs
let empty = {
cunknown = Conunknown.empty;
ctags = Tags.empty;
+ decs = Bag.empty;
}
let is_empty t = t == empty
@@ -116,6 +119,7 @@ module Deps = struct
ctags = Tags.union t1.ctags t2.ctags;
cunknown = Conunknown.union {Conunknown.union = conunion}
t1.cunknown t2.cunknown;
+ decs = Bag.concat t1.decs t2.decs;
}
let add_tags t tags =
@@ -128,6 +132,9 @@ module Deps = struct
con a t.cunknown
}
+ let add_chogen t chogen =
+ { t with decs = Bag.add chogen t.decs }
+
end
module Concache = struct
diff --git a/src/explanation.mli b/src/explanation.mli
index f382e21bfbf2432ae60dcb9368e21fd1579626be..687f817a6e8e95921fbb7634f1e45bd1b0be74b8 100644
--- a/src/explanation.mli
+++ b/src/explanation.mli
@@ -148,6 +148,7 @@ module Deps : sig
val tags : t -> tags
val cunknown: t -> conunknown
+ val decs : t -> chogen Bag.t
val empty: t
val is_empty: t -> bool
@@ -155,6 +156,7 @@ module Deps : sig
val add_tags: t -> tags -> t
val add_unknown_con: t -> 'a con -> 'a -> t
+ val add_chogen: t -> chogen -> t
end
diff --git a/src/scheduler_queue.ml b/src/scheduler_queue.ml
index 35d30503d1f74c4d5611d2ca35743fc5ee0323cf..dc9df96d0289d90edc7403bb86787142c206b249 100644
--- a/src/scheduler_queue.ml
+++ b/src/scheduler_queue.ml
@@ -45,6 +45,9 @@ module Att = struct
type prio = float
type db = float Conflict.ChoGenH.t
+ let get_prio db chogen =
+ Conflict.ChoGenH.find_def db 0. chogen
+
let le (x:t) (xp:float) (y:t) (yp:float) =
match x, y with
| Daemon (x,_) , Daemon (y,_) -> x <= y
@@ -54,7 +57,7 @@ module Att = struct
| Decision _, Daemon _ -> false
let reprio db = function
| Daemon _ -> 0.
- | Decision (_,chogen) -> Conflict.ChoGenH.find_def db 0. chogen
+ | Decision (_,chogen) -> get_prio db chogen
end
exception Contradiction
@@ -167,17 +170,42 @@ let new_delayed =
conflict_analysis t pexp
*)
-let rec apply_learnt learntdec llearnt t d =
+type choice =
+ | Choice: ('k,'d) Explanation.cho * 'k * 'd * float -> choice
+ | NoChoice
+
+let rec apply_learnt (learntdec: Conflict.finalized) tags llearnt t d =
try
Debug.dprintf0 debug "[Scheduler] Apply previously learnt@.";
- List.iter (fun f ->
- Debug.dprintf2 debug "[Scheduler] @[Apply %a@]@."
- Conflict.print_finalized f;
- ignore (f#conflict_add d); S.flush d) llearnt;
+ let iter_learnt f =
+ Debug.dprintf2 debug "[Scheduler] @[Apply %a@]@."
+ Conflict.print_finalized f;
+ let clauses = f#conflict_add d in
+ let cl = Bool.mk_clause d clauses in
+ (** What is learnt is a general consequence *)
+ let pexp = Solver.Delayed.mk_pexp ~age:Explanation.Age.min
+ d Conflict.explearnt (Conflict.ExpLearnt tags) in
+ Solver.Delayed.propagate d cl;
+ Bool.set_true d pexp cl;
+ S.flush d in
+ List.iter iter_learnt llearnt;
+ iter_learnt learntdec;
run_until_dec t d;
Debug.dprintf0 debug "[Scheduler] Apply learntdec@.";
- let Explanation.GCho(cho,k) = learntdec in
- run_dec t d t.wakeup_daemons cho k
+ (** Do directly a decision on the last conflict learnt *)
+ let fold_decisions acc cho' k' d' =
+ match acc with
+ | NoChoice ->
+ let f' = Att.get_prio t.decprio (Explanation.GCho(cho',k')) in
+ Choice(cho',k',d',f')
+ | Choice(_,_,_,f) ->
+ let f' = Att.get_prio t.decprio (Explanation.GCho(cho',k')) in
+ if f >= f' then acc else Choice(cho',k',d',f')
+ in
+ match learntdec#decide {Conflict.fold_decisions} d NoChoice with
+ | NoChoice -> d
+ | Choice(cho,k,v,_) ->
+ run_dec t d cho k v
with S.Contradiction pexp ->
Debug.dprintf0 debug "[Scheduler] Contradiction during apply learnt@.";
conflict_analysis t pexp
@@ -219,9 +247,9 @@ and conflict_analysis t pexp =
Debug.incr stats_con;
if Solver.current_nbdec t.solver_state = 0 then raise Contradiction
else
- let learnt,_tags, decs = Conflict.analyse t.solver_state pexp in
+ let learnt,tags, decs = Conflict.analyse t.solver_state pexp in
t.var_inc := !(t.var_inc) *. var_decay;
- List.iter (update_prio t) decs;
+ Bag.iter (update_prio t) decs;
let learnt = match learnt with
| None -> raise Contradiction
| Some learnt -> learnt in
@@ -236,22 +264,22 @@ and conflict_analysis t pexp =
let llearnt_all = List.rev_append llearnt prev.pre_learnt in
let open Conflict in
match learnt#test d with
- | True -> raise Types.Impossible (** understand why *)
+ | True -> raise Types.Impossible (** understand why that happend *)
| False -> rewind t learnt llearnt_all prev.pre_prev_scheduler_state
- | ToDecide learntdec ->
+ | ToDecide ->
(** we found the level *)
Debug.dprintf4 debug_pushpop "[Scheduler] Pop to level %a %a@."
Explanation.Age.print prevage print_level t;
t.learnt <- learnt::llearnt_all;
- d,learntdec,learnt::llearnt
+ d,learnt,llearnt
in
let d,learntdec,llearnt =
rewind t learnt t.learnt t.prev_scheduler_state in
t.wakeup_daemons <- Prio.reprio t.decprio t.wakeup_daemons;
- apply_learnt learntdec llearnt t d
+ apply_learnt learntdec tags llearnt t d
-and run_dec:
+and try_run_dec:
type k d. t -> Delayed.t -> Prio.t -> ((k,d) Explanation.cho) -> k ->
Delayed.t = fun t d prio cho k ->
(** First we verify its the decision is at this point needed *)
@@ -277,6 +305,26 @@ and run_dec:
Debug.dprintf0 debug "[Scheduler] Contradiction@.";
conflict_analysis t pexp
+and run_dec:
+ type k d. t -> Delayed.t -> ((k,d) Explanation.cho) -> k -> d ->
+ Delayed.t = fun t d cho k v ->
+ (** First we verify its the decision is at this point needed *)
+ try
+ Debug.incr stats_dec;
+ S.delayed_stop d;
+ Debug.dprintf2 debug_pushpop
+ "[Scheduler] Make decision: level %a@."
+ print_level t;
+ (** The registered state keep the old prio *)
+ push t (Explanation.GCho(cho,k));
+ let declevel = Explanation.new_dec (S.get_trail t.solver_state) in
+ let d = new_delayed t in
+ Conflict.make_decision d cho k v declevel;
+ d
+ with S.Contradiction pexp ->
+ Debug.dprintf0 debug "[Scheduler] Contradiction@.";
+ conflict_analysis t pexp
+
and run_until_dec t d =
let act = Prio.min t.wakeup_daemons in
match act with
@@ -303,7 +351,7 @@ let run_one_step t d =
Debug.dprintf0 debug "[Scheduler] Contradiction@.";
conflict_analysis t pexp
end
- | Att.Decision (_,Explanation.GCho(cho,k)) -> run_dec t d prio cho k
+ | Att.Decision (_,Explanation.GCho(cho,k)) -> try_run_dec t d prio cho k
let rec flush t d =
try
diff --git a/src/solver.ml b/src/solver.ml
index 90db3b06e8e460116dc125951e1099b6cacb9241..17dd080e905b8f6c7e84a753ddfe97ece48bcff3 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -1114,10 +1114,6 @@ module Delayed = struct
) [] (Cl.M.find_def Bag.empty cl d.env.event)
- (** permanent class that will always have a semantic value associated to it *)
- type gensem =
- | GSem: (t -> Cl.t -> unit) option * 'a sem * 'a -> gensem
- let permanent : gensem Cl.H.t = Cl.H.create 16
(** *)
@@ -1138,12 +1134,6 @@ module Delayed = struct
t.env.when_propa <- when_propa;
List.iter (fun f -> f t cl) todos
end;
- (** Here or delayed? *)
- try
- let (GSem(propa,sem,v)) = Cl.H.find permanent cl in
- begin match propa with None -> () | Some propa -> propa t cl end;
- add_pending_set_sem t Explanation.pexpfact sem cl v
- with Not_found -> ()
end
let set_sem_pending (type a) t pexp (sem : a sem) cl v =
@@ -1717,13 +1707,6 @@ let get_direct_dom t dom cl =
assert (t.current_delayed == unsat_delayed);
get_direct_dom t dom cl
-let new_permanent ?propa sem v ty =
- let s = Pp.string_of_wnl (print_sem sem) v in
- let cl = Cl.create s ty in
- Cl.H.add Delayed.permanent cl (Delayed.GSem(propa,sem,v));
- cl
-
-
module type Ro = sig
type t
(** {3 Immediate information} *)
diff --git a/src/solver.mli b/src/solver.mli
index 4a6249098d1faee92e270617cf84d20b72a05133..aa1824196b15a34b23fa047d112427b75a0ce094 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -287,12 +287,6 @@ val get_sem_first : t -> 'a sem -> 'a -> (Cl.t * age) option
val get_direct_dom : t -> 'a dom -> Cl.t -> 'a option
(** dom of the class directly (the last time modified) *)
-val new_permanent:
- ?propa:(Delayed.t -> Cl.t -> unit) ->
- 'a sem -> 'a -> Ty.t -> Cl.t
-(** To use (when there is nothing else)
- in conflict when creating new classes *)
-
(** {2 Implementation Specifics } *)
(** Because this module is implemented with persistent datastructure *)
diff --git a/src/types.ml b/src/types.ml
index 520469c49a62e717a08ce22f59fb27ec810043c4..52e49a3724a9b8b97d41f38c2582b994cfbbd5b8 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -84,6 +84,7 @@ module type Key = sig
module K: Datatype
type 'a k = private K.t
val print: 'a k Pp.printer
+ val compare: 'a k -> 'b k -> int
val equal: 'a k -> 'b k -> bool
val hash : 'a k -> int
@@ -111,6 +112,7 @@ module Make_key(X:sig end) : Key = struct
type 'a k = K.t (* >= 0 *)
let print fmt x = K.print fmt x
+ let compare x y = K.compare x y
let equal x y = K.equal x y
let hash x = K.hash x
diff --git a/src/types.mli b/src/types.mli
index d4442ef48d93c6d8d94402a8b7ec9abf8e19d5c8..a62baf6c13580fa60c43ef18872205b77b4310bf 100644
--- a/src/types.mli
+++ b/src/types.mli
@@ -72,6 +72,7 @@ module type Key = sig
type 'a k = private K.t
val print: 'a k Pp.printer
+ val compare: 'a k -> 'b k -> int
val equal: 'a k -> 'b k -> bool
val hash : 'a k -> int
diff --git a/src/util/bag.ml b/src/util/bag.ml
index c8500b13129912af35fff55170a379c45733046e..3096378799cbd0f26128a87493b3a742bbe74ecb 100644
--- a/src/util/bag.ml
+++ b/src/util/bag.ml
@@ -153,6 +153,11 @@ let rec singleton = function
| Some x -> if is_empty b then Some x else None
| None -> if is_empty a then singleton b else None
+let rec choose = function
+ | Empty | List [] -> raise Not_found
+ | Elt x | List(x::_) | Add(x,_) | App(_,x) -> x
+ | Concat(a,b) -> try choose a with Not_found -> choose b
+
let rec collect t xs =
match t with
| Elt x -> x :: xs
diff --git a/src/util/bag.mli b/src/util/bag.mli
index 2363f347589d39a2a8dcb7c58853ec57d91b1ecc..8cdc7157bb7ee2ca766575c03d79cecdb935573a 100644
--- a/src/util/bag.mli
+++ b/src/util/bag.mli
@@ -49,7 +49,7 @@ val length : 'a t -> int
val is_empty : 'a t -> bool
val singleton : 'a t -> 'a option
val elements : 'a t -> 'a list
-
+val choose: 'a t -> 'a
val print:
(unit Pp.printer) ->
diff --git a/src/util/stdlib.ml b/src/util/stdlib.ml
index e62fa8fde0a0a6d6f816d1f4864a0be2420cbb3d..c2ca7f089c465bb88e8a9ae67b1d17eb2098aaa8 100644
--- a/src/util/stdlib.ml
+++ b/src/util/stdlib.ml
@@ -83,6 +83,13 @@ module type Datatype = sig
val print: t Pp.printer
end
+module MkDatatype(T : OrderedHashedType) = struct
+ include T
+ module M = Map.Make(T)
+ module S = M.Set
+ module H = XHashtbl.Make(T)
+end
+
(* Set, Map, Hashtbl on ints and strings *)
module Int = struct
diff --git a/src/util/stdlib.mli b/src/util/stdlib.mli
index ee0589716899cd837f4eb8e17128c5afd5c4d1d3..2b75450407928a135e686dee7054dca3d0c4a654 100644
--- a/src/util/stdlib.mli
+++ b/src/util/stdlib.mli
@@ -38,6 +38,8 @@ module type Datatype = sig
val print: t Pp.printer
end
+module MkDatatype(T : OrderedHashedType) : Datatype with type t = T.t
+
module OrderedHashed (X : TaggedType) :
OrderedHashedType with type t = X.t
diff --git a/tests/smtlib2/uf/sat/conflict_complete_needed_cl.ml b/tests/smtlib2/uf/sat/conflict_complete_needed_cl.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/conflict_complete_needed_cl.ml
rename to tests/smtlib2/uf/sat/conflict_complete_needed_cl.smt2