#!/usr/bin/env perl
use feature qw(say);
use strict;
use warnings;

use File::Temp qw(tempfile);
use List::Util qw(sum);

my $total = 0;
while (<>) {
  chomp(my $line = $_);
  my (undef, @A) = split " ", $line;
  my @target = map 0 + $_, (pop(@A) =~ /(\d+)/g);
  my %var;
  $var{"a$_"} = $A[$_] =~ s/[()]/,/gr for 0..$#A;

  my ($fh, $fn) = tempfile();
  for (keys %var) {
    say $fh "(declare-const $_ Int)";
    say $fh "(assert (<= 0 $_))";
  }
  for my $i (0..$#target) {
    print $fh "(assert (= (+";
    $b =~ /,$i,/ and print $fh " $a" while ($a, $b) = each %var;
    say $fh ") ${target[$i]}))";
  }
  my $pos = tell $fh;

  my ($lo, $hi) = (0, sum @target);
  while ($lo + 1 < $hi) {
    seek $fh, $pos, 0;
    truncate $fh, $pos;
    my $mid = do {
      use integer;
      $lo + ($hi - $lo) / 2;
    };
    say $fh "(assert (<= (+ @{[keys %var]}) $mid))";
    say $fh "(check-sat)";
    chomp(my $r = qx(z3 $fn));
    if ($r eq 'sat') {
      $hi = $mid;
    } elsif ($r eq 'unsat') {
      $lo = $mid;
    } else {
      die $r;
    }
  }
  say "$line = $hi";
  $total += $hi;
}
say $total;