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

Propagation reasons are now far more explicit

Browse source
This commit is contained in:
Guillaume Bury 2016-04-15 12:09:23 +02:00
parent 0186edbf34
commit 815098dde4
5 changed files with 42 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
solver/internal.ml
View file

@ -288,9 +288,10 @@ module Make
if a.is_true then raise Trivial; if a.is_true then raise Trivial;
if a.neg.is_true then begin if a.neg.is_true then begin
match a.var.reason with match a.var.reason with
| Bcp (Some cl) -> atoms, cl :: history, max lvl cl.c_level | None | Some Decision -> assert false
| Semantic 0 -> atoms, history, lvl | Some (Bcp cl) -> atoms, cl :: history, max lvl cl.c_level
| _ -> | Some (Semantic 0) -> atoms, history, lvl
| Some (Semantic _) ->
Log.debugf 0 "Unexpected semantic propagation at level 0: %a" Log.debugf 0 "Unexpected semantic propagation at level 0: %a"
(fun k->k St.pp_atom a); (fun k->k St.pp_atom a);
assert false assert false
@ -311,9 +312,9 @@ module Make
else if a.neg.is_true then else if a.neg.is_true then
if a.var.v_level = 0 then begin if a.var.v_level = 0 then begin
match a.var.reason with match a.var.reason with
| Bcp (Some cl) -> | Some (Bcp cl) ->
partition_aux trues unassigned falses (cl :: history) (max lvl cl.c_level) r partition_aux trues unassigned falses (cl :: history) (max lvl cl.c_level) r
| Semantic 0 -> | Some (Semantic 0) ->
partition_aux trues unassigned falses history lvl r partition_aux trues unassigned falses history lvl r
| _ -> assert false | _ -> assert false
end else end else
@ -393,7 +394,7 @@ module Make
a.is_true <- false; a.is_true <- false;
a.neg.is_true <- false; a.neg.is_true <- false;
a.var.v_level <- -1; a.var.v_level <- -1;
a.var.reason <- Bcp None; a.var.reason <- None;
insert_var_order (elt_of_var a.var) insert_var_order (elt_of_var a.var)
end end
done; done;
@ -411,14 +412,14 @@ module Make
raise Unsat raise Unsat
let simpl_reason = function let simpl_reason = function
| (Bcp Some cl) as r -> | (Bcp cl) as r ->
let l, history, c_lvl = partition (Vec.to_list cl.atoms) 0 in let l, history, c_lvl = partition (Vec.to_list cl.atoms) 0 in
begin match l with begin match l with
| [ a ] -> | [ a ] ->
if history = [] then r if history = [] then r
else else
let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) c_lvl in let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) c_lvl in
Bcp (Some tmp_cl) Bcp tmp_cl
| _ -> assert false | _ -> assert false
end end
| r -> r | r -> r
@ -429,14 +430,14 @@ module Make
assert false assert false
end; end;
if not a.is_true then begin if not a.is_true then begin
assert (a.var.v_level < 0 && a.var.reason = Bcp None && lvl >= 0); assert (a.var.v_level < 0 && a.var.reason = None && lvl >= 0);
let reason = let reason =
if lvl > 0 then reason if lvl > 0 then reason
else simpl_reason reason else simpl_reason reason
in in
a.is_true <- true; a.is_true <- true;
a.var.v_level <- lvl; a.var.v_level <- lvl;
a.var.reason <- reason; a.var.reason <- Some reason;
Vec.push env.elt_queue (of_atom a); Vec.push env.elt_queue (of_atom a);
Log.debugf 20 "Enqueue (%d): %a" Log.debugf 20 "Enqueue (%d): %a"
(fun k->k (Vec.size env.elt_queue) pp_atom a) (fun k->k (Vec.size env.elt_queue) pp_atom a)
@ -480,7 +481,7 @@ module Make
let c_level = ref 0 in let c_level = ref 0 in
clause_bump_activity c_clause; clause_bump_activity c_clause;
let is_semantic a = match a.var.reason with let is_semantic a = match a.var.reason with
| Semantic _ -> true | Some Semantic _ -> true
| _ -> false | _ -> false
in in
try while true do try while true do
@ -499,7 +500,7 @@ module Make
| Either.Left _ -> () | Either.Left _ -> ()
| Either.Right a -> | Either.Right a ->
begin match a.var.reason with begin match a.var.reason with
| Bcp (Some d) -> | Some (Bcp d) ->
let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in
begin match tmp with begin match tmp with
| [] -> () | [] -> ()
@ -511,8 +512,7 @@ module Make
c := res c := res
| _ -> assert false | _ -> assert false
end end
| Bcp None -> () | None | Some Decision | Some Semantic _ -> ()
| Semantic _ -> ()
end end
done; assert false done; assert false
with Exit -> with Exit ->
@ -546,7 +546,7 @@ module Make
if q.var.v_level = 0 then begin if q.var.v_level = 0 then begin
assert (q.neg.is_true); assert (q.neg.is_true);
match q.var.reason with match q.var.reason with
| Bcp Some cl -> history := cl :: !history | Some Bcp cl -> history := cl :: !history
| _ -> assert false | _ -> assert false
end; end;
if not q.var.seen then begin if not q.var.seen then begin
@ -574,7 +574,7 @@ module Make
| 0, _ -> | 0, _ ->
cond := false; cond := false;
learnt := p.neg :: (List.rev !learnt) learnt := p.neg :: (List.rev !learnt)
| n, Bcp Some cl -> | n, Some Bcp cl ->
c_level := max !c_level cl.c_level; c_level := max !c_level cl.c_level;
c := cl c := cl
| n, _ -> assert false | n, _ -> assert false
@ -599,7 +599,7 @@ module Make
let name = fresh_lname () in let name = fresh_lname () in
let uclause = make_clause name learnt (List.length learnt) true history lvl in let uclause = make_clause name learnt (List.length learnt) true history lvl in
Vec.push env.clauses_learnt uclause; Vec.push env.clauses_learnt uclause;
enqueue_bool fuip 0 (Bcp (Some uclause)) enqueue_bool fuip 0 (Bcp uclause)
end end
| fuip :: _ -> | fuip :: _ ->
let name = fresh_lname () in let name = fresh_lname () in
@ -608,7 +608,7 @@ module Make
attach_clause lclause; attach_clause lclause;
clause_bump_activity lclause; clause_bump_activity lclause;
if is_uip then if is_uip then
enqueue_bool fuip blevel (Bcp (Some lclause)) enqueue_bool fuip blevel (Bcp lclause)
else begin else begin
env.next_decision <- Some fuip.neg env.next_decision <- Some fuip.neg
end end
@ -656,12 +656,12 @@ module Make
end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
cancel_until lvl; cancel_until lvl;
enqueue_bool a lvl (Bcp (Some clause)) enqueue_bool a lvl (Bcp clause)
end end
| [a] -> | [a] ->
Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a); Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a);
cancel_until 0; cancel_until 0;
enqueue_bool a 0 (Bcp (Some init0)) enqueue_bool a 0 (Bcp init0)
with Trivial -> with Trivial ->
Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init0) Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init0)
@ -703,7 +703,7 @@ module Make
(* clause is unit *) (* clause is unit *)
Vec.set watched !new_sz c; Vec.set watched !new_sz c;
incr new_sz; incr new_sz;
enqueue_bool first (decision_level ()) (Bcp (Some c)) enqueue_bool first (decision_level ()) (Bcp c)
end end
with Exit -> () with Exit -> ()
@ -887,7 +887,7 @@ module Make
env.decisions <- env.decisions + 1; env.decisions <- env.decisions + 1;
new_decision_level(); new_decision_level();
let current_level = decision_level () in let current_level = decision_level () in
enqueue_bool atom current_level (Bcp None) enqueue_bool atom current_level Decision
| Th.Valued (b, lvl) -> | Th.Valued (b, lvl) ->
let a = if b then atom else atom.neg in let a = if b then atom else atom.neg in
enqueue_bool a lvl (Semantic lvl) enqueue_bool a lvl (Semantic lvl)
@ -1040,11 +1040,11 @@ module Make
insert_var_order (elt_of_lit l) insert_var_order (elt_of_lit l)
| Either.Right a -> | Either.Right a ->
begin match a.var.reason with begin match a.var.reason with
| Bcp Some { c_level } when c_level > push_lvl -> | Some Bcp { c_level } when c_level > push_lvl ->
a.is_true <- false; a.is_true <- false;
a.neg.is_true <- false; a.neg.is_true <- false;
a.var.v_level <- -1; a.var.v_level <- -1;
a.var.reason <- Bcp None; a.var.reason <- None;
insert_var_order (elt_of_var a.var) insert_var_order (elt_of_var a.var)
| _ -> | _ ->
if a.var.v_level = 0 then begin if a.var.v_level = 0 then begin
@ -1054,7 +1054,7 @@ module Make
a.is_true <- false; a.is_true <- false;
a.neg.is_true <- false; a.neg.is_true <- false;
a.var.v_level <- -1; a.var.v_level <- -1;
a.var.reason <- Bcp None; a.var.reason <- None;
insert_var_order (elt_of_var a.var) insert_var_order (elt_of_var a.var)
end end
end end

