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

Fixed dot printing bug

Browse source
This commit is contained in:
Guillaume Bury 2016-06-26 18:49:21 +02:00
parent 1e2dc299ce
commit f19c6b9b77
4 changed files with 18 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
Makefile
View file

@ -3,7 +3,6 @@
LOG=build.log
COMP=ocamlbuild -log $(LOG) -use-ocamlfind
FLAGS=
# -cflags -color,always
DOC=msat.docdir/index.html
BIN=main.native
NAME=msat

3
_tags
View file

@ -1,3 +1,6 @@
# colors
true: color(always)
# optimization options
true: optimize(3), unbox_closures

11
backend/dot.ml
View file

@ -18,6 +18,15 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
let proof_id p = node_id (S.expand p)
let print_clause fmt c =
let v = c.S.St.atoms in
let n = Vec.size v in
for i = 0 to n - 1 do
Format.fprintf fmt "%a" A.print_atom (Vec.get v i);
if i < n - 1 then
Format.fprintf fmt ", "
done
let print_edge fmt i j =
Format.fprintf fmt "%s -> %s;@\n" i j
@ -32,7 +41,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
let table fmt (c, rule, color, l) =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" S.print_clause c;
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" print_clause c;
match l with
| [] ->
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule

17
solver/solver.mli
View file

@ -1,15 +1,8 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Mohamed Iguernelala *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module type S = Solver_intf.S