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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
#!%PERL%
# %CREATE_GENERATED_WARNING%
$old_input_file = "old_sexpr.sexpr";
$pushed_input_file = "pushed_sexpr.sexpr";
$dimacs_input_file = "input.d";
$sat_output_file = "sat_output";
$sat_summary_file = "sat_summary";
$numargs = $#ARGV + 1;
if ($numargs < 1) {
print "ERROR: Too few arguments to sexpr-sat-solver.\n";
printCommand();
exit 1;
}
if ($numargs < 2) {
print "ERROR: Too few arguments to sexpr-sat-solver\n";
printCommand();
exit 1;
}
if ($ARGV[0] =~ m/-dir/) {
if ($numargs < 4) {
print "ERROR: Too few arguments to sexpr-sat-solver\n";
printCommand();
exit 1;
}
$dir = $ARGV[1] . "/";
$input_file = $ARGV[2];
$com = 3;
} else {
$dir = "./";
$input_file = $ARGV[0];
$com = 1;
}
$remaining_args = $numargs - $com;
if ($ARGV[$com] =~ m/--new-problem/) {
system "mkdir -p " . $dir;
system "rm -f " . $dir . $input_file ;
system "touch " . $dir . $input_file;
system "rm -f " . $dir . $old_input_file ;
system "touch " . $dir . $old_input_file;
} elsif ($ARGV[$com] =~ m/--push/) {
system "cp " . $dir . $old_input_file . " " . $dir . $pushed_input_file ;
} elsif ($ARGV[$com] =~ m/--pop/) {
system "rm -f " . $dir . $old_input_file ;
system "mv " . $dir . $pushed_input_file . " " . $dir . $old_input_file ;
} elsif ($ARGV[$com] =~ m/--solve/) {
if ($remaining_args < 4) {
print "ERROR: Too few arguments to --solve command\n";
printCommand();
exit 1;
}
if (!(-x "%SAT_SOLVER%")) {
print "ERROR: Cannot find the specified SAT solver: %SAT_SOLVER%\n";
print "Note that the SAT solver must be executable and must be specified through an absolute pathname.\n";
exit 1;
}
$num_vars = $ARGV[$com+1];
$num_clauses = $ARGV[$com+2];
$output_file = $ARGV[$com+3];
# print "cat " . $dir . $input_file . " >> " . $dir . $old_input_file ;
system "cat " . $dir . $input_file . " >> " . $dir . $old_input_file;
# system "rm -f " . $dir . $input_file;
# system "touch " . $dir . $input_file;
# print "sat-input-formater " . $dir . $old_input_file . " " . $num_vars . " " . $num_clauses . " > " . $dir . $dimacs_input_file . "\n";
system "%SULFA_DIR%/c-files/sat-input-formater " . $dir . $old_input_file . " " . $num_vars . " " . $num_clauses . " > " . $dir . $dimacs_input_file;
# print "format complete\n";
if ("%SAT_SOLVER_TYPE%" eq "zchaff") {
system "%SAT_SOLVER% " . $dir . $dimacs_input_file . " > " . $dir . $sat_output_file;
system "%SULFA_DIR%/c-files/zchaff-output-formater " . $dir . $sat_output_file . " > " . $dir . $output_file;
} elsif ("%SAT_SOLVER_TYPE%" eq "minisat") {
# system "%TCSH_SHELL%";
system "%SAT_SOLVER% " . $dir . $dimacs_input_file . " " . $dir . $sat_output_file;
system "%SULFA_DIR%/c-files/minisat-output-formater " . $dir . $sat_output_file . " > " . $dir . $output_file;
} elsif ("%SAT_SOLVER_TYPE%" eq "minisat1.4") {
system "%SAT_SOLVER% " . $dir . $dimacs_input_file . " > " . $dir . $sat_output_file;
system "%SULFA_DIR%/c-files/minisat-output-formater-1.4 " . $dir . $sat_output_file . " > " . $dir . $output_file;
} else {
die "Unsupported SAT SOLVER type, currently supported types: zchaff\n";
}
} elsif ($ARGV[$com] =~ m/--end-problem/) {
system "rm -f " . $dir . $input_file;
system "rm -f " . $dir . $old_input_file ;
system "rm -f " . $dir . $pushed_input_file ;
system "rm -f " . $dir . $dimacs_input_file ;
system "rm -f " . $dir . $sat_output_file ;
} else {
print "ERROR: Unrecognized command\n";
printCommand();
exit 1;
}
sub printCommand {
print "Command: sexpr-sat-solver";
for ($i=0; $i<=$#ARGV; $i++) {
print " " . $ARGV[$i];
}
print "\n";
}
|
