Testsuite.ml 1.8 KB
Newer Older
1
2
3


module CM = CoAlgMisc
4
module PF = Printf
5
6
7
8
9
10
11

module CR = CoAlgReasoner

(* sort should be of the form:
    sorts = [| (parseFunctor Sys.argv.(2), [0]) |]
*)

12
13
14
15
type testResult = | Sat
                  | Unsat
                  | ParseError

16
17
                (* sat * functors * formula *)
type satCheck = testResult * (CoAlgMisc.sortTable) * string
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45



let colored_string_of_testResult tr =
    match tr with
    | Sat -> ("1;33","sat")
    | Unsat -> ("1;34","unsat")
    | ParseError -> ("31","unparseable")

let colored_string col str =
    "\027["^col^"m"^str^"\027[0m"

let terminal_string_of_testResult tr =
    let (col,str) = colored_string_of_testResult tr in
    colored_string col str

let runSatCheck (_,logic,input) =
  try
      let nomTable name =
        assert (CoAlgFormula.isNominal name);
        Some 0
      in
      let (tbox, f) = CoAlgFormula.importQuery input in
      let res = CoAlgReasoner.isSat logic nomTable tbox f in
      if res then Sat else Unsat
  with | Stream.Error _ -> ParseError
       | CoAlgFormula.CoAlgException _ -> ParseError

46
47
48
49
50
51
52
53
let stringCrop width str =
    if (String.length str <= width) then str
    else ((Str.string_before str (width-1)) ^ "…")

let columnCreate width str =
    let shorten = (stringCrop width str) in
    let pad = String.make (max 0 (width - (String.length shorten))) ' ' in
    (shorten ^ pad)
54
55
56
57
58

let runSatCheckVerbose (sc:satCheck) =
    let cs = colored_string in
    let sotr = terminal_string_of_testResult in
    let (expectation,_,title) = sc in
Thorsten Wißmann's avatar
Thorsten Wißmann committed
59
    PF.printf "Is %s " (cs "1" (columnCreate 60 title));
60
    PF.printf "%s? → " (sotr expectation);
61
    let res = runSatCheck sc in
62
    (if (res = expectation)
63
    then PF.printf "%s\n" (cs "1;32" "Yes")
Thorsten Wißmann's avatar
Thorsten Wißmann committed
64
    else PF.printf "%s, it is %s\n"
65
                    (cs "1;31" "No")
66
67
                    (sotr res));
    res
68
69