4
solver/res.ml
View file

@ -90,7 +90,7 @@ module Make(St : Solver_types.S) = struct
let l = Vec.to_list c.St.atoms in let l = Vec.to_list c.St.atoms in
let l = List.map (fun a -> let l = List.map (fun a ->
match St.(a.var.reason) with match St.(a.var.reason) with
| St.Bcp Some d -> d | Some St.Bcp d -> d
| _ -> assert false) l | _ -> assert false) l
in in
St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l)) St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l))
@ -99,7 +99,7 @@ module Make(St : Solver_types.S) = struct
let prove_atom a = let prove_atom a =
if St.(a.is_true && a.var.v_level = 0) then begin if St.(a.is_true && a.var.v_level = 0) then begin
match St.(a.var.reason) with match St.(a.var.reason) with
| St.Bcp Some c -> | Some St.Bcp c ->
assert (Vec.size St.(c.atoms) = 1 && equal_atoms a (Vec.get St.(c.atoms) 0)); assert (Vec.size St.(c.atoms) = 1 && equal_atoms a (Vec.get St.(c.atoms) 0));
Some c Some c
| _ -> assert false | _ -> assert false

19
solver/solver_types.ml
View file

@ -42,7 +42,7 @@ module McMake (E : Expr_intf.S) = struct
mutable seen : bool; mutable seen : bool;
mutable v_level : int; mutable v_level : int;
mutable v_weight : float; mutable v_weight : float;
mutable reason : reason; mutable reason : reason option;
} }
and atom = { and atom = {
@ -66,8 +66,9 @@ module McMake (E : Expr_intf.S) = struct
} }
and reason = and reason =
| Decision
| Bcp of clause
| Semantic of int | Semantic of int
| Bcp of clause option
and premise = and premise =
| Lemma of proof | Lemma of proof
@ -85,7 +86,7 @@ module McMake (E : Expr_intf.S) = struct
seen = false; seen = false;
v_level = -1; v_level = -1;
v_weight = -1.; v_weight = -1.;
reason = Bcp None; reason = None;
} }
and dummy_atom = and dummy_atom =
{ var = dummy_var; { var = dummy_var;
@ -151,7 +152,7 @@ module McMake (E : Expr_intf.S) = struct
seen = false; seen = false;
v_level = -1; v_level = -1;
v_weight = 0.; v_weight = 0.;
reason = Bcp None; reason = None;
} }
and pa = and pa =
{ var = var; { var = var;
@ -257,11 +258,11 @@ module McMake (E : Expr_intf.S) = struct
let level a = let level a =
match a.var.v_level, a.var.reason with match a.var.v_level, a.var.reason with
| n, _ when n < 0 -> assert false | n, _ when n < 0 -> assert false
| 0, Bcp (Some c) -> sprintf "->0/%s" c.name | 0, Some (Bcp c) -> sprintf "->0/%s" c.name
| 0, Bcp None -> "@0" | 0, None -> "@0"
| n, Bcp (Some c) -> sprintf "->%d/%s" n c.name | n, Some (Bcp c) -> sprintf "->%d/%s" n c.name
| n, Bcp None -> sprintf "@@%d" n | n, None -> sprintf "@@%d" n
| n, Semantic lvl -> sprintf "::%d/%d" n lvl | n, Some (Semantic lvl) -> sprintf "::%d/%d" n lvl
let value a = let value a =
if a.is_true then sprintf "[T%s]" (level a) if a.is_true then sprintf "[T%s]" (level a)

5
solver/solver_types_intf.ml
View file

@ -37,7 +37,7 @@ module type S = sig
mutable seen : bool; mutable seen : bool;
mutable v_level : int; mutable v_level : int;
mutable v_weight : float; mutable v_weight : float;
mutable reason : reason; mutable reason : reason option;
} }
and atom = { and atom = {
@ -61,8 +61,9 @@ module type S = sig
} }
and reason = and reason =
| Decision
| Bcp of clause
| Semantic of int | Semantic of int
| Bcp of clause option
and premise = and premise =
| Lemma of proof | Lemma of proof