Skip to content

Commit

Permalink
replace splitted with splits
Browse files Browse the repository at this point in the history
  • Loading branch information
ghilesZ committed May 12, 2024
1 parent aaffbcc commit 520e35f
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions lib/solver/graphiterator.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ module Make (D : Domain) = struct
let print_graph fmt g =
Format.fprintf fmt "%a" (Cgraph.print Format.pp_print_string print_constr) g

type t = {space: space; graph: constraint_graph; splitted: Tools.VarSet.t}
type t = {space: space; graph: constraint_graph; splits: Tools.VarSet.t}

let init ?(verbose = false) (p : Csp.t) : t =
if verbose then Format.printf "variable declaration ...%!" ;
Expand All @@ -37,10 +37,10 @@ module Make (D : Domain) = struct
let graph = Cgraph.build n constraints in
if verbose then Format.printf " done.\n%!" ;
if verbose then Format.printf "edges:@,%a\n%!" print_graph graph ;
{space; graph; splitted= Tools.VarSet.empty}
{space; graph; splits= Tools.VarSet.empty}

(* graph propagation : each constraint is activated at most once *)
let propagate {space; graph; splitted} : t Consistency.t =
let propagate {space; graph; splits} : t Consistency.t =
let queue = Queue.create () in
let activated = Hashtbl.create (Cgraph.nb_edges graph) in
let add_to_queue c =
Expand All @@ -51,7 +51,7 @@ module Make (D : Domain) = struct
let add_from v = Cgraph.iter_edges_from add_to_queue graph v in
let rec loop graph sat abs =
if Queue.is_empty queue then
Filtered ({space= abs; graph; splitted= Tools.VarSet.empty}, sat)
Filtered ({space= abs; graph; splits= Tools.VarSet.empty}, sat)
else
let c = Queue.pop queue in
match D.filter_diff abs c with
Expand All @@ -70,15 +70,15 @@ module Make (D : Domain) = struct
loop graph false abs'
| Pruned {sure; unsure} -> prune sat sure unsure
and prune _sat _sure _unsure = failwith "pruning not implemented" in
(* if no variable have been splitted, perform a full propagation *)
if Tools.VarSet.is_empty splitted then
(* if no variable have been split, perform a full propagation *)
if Tools.VarSet.is_empty splits then
List.iter add_to_queue (Cgraph.get_edges graph)
else Tools.VarSet.iter add_from splitted ;
else Tools.VarSet.iter add_from splits ;
loop graph true space

let split ?prec e =
let splits, diff = D.split_diff ?prec e.space in
List.rev_map (fun space -> {e with space; splitted= diff}) splits
List.rev_map (fun space -> {e with space; splits= diff}) splits

let spawn elm = D.spawn elm.space

Expand Down

0 comments on commit 520e35f

Please sign in to comment.