From 434697ea478faacd4410faec7b2076b911da7337 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 28 Jul 2015 23:23:05 +0200 Subject: [PATCH] Better dot backend --- backend/dot.ml | 5 ++--- backend/dot.mli | 2 +- msat.mlpack | 1 + opam | 2 +- tests/run | 2 +- util/sat_solve.ml | 15 +++++++++------ 6 files changed, 15 insertions(+), 12 deletions(-) diff --git a/backend/dot.ml b/backend/dot.ml index ab8ca4a7..894449a5 100644 --- a/backend/dot.ml +++ b/backend/dot.ml @@ -8,7 +8,7 @@ module type Arg = sig val clause_name : clause -> string val print_atom : Format.formatter -> atom -> unit - val lemma_info : lemma -> string * string option * atom list + val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list end module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) = struct @@ -57,9 +57,8 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.cla print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE" [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))]; | S.Lemma lemma -> - let rule, color, args = A.lemma_info lemma in + let rule, color, l = A.lemma_info lemma in let color = match color with None -> "YELLOW" | Some c -> c in - let l = List.map (ttify A.print_atom) 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" diff --git a/backend/dot.mli b/backend/dot.mli index 10ee95ef..2520aef4 100644 --- a/backend/dot.mli +++ b/backend/dot.mli @@ -8,7 +8,7 @@ module type Arg = sig val clause_name : clause -> string val print_atom : Format.formatter -> atom -> unit - val lemma_info : lemma -> string * string option * atom list + val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list end module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) : diff --git a/msat.mlpack b/msat.mlpack index dc460ee5..ffd5248e 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -9,6 +9,7 @@ Plugin_intf Expr_intf Tseitin_intf Res_intf +Solver_types_intf # Solver Modules Internal diff --git a/opam b/opam index e4e7d2ec..b4cb96fa 100644 --- a/opam +++ b/opam @@ -1,6 +1,6 @@ opam-version: "1.2" license: "Apache" -version: "1.1" +version: "dev" author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"] maintainer: ["guillaume.bury@gmail.com" "simon.cruanes@inria.fr"] build: [ diff --git a/tests/run b/tests/run index 7ad8e67a..882ff2a2 100755 --- a/tests/run +++ b/tests/run @@ -7,7 +7,7 @@ solvertest () { for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'` do echo -ne "\r\033[KTesting $f..." - "$SOLVER" -s $3 -check -time 30s -size 1G $f | grep $2 > /dev/null 2> /dev/null + "$SOLVER" -s $3 -check -time 30s -size 1G $f | grep $2 RET=$? if [ $RET -ne 0 ]; then diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 51e4980c..afabf93e 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -91,8 +91,11 @@ let parse_input file = let std = Format.std_formatter let print format = match !output with - | Standard -> Format.fprintf std "%( fmt %)@." format - | Dot -> Format.fprintf std "/* %( fmt %) */@." format + | Standard -> + Format.kfprintf (fun fmt -> Format.fprintf fmt "@.") std format + | Dot -> + Format.fprintf std "/* "; + Format.kfprintf (fun fmt -> Format.fprintf fmt " */@.") std format let print_proof proof = match !output with | Standard -> () @@ -225,12 +228,12 @@ let main () = Gc.delete_alarm al; begin match res with | Smt.Sat -> - print "Sat"; + print "Sat (%f)" (Sys.time ()); if !p_check then if not (List.for_all (List.exists Smt.eval) cnf) then raise Incorrect_model | Smt.Unsat -> - print "Unsat"; + print "Unsat (%f)" (Sys.time ()); if !p_check then begin let p = Smt.get_proof () in print_proof p; @@ -244,12 +247,12 @@ let main () = Gc.delete_alarm al; begin match res with | Mcsat.Sat -> - print "Sat"; + print "Sat (%f)" (Sys.time ()); if !p_check then if not (List.for_all (List.exists Mcsat.eval) cnf) then raise Incorrect_model | Mcsat.Unsat -> - print "Unsat"; + print "Unsat (%f)" (Sys.time ()); if !p_check then begin let p = Mcsat.get_proof () in print_mcproof p;