Newer
Older
module CR = CoAlgReasoner
(* sort should be of the form:
sorts = [| (parseFunctor Sys.argv.(2), [0]) |]
*)
12
13
14
15
16
17
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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
type testResult = | Sat
| Unsat
| ParseError
type satCheck = testResult * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
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
let runSatCheckVerbose (sc:satCheck) =
let cs = colored_string in
let sotr = terminal_string_of_testResult in
let (expectation,_,title) = sc in
PF.printf "Is %-50s " (cs "1" title);
PF.printf "%s?… " (sotr expectation);
let res = runSatCheck sc in
if (res = expectation)
then PF.printf "%s\n" (cs "1;32" "Yes")
else PF.printf "%s\n -> %s: Expected %s but got %s!\n"
(cs "1;31" "No")
(cs "1;31" "Failure")
(sotr expectation)
(sotr res)