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

Updated some logging levels

Browse source
This commit is contained in:
Guillaume Bury 2016-11-22 18:07:32 +01:00
parent 3124d55209
commit c64a94c2aa
2 changed files with 74 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

84
src/core/internal.ml
View file

@ -22,6 +22,12 @@ module Make
exception Restart exception Restart
exception Conflict of clause exception Conflict of clause
(* Log levels *)
let error = 1
let warn = 3
let info = 5
let debug = 50
(* Singleton type containing the current state *) (* Singleton type containing the current state *)
type env = { type env = {
@ -362,7 +368,7 @@ module Make
*) *)
let attach_clause c = let attach_clause c =
assert (not c.attached); assert (not c.attached);
Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c); Log.debugf debug "Attaching %a" (fun k -> k St.pp_clause c);
Vec.push c.atoms.(0).neg.watched c; Vec.push c.atoms.(0).neg.watched c;
Vec.push c.atoms.(1).neg.watched c; Vec.push c.atoms.(1).neg.watched c;
c.attached <- true; c.attached <- true;
@ -379,9 +385,9 @@ module Make
assert (lvl >= base_level ()); assert (lvl >= base_level ());
(* Nothing to do if we try to backtrack to a non-existent level. *) (* Nothing to do if we try to backtrack to a non-existent level. *)
if decision_level () <= lvl then if decision_level () <= lvl then
Log.debugf 5 "Already at level <= %d" (fun k -> k lvl) Log.debugf debug "Already at level <= %d" (fun k -> k lvl)
else begin else begin
Log.debugf 5 "Backtracking to lvl %d" (fun k -> k lvl); Log.debugf info "Backtracking to lvl %d" (fun k -> k lvl);
(* We set the head of the solver and theory queue to what it was. *) (* We set the head of the solver and theory queue to what it was. *)
let head = ref (Vec.get env.elt_levels lvl) in let head = ref (Vec.get env.elt_levels lvl) in
env.elt_head <- !head; env.elt_head <- !head;
@ -434,7 +440,7 @@ module Make
(* Unsatisfiability is signaled through an exception, since it can happen (* Unsatisfiability is signaled through an exception, since it can happen
in multiple places (adding new clauses, or solving for instance). *) in multiple places (adding new clauses, or solving for instance). *)
let report_unsat ({atoms=atoms} as confl) : _ = let report_unsat ({atoms=atoms} as confl) : _ =
Log.debugf 5 "@[Unsat conflict: %a@]" (fun k -> k St.pp_clause confl); Log.debugf info "@[Unsat conflict: %a@]" (fun k -> k St.pp_clause confl);
env.unsat_conflict <- Some confl; env.unsat_conflict <- Some confl;
raise Unsat raise Unsat
@ -452,13 +458,23 @@ module Make
if history = [] then r if history = [] then r
(* no simplification has been done, so [cl] is actually a clause with only (* no simplification has been done, so [cl] is actually a clause with only
[a], so it is a valid reason for propagating [a]. *) [a], so it is a valid reason for propagating [a]. *)
else else begin
(* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl] (* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl]
with only one formula (which is [a]). So we explicitly create that clause with only one formula (which is [a]). So we explicitly create that clause
and set it as the cause for the propagation of [a], that way we can and set it as the cause for the propagation of [a], that way we can
rebuild the whole resolution tree when we want to prove [a]. *) rebuild the whole resolution tree when we want to prove [a]. *)
Bcp (make_clause (fresh_tname ()) l (History (cl :: history))) let c' = make_clause (fresh_lname ()) l (History (cl :: history)) in
| _ -> assert false Log.debugf debug "Simplified reason: @[<v>%a@,%a@]"
(fun k -> k St.pp_clause cl St.pp_clause c');
Bcp c'
end
| _ ->
Log.debugf error "@[<v 2>Failed at reason simplification:@,%a@,%a@]"
(fun k ->
k (Vec.print ~sep:"" St.pp_atom)
(Vec.from_list l (List.length l) St.dummy_atom)
St.pp_clause cl);
assert false
end end
| r -> r | r -> r
@ -466,7 +482,7 @@ module Make
Wrapper function for adding a new propagated formula. *) Wrapper function for adding a new propagated formula. *)
let enqueue_bool a ~level:lvl reason : unit = let enqueue_bool a ~level:lvl reason : unit =
if a.neg.is_true then begin if a.neg.is_true then begin
Log.debugf 0 "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a); Log.debugf error "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a);
assert false assert false
end; end;
assert (not a.is_true && a.var.v_level < 0 && assert (not a.is_true && a.var.v_level < 0 &&
@ -479,14 +495,14 @@ module Make
a.var.v_level <- lvl; a.var.v_level <- lvl;
a.var.reason <- Some 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 debug "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)
(* MCsat semantic assignment *) (* MCsat semantic assignment *)
let enqueue_assign l value lvl = let enqueue_assign l value lvl =
match l.assigned with match l.assigned with
| Some _ -> | Some _ ->
Log.debugf 0 "Trying to assign an already assigned literal: %a" Log.debugf error "Trying to assign an already assigned literal: %a"
(fun k -> k St.pp_lit l); (fun k -> k St.pp_lit l);
assert false assert false
| None -> | None ->
@ -494,7 +510,7 @@ module Make
l.assigned <- Some value; l.assigned <- Some value;
l.l_level <- lvl; l.l_level <- lvl;
Vec.push env.elt_queue (of_lit l); Vec.push env.elt_queue (of_lit l);
Log.debugf 20 "Enqueue (%d): %a" Log.debugf debug "Enqueue (%d): %a"
(fun k -> k (Vec.size env.elt_queue) pp_lit l) (fun k -> k (Vec.size env.elt_queue) pp_lit l)
(* evaluate an atom for MCsat, if it's not assigned (* evaluate an atom for MCsat, if it's not assigned
@ -678,6 +694,7 @@ module Make
- report unsat if conflict at level 0 - report unsat if conflict at level 0
*) *)
let add_boolean_conflict (confl:clause): unit = let add_boolean_conflict (confl:clause): unit =
Log.debugf info "Boolean conflict: %a" (fun k -> k St.pp_clause confl);
env.next_decision <- None; env.next_decision <- None;
env.conflicts <- env.conflicts + 1; env.conflicts <- env.conflicts + 1;
assert (decision_level() >= base_level ()); assert (decision_level() >= base_level ());
@ -691,7 +708,7 @@ module Make
(* Add a new clause, simplifying, propagating, and backtracking if (* Add a new clause, simplifying, propagating, and backtracking if
the clause is false in the current trail *) the clause is false in the current trail *)
let add_clause ?(force=false) (init:clause) : unit = let add_clause ?(force=false) (init:clause) : unit =
Log.debugf 90 "Adding clause: @[<hov>%a@]" (fun k -> k St.pp_clause init); Log.debugf debug "Adding clause: @[<hov>%a@]" (fun k -> k St.pp_clause init);
let vec = match init.cpremise with let vec = match init.cpremise with
| Hyp -> env.clauses_hyps | Hyp -> env.clauses_hyps
| Local -> env.clauses_temp | Local -> env.clauses_temp
@ -708,7 +725,7 @@ module Make
) )
else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history)) else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history))
in in
Log.debugf 4 "New clause: @[<hov>%a@]" (fun k->k St.pp_clause clause); Log.debugf info "New clause: @[<hov>%a@]" (fun k->k St.pp_clause clause);
Array.iter (fun x -> insert_var_order (elt_of_var x.var)) clause.atoms; Array.iter (fun x -> insert_var_order (elt_of_var x.var)) clause.atoms;
match atoms with match atoms with
| [] -> | [] ->
@ -723,7 +740,7 @@ module Make
(* Since we cannot propagate the atom [a], in order to not lose (* Since we cannot propagate the atom [a], in order to not lose
the information that [a] must be true, we add clause to the list the information that [a] must be true, we add clause to the list
of clauses to add, so that it will be e-examined later. *) of clauses to add, so that it will be e-examined later. *)
Log.debugf 5 "Unit clause, adding to clauses to add" (fun k -> k); Log.debugf debug "Unit clause, adding to clauses to add" (fun k -> k);
Stack.push clause env.clauses_to_add; Stack.push clause env.clauses_to_add;
report_unsat clause report_unsat clause
end else if a.is_true then begin end else if a.is_true then begin
@ -731,12 +748,12 @@ module Make
However it means we can't propagate it at level 0. In order to not lose However it means we can't propagate it at level 0. In order to not lose
that information, we store the clause in a stack of clauses that we will that information, we store the clause in a stack of clauses that we will
add to the solver at the next pop. *) add to the solver at the next pop. *)
Log.debugf 5 "Unit clause, adding to root clauses" (fun k -> k); Log.debugf debug "Unit clause, adding to root clauses" (fun k -> k);
assert (0 < a.var.v_level && a.var.v_level <= base_level ()); assert (0 < a.var.v_level && a.var.v_level <= base_level ());
Stack.push clause env.clauses_root; Stack.push clause env.clauses_root;
() ()
end else begin end else begin
Log.debugf 5 "Unit clause, propagating: %a" (fun k->k St.pp_atom a); Log.debugf debug "Unit clause, propagating: %a" (fun k->k St.pp_atom a);
Vec.push vec clause; Vec.push vec clause;
enqueue_bool a ~level:0 (Bcp clause) enqueue_bool a ~level:0 (Bcp clause)
end end
@ -760,7 +777,7 @@ module Make
end end
with Trivial -> with Trivial ->
Vec.push vec init; Vec.push vec init;
Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init) Log.debugf info "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init)
let flush_clauses () = let flush_clauses () =
if not (Stack.is_empty env.clauses_to_add) then begin if not (Stack.is_empty env.clauses_to_add) then begin
@ -874,7 +891,7 @@ module Make
let slice_push (l:formula list) (lemma:proof): unit = let slice_push (l:formula list) (lemma:proof): unit =
let atoms = List.rev_map (fun x -> new_atom x) l in let atoms = List.rev_map (fun x -> new_atom x) l in
let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in
Log.debugf 10 "Pushing clause %a" (fun k->k St.pp_clause c); Log.debugf info "Pushing clause %a" (fun k->k St.pp_clause c);
(* do not add the clause yet, wait for the theory propagation to (* do not add the clause yet, wait for the theory propagation to
be done *) be done *)
Stack.push c env.clauses_to_add Stack.push c env.clauses_to_add
@ -1021,6 +1038,7 @@ module Make
if Vec.size env.elt_queue = St.nb_elt () if Vec.size env.elt_queue = St.nb_elt ()
then raise Sat; then raise Sat;
if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin
Log.debugf info "Restarting..." (fun k -> k);
cancel_until (base_level ()); cancel_until (base_level ());
raise Restart raise Restart
end; end;
@ -1086,6 +1104,7 @@ module Make
| Plugin_intf.Unsat (l, p) -> | Plugin_intf.Unsat (l, p) ->
let atoms = List.rev_map new_atom l in let atoms = List.rev_map new_atom l in
let c = make_clause (fresh_tname ()) atoms (Lemma p) in let c = make_clause (fresh_tname ()) atoms (Lemma p) in
Log.debugf info "Theory conflict clause: %a" (fun k -> k St.pp_clause c);
Stack.push c env.clauses_to_add Stack.push c env.clauses_to_add
end; end;
if Stack.is_empty env.clauses_to_add then raise Sat if Stack.is_empty env.clauses_to_add then raise Sat
@ -1103,10 +1122,17 @@ 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);
cancel_until (base_level ()); cancel_until (base_level ());
Log.debugf debug "@[<v>Status:@,@[<hov 2>trail: %d - %d@,%a@]"
(fun k -> k env.elt_head env.th_head (Vec.print ~sep:"" St.pp) env.elt_queue);
begin match propagate () with begin match propagate () with
| Some confl -> report_unsat confl | Some confl ->
report_unsat confl
| None -> | None ->
Log.debugf debug "@[<v>Current trail:@,@[<hov>%a@]@]"
(fun k -> k (Vec.print ~sep:"" St.pp) env.elt_queue);
Log.debugf info "Creating new user level" (fun k -> k);
new_decision_level (); new_decision_level ();
Vec.push env.user_levels (Vec.size env.clauses_temp); Vec.push env.user_levels (Vec.size env.clauses_temp);
assert (decision_level () = base_level ()) assert (decision_level () = base_level ())
@ -1114,8 +1140,10 @@ module Make
(* 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)
else begin else begin
Log.debugf info "Popping user level" (fun k -> k);
assert (base_level () > 0); assert (base_level () > 0);
env.unsat_conflict <- None; env.unsat_conflict <- None;
let n = Vec.last env.user_levels in let n = Vec.last env.user_levels in
@ -1134,12 +1162,12 @@ module Make
let local l = let local l =
let aux lit = let aux lit =
let a = atom lit in let a = atom lit in
Log.debugf 10 "Local assumption: @[%a@]" (fun k-> k pp_atom a); Log.debugf info "Local assumption: @[%a@]" (fun k-> k pp_atom a);
assert (decision_level () = base_level ()); assert (decision_level () = base_level ());
if a.is_true then () if a.is_true then ()
else else
let c = make_clause (fresh_hname ()) [a] Local in let c = make_clause (fresh_hname ()) [a] Local in
Log.debugf 10 "Temp clause: @[%a@]" (fun k -> k pp_clause c); Log.debugf debug "Temp clause: @[%a@]" (fun k -> k pp_clause c);
Vec.push env.clauses_temp c; Vec.push env.clauses_temp c;
if a.neg.is_true then begin if a.neg.is_true then begin
(* conflict between assumptions: UNSAT *) (* conflict between assumptions: UNSAT *)
@ -1156,13 +1184,21 @@ module Make
assert (base_level () > 0); assert (base_level () > 0);
match env.unsat_conflict with match env.unsat_conflict with
| None -> | None ->
Log.debugf info "Adding local assumption" (fun k -> k);
cancel_until (base_level ()); cancel_until (base_level ());
List.iter aux l List.iter aux l
| Some _ -> () | Some _ ->
Log.debugf warn "Cannot add local assumption (already unsat)" (fun k -> k)
(* Check satisfiability *) (* Check satisfiability *)
let check_clause c = let check_clause c =
Array_util.exists (fun a -> a.is_true) c.atoms let res = Array_util.exists (fun a -> a.is_true) c.atoms in
if not res then begin
Log.debugf debug "Clause not satisfied: @[<hov>%a@]"
(fun k -> k St.pp_clause c);
false
end else
true
let check_vec v = let check_vec v =
Vec.for_all check_clause v Vec.for_all check_clause v

20
src/core/res.ml
View file

@ -19,6 +19,12 @@ module Make(St : Solver_types.S) = struct
exception Insuficient_hyps exception Insuficient_hyps
exception Resolution_error of string exception Resolution_error of string
(* Log levels *)
let error = 1
let warn = 3
let info = 10
let debug = 80
(* Misc functions *) (* Misc functions *)
let equal_atoms a b = St.(a.aid) = St.(b.aid) let equal_atoms a b = St.(a.aid) = St.(b.aid)
let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
@ -91,17 +97,17 @@ module Make(St : Solver_types.S) = struct
assert St.(a.var.v_level >= 0); assert St.(a.var.v_level >= 0);
match St.(a.var.reason) with match St.(a.var.reason) with
| Some St.Bcp c -> | Some St.Bcp c ->
Log.debugf 50 "Analysing: @[%a@ %a@]" Log.debugf debug "Analysing: @[%a@ %a@]"
(fun k -> k St.pp_atom a St.pp_clause c); (fun k -> k St.pp_atom a St.pp_clause c);
if Array.length c.St.atoms = 1 then begin if Array.length c.St.atoms = 1 then begin
Log.debugf 30 "Old reason: @[%a@]" (fun k -> k St.pp_atom a); Log.debugf debug "Old reason: @[%a@]" (fun k -> k St.pp_atom a);
c c
end else begin end else begin
assert (a.St.neg.St.is_true); assert (a.St.neg.St.is_true);
let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
let c' = St.make_clause (fresh_pcl_name ()) [a.St.neg] r in let c' = St.make_clause (fresh_pcl_name ()) [a.St.neg] r in
a.St.var.St.reason <- Some St.(Bcp c'); a.St.var.St.reason <- Some St.(Bcp c');
Log.debugf 30 "New reason: @[%a@ %a@]" Log.debugf debug "New reason: @[%a@ %a@]"
(fun k -> k St.pp_atom a St.pp_clause c'); (fun k -> k St.pp_atom a St.pp_clause c');
c' c'
end end
@ -110,10 +116,10 @@ module Make(St : Solver_types.S) = struct
let prove_unsat conflict = let prove_unsat conflict =
if Array.length conflict.St.atoms = 0 then conflict if Array.length conflict.St.atoms = 0 then conflict
else begin else begin
Log.debugf 3 "Proving unsat from: @[%a@]" (fun k -> k St.pp_clause conflict); Log.debugf info "Proving unsat from: @[%a@]" (fun k -> k St.pp_clause conflict);
let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
let res = St.make_clause (fresh_pcl_name ()) [] (St.History (conflict :: l)) in let res = St.make_clause (fresh_pcl_name ()) [] (St.History (conflict :: l)) in
Log.debugf 5 "Proof found: @[%a@]" (fun k -> k St.pp_clause res); Log.debugf info "Proof found: @[%a@]" (fun k -> k St.pp_clause res);
res res
end end
@ -137,7 +143,7 @@ module Make(St : Solver_types.S) = struct
let rec chain_res (c, cl) = function let rec chain_res (c, cl) = function
| d :: r -> | d :: r ->
Log.debugf 7 " Resolving clauses : @[%a@\n%a@]" Log.debugf debug " Resolving clauses : @[%a@\n%a@]"
(fun k -> k St.pp_clause c St.pp_clause d); (fun k -> k St.pp_clause c St.pp_clause d);
let dl = to_list d in let dl = to_list d in
begin match resolve (merge cl dl) with begin match resolve (merge cl dl) with
@ -154,7 +160,7 @@ module Make(St : Solver_types.S) = struct
| _ -> assert false | _ -> assert false
let rec expand conclusion = let rec expand conclusion =
Log.debugf 5 "Expanding : @[%a@]" (fun k -> k St.pp_clause conclusion); Log.debugf debug "Expanding : @[%a@]" (fun k -> k St.pp_clause conclusion);
match conclusion.St.cpremise with match conclusion.St.cpremise with
| St.Lemma l -> | St.Lemma l ->
{conclusion; step = Lemma l; } {conclusion; step = Lemma l; }