From 9c1ca06aeab49d4719066842659f5f755c5cd3c0 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 9 Jul 2015 19:03:44 +0200 Subject: [PATCH] Dot output is now available through independent backend --- backend/backend_intf.ml | 15 +++++++ backend/dedukti.ml | 30 ++++++++++++++ backend/dedukti.mli | 8 ++++ backend/dot.ml | 79 +++++++++++++++++++++++++++++++++++++ msat.mlpack | 1 + sat/sat.ml | 4 +- smt/.merlin | 10 ----- smt/mcsat.ml | 4 +- smt/smt.ml | 4 +- solver/.merlin | 6 --- solver/internal.ml | 3 +- solver/mcsolver.mli | 1 + solver/res.ml | 39 +++++++++++++++--- solver/res_intf.ml | 11 +++++- solver/solver.mli | 1 + solver/solver_types.ml | 30 ++++++++------ solver/solver_types_intf.ml | 1 - 17 files changed, 207 insertions(+), 40 deletions(-) create mode 100644 backend/backend_intf.ml create mode 100644 backend/dedukti.ml create mode 100644 backend/dedukti.mli create mode 100644 backend/dot.ml delete mode 100644 smt/.merlin delete mode 100644 solver/.merlin diff --git a/backend/backend_intf.ml b/backend/backend_intf.ml new file mode 100644 index 00000000..82205f94 --- /dev/null +++ b/backend/backend_intf.ml @@ -0,0 +1,15 @@ + +module type Arg = sig + type proof + type formula + val prove : Format.formatter -> formula list -> unit + val context : Format.formatter -> proof -> unit + val translate : Format.formatter -> formula -> unit +end + +module type S = sig + type t + val print : Format.formatter -> t -> unit +end + + diff --git a/backend/dedukti.ml b/backend/dedukti.ml new file mode 100644 index 00000000..107d9fe5 --- /dev/null +++ b/backend/dedukti.ml @@ -0,0 +1,30 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module type S = Backend_intf.S + +module Make(S : Res.S)(A : Backend_intf.Arg with type formula := S.atom and type proof := S.proof) = struct + + let print_aux fmt = Format.fprintf fmt "@\n" + + let fprintf fmt format = Format.kfprintf print_aux fmt format + + let context fmt () = + fprintf fmt "(; Embedding ;)"; + fprintf fmt "Prop : Type."; + fprintf fmt "_proof : Prop -> Type."; + fprintf fmt "(; Notations for clauses ;)"; + fprintf fmt "_pos : Prop -> Prop -> Type."; + fprintf fmt "_neg : Prop -> Prop -> Type."; + fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b."; + fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b." + + let print fmt _ = + context fmt (); + () + +end + diff --git a/backend/dedukti.mli b/backend/dedukti.mli new file mode 100644 index 00000000..9f1b3ee9 --- /dev/null +++ b/backend/dedukti.mli @@ -0,0 +1,8 @@ + +module type S = Backend_intf.S + +module Make : + functor(S : Res.S) -> + functor(A : Backend_intf.Arg with type formula := S.atom and type proof := S.proof) -> + S with type t := S.proof +(** Functor to generate a backend to output proofs for the dedukti type checker. *) diff --git a/backend/dot.ml b/backend/dot.ml new file mode 100644 index 00000000..8a00ef27 --- /dev/null +++ b/backend/dot.ml @@ -0,0 +1,79 @@ + +module type S = Backend_intf.S + +module Make + (St : Solver_types.S) + (S : Res.S with type clause = St.clause + and type lemma = St.proof + and type atom = St.atom) = struct + + let clause_id c = St.(c.name) + + let node_id n = clause_id S.(n.conclusion) + + let res_node_id n = (node_id n) ^ "_res" + + let proof_id p = node_id (S.expand p) + + let print_edge fmt i j = + Format.fprintf fmt "%s -> %s;@\n" i j + + let print_edges fmt n = + match S.(n.step) with + | S.Resolution (p1, p2, _) -> + print_edge fmt (res_node_id n) (proof_id p1); + print_edge fmt (res_node_id n) (proof_id p2) + | _ -> () + + let table_options fmt color = + Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color + + let table fmt (c, rule, color, l) = + Format.fprintf fmt "%a" S.print_clause c; + match l with + | [] -> + Format.fprintf fmt "%s" color rule + | f :: r -> + Format.fprintf fmt "%s%a" + color (List.length l) rule f (); + List.iter (fun f -> Format.fprintf fmt "%a" f ()) r + + let print_dot_node fmt id color c rule rule_color l = + Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" + id table_options color table (c, rule, rule_color, l) + + let print_dot_res_node fmt id a = + Format.fprintf fmt "%s [label=\"%a\"];@\n" id St.print_atom a + + let ttify f c = fun fmt () -> f fmt c + + let print_contents fmt n = + match S.(n.step) with + | S.Hypothesis -> + print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE" + [(fun fmt () -> (Format.fprintf fmt "%s" n.S.conclusion.St.name))]; + | S.Lemma lemma -> + let rule, f_args, t_args, color = St.proof_debug lemma in + let color = match color with None -> "YELLOW" | Some c -> c in + let l = List.map (ttify St.print_atom) f_args @ + List.map (ttify St.print_lit) t_args in + print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l + | S.Resolution (_, _, a) -> + print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY" + [(fun fmt () -> (Format.fprintf fmt "%s" n.S.conclusion.St.name))]; + print_dot_res_node fmt (res_node_id n) a; + print_edge fmt (node_id n) (res_node_id n) + + let print_node fmt n = + print_contents fmt n; + print_edges fmt n + + let print fmt p = + Format.fprintf fmt "digraph proof {@\n"; + S.fold (fun () -> print_node fmt) () p; + Format.fprintf fmt "}@." + +end + + + diff --git a/msat.mlpack b/msat.mlpack index b83d8281..dc460ee5 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -17,6 +17,7 @@ Mcsolver Solver_types # Backends +Dot Dedukti # Auxiliary modules diff --git a/sat/sat.ml b/sat/sat.ml index fe1ed80a..40731ee6 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -88,7 +88,9 @@ module Tsat = struct end module Make(Log : Log_intf.S) = struct + module SatSolver = Solver.Make(Log)(Fsat)(Tsat) + module Dot = Dot.Make(SatSolver.St)(SatSolver.Proof) exception Bad_atom @@ -150,6 +152,6 @@ module Make(Log : Log_intf.S) = struct let print_atom = Fsat.print let print_clause = SatSolver.St.print_clause - let print_proof = SatSolver.Proof.print_dot + let print_proof = Dot.print end diff --git a/smt/.merlin b/smt/.merlin deleted file mode 100644 index 022353bf..00000000 --- a/smt/.merlin +++ /dev/null @@ -1,10 +0,0 @@ -S ./ -S ../sat/ -S ../util/ -S ../solver/ - -B ../_build/ -B ../_build/sat/ -B ../_build/smt/ -B ../_build/util/ -B ../_build/solver/ diff --git a/smt/mcsat.ml b/smt/mcsat.ml index 515181cc..ce4fd320 100644 --- a/smt/mcsat.ml +++ b/smt/mcsat.ml @@ -113,7 +113,9 @@ module Tsmt = struct end module Make(Dummy:sig end) = struct + module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt) + module Dot = Dot.Make(SmtSolver.St)(SmtSolver.Proof) type atom = Fsmt.t type clause = SmtSolver.St.clause @@ -146,5 +148,5 @@ module Make(Dummy:sig end) = struct let print_atom = Fsmt.print let print_clause = SmtSolver.St.print_clause - let print_proof = SmtSolver.Proof.print_dot + let print_proof = Dot.print end diff --git a/smt/smt.ml b/smt/smt.ml index 0a076f15..6ef3ad7f 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -59,7 +59,9 @@ module Tsmt = struct end module Make(Dummy:sig end) = struct + module SmtSolver = Solver.Make(Log)(Fsmt)(Tsmt) + module Dot = Dot.Make(SmtSolver.St)(SmtSolver.Proof) type atom = Fsmt.t type clause = SmtSolver.St.clause @@ -91,5 +93,5 @@ module Make(Dummy:sig end) = struct let print_atom = Fsmt.print let print_clause = SmtSolver.St.print_clause - let print_proof = SmtSolver.Proof.print_dot + let print_proof = Dot.print end diff --git a/solver/.merlin b/solver/.merlin deleted file mode 100644 index d9b70b68..00000000 --- a/solver/.merlin +++ /dev/null @@ -1,6 +0,0 @@ -S ./ -S ../util/ - -B ../_build/ -B ../_build/solver/ -B ../_build/util/ diff --git a/solver/internal.ml b/solver/internal.ml index e3dbfc5a..6ce611b9 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -521,10 +521,9 @@ module Make (L : Log_intf.S)(St : Solver_types.S) | [] -> report_unsat init0; | a::b::_ -> - let name = fresh_name () in let clause = if init then init0 - else make_clause ?tag name atoms size true (History [init0]) + else make_clause ?tag (fresh_name ()) atoms size true (History [init0]) in L.debug 1 "New clause : %a" St.pp_clause clause; attach_clause clause; diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index 58ac31cc..d7f8b5d3 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -13,6 +13,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) module St : Solver_types.S with type term = E.Term.t and type formula = E.Formula.t + and type proof = Th.proof module Proof : Res.S with type atom = St.atom diff --git a/solver/res.ml b/solver/res.ml index 93746de3..79a9823a 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -91,6 +91,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct L.debug 3 "Input clause is a tautology"; res + let print_clause fmt c = print_cl fmt (to_list c) + (* Adding hyptoheses *) let has_been_proved c = H.mem proof (to_list c) @@ -225,7 +227,6 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct | Resolution of proof * proof * atom 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 @@ -261,6 +262,38 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct in sort_uniq compare_cl (aux [] proof) + (* Iter on proofs *) + type task = + | Enter of proof + | Leaving of proof + + let pop s = try Some (Stack.pop s) with Stack.Empty -> None + + let rec fold_aux s h f acc = + match pop s with + | None -> acc + | Some (Leaving ((_, cl) as p)) -> + H.add h cl true; + fold_aux s h f (f acc (expand p)) + | Some (Enter ((_, cl) as p)) -> + if not (H.mem h cl) then begin + Stack.push (Leaving p) s; + let node = expand p in + begin match node.step with + | Resolution (p1, p2, _) -> + Stack.push (Enter p2) s; + Stack.push (Enter p1) s + | _ -> () + end + end; + fold_aux s h f acc + + let fold f acc p = + let h = H.create 42 in + let s = Stack.create () in + Stack.push (Enter p) s; + fold_aux s h f acc + (* Dot proof printing *) module Dot = struct let _i = ref 0 @@ -289,10 +322,6 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct 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 diff --git a/solver/res_intf.ml b/solver/res_intf.ml index 9ce663d3..7334cdc4 100644 --- a/solver/res_intf.ml +++ b/solver/res_intf.ml @@ -72,13 +72,20 @@ module type S = sig val expand : proof -> proof_node (** Return the proof step at the root of a given proof. *) + val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a + (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that + [f] is executed exactly once on each proof ndoe in the tree, and that the execution of + [f] on a proof node happens after the execution on the children of the nodes. *) + 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. - @deprecated *) + @deprecated use the Dot backend module instead. *) - module Dot : Backend_intf.S with type t := proof + (** {3 Misc} *) + val print_clause : Format.formatter -> clause -> unit + (** A nice looking printer for clauses, which sort the atoms before printing. *) end diff --git a/solver/solver.mli b/solver/solver.mli index ab28c2b9..53e88b3d 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -20,6 +20,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) module St : Solver_types.S with type formula = F.t + and type proof = Th.proof module Proof : Res.S with type atom = St.atom diff --git a/solver/solver_types.ml b/solver/solver_types.ml index af0f4c47..4e45a7e6 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -259,11 +259,15 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with let print_atom fmt a = E.Formula.print fmt a.lit let print_atoms fmt v = - print_atom fmt (Vec.get v 0); - if (Vec.size v) > 1 then begin - for i = 1 to (Vec.size v) - 1 do - Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i) - done + if Vec.size v = 0 then + Format.fprintf fmt "∅" + else begin + print_atom fmt (Vec.get v 0); + if (Vec.size v) > 1 then begin + for i = 1 to (Vec.size v) - 1 do + Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i) + done + end end let print_clause fmt c = @@ -518,7 +522,7 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S) let iter_sub _ _ = () (* Proof debug info *) - let proof_debug _ = assert false + let proof_debug _ = "lemma", [], [], None (* Pretty printing for atoms and clauses *) let print_lit _ _ = assert false @@ -526,11 +530,15 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S) let print_atom fmt a = E.print fmt a.lit let print_atoms fmt v = - print_atom fmt (Vec.get v 0); - if (Vec.size v) > 1 then begin - for i = 1 to (Vec.size v) - 1 do - Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i) - done + if Vec.size v = 0 then + Format.fprintf fmt "∅" + else begin + print_atom fmt (Vec.get v 0); + if (Vec.size v) > 1 then begin + for i = 1 to (Vec.size v) - 1 do + Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i) + done + end end let print_clause fmt c = diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index 5e1e8f0f..fd1c506a 100644 --- a/solver/solver_types_intf.ml +++ b/solver/solver_types_intf.ml @@ -16,7 +16,6 @@ module type S = sig val mcsat : bool - (** {2 Type definitions} *) type term