simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

push/pop: restore trail, causes, learnts

Browse source
This commit is contained in:
Simon Cruanes 2014-11-15 21:26:49 +01:00
parent bfce3e54a2
commit 36e0466304
1 changed files with 23 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
sat/solver.ml
View file

@ -23,6 +23,13 @@ module Make (F : Formula_intf.S)
exception Restart exception Restart
exception Conflict of clause exception Conflict of clause
(* a push/pop state *)
type user_level = {
ul_trail : int; (* height of the decision trail *)
ul_clauses : int; (* number of clauses *)
ul_learnt : int; (* number of learnt clauses *)
}
(* Singleton type containing the current state *) (* Singleton type containing the current state *)
type env = { type env = {
@ -53,8 +60,8 @@ module Make (F : Formula_intf.S)
trail_lim : int Vec.t; trail_lim : int Vec.t;
(* decision levels in [trail] *) (* decision levels in [trail] *)
levels : int Vec.t; user_levels : user_level Vec.t;
(* user-defined levels. Subset of [trail_lim] *) (* user-defined levels, for {!push} and {!pop} *)
mutable qhead : int; mutable qhead : int;
(* Start offset in the queue of unit facts to propagate, within the trail *) (* Start offset in the queue of unit facts to propagate, within the trail *)
@ -123,7 +130,7 @@ module Make (F : Formula_intf.S)
vars = Vec.make 0 dummy_var; (*updated during parsing*) vars = Vec.make 0 dummy_var; (*updated during parsing*)
trail = Vec.make 601 dummy_atom; trail = Vec.make 601 dummy_atom;
trail_lim = Vec.make 601 (-1); trail_lim = Vec.make 601 (-1);
levels = Vec.make 20 (-1); user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
qhead = 0; qhead = 0;
simpDB_assigns = -1; simpDB_assigns = -1;
simpDB_props = 0; simpDB_props = 0;
@ -725,28 +732,31 @@ module Make (F : Formula_intf.S)
let base_level = 0 let base_level = 0
let current_level () = let current_level () = Vec.size env.user_levels
if Vec.is_empty env.levels then base_level else Vec.last env.levels
let push () = let push () =
let l = if Vec.is_empty env.trail_lim let ul_trail = if Vec.is_empty env.trail_lim
then base_level then base_level
else Vec.last env.trail_lim else Vec.last env.trail_lim
in and ul_clauses = Vec.size env.clauses
Vec.push env.levels l; and ul_learnt = Vec.size env.learnts in
l Vec.push env.user_levels {ul_trail; ul_clauses;ul_learnt};
Vec.size env.user_levels
let pop l = let pop l =
if l > current_level() if l > current_level()
then invalid_arg "cannot pop() to level, it is too high"; then invalid_arg "cannot pop() to level, it is too high";
let i = Vec.get env.levels l in let ul = Vec.get env.user_levels l in
(* see whether we can reset [env.is_unsat] *) (* see whether we can reset [env.is_unsat] *)
if env.is_unsat && not (Vec.is_empty env.trail_lim) then ( if env.is_unsat && not (Vec.is_empty env.trail_lim) then (
(* level at which the decision that lead to unsat was made *) (* level at which the decision that lead to unsat was made *)
let last = Vec.last env.trail_lim in let last = Vec.last env.trail_lim in
if i < last then env.is_unsat <- false if ul.ul_trail < last then env.is_unsat <- false
); );
cancel_until i cancel_until ul.ul_trail;
Vec.shrink env.clauses ul.ul_clauses;
Vec.shrink env.learnts ul.ul_learnt;
()
let clear () = pop base_level let clear () = pop base_level
end end