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

fix: some fixes in SAT

Browse source
This commit is contained in:
Simon Cruanes 2018-05-20 14:43:33 -05:00
parent fade033458
commit 208f51276d
1 changed files with 7 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/sat/Internal.ml
View file

@ -1181,7 +1181,7 @@ module Make (Th : Theory_intf.S) = struct
) else if a.is_true then ( ) else if a.is_true then (
(* ignore clause, will never be useful *) (* ignore clause, will never be useful *)
Log.debug 5 "(sat.add_clause: true unit clause, ignore)"; Log.debug 5 "(sat.add_clause: true unit clause, ignore)";
assert (0 < a.var.v_level && a.var.v_level <= base_level st); assert (a.var.v_level >= base_level st);
) else ( ) else (
Log.debugf 5 Log.debugf 5
(fun k->k "(@[sat.add_clause.unit_clause@ :propagating %a@])" Atom.debug a); (fun k->k "(@[sat.add_clause.unit_clause@ :propagating %a@])" Atom.debug a);
@ -1230,7 +1230,10 @@ module Make (Th : Theory_intf.S) = struct
(* Top-level conflict *) (* Top-level conflict *)
report_unsat st confl; report_unsat st confl;
); );
(* compute learnt clause with conflict resolution *)
let cr = analyze st confl in let cr = analyze st confl in
let confl = Clause.make_l cr.cr_learnt (History cr.cr_history) in
Log.debugf 5 (fun k->k "(@[sat.conflict-clause@ %a@])" Clause.debug confl);
cancel_until st (max cr.cr_backtrack_lvl (base_level st)); cancel_until st (max cr.cr_backtrack_lvl (base_level st));
(* make some progress *) (* make some progress *)
var_decay_activity st; var_decay_activity st;
@ -1300,7 +1303,6 @@ module Make (Th : Theory_intf.S) = struct
let i = ref 0 in let i = ref 0 in
while !i < Vec.size watched do while !i < Vec.size watched do
let c = Vec.get watched !i in let c = Vec.get watched !i in
assert (Clause.attached c);
if not (Clause.attached c) then ( if not (Clause.attached c) then (
Vec.fast_remove watched !i (* remove *) Vec.fast_remove watched !i (* remove *)
) else ( ) else (
@ -1569,15 +1571,14 @@ module Make (Th : Theory_intf.S) = struct
Log.debugf 3 Log.debugf 3
(fun k -> k "(@[@{<Yellow>sat.theory_conflict_clause@}@ %a@])" Clause.debug c); (fun k -> k "(@[@{<Yellow>sat.theory_conflict_clause@}@ %a@])" Clause.debug c);
(* must backtrack *) (* must backtrack *)
(* TODO: assert that this is indeed a conflict, add_boolean_conflict st c
then call [add_boolean_conflict st c] *)
add_clause ~permanent:false st c
end end
in in
try try
cancel_until st 0; cancel_until st 0;
local st assumptions; (* push decision level before calling [local] *)
new_decision_level st; new_decision_level st;
local st assumptions;
add_clauses() add_clauses()
with Sat -> () with Sat -> ()
@ -1589,32 +1590,6 @@ module Make (Th : Theory_intf.S) = struct
add_clause_user st ~permanent c) add_clause_user st ~permanent c)
cnf cnf
(* Check satisfiability *)
let check_clause c =
let tmp = Array.map (fun a ->
if a.is_true then true
else if a.neg.is_true then false
else raise UndecidedLit) c.atoms in
let res = Array.exists (fun x -> x) tmp in
if not res then (
Log.debugf 5
(fun k -> k "(@[sat.check-clause.1@ :not-satisfied %a@])" Clause.debug c);
false
) else
true
let check_vec v =
Vec.for_all check_clause v
let check_stack s =
try
Stack.iter (fun c -> if not (check_clause c) then raise Exit) s;
true
with Exit ->
false
let check st : bool = check_vec st.clauses
(* Unsafe access to internal data *) (* Unsafe access to internal data *)
let trail st = st.trail let trail st = st.trail