1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SMT/lib/scripts/remote_smt	Mon Feb 08 11:01:47 2010 +0100
     1.3 @@ -0,0 +1,31 @@
     1.4 +#!/usr/bin/env perl
     1.5 +#
     1.6 +# Author: Sascha Boehme, TU Muenchen
     1.7 +#
     1.8 +# Invoke remote SMT solvers.
     1.9 +
    1.10 +use strict;
    1.11 +use warnings;
    1.12 +use LWP;
    1.13 +
    1.14 +
    1.15 +# arguments
    1.16 +
    1.17 +my $solver = $ARGV[0];
    1.18 +my @options = @ARGV[1 .. ($#ARGV - 1)];
    1.19 +my $problem_file = $ARGV[-1];
    1.20 +
    1.21 +
    1.22 +# call solver
    1.23 +
    1.24 +my $agent = LWP::UserAgent->new;
    1.25 +$agent->agent("SMT-Request");
    1.26 +$agent->timeout(180);
    1.27 +my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [
    1.28 +  "Solver" => $solver,
    1.29 +  "Options" => join(" ", @options),
    1.30 +  "Problem" => [$problem_file] ],
    1.31 +  "Content_Type" => "form-data");
    1.32 +if (not $response->is_success) { die "HTTP-Error: " . $response->message; }
    1.33 +else { print $response->content; }
    1.34 +