1
2
3
4
5
6
7
8
9
10
11
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
#!%PERL%
# %CREATE_GENERATED_WARNING%
# print "usage: sulfa-smt <smt-file> [-temp_dir <temp directory> -v <verbosity level: 0 to 4>]\n";
$numargs = $#ARGV + 1;
$temp_dir = "./sulfa_smt_temp/";
$verbosity = 1;
$i=0;
while ($i < $numargs) {
if (($ARGV[$i] eq "-temp_dir") && ($i+1 < $numargs)) {
$temp_dir = $ARGV[$i+1] . "/";
$i += 2;
} elsif (($ARGV[$i] eq "-v") && ($i+1 < $numargs)) {
$verbosity = $ARGV[$i+1];
$i += 2;
} else {
print "ERROR: Unrecognized command: " . $ARGV[$i] . "\n";
print "usage: sulfa-smt <smt-file> [-temp_dir <temp directory> -v <verbosity level: 0 to 4>]\n";
exit 1;
}
}
$ACL2_out_file = $temp_dir . "out.sof";
$prepped_smt_file = $temp_dir . "smt_file.prepped";
$ACL2_smt_file = $temp_dir . "smt_file.lisp";
$ACL2_cmd_file = $temp_dir . "ACL2_cmd_file.lisp";
$prepper = "%SULFA_DIR%/c-files/smt-prep";
$ACL2 = "%SULFA_DIR%/acl2/saved_acl2";
system "rm -f -r " . $temp_dir;
system "mkdir " . $temp_dir;
system $prepper . " > " . $prepped_smt_file;
open(OUTP, "> $ACL2_cmd_file") or die("Cannot open $ACL2_cmd_file for writing\n");
if ($verbosity < 4) {
# Inihibit ACL2 proof output
print OUTP "(set-inhibit-output-lst '(error warning warning! observation prove proof-builder event expansion summary proof-tree))";
}
print OUTP "(include-book \"%SULFA_DIR%/books/bv-smt-solver/translation\" :ttags (sat sat-cl smt))\n";
print OUTP "(include-book \"%SULFA_DIR%/books/bv-smt-solver/smt\" :skip-proofs-okp t :ttags (sat sat-cl smt))\n";
print OUTP "(translate-smt-file \"" . $prepped_smt_file . "\" \"" . $ACL2_smt_file . "\" \"" .
$ACL2_out_file . "\" state)";
print OUTP "(ld \"" . $ACL2_smt_file . "\")";
close OUTP;
if ($verbosity < 3) {
system $ACL2 . " < " . $ACL2_cmd_file . " >& /dev/null";
} else {
system $ACL2 . " < " . $ACL2_cmd_file;
}
if ($verbosity < 1) {
open(INP, "< $ACL2_out_file") or die("Cannot open $ACL2_out_file for reading\n");
while ($line = <INP>) {
if ($line =~ m/UNSAT/) {
print "unsat";
} elsif ($line =~ m/SAT/) {
print "sat";
}
}
close INP;
print "\n";
} elsif ($verbosity < 2) {
open(INP, "< $ACL2_out_file") or die("Cannot open $ACL2_out_file for reading\n");
while ($line = <INP>) {
if ($line =~ m/ERROR/) {
print "ERROR: ";
}
if ($line =~ m/UNSAT/) {
print "unsat";
} elsif ($line =~ m/SAT/) {
print "sat";
}
}
close INP;
print "\n";
} else {
system "cat " . $ACL2_out_file;
}
system "rm -f -r " . $temp_dir
|
