simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Better dot backend

Browse source
This commit is contained in:
Guillaume Bury 2015-07-28 23:23:05 +02:00
parent aed3aeb17c
commit 434697ea47
6 changed files with 15 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
backend/dot.ml
View file

@ -8,7 +8,7 @@ module type Arg = sig
val clause_name : clause -> string val clause_name : clause -> string
val print_atom : Format.formatter -> atom -> unit 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 end
module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) = struct 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" 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)))]; [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))];
| S.Lemma lemma -> | 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 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 print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
| S.Resolution (_, _, a) -> | S.Resolution (_, _, a) ->
print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY" print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY"

2
backend/dot.mli
View file

@ -8,7 +8,7 @@ module type Arg = sig
val clause_name : clause -> string val clause_name : clause -> string
val print_atom : Format.formatter -> atom -> unit 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 end
module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) : module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) :

1
msat.mlpack
View file

@ -9,6 +9,7 @@ Plugin_intf
Expr_intf Expr_intf
Tseitin_intf Tseitin_intf
Res_intf Res_intf
Solver_types_intf
# Solver Modules # Solver Modules
Internal Internal

2
opam
View file

@ -1,6 +1,6 @@
opam-version: "1.2" opam-version: "1.2"
license: "Apache" license: "Apache"
version: "1.1" version: "dev"
author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"] author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
maintainer: ["guillaume.bury@gmail.com" "simon.cruanes@inria.fr"] maintainer: ["guillaume.bury@gmail.com" "simon.cruanes@inria.fr"]
build: [ build: [

2
tests/run
View file

@ -7,7 +7,7 @@ solvertest () {
for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'` for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`
do do
echo -ne "\r\033[KTesting $f..." 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=$? RET=$?
if [ $RET -ne 0 ]; if [ $RET -ne 0 ];
then then

15
util/sat_solve.ml
View file

@ -91,8 +91,11 @@ let parse_input file =
let std = Format.std_formatter let std = Format.std_formatter
let print format = match !output with let print format = match !output with
| Standard -> Format.fprintf std "%( fmt %)@." format | Standard ->
| Dot -> Format.fprintf std "/* %( fmt %) */@." format 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 let print_proof proof = match !output with
| Standard -> () | Standard -> ()
@ -225,12 +228,12 @@ let main () =
Gc.delete_alarm al; Gc.delete_alarm al;
begin match res with begin match res with
| Smt.Sat -> | Smt.Sat ->
print "Sat"; print "Sat (%f)" (Sys.time ());
if !p_check then if !p_check then
if not (List.for_all (List.exists Smt.eval) cnf) then if not (List.for_all (List.exists Smt.eval) cnf) then
raise Incorrect_model raise Incorrect_model
| Smt.Unsat -> | Smt.Unsat ->
print "Unsat"; print "Unsat (%f)" (Sys.time ());
if !p_check then begin if !p_check then begin
let p = Smt.get_proof () in let p = Smt.get_proof () in
print_proof p; print_proof p;
@ -244,12 +247,12 @@ let main () =
Gc.delete_alarm al; Gc.delete_alarm al;
begin match res with begin match res with
| Mcsat.Sat -> | Mcsat.Sat ->
print "Sat"; print "Sat (%f)" (Sys.time ());
if !p_check then if !p_check then
if not (List.for_all (List.exists Mcsat.eval) cnf) then if not (List.for_all (List.exists Mcsat.eval) cnf) then
raise Incorrect_model raise Incorrect_model
| Mcsat.Unsat -> | Mcsat.Unsat ->
print "Unsat"; print "Unsat (%f)" (Sys.time ());
if !p_check then begin if !p_check then begin
let p = Mcsat.get_proof () in let p = Mcsat.get_proof () in
print_mcproof p; print_mcproof p;