author | blanchet |
Tue, 17 Jan 2012 18:25:36 +0100 | |
changeset 46241 | 1a0b8f529b96 |
parent 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; |
|
46241
1a0b8f529b96
allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script
blanchet
parents:
41432
diff
changeset
|
22 |
$agent->env_proxy; |
36898 | 23 |
$agent->agent("SMT-Request"); |
24 |
$agent->timeout(180); |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
40684
diff
changeset
|
25 |
my $response = $agent->post($ENV{"ISABELLE_SMT_REMOTE_URL"}, [ |
36898 | 26 |
"Solver" => $solver, |
27 |
"Options" => join(" ", @options), |
|
28 |
"Problem" => [$problem_file] ], |
|
29 |
"Content_Type" => "form-data"); |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
36898
diff
changeset
|
30 |
if (not $response->is_success) { die "HTTP error: " . $response->message; } |
36898 | 31 |
else { print $response->content; } |
32 |