| author | blanchet |
| Thu, 29 Apr 2010 18:24:52 +0200 | |
| changeset 36565 | 061475351a09 |
| parent 35025 | 0ea45a4d32f3 |
| permissions | -rwxr-xr-x |
|
35025
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
1 |
#!/usr/bin/env perl |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
2 |
# |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
3 |
# Author: Sascha Boehme, TU Muenchen |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
4 |
# |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
5 |
# Invoke remote SMT solvers. |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
6 |
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
7 |
use strict; |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
8 |
use warnings; |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
9 |
use LWP; |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
10 |
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
11 |
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
12 |
# arguments |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
13 |
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
14 |
my $solver = $ARGV[0]; |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
15 |
my @options = @ARGV[1 .. ($#ARGV - 1)]; |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
16 |
my $problem_file = $ARGV[-1]; |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
17 |
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
18 |
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
19 |
# call solver |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
20 |
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
21 |
my $agent = LWP::UserAgent->new; |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
22 |
$agent->agent("SMT-Request");
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
23 |
$agent->timeout(180); |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
24 |
my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
25 |
"Solver" => $solver, |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
26 |
"Options" => join(" ", @options),
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
27 |
"Problem" => [$problem_file] ], |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
28 |
"Content_Type" => "form-data"); |
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
29 |
if (not $response->is_success) { die "HTTP-Error: " . $response->message; }
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
30 |
else { print $response->content; }
|
|
0ea45a4d32f3
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
boehmes
parents:
diff
changeset
|
31 |