From d0ca516eb0ae2af1c4325e5c0fd23c11e94d5a4f Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sun, 16 Nov 2014 21:23:54 +0100 Subject: [PATCH] Fix for iteration on variables --- sat/solver.ml | 10 ++++------ sat/solver_types.ml | 1 + sat/solver_types_intf.ml | 1 + util/vec.ml | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/sat/solver.ml b/sat/solver.ml index 38f85693..4effbad9 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -698,12 +698,10 @@ module Make (F : Formula_intf.S) let nbv = St.nb_vars () in let nbc = env.nb_init_clauses + List.length cnf in Iheap.grow_to_by_double env.order nbv; - List.iter - (List.iter - (fun a -> - insert_var_order a.var - ) - ) cnf; + (* + List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; + *) + St.iter_vars insert_var_order; Vec.grow_to_by_double env.model nbv; Vec.grow_to_by_double env.clauses nbc; Vec.grow_to_by_double env.learnts nbc; diff --git a/sat/solver_types.ml b/sat/solver_types.ml index e517a795..e36abdb4 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -93,6 +93,7 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct let nb_vars () = Vec.size vars let get_var i = Vec.get vars i + let iter_vars f = Vec.iter f vars let cpt_mk_var = ref 0 let make_var = diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml index a58afbe1..724bc3f3 100644 --- a/sat/solver_types_intf.ml +++ b/sat/solver_types_intf.ml @@ -72,6 +72,7 @@ module type S = sig val nb_vars : unit -> int val get_var : int -> var + val iter_vars : (var -> unit) -> unit (** Read access to the vector of variables created *) val fresh_name : unit -> string diff --git a/util/vec.ml b/util/vec.ml index 7c1333cd..2c53f3d4 100644 --- a/util/vec.ml +++ b/util/vec.ml @@ -125,7 +125,7 @@ let sort t f = let iter f t = for i = 0 to size t - 1 do - f (get t i) + f t.data.(i) done let fold f acc t =