author | blanchet |
Wed, 24 Nov 2010 16:15:15 +0100 | |
changeset 40684 | c7ba327eb58c |
parent 36898 | 8e55aa1306c5 |
child 41432 | 3214c39777ab |
permissions | -rwxr-xr-x |
36898 | 1 |
#!/usr/bin/env perl |
2 |
# |
|
3 |
# Author: Sascha Boehme, TU Muenchen |
|
4 |
# |
|
5 |
# Invoke remote SMT solvers. |
|
6 |
||
7 |
use strict; |
|
8 |
use warnings; |
|
9 |
use LWP; |
|
10 |
||
11 |
||
12 |
# arguments |
|
13 |
||
14 |
my $solver = $ARGV[0]; |
|
15 |
my @options = @ARGV[1 .. ($#ARGV - 1)]; |
|
16 |
my $problem_file = $ARGV[-1]; |
|
17 |
||
18 |
||
19 |
# call solver |
|
20 |
||
21 |
my $agent = LWP::UserAgent->new; |
|
22 |
$agent->agent("SMT-Request"); |
|
23 |
$agent->timeout(180); |
|
24 |
my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [ |
|
25 |
"Solver" => $solver, |
|
26 |
"Options" => join(" ", @options), |
|
27 |
"Problem" => [$problem_file] ], |
|
28 |
"Content_Type" => "form-data"); |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
36898
diff
changeset
|
29 |
if (not $response->is_success) { die "HTTP error: " . $response->message; } |
36898 | 30 |
else { print $response->content; } |
31 |