From 4b51f22464de98deae0f5f0639aac29e01457a72 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 9 Jul 2015 16:29:57 +0200 Subject: [PATCH] Changed internal representation of proofs --- .merlin | 2 + Makefile | 2 +- _tags | 1 + msat.mlpack | 3 + msat.odocl | 2 + solver/internal.ml | 1 - solver/res.ml | 186 +++++++++++++++++++++++---------------------- solver/res_intf.ml | 20 +++-- 8 files changed, 118 insertions(+), 99 deletions(-) diff --git a/.merlin b/.merlin index 63265db9..2354e067 100644 --- a/.merlin +++ b/.merlin @@ -2,9 +2,11 @@ S sat S smt S solver S util +S backend B _build/ B _build/sat B _build/smt B _build/solver B _build/util +B _build/backend diff --git a/Makefile b/Makefile index bdaf5f5a..42240609 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display FLAGS= -DIRS=-Is solver,sat,smt,util,util/smtlib +DIRS=-Is solver,sat,smt,backend,util,util/smtlib DOC=msat.docdir/index.html TEST=sat_solve.native diff --git a/_tags b/_tags index ed5642f1..044a9402 100644 --- a/_tags +++ b/_tags @@ -3,6 +3,7 @@ : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) +: for-pack(Msat) # enable stronger inlining everywhere : inline(100) diff --git a/msat.mlpack b/msat.mlpack index 9aac5035..b83d8281 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -16,6 +16,9 @@ Solver Mcsolver Solver_types +# Backends +Dedukti + # Auxiliary modules Res Tseitin diff --git a/msat.odocl b/msat.odocl index 08fe2c1f..677dea71 100644 --- a/msat.odocl +++ b/msat.odocl @@ -22,3 +22,5 @@ solver/Tseitin solver/Tseitin_intf sat/Sat + +backend/Dedukti diff --git a/solver/internal.ml b/solver/internal.ml index a8508997..e3dbfc5a 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -395,7 +395,6 @@ module Make (L : Log_intf.S)(St : Solver_types.S) (* visit the current predecessors *) for j = 0 to Vec.size !c.atoms - 1 do let q = Vec.get !c.atoms j in - (*printf "I visit %a@." D1.atom q;*) assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) if not q.var.seen && q.var.level > 0 then begin var_bump_activity q.var; diff --git a/solver/res.ml b/solver/res.ml index fb258703..93746de3 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -218,25 +218,25 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct conclusion : clause; step : step; } - and proof = unit -> proof_node + and proof = clause * atom list and step = | Hypothesis | Lemma of lemma | Resolution of proof * proof * atom - let rec return_proof (c, cl) () = + let expand (c, cl) = L.debug 8 "Returning proof for : %a" St.pp_clause c; let st = match H.find proof cl with | Assumption -> Hypothesis | Lemma l -> Lemma l | Resolution (a, cl_c, cl_d) -> - Resolution (return_proof cl_c, return_proof cl_d, a) + Resolution (cl_c, cl_d, a) in { conclusion = c; step = st } let prove_unsat c = assert_can_prove_unsat c; - return_proof (St.empty_clause, []) + (St.empty_clause, []) (* Compute unsat-core *) let compare_cl c d = @@ -253,7 +253,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct let unsat_core proof = let rec aux acc proof = - let p = proof () in + let p = expand proof in match p.step with | Hypothesis | Lemma _ -> p.conclusion :: acc | Resolution (proof1, proof2, _) -> @@ -261,105 +261,109 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct in sort_uniq compare_cl (aux [] proof) - (* Print proof graph *) - let _i = ref 0 - let new_id () = incr _i; "id_" ^ (string_of_int !_i) + (* Dot proof printing *) + module Dot = struct + let _i = ref 0 + let new_id () = incr _i; "id_" ^ (string_of_int !_i) - let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;; - let c_id c = - try - snd (Hashtbl.find ids c) - with Not_found -> + let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;; + let c_id c = + try + snd (Hashtbl.find ids c) + with Not_found -> + let id = new_id () in + Hashtbl.add ids c (false, id); + id + + let clear_ids () = + Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids + + let is_drawn c = + ignore (c_id c); + fst (Hashtbl.find ids c) + + let has_drawn c = + if not (is_drawn c) then + let b, id = Hashtbl.find ids c in + Hashtbl.replace ids c (true, id) + else + () + + (* We use a custom function instead of the functions in Solver_type, + so that atoms are sorted before printing. *) + let print_clause fmt c = print_cl fmt (to_list c) + + let print_dot_rule opt f arg fmt cl = + Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" + (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" opt f arg + + let print_dot_edge id_c fmt id_d = + Format.fprintf fmt "%s -> %s;@\n" id_c id_d + + let print_res_atom id fmt a = + Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a + + let print_res_node concl p1 p2 fmt atom = let id = new_id () in - Hashtbl.add ids c (false, id); - id + Format.fprintf fmt "%a;@\n%a%a%a" + (print_res_atom id) atom + (print_dot_edge (c_id concl)) id + (print_dot_edge id) (c_id p1) + (print_dot_edge id) (c_id p2) - let clear_ids () = - Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids - - let is_drawn c = - ignore (c_id c); - fst (Hashtbl.find ids c) - - let has_drawn c = - if not (is_drawn c) then - let b, id = Hashtbl.find ids c in - Hashtbl.replace ids c (true, id) - else - () - - (* We use a custom function instead of the functions in Solver_type, - so that atoms are sorted before printing. *) - let print_clause fmt c = print_cl fmt (to_list c) - - let print_dot_rule opt f arg fmt cl = - Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" - (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" opt f arg - - let print_dot_edge id_c fmt id_d = - Format.fprintf fmt "%s -> %s;@\n" id_c id_d - - let print_res_atom id fmt a = - Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a - - let print_res_node concl p1 p2 fmt atom = - let id = new_id () in - Format.fprintf fmt "%a;@\n%a%a%a" - (print_res_atom id) atom - (print_dot_edge (c_id concl)) id - (print_dot_edge id) (c_id p1) - (print_dot_edge id) (c_id p2) - - let color s = match s.[0] with + let color s = match s.[0] with | 'E' -> "BGCOLOR=\"GREEN\"" | 'L' -> "BGCOLOR=\"GREEN\"" | _ -> "BGCOLOR=\"GREY\"" - let rec print_dot_proof fmt p = - if not (is_drawn p.conclusion) then begin - has_drawn p.conclusion; - match p.step with - | Hypothesis -> - let aux fmt () = - Format.fprintf fmt "%aHypothesis%s" - print_clause p.conclusion St.(p.conclusion.name) - in - print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion - | Lemma proof -> - let name, f_args, t_args, color = St.proof_debug proof in - let color = match color with None -> "YELLOW" | Some c -> c in - let aux fmt () = - Format.fprintf fmt "%a%s" - print_clause p.conclusion color (max (List.length f_args + List.length t_args) 1) name; - if f_args <> [] then + let rec print_dot_proof fmt p = + if not (is_drawn p.conclusion) then begin + has_drawn p.conclusion; + match p.step with + | Hypothesis -> + let aux fmt () = + Format.fprintf fmt "%aHypothesis%s" + print_clause p.conclusion St.(p.conclusion.name) + in + print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion + | Lemma proof -> + let name, f_args, t_args, color = St.proof_debug proof in + let color = match color with None -> "YELLOW" | Some c -> c in + let aux fmt () = + Format.fprintf fmt "%a%s" + print_clause p.conclusion color (max (List.length f_args + List.length t_args) 1) name; + if f_args <> [] then Format.fprintf fmt "%a%a%a" St.print_atom (List.hd f_args) (fun fmt -> List.iter (fun a -> Format.fprintf fmt "%a" St.print_atom a)) (List.tl f_args) (fun fmt -> List.iter (fun v -> Format.fprintf fmt "%a" St.print_lit v)) t_args - else if t_args <> [] then - Format.fprintf fmt "%a%a" St.print_lit (List.hd t_args) + else if t_args <> [] then + Format.fprintf fmt "%a%a" St.print_lit (List.hd t_args) (fun fmt -> List.iter (fun v -> Format.fprintf fmt "%a" St.print_lit v)) (List.tl t_args) - else + else Format.fprintf fmt "" - in - print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion - | Resolution (proof1, proof2, a) -> - let aux fmt () = - Format.fprintf fmt "%a%s%s" - print_clause p.conclusion - "Resolution" St.(p.conclusion.name) - in - let p1 = proof1 () in - let p2 = proof2 () in - Format.fprintf fmt "%a%a%a%a" - (print_dot_rule (color p.conclusion.St.name) aux ()) p.conclusion - (print_res_node p.conclusion p1.conclusion p2.conclusion) a - print_dot_proof p1 - print_dot_proof p2 - end + in + print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion + | Resolution (proof1, proof2, a) -> + let aux fmt () = + Format.fprintf fmt "%a%s%s" + print_clause p.conclusion + "Resolution" St.(p.conclusion.name) + in + let p1 = expand proof1 in + let p2 = expand proof2 in + Format.fprintf fmt "%a%a%a%a" + (print_dot_rule (color p.conclusion.St.name) aux ()) p.conclusion + (print_res_node p.conclusion p1.conclusion p2.conclusion) a + print_dot_proof p1 + print_dot_proof p2 + end - let print_dot fmt proof = - clear_ids (); - Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ()) + let print fmt proof = + clear_ids (); + Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (expand proof) + end + + let print_dot = Dot.print end diff --git a/solver/res_intf.ml b/solver/res_intf.ml index 78344400..9ce663d3 100644 --- a/solver/res_intf.ml +++ b/solver/res_intf.ml @@ -7,7 +7,7 @@ Copyright 2014 Simon Cruanes module type S = sig (** Signature for a module handling proof by resolution from sat solving traces *) - (** {3 Type declarations} *) + (** {3 Type declarations} *) exception Insuficient_hyps (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) @@ -15,18 +15,18 @@ module type S = sig type atom type clause type lemma - (** Abstract types for atoms, clauses and theoriy-specific lemmas *) + (** Abstract types for atoms, clauses and theory-specific lemmas *) - type proof_node = { + type proof + and proof_node = { conclusion : clause; step : step; } - and proof = unit -> proof_node and step = | Hypothesis | Lemma of lemma | Resolution of proof * proof * atom - (** Lazy type for proof trees. *) + (** Lazy type for proof trees. Proofs can be extended to proof nodes using functions defined later. *) (** {3 Resolution helpers} *) val to_list : clause -> atom list @@ -67,10 +67,18 @@ module type S = sig the proof if it succeeds. @raise Insuficient_hyps if it does not succeed. *) + (** {3 Proof Manipulation} *) + + val expand : proof -> proof_node + (** Return the proof step at the root of a given proof. *) + val unsat_core : proof -> clause list (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. *) val print_dot : Format.formatter -> proof -> unit - (** Print the given proof in dot format on the given formatter. *) + (** Print the given proof in dot format on the given formatter. + @deprecated *) + + module Dot : Backend_intf.S with type t := proof end