int next_int() {
  char c;
  do { c = getchar(); } while( c != '-' && !isdigit(c) );
  bool neg = (c == '-');
  int result = neg ? 0 : c - '0';
  while( isdigit(c = getchar()) )
    result = 10 * result + (c - '0');
  return neg ? -result : result;
}