From e30c54e11bcec2bc24e04ed1b79403a4be32867f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 15 Feb 2019 19:06:39 -0600 Subject: [PATCH] refactor: use hyper-res steps in proofs - accelerates proof checking significantly - provide a way to expand hyper-res steps into individual resolutions (eg for the Coq backend) --- src/backend/Coq.ml | 3 +- src/backend/Dot.ml | 23 +++++--- src/core/Internal.ml | 128 ++++++++++++++++++++++++++-------------- src/core/Solver_intf.ml | 15 ++++- 4 files changed, 112 insertions(+), 57 deletions(-) diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml index e4e9f56b..ffb736fd 100644 --- a/src/backend/Coq.ml +++ b/src/backend/Coq.ml @@ -134,7 +134,8 @@ module Make(S : Msat.S)(A : Arg with type hyp := S.clause let c = P.conclusion p in let () = elim_duplicate fmt clause c l in clean t fmt [c] - | P.Resolution (p1, p2, a) -> + | P.Hyper_res hr -> + let (p1, p2, a) = P.res_of_hyper_res hr in let c1 = P.conclusion p1 in let c2 = P.conclusion p2 in if resolution fmt clause c1 c2 a then clean t fmt [c1; c2] diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index ea1badcd..2ae46139 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -58,10 +58,9 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom module P = S.Proof let node_id n = Clause.name n.P.conclusion - - let res_node_id n = (node_id n) ^ "_res" - let proof_id p = node_id (P.expand p) + let res_nn_id n1 n2 = node_id n1 ^ "_" ^ node_id n2 ^ "_res" + let res_np_id n1 n2 = node_id n1 ^ "_" ^ proof_id n2 ^ "_res" let print_clause fmt c = let v = Clause.atoms c in @@ -80,9 +79,11 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom let print_edges fmt n = match P.(n.step) with - | P.Resolution (p1, p2, _) -> - print_edge fmt (res_node_id n) (proof_id p1); - print_edge fmt (res_node_id n) (proof_id p2) + | P.Hyper_res {P.hr_init; hr_steps} -> + print_edge fmt (res_np_id n hr_init) (proof_id hr_init); + List.iter + (fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2)) + hr_steps; | _ -> () let table_options fmt color = @@ -129,11 +130,15 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) :: List.map (ttify A.print_atom) l); print_edge fmt (node_id n) (node_id (P.expand p)) - | P.Resolution (_, _, a) -> + | P.Hyper_res {P.hr_init; hr_steps} -> print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY" [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; - print_dot_res_node fmt (res_node_id n) a; - print_edge fmt (node_id n) (res_node_id n) + print_edge fmt (node_id n) (res_np_id n hr_init); + List.iter + (fun (a,p2) -> + print_dot_res_node fmt (res_np_id n p2) a; + print_edge fmt (node_id n) (res_np_id n p2)) + hr_steps let print_node fmt n = print_contents fmt n; diff --git a/src/core/Internal.ml b/src/core/Internal.ml index a1c5c338..03511c7d 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -302,6 +302,8 @@ module Make(Plugin : PLUGIN) let debug_a out vec = Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec + let debug_l out l = + List.iter (fun a -> Format.fprintf out "%a@ " debug a) l module Set = Set.Make(struct type t=atom let compare=compare end) end @@ -360,6 +362,7 @@ module Make(Plugin : PLUGIN) let[@inline] equal c1 c2 = c1.cid = c2.cid let[@inline] hash c = Hashtbl.hash c.cid let[@inline] atoms c = c.atoms + let[@inline] atoms_seq c = Sequence.of_array c.atoms let[@inline] atoms_l c = Array.to_list c.atoms let flag_attached = 0b1 @@ -424,9 +427,10 @@ module Make(Plugin : PLUGIN) let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg - let[@inline] cleanup_ (a:atom) = Var.clear a.var + let[@inline] clear_var_of_ (a:atom) = Var.clear a.var - (* Compute resolution of 2 clauses *) + (* Compute resolution of 2 clauses. + returns [pivots, resulting_atoms] *) let resolve (c1:clause) (c2:clause) : atom list * atom list = (* invariants: only atoms in [c2] are marked, and the pivot is cleared when traversing [c1] *) @@ -438,7 +442,7 @@ module Make(Plugin : PLUGIN) if Atom.seen a then l else if Atom.seen a.neg then ( pivots := a.var.pa :: !pivots; - cleanup_ a; + clear_var_of_ a; l ) else a::l) [] c1.atoms @@ -446,7 +450,7 @@ module Make(Plugin : PLUGIN) let l = Array.fold_left (fun l a -> if Atom.seen a then a::l else l) l c2.atoms in - Array.iter cleanup_ c2.atoms; + Array.iter clear_var_of_ c2.atoms; !pivots, l (* [find_dups c] returns a list of duplicate atoms, and the deduplicated list *) @@ -462,15 +466,15 @@ module Make(Plugin : PLUGIN) )) ([], []) c.atoms in - Array.iter cleanup_ c.atoms; + Array.iter clear_var_of_ c.atoms; res (* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *) - let same_lits (c1:atom array) (c2:atom array): bool = + let same_lits (c1:atom Sequence.t) (c2:atom Sequence.t): bool = let subset a b = - Array.iter Atom.mark b; - let res = Array.for_all Atom.seen a in - Array.iter cleanup_ b; + Sequence.iter Atom.mark b; + let res = Sequence.for_all Atom.seen a in + Sequence.iter clear_var_of_ b; res in subset c1 c2 && subset c2 c1 @@ -533,7 +537,12 @@ module Make(Plugin : PLUGIN) | Assumption | Lemma of lemma | Duplicate of t * atom list - | Resolution of t * t * atom + | Hyper_res of hyper_res_step + + and hyper_res_step = { + hr_init: t; + hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) + } let[@inline] conclusion (p:t) : clause = p @@ -544,31 +553,51 @@ module Make(Plugin : PLUGIN) rs_pivot: atom; } - let rec chain_res (c:clause) (hist:_ list) : res_step = - match hist with - | d :: r -> - Log.debugf 5 - (fun k -> k "(@[sat.analyze.resolving@ :c1 %a@ :c2 %a@])" Clause.debug c Clause.debug d); - begin match resolve c d with - | [a], l -> - begin match r with - | [] -> {rs_res=l; rs_c1=c; rs_c2=d; rs_pivot=a} - | _ -> - let new_clause = Clause.make ~flags:c.flags l (History [c; d]) in - chain_res new_clause r - end - | _ -> - error_res_f "@[<2>clause mismatch while resolving@ %a@ and %a@]" - Clause.debug c Clause.debug d - end - | _ -> - error_res_f "bad history" + (* find pivots for resolving [l] with [init], and also return + the atoms of the conclusion *) + let find_pivots (init:clause) (l:clause list) : _ * (atom * t) list = + Log.debugf 15 + (fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])" + Clause.debug init (Format.pp_print_list Clause.debug) l); + Array.iter Atom.mark init.atoms; + let steps = + List.map + (fun c -> + let pivot = + match + Sequence.of_array c.atoms + |> Sequence.filter (fun a -> Atom.seen (Atom.neg a)) + |> Sequence.to_list + with + | [a] -> a + | [] -> + error_res_f "(@[proof.expand.pivot_missing@ %a@])" Clause.debug c + | pivots -> + error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])" + Clause.debug c Atom.debug_l pivots + in + Array.iter Atom.mark c.atoms; (* add atoms to result *) + clear_var_of_ pivot; + Atom.abs pivot, c) + l + in + (* cleanup *) + let res = ref [] in + let cleanup_a_ a = + if Atom.seen a then ( + res := a :: !res; + clear_var_of_ a + ) + in + Array.iter cleanup_a_ init.atoms; + List.iter (fun c -> Array.iter cleanup_a_ c.atoms) l; + !res, steps let expand conclusion = Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" Clause.debug conclusion); match conclusion.cpremise with | Lemma l -> - {conclusion; step = Lemma l; } + { conclusion; step = Lemma l; } | Local -> { conclusion; step = Assumption; } | Hyp l -> @@ -577,40 +606,51 @@ module Make(Plugin : PLUGIN) error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion | History [c] -> let duplicates, res = find_dups c in - assert (same_lits (Array.of_list res) conclusion.atoms); + assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion)); { conclusion; step = Duplicate (c, duplicates) } | History (c :: ([_] as r)) -> - let rs = chain_res c r in - assert (same_lits (Array.of_list rs.rs_res) conclusion.atoms); - { conclusion; step = Resolution (rs.rs_c1, rs.rs_c2, rs.rs_pivot); } + let res, steps = find_pivots c r in + assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion)); + { conclusion; step = Hyper_res { hr_init=c; hr_steps=steps; }; } | History (c :: r) -> - let rs = chain_res c r in - conclusion.cpremise <- History [rs.rs_c1; rs.rs_c2]; - assert (same_lits (Array.of_list rs.rs_res) conclusion.atoms); - { conclusion; step = Resolution (rs.rs_c1, rs.rs_c2, rs.rs_pivot); } + let res, steps = find_pivots c r in + assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion)); + { conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; } | Empty_premise -> raise Solver_intf.No_proof + let rec res_of_hyper_res (hr: hyper_res_step) : _ * _ * atom = + let {hr_init=c1; hr_steps=l} = hr in + match l with + | [] -> assert false + | [a, c2] -> c1, c2, a (* done *) + | (a,c2) :: steps' -> + (* resolve [c1] with [c2], then resolve that against [steps] *) + let pivots, l = resolve c1 c2 in + assert (match pivots with [a'] -> Atom.equal a a' | _ -> false); + let c_1_2 = Clause.make_removable l (History [c1; c2]) in + res_of_hyper_res {hr_init=c_1_2; hr_steps=steps'} + (* Proof nodes manipulation *) let is_leaf = function | Hypothesis _ | Assumption | Lemma _ -> true | Duplicate _ - | Resolution _ -> false + | Hyper_res _ -> false let parents = function | Hypothesis _ | Assumption | Lemma _ -> [] | Duplicate (p, _) -> [p] - | Resolution (p, p', _) -> [p; p'] + | Hyper_res {hr_init; hr_steps} -> hr_init :: List.map snd hr_steps let expl = function | Hypothesis _ -> "hypothesis" | Assumption -> "assumption" | Lemma _ -> "lemma" | Duplicate _ -> "duplicate" - | Resolution _ -> "resolution" + | Hyper_res _ -> "hyper-resolution" (* Compute unsat-core TODO: replace visited bool by a int unique to each call @@ -658,9 +698,9 @@ module Make(Plugin : PLUGIN) begin match node.step with | Duplicate (p1, _) -> Stack.push (Enter p1) s - | Resolution (p1, p2, _) -> - Stack.push (Enter p2) s; - Stack.push (Enter p1) s + | Hyper_res {hr_init=p1; hr_steps=l} -> + List.iter (fun (_,p2) -> Stack.push (Enter p2) s) l; + Stack.push (Enter p1) s; | Hypothesis _ | Assumption | Lemma _ -> () end end; diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 4f50a6e7..8ed3d9f1 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -286,9 +286,12 @@ module type PROOF = sig | Duplicate of t * atom list (** The conclusion is obtained by eliminating multiple occurences of the atom in the conclusion of the provided proof. *) - | Resolution of t * t * atom - (** The conclusion can be deduced by performing a resolution between the conclusions - of the two given proofs. The atom on which to perform the resolution is also given. *) + | Hyper_res of hyper_res_step + + and hyper_res_step = { + hr_init: t; + hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) + } (** {3 Proof building functions} *) @@ -303,6 +306,12 @@ module type PROOF = sig val prove_atom : atom -> t option (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *) + val res_of_hyper_res : hyper_res_step -> t * t * atom + (** Turn an hyper resolution step into a resolution step. + The conclusion can be deduced by performing a resolution between the conclusions + of the two given proofs. + The atom on which to perform the resolution is also given. *) + (** {3 Proof Nodes} *) val parents : step -> t list