author | boehmes |
Mon, 21 Sep 2009 11:15:21 +0200 | |
changeset 32622 | 8ed38c7bd21a |
parent 32619 | 02f45a09a9f2 |
child 33010 | 39f73a59e855 |
permissions | -rwxr-xr-x |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
1 |
# |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
2 |
# Script to invoke remote SMT solvers. |
32619 | 3 |
# Author: Sascha Boehme, TU Muenchen |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
4 |
# |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
5 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
6 |
use strict; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
7 |
use LWP; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
8 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
9 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
10 |
# environment |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
11 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
12 |
my $remote_smt_url = $ENV{"REMOTE_SMT_URL"}; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
13 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
14 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
15 |
# arguments |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
16 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
17 |
my $solver = $ARGV[0]; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
18 |
my @options = @ARGV[1 .. ($#ARGV - 2)]; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
19 |
my $problem_file = $ARGV[-2]; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
20 |
my $output_file = $ARGV[-1]; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
21 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
22 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
23 |
# call solver |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
24 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
25 |
my $agent = LWP::UserAgent->new; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
26 |
$agent->agent("SMT-Request"); |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
27 |
$agent->timeout(180); |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
28 |
my $response = $agent->post($remote_smt_url, [ |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
29 |
"Solver" => $solver, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
30 |
"Options" => join(" ", @options), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
31 |
"Problem" => [$problem_file] ], |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
32 |
"Content_Type" => "form-data"); |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
33 |
if (not $response->is_success) { |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
34 |
print "HTTP-Error: " . $response->message . "\n"; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
35 |
exit 1; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
36 |
} |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
37 |
else { |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
38 |
open(FILE, ">$output_file"); |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
39 |
print FILE $response->content; |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
40 |
close(FILE); |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
41 |
} |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
42 |