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

Merge branch 'master' of github.com:Gbury/mSAT

Browse source 
Conflicts:
	solver/mcsolver.ml
This commit is contained in:
Guillaume Bury 2015-01-26 15:02:44 +01:00
commit 3ed5d26ac7
1 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
solver/mcsolver.ml
View file

@ -280,12 +280,12 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl);
Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl) Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl);
end; end;
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
let report_unsat ({atoms=atoms} as confl) = let report_unsat ({atoms=atoms} as confl) =
L.debug 5 "Unsat conflict : %a" St.pp_clause confl; L.debug 4 "Unsat conflict : %a" St.pp_clause confl;
env.unsat_conflict <- Some confl; env.unsat_conflict <- Some confl;
env.is_unsat <- true; env.is_unsat <- true;
raise Unsat raise Unsat
@ -299,16 +299,15 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
a.is_true <- true; a.is_true <- true;
a.var.level <- lvl; a.var.level <- lvl;
a.var.tag.reason <- reason; a.var.tag.reason <- reason;
L.debug 8 "Enqueue: %a" pp_atom a; Vec.push env.trail (Either.mk_right a);
Vec.push env.trail (Either.mk_right a) L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom a
end end
let enqueue_assign v value lvl = let enqueue_assign v value lvl =
v.tag.assigned <- Some value; v.tag.assigned <- Some value;
v.level <- lvl; v.level <- lvl;
L.debug 5 "Enqueue: %a" St.pp_semantic_var v;
Vec.push env.trail (Either.mk_left v); Vec.push env.trail (Either.mk_left v);
L.debug 15 "Done." L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_semantic_var v
(* conflict analysis *) (* conflict analysis *)
let max_lvl_atoms l = let max_lvl_atoms l =
@ -426,14 +425,14 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
fuip.var.tag.vpremise <- history; fuip.var.tag.vpremise <- history;
let name = fresh_lname () in let name = fresh_lname () in
let uclause = make_clause name learnt (List.length learnt) true history in let uclause = make_clause name learnt (List.length learnt) true history in
L.debug 2 "Unit clause learnt : %a" St.pp_clause uclause; L.debug 1 "Unit clause learnt : %a" St.pp_clause uclause;
Vec.push env.learnts uclause; Vec.push env.learnts uclause;
enqueue_bool fuip 0 (Bcp (Some uclause)) enqueue_bool fuip 0 (Bcp (Some uclause))
end end
| fuip :: _ -> | fuip :: _ ->
let name = fresh_lname () in let name = fresh_lname () in
let lclause = make_clause name learnt (List.length learnt) true history in let lclause = make_clause name learnt (List.length learnt) true history in
L.debug 2 "New clause learnt : %a" St.pp_clause lclause; L.debug 1 "New clause learnt : %a" St.pp_clause lclause;
Vec.push env.learnts lclause; Vec.push env.learnts lclause;
attach_clause lclause; attach_clause lclause;
clause_bump_activity lclause; clause_bump_activity lclause;
@ -512,7 +511,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
| a::b::_ -> | a::b::_ ->
let name = fresh_name () in let name = fresh_name () in
let clause = make_clause name atoms size (history <> History []) history in let clause = make_clause name atoms size (history <> History []) history in
L.debug 10 "New clause : %a" St.pp_clause init0; L.debug 1 "New clause : %a" St.pp_clause init0;
attach_clause clause; attach_clause clause;
Vec.push env.clauses clause; Vec.push env.clauses clause;
if a.neg.is_true then begin if a.neg.is_true then begin
@ -641,10 +640,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
}) })
let rec theory_propagate () = let rec theory_propagate () =
let head = Vec.size env.trail in let slice = current_slice () in
match Th.assume (current_slice ()) with env.tatoms_qhead <- nb_assigns ();
match Th.assume slice with
| Th.Sat -> | Th.Sat ->
env.tatoms_qhead <- head;
propagate () propagate ()
| Th.Unsat (l, p) -> | Th.Unsat (l, p) ->
let l = List.rev_map St.add_atom l in let l = List.rev_map St.add_atom l in