From 5911f18cb4ae0a414a24c647ac8b2974f3aa4605 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 19 Nov 2015 14:59:54 +0100 Subject: [PATCH] Res module adapted to accomodate puush/pop --- solver/internal.ml | 10 ++++++++-- solver/res.ml | 46 ++++++++++++++++++++++++++++++---------------- solver/res.mli | 6 +++++- 3 files changed, 43 insertions(+), 19 deletions(-) diff --git a/solver/internal.ml b/solver/internal.ml index 40b049bb..75ea45a1 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -23,6 +23,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S) ul_th_env : Th.level; (* Theory state at level 0 *) ul_clauses : int; (* number of clauses *) ul_learnt : int; (* number of learnt clauses *) + ul_proof_lvl : int; (* push/pop index for Res module *) } (* Singleton type containing the current state *) @@ -128,6 +129,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S) ul_learnt = 0; ul_clauses = 0; ul_th_env = Th.dummy; + ul_proof_lvl = -1; }; qhead = 0; simpDB_assigns = -1; @@ -968,7 +970,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S) in let ul_clauses = Vec.size env.clauses in let ul_learnt = Vec.size env.learnts in - Vec.push env.user_levels {ul_trail; ul_th_env; ul_clauses;ul_learnt}; + let ul_proof_lvl = Proof.push () in + Vec.push env.user_levels {ul_trail; ul_th_env; ul_clauses; ul_learnt; ul_proof_lvl;}; res (* Backtrack to decision_level 0, with trail_lim && theory env specified *) @@ -1014,7 +1017,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S) (* It is quite hard to check wether unsat status can be kept, so in doubt, we remove it *) env.is_unsat <- false; - (* Backtrack to the right level *) + (* Backtrack to the level 0 with appropriate settings *) reset_until l ul.ul_trail ul.ul_th_env; (* Clear hypothesis not valid anymore *) @@ -1025,6 +1028,9 @@ module Make (L : Log_intf.S)(St : Solver_types.S) done; Vec.shrink env.clauses (Vec.size env.clauses - ul.ul_clauses); + (* Backtrack the Proof module *) + Proof.pop ul.ul_proof_lvl; + (* Refresh the known tautologies simplified because of clauses that have been removed *) let s = Stack.create () in let new_sz = ref ul.ul_learnt in diff --git a/solver/res.ml b/solver/res.ml index 8c03ec57..5a08cd7e 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -40,7 +40,18 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct let hash = hash_cl let equal = equal_cl end) - let proof : node H.t = H.create 1007;; + let proof : node H.t ref = ref (H.create 1007);; + + let push_stack = Vec.make 0 (H.create 0) + + let push () = + let res = Vec.size push_stack in + Vec.push push_stack (H.copy !proof); + res + + let pop i = + proof := Vec.get push_stack i; + Vec.shrink push_stack (Vec.size push_stack - i) (* Misc functions *) let equal_atoms a b = St.(a.aid) = St.(b.aid) @@ -96,16 +107,16 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct let print_clause fmt c = print_cl fmt (to_list c) (* Adding hyptoheses *) - let has_been_proved c = H.mem proof (to_list c) + let has_been_proved c = H.mem !proof (to_list c) let is_proved (c, cl) = - if H.mem proof cl then + if H.mem !proof cl then true else if not St.(c.learnt) then begin - H.add proof cl Assumption; + H.add !proof cl Assumption; true end else match St.(c.cpremise) with - | St.Lemma p -> H.add proof cl (Lemma p); true + | St.Lemma p -> H.add !proof cl (Lemma p); true | St.History _ -> false let is_proven c = is_proved (c, to_list c) @@ -121,7 +132,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct match resolved with | [] -> raise (Resolution_error "No literal to resolve over") | [a] -> - H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); + H.add !proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) (max c.St.c_level d.St.c_level) in L.debug 5 "New clause : %a" St.pp_clause new_c; @@ -219,28 +230,31 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct raise Insuficient_hyps (* Interface exposed *) - type proof_node = { + type proof = { + table : node H.t; + clause : clause * atom list; + } + and proof_node = { conclusion : clause; step : step; } - and proof = clause * atom list and step = | Hypothesis | Lemma of lemma | Resolution of proof * proof * atom - let expand (c, cl) = - let st = match H.find proof cl with + let expand { clause = (c, cl); table; } = + let st = match H.find table cl with | Assumption -> Hypothesis | Lemma l -> Lemma l | Resolution (a, cl_c, cl_d) -> - Resolution (cl_c, cl_d, a) + Resolution ({ clause = cl_c; table}, {clause = cl_d; table}, a) in { conclusion = c; step = st } let prove_unsat c = assert_can_prove_unsat c; - (St.empty_clause, []) + {clause = St.empty_clause, []; table = !proof; } (* Compute unsat-core *) let compare_cl c d = @@ -270,15 +284,15 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct | Enter of proof | Leaving of proof - let pop s = try Some (Stack.pop s) with Stack.Empty -> None + let spop s = try Some (Stack.pop s) with Stack.Empty -> None let rec fold_aux s h f acc = - match pop s with + match spop s with | None -> acc - | Some (Leaving ((_, cl) as p)) -> + | Some (Leaving ({clause = (_, cl)} as p)) -> H.add h cl true; fold_aux s h f (f acc (expand p)) - | Some (Enter ((_, cl) as p)) -> + | Some (Enter ({clause = (_, cl)} as p)) -> if not (H.mem h cl) then begin Stack.push (Leaving p) s; let node = expand p in diff --git a/solver/res.mli b/solver/res.mli index fef361ca..6fe8f9e9 100644 --- a/solver/res.mli +++ b/solver/res.mli @@ -8,5 +8,9 @@ module type S = Res_intf.S module Make : functor (L : Log_intf.S) -> - functor (St : Solver_types.S) -> S with module St = St + functor (St : Solver_types.S) -> sig + include S with module St = St + val push : unit -> int + val pop : int -> unit + end (** Functor to create a module building proofs from a sat-solver unsat trace. *)