simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

add some array utils for pre-4.03 compat

Browse source
This commit is contained in:
Simon Cruanes 2016-07-22 11:25:00 +02:00
parent 216ca82fe7
commit e251799f8e
2 changed files with 26 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/core/internal.ml
View file

@ -437,7 +437,7 @@ module Make
end
(* Is a clause satisfied ? *)
let satisfied c = Array.exists (fun atom -> atom.is_true) c.atoms
let satisfied c = Array_util.exists (fun atom -> atom.is_true) c.atoms
(* Backtracking.
Used to backtrack, i.e cancel down to [lvl] excluded,
@ -717,7 +717,7 @@ module Make
let add_boolean_conflict confl =
env.next_decision <- None;
env.conflicts <- env.conflicts + 1;
if decision_level() = 0 || Array.for_all (fun a -> a.var.v_level = 0) confl.atoms then
if decision_level() = 0 || Array_util.for_all (fun a -> a.var.v_level = 0) confl.atoms then
report_unsat confl; (* Top-level conflict *)
let blevel, learnt, history, is_uip = analyze confl in
cancel_until blevel;

24
src/util/array_util.ml Normal file
View file

@ -0,0 +1,24 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** {1 Utils for Arrays} *)
let exists p a =
let n = Array.length a in
let rec loop i =
if i = n then false
else if p (Array.unsafe_get a i) then true
else loop (succ i) in
loop 0
let for_all p a =
let n = Array.length a in
let rec loop i =
if i = n then true
else if p (Array.unsafe_get a i) then loop (succ i)
else false in
loop 0