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

use Neperien for logging

Browse source
This commit is contained in:
Simon Cruanes 2014-11-05 21:15:06 +01:00
parent f9d4b9a00e
commit fad14a7e4f
7 changed files with 79 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.merlin
View file

@ -4,3 +4,4 @@ S util
B _build/sat
B _build/smt
B _build/util
PKG neperien

3
_tags
View file

@ -1,5 +1,8 @@
<smt/*.cmx>: for-pack(Msat), package(zarith)
<sat/*.cmx>: for-pack(Msat)
<sat/*.ml*>: package(neperien)
<util/*.ml*>: package(neperien)
<**/*.native>: package(neperien)
# enable stronger inlining everywhere
<util/{vec,hashcons,hstring,iheap}.cmx>: inline(15)

4
sat/sat.ml
View file

@ -70,8 +70,8 @@ module Tsat = struct
let assume ~cs:_ _ _ _ = 0
end
module Make(Dummy : sig end) = struct
module SatSolver = Solver.Make(Fsat)(Stypes)(Exp)(Tsat)
module Make(L : Neperien.S) = struct
module SatSolver = Solver.Make(Fsat)(Stypes)(Exp)(Tsat)(L)
exception Bad_atom

5
sat/sat.mli
View file

@ -1,6 +1,6 @@
(* Copyright 2014 Guillaume Bury *)
module Make(Dummy: sig end) : sig
module Make(L: Neperien.S) : sig
(** Fonctor to make a pure SAT Solver module with built-in literals. *)
exception Bad_atom
@ -14,7 +14,8 @@ module Make(Dummy: sig end) : sig
val new_atom : unit -> atom
(** [new_atom ()] returns a fresh literal.
@raise Bad_atom if there are no more integer available to represent new atoms. *)
@raise Bad_atom if there are no more integer available
to represent new atoms. *)
val make : int -> atom
(** Returns the literal corresponding to the integer.

36
sat/solver.ml
View file

@ -13,7 +13,8 @@
module Make (F : Formula_intf.S)
(St : Solver_types.S with type formula = F.t)
(Ex : Explanation.S with type atom = St.atom)
(Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) = struct
(Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t)
(L : Neperien.S) = struct
open St
@ -201,15 +202,17 @@ module Make (F : Formula_intf.S)
let new_decision_level() =
Vec.push env.trail_lim (Vec.size env.trail);
Vec.push env.tenv_queue env.tenv; (* save the current tenv *)
Log.debug 5 "New decision level : %d (%d in env queue)(%d in trail)"
L.send_b' "New decision level : %d (%d in env queue)(%d in trail)"
(Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail);
()
let attach_clause c =
let lev = L.Unsafe.within_enter () in
Vec.push (Vec.get c.atoms 0).neg.watched c;
Vec.push (Vec.get c.atoms 1).neg.watched c;
Log.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 0).neg St.pp_clause c;
Log.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).neg St.pp_clause c;
L.send_b' "%a <-- %a" St.pp_atom (Vec.get c.atoms 0).neg St.pp_clause c;
L.send_b' "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).neg St.pp_clause c;
L.Unsafe.within_exit_b' lev "attach clause %a" St.pp_clause c;
if c.learnt then
env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
else
@ -233,7 +236,7 @@ module Make (F : Formula_intf.S)
(* cancel down to [lvl] excluded *)
let cancel_until lvl =
Log.debug 5 "Bactracking to decision level %d (excluded)" lvl;
let lev = L.Unsafe.within_enter () in
if decision_level () > lvl then begin
env.qhead <- Vec.get env.trail_lim lvl;
for c = Vec.size env.trail - 1 downto env.qhead do
@ -251,6 +254,7 @@ module Make (F : Formula_intf.S)
Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl);
Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl)
end;
L.Unsafe.within_exit_b' lev "Bactracking to decision level %d (excluded)" lvl;
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
let rec pick_branch_lit () =
@ -270,7 +274,7 @@ module Make (F : Formula_intf.S)
a.is_true <- true;
a.var.level <- lvl;
a.var.reason <- reason;
Log.debug 8 "Enqueue: %a" pp_atom a;
L.send_b' "Enqueue: %a" pp_atom a;
Vec.push env.trail a
let progress_estimate () =
@ -307,7 +311,8 @@ module Make (F : Formula_intf.S)
Vec.set atoms 1 ak;
Vec.set atoms k a.neg;
Vec.push ak.neg.watched c;
Log.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c;
L.send_b' "New watcher (%a) for clause : %a"
St.pp_atom ak.neg St.pp_clause c;
raise Exit
end
done;
@ -319,22 +324,22 @@ module Make (F : Formula_intf.S)
Vec.set watched !new_sz (Vec.get watched k);
incr new_sz;
done;
Log.debug 3 "Conflict found : %a" St.pp_clause c;
L.send_b' "Conflict found : %a" St.pp_clause c;
raise (Conflict c)
end
else begin
(* clause is unit *)
Vec.set watched !new_sz c;
incr new_sz;
Log.debug 5 "Unit clause : %a" St.pp_clause c;
L.send_b' "Unit clause : %a" St.pp_clause c;
enqueue first (decision_level ()) (Some c)
end
with Exit -> ()
let propagate_atom a res =
Log.debug 8 "Propagating %a" St.pp_atom a;
let lev = L.Unsafe.within_enter () in
let watched = a.watched in
Log.debug 10 "Watching %a :" St.pp_atom a;
L.send_b' "Watching %a :" St.pp_atom a;
Vec.iter (fun c -> Log.debug 10 " %a" St.pp_clause c) watched;
let new_sz_w = ref 0 in
begin
@ -345,6 +350,7 @@ module Make (F : Formula_intf.S)
done;
with Conflict c -> assert (!res = None); res := Some c
end;
L.Unsafe.within_exit_b' lev "Propagating %a" St.pp_atom a;
let dead_part = Vec.size watched - !new_sz_w in
Vec.shrink watched dead_part
@ -389,6 +395,7 @@ module Make (F : Formula_intf.S)
let propagate () =
let num_props = ref 0 in
let res = ref None in
let lev = L.Unsafe.within_enter () in
(*assert (Queue.is_empty env.tqueue);*)
while env.qhead < Vec.size env.trail do
let a = Vec.get env.trail env.qhead in
@ -399,6 +406,7 @@ module Make (F : Formula_intf.S)
done;
env.propagations <- env.propagations + !num_props;
env.simpDB_props <- env.simpDB_props - !num_props;
L.Unsafe.within_exit' lev "boolean propagation";
!res
(* conflict analysis *)
@ -634,13 +642,13 @@ module Make (F : Formula_intf.S)
| [] -> assert false
| [fuip] ->
assert (blevel = 0);
Log.debug 2 "Unit clause learnt : %a" St.pp_atom fuip;
L.send_b' "Unit clause learnt : %a" St.pp_atom fuip;
fuip.var.vpremise <- history;
enqueue fuip 0 None
| fuip :: _ ->
let name = fresh_lname () in
let lclause = make_clause name learnt size true history in
Log.debug 2 "New clause learnt : %a" St.pp_clause lclause;
L.send_b' "New clause learnt : %a" St.pp_clause lclause;
Vec.push env.learnts lclause;
attach_clause lclause;
clause_bump_activity lclause;
@ -773,7 +781,7 @@ module Make (F : Formula_intf.S)
let next = pick_branch_lit () in
let current_level = decision_level () in
assert (next.level < 0);
Log.debug 5 "Deciding on %a" St.pp_atom next.pa;
L.send_b' "Deciding on %a" St.pp_atom next.pa;
enqueue next.pa current_level None
done

