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

Bugfix for user lvl push when already unsat

Browse source
This commit is contained in:
Guillaume Bury 2018-09-11 14:19:22 +02:00
parent 2bba885266
commit 5e57bfc827
1 changed files with 18 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/core/internal.ml
View file

@ -1199,25 +1199,28 @@ module Make
(* create a factice decision level for local assumptions *) (* create a factice decision level for local assumptions *)
let push (): unit = let push (): unit =
Log.debugf debug "Pushing a new user level" (fun k -> k); Log.debugf debug "Pushing a new user level" (fun k -> k);
cancel_until (base_level ()); match env.unsat_conflict with
Log.debugf debug "@[<v>Status:@,@[<hov 2>trail: %d - %d@,%a@]" | Some confl -> raise Unsat
(fun k -> k env.elt_head env.th_head (Vec.print ~sep:"" St.pp) env.elt_queue); | None ->
begin match propagate () with cancel_until (base_level ());
| Some confl -> Log.debugf debug "@[<v>Status:@,@[<hov 2>trail: %d - %d@]@,%a@]"
report_unsat confl (fun k -> k env.elt_head env.th_head (Vec.print ~sep:"" St.pp) env.elt_queue);
| None -> begin match propagate () with
Log.debugf debug "@[<v>Current trail:@,@[<hov>%a@]@]" | Some confl ->
(fun k -> k (Vec.print ~sep:"" St.pp) env.elt_queue); report_unsat confl
Log.debugf info "Creating new user level" (fun k -> k); | None ->
new_decision_level (); Log.debugf debug "@[<v>Current trail:@,@[<hov>%a@]@]"
Vec.push env.user_levels (Vec.size env.clauses_temp); (fun k -> k (Vec.print ~sep:"" St.pp) env.elt_queue);
assert (decision_level () = base_level ()) Log.debugf info "Creating new user level" (fun k -> k);
end new_decision_level ();
Vec.push env.user_levels (Vec.size env.clauses_temp);
assert (decision_level () = base_level ())
end
(* pop the last factice decision level *) (* pop the last factice decision level *)
let pop (): unit = let pop (): unit =
if base_level () = 0 then if base_level () = 0 then
Log.debugf warn "Cannot pop (already at level 0)" (fun k -> k) Log.debugf warn "Cannot pop (already at user level 0)" (fun k -> k)
else begin else begin
Log.debugf info "Popping user level" (fun k -> k); Log.debugf info "Popping user level" (fun k -> k);
assert (base_level () > 0); assert (base_level () > 0);