int read_int(){ int res = 0; char c; while (isdigit(c = getchar())) res = res * 10 + (c - '0'); return res; }