fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
#!/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->env_proxy;
$agent->agent("SMT-Request");
$agent->timeout(180);
my $response = $agent->post($ENV{"ISABELLE_SMT_REMOTE_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; }