diff --git a/.merlin b/.merlin index cc724db2..f60cb339 100644 --- a/.merlin +++ b/.merlin @@ -4,3 +4,4 @@ S util B _build/sat B _build/smt B _build/util +PKG neperien diff --git a/_tags b/_tags index 813c5403..533ab636 100644 --- a/_tags +++ b/_tags @@ -1,5 +1,8 @@ : for-pack(Msat), package(zarith) : for-pack(Msat) +: package(neperien) +: package(neperien) +<**/*.native>: package(neperien) # enable stronger inlining everywhere : inline(15) diff --git a/sat/sat.ml b/sat/sat.ml index 01105aca..23a4f875 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -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 diff --git a/sat/sat.mli b/sat/sat.mli index bf3bc55f..58abdd35 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -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. diff --git a/sat/solver.ml b/sat/solver.ml index 26729ebf..1345ad81 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -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 diff --git a/sat/solver.mli b/sat/solver.mli index 792530f5..7565dca5 100644 --- a/sat/solver.mli +++ b/sat/solver.mli @@ -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. *) diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 27ee05d9..b90f7acb 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -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] " let argspec = Arg.align [ - "-v", Arg.Int (fun i -> Log.set_debug i), + "-v", Arg.Set_int debug_level, " Sets the debug verbose level"; + "-log", Arg.Set_string log_file, + " Sets the log file"; "-t", Arg.String (int_arg time_limit), "[smhd] Sets the time limit for the sat solver"; "-s", Arg.String (int_arg size_limit), @@ -62,36 +64,40 @@ 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 = - Format.printf "CNF :@\n"; - List.iter (fun c -> - Format.fprintf Format.std_formatter "%a;@\n" - (fun fmt -> List.iter (fun a -> - Format.fprintf fmt "%a@ " S.print_atom a - ) - ) c - ) cnf + (* Entry file parsing *) + let get_cnf () = + List.rev_map (List.rev_map S.make) (Parser.parse !file) + in -(* 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 print_cnf cnf = + Format.printf "CNF :@\n"; + List.iter (fun c -> + Format.fprintf Format.std_formatter "%a;@\n" + (fun fmt -> List.iter (fun a -> + Format.fprintf fmt "%a@ " S.print_atom a + ) + ) c + ) cnf + in -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); + (* 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") + ) + 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 ()