diff --git a/src/core/Internal.ml b/src/core/Internal.ml index ac7fbfc2..0fc077a3 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -74,6 +74,7 @@ module Make(Plugin : PLUGIN) | Local | Lemma of lemma | History of clause list + | Empty_premise type elt = | E_lit of lit @@ -117,6 +118,7 @@ module Make(Plugin : PLUGIN) | Lemma _ -> "T" ^ string_of_int c.name | Local -> "L" ^ string_of_int c.name | History _ -> "C" ^ string_of_int c.name + | Empty_premise -> string_of_int c.name module Lit = struct type t = lit @@ -396,6 +398,7 @@ module Make(Plugin : PLUGIN) | Local -> Format.fprintf out "local" | History v -> List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v + | Empty_premise -> Format.fprintf out "" let debug out ({atoms=arr; cpremise=cp;_}as c) = Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" @@ -478,9 +481,11 @@ module Make(Plugin : PLUGIN) in aux (c, d) - let[@inline] prove conclusion = - assert (conclusion.cpremise <> History []); - conclusion + let prove conclusion = + match conclusion.cpremise with + | History [] -> assert false + | Empty_premise -> raise Solver_intf.No_proof + | _ -> conclusion let rec set_atom_proof a = let aux acc b = @@ -582,6 +587,7 @@ module Make(Plugin : PLUGIN) conclusion.cpremise <- History [c'; d']; assert (cmp_cl l (to_list conclusion) = 0); { conclusion; step = Resolution (c', d', a); } + | Empty_premise -> raise Solver_intf.No_proof (* Proof nodes manipulation *) let is_leaf = function @@ -615,6 +621,7 @@ module Make(Plugin : PLUGIN) if not @@ Clause.visited c then ( Clause.set_visited c true; match c.cpremise with + | Empty_premise -> raise Solver_intf.No_proof | Hyp _ | Lemma _ | Local -> aux (c :: res) acc r | History h -> let l = List.fold_left (fun acc c -> @@ -712,6 +719,8 @@ module Make(Plugin : PLUGIN) st : st; th: theory; + log_proof: bool; (* do we store proofs? *) + (* Clauses are simplified for eficiency purposes. In the following vectors, the comments actually refer to the original non-simplified clause. *) @@ -778,7 +787,7 @@ module Make(Plugin : PLUGIN) type solver = t (* Starting environment. *) - let create_ ~st (th:theory) : t = { + let create_ ~st ~log_proof (th:theory) : t = { st; th; unsat_at_0=None; next_decision = None; @@ -800,15 +809,16 @@ module Make(Plugin : PLUGIN) var_incr = 1.; clause_incr = 1.; + log_proof; restart_first = 100; learntsize_factor = 1. /. 3. ; } - let create ?(size=`Big) (th:theory) : t = + let create ?(log_proof=true) ?(size=`Big) (th:theory) : t = let st = create_st ~size () in - create_ ~st th + create_ ~st ~log_proof th let[@inline] st t = t.st let[@inline] nb_clauses st = Vec.size st.clauses_hyps @@ -1317,10 +1327,9 @@ module Make(Plugin : PLUGIN) Log.debug debug "(@[sat.analyze-conflict: skipping resolution for semantic propagation@])" | Some clause -> Log.debugf debug (fun k->k"(@[sat.analyze-conflict.resolve@ %a@])" Clause.debug clause); - begin match clause.cpremise with - | History _ -> clause_bump_activity st clause - | Hyp _ | Local | Lemma _ -> () - end; + if Clause.learnt clause then ( + clause_bump_activity st clause; + ); history := clause :: !history; (* visit the current predecessors *) for j = 0 to Array.length clause.atoms - 1 do @@ -1393,6 +1402,7 @@ module Make(Plugin : PLUGIN) (* add the learnt clause to the clause database, propagate, etc. *) let record_learnt_clause st (confl:clause) (cr:conflict_res): unit = + let proof = if st.log_proof then History cr.cr_history else Empty_premise in begin match cr.cr_learnt with | [] -> assert false | [fuip] -> @@ -1401,13 +1411,13 @@ module Make(Plugin : PLUGIN) (* incompatible at level 0 *) report_unsat st (US_false confl) ) else ( - let uclause = Clause.make cr.cr_learnt (History cr.cr_history) in + let uclause = Clause.make cr.cr_learnt proof in (* no need to attach [uclause], it is true at level 0 *) Clause.set_learnt uclause true; enqueue_bool st fuip ~level:0 (Bcp uclause) ) | fuip :: _ -> - let lclause = Clause.make cr.cr_learnt (History cr.cr_history) in + let lclause = Clause.make cr.cr_learnt proof in Clause.set_learnt lclause true; if Array.length lclause.atoms > 2 then ( Vec.push st.clauses_learnt lclause; (* potentially gc'able *) @@ -1459,13 +1469,14 @@ module Make(Plugin : PLUGIN) Log.debugf debug (fun k -> k "(@[sat.dups-removed@ %a@])" Clause.debug c); let atoms, history = partition c.atoms in let clause = - if history = [] - then ( - (* update order of atoms *) + if history = [] then ( + (* just update order of atoms *) List.iteri (fun i a -> c.atoms.(i) <- a) atoms; c + ) else ( + let proof = if st.log_proof then History (c::history) else Empty_premise in + Clause.make atoms proof ) - else Clause.make atoms (History (c :: history)) in Log.debugf info (fun k->k "(@[sat.new-clause@ @[%a@]@])" Clause.debug clause); match atoms with diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 90e06822..f52b5466 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -124,6 +124,8 @@ type ('a, 'b) gadt_eq = GADT_EQ : ('a, 'a) gadt_eq type void = (unit,bool) gadt_eq (** A provably empty type *) +exception No_proof + module type FORMULA = sig (** formulas *) @@ -408,9 +410,15 @@ module type S = sig type t = solver (** Main solver type, containing all state for solving. *) - val create : ?size:[`Tiny|`Small|`Big] -> theory -> t + val create : + ?log_proof:bool -> + ?size:[`Tiny|`Small|`Big] -> + theory -> + t (** Create new solver @param theory the theory + @param log_proof if true, stores proof (default [true]). Otherwise + the functions that return proofs will fail with [No_proof] @param size the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses. *) diff --git a/src/main/main.ml b/src/main/main.ml index 79745c5e..d60fe072 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -15,15 +15,16 @@ let p_dot_proof = ref "" let p_proof_print = ref false let time_limit = ref 300. let size_limit = ref 1000_000_000. +let no_proof = ref false module S = Msat_sat -module Process = struct +module Process() = struct module D = Msat_backend.Dot.Make(S)(Msat_backend.Dot.Default(S)) let hyps = ref [] - let st = S.create ~size:`Big () + let st = S.create ~log_proof:(not !no_proof) ~size:`Big () let check_model sat = let check_clause c = @@ -63,7 +64,7 @@ module Process = struct let add_clauses cs = S.assume st (CCList.map conv_c cs) () -end +end[@@inline] let parse_file f = let module L = Lexing in @@ -126,6 +127,7 @@ let argspec = Arg.align [ "[smhd] Sets the time limit for the sat solver"; "-v", Arg.Int (fun i -> Log.set_debug i), " Sets the debug verbose level"; + "-no-proof", Arg.Set no_proof, " disable proof logging"; ] (* Limits alarm *) @@ -147,10 +149,12 @@ let main () = ); let al = Gc.create_alarm check in + let module P = Process() in + (* Interesting stuff happening *) let clauses = parse_file !file in - Process.add_clauses clauses; - Process.prove ~assumptions:[] (); + P.add_clauses clauses; + P.prove ~assumptions:[] (); Gc.delete_alarm al; () diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml index 0dfb04fc..0a873079 100644 --- a/src/sudoku/sudoku_solve.ml +++ b/src/sudoku/sudoku_solve.ml @@ -271,7 +271,7 @@ end = struct r let create g : t = - { solver=S.create (Theory.create g); grid0=g } + { solver=S.create ~log_proof:false (Theory.create g); grid0=g } end let solve_grid (g:Grid.t) : Grid.t option =