src/HOL/Tools/SMT/lib/scripts/remote_smt
author blanchet
Fri, 17 Dec 2010 00:11:06 +0100
changeset 41221 da6907b67fac
parent 40684 c7ba327eb58c
child 41432 3214c39777ab
permissions -rwxr-xr-x
fixed off-by-one and return proper error code -- never underestimate the number of oddities in Perl

#!/usr/bin/env perl
#
# Author: Sascha Boehme, TU Muenchen
#
# Invoke remote SMT solvers.

use strict;
use warnings;
use LWP;


# arguments

my $solver = $ARGV[0];
my @options = @ARGV[1 .. ($#ARGV - 1)];
my $problem_file = $ARGV[-1];


# call solver

my $agent = LWP::UserAgent->new;
$agent->agent("SMT-Request");
$agent->timeout(180);
my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [
  "Solver" => $solver,
  "Options" => join(" ", @options),
  "Problem" => [$problem_file] ],
  "Content_Type" => "form-data");
if (not $response->is_success) { die "HTTP error: " . $response->message; }
else { print $response->content; }