3
sat/solver.mli
View file

@ -14,7 +14,8 @@
module Make (F : Formula_intf.S)
(St : Solver_types.S with type formula = F.t)
(Ex : Explanation.S with type atom = St.atom)
(Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) :
(Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t)
(L : Neperien.S) :
sig
(** Functor to create a SMT Solver parametrised by the atomic
formulas and a theory. *)

52
util/sat_solve.ml
View file

@ -1,6 +1,4 @@
module S = Sat.Make(struct end)
exception Out_of_time
exception Out_of_space
@ -38,10 +36,14 @@ let setup_gc_stat () =
)
let input_file = fun s -> file := s
let log_file = ref ""
let debug_level = ref max_int
let usage = "Usage : main [options] <file>"
let argspec = Arg.align [
"-v", Arg.Int (fun i -> Log.set_debug i),
"-v", Arg.Set_int debug_level,
"<lvl> Sets the debug verbose level";
"-log", Arg.Set_string log_file,
"<file> Sets the log file";
"-t", Arg.String (int_arg time_limit),
"<t>[smhd] Sets the time limit for the sat solver";
"-s", Arg.String (int_arg size_limit),
@ -62,11 +64,22 @@ let check () =
else if s > !size_limit then
raise Out_of_space
(* Entry file parsing *)
let get_cnf () =
List.rev_map (List.rev_map S.make) (Parser.parse !file)
let proceed () =
(* logging module *)
let log = match !log_file with
| "" -> Neperien.dummy
| filename -> Neperien.log_to_file_mod_exn filename
in
let module NLog = (val log : Neperien.S) in
NLog.set_max_level !debug_level;
let module S = Sat.Make(NLog) in
let print_cnf cnf =
(* Entry file parsing *)
let get_cnf () =
List.rev_map (List.rev_map S.make) (Parser.parse !file)
in
let print_cnf cnf =
Format.printf "CNF :@\n";
List.iter (fun c ->
Format.fprintf Format.std_formatter "%a;@\n"
@ -75,23 +88,16 @@ let print_cnf cnf =
)
) c
) cnf
in
(* Iterate over all variables created *)
let print_assign fmt () =
(* Iterate over all variables created *)
let print_assign fmt () =
S.iter_atoms (fun a ->
Format.fprintf fmt "%a -> %s,@ "
S.print_atom a
(if S.eval a then "T" else "F")
)
let main () =
(* Administrative duties *)
Arg.parse argspec input_file usage;
if !file = "" then begin
Arg.usage argspec usage;
exit 2
end;
ignore(Gc.create_alarm check);
in
(* Interesting stuff happening *)
let cnf = get_cnf () in
@ -104,6 +110,16 @@ let main () =
| S.Unsat ->
Format.printf "Unsat@."
let main () =
(* Administrative duties *)
Arg.parse argspec input_file usage;
if !file = "" then begin
Arg.usage argspec usage;
exit 2
end;
ignore(Gc.create_alarm check);
proceed ()
let () =
try
main ()