| author | haftmann | 
| Thu, 16 Dec 2010 09:28:19 +0100 | |
| changeset 41188 | 7cded8957e72 | 
| parent 40684 | c7ba327eb58c | 
| 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: 
36898diff
changeset | 29 | if (not $response->is_success) { die "HTTP error: " . $response->message; }
 | 
| 36898 | 30 | else { print $response->content; }
 | 
| 31 |