ICPC 2019 - I. Karel the Robot

#include <bits/stdc++.h>
using namespace std;

namespace {

struct Node {
    char type = 0;
    char cond = 0;
    char proc = 0;
    int next = 0;
    int first = 0;
    int second = 0;
};

constexpr short INF_STATE = -1;
constexpr short UNVISITED = -2;
constexpr short IN_PROGRESS = -3;

int rows_count;
int cols_count;
vector<string> grid_cells;
vector<Node> nodes(1);
int proc_root[26];
vector<int> query_root;

int state_count;
vector<int> move_forward_state;
vector<int> turn_left_state;
vector<unsigned char> barrier_ahead;
vector<short> memo;

int encode_state(int r, int c, int dir) {
    return ((r * cols_count + c) << 2) | dir;
}

void decode_state(int state, int& r, int& c, int& dir) {
    dir = state & 3;
    state >>= 2;
    c = state % cols_count;
    r = state / cols_count;
}

bool check_condition(int state, char cond) {
    if (cond == 'b') {
        return barrier_ahead[state] != 0;
    }
    int dir = state & 3;
    if (cond == 'n') {
        return dir == 0;
    }
    if (cond == 'e') {
        return dir == 1;
    }
    if (cond == 's') {
        return dir == 2;
    }
    return dir == 3;
}

int parse_program(const string& s, int& pos);

int add_node(const Node& node) {
    nodes.push_back(node);
    return static_cast<int>(nodes.size()) - 1;
}

int parse_command_and_rest(const string& s, int& pos) {
    Node node;
    char ch = s[pos++];
    if (ch == 'm' || ch == 'l' || ('A' <= ch && ch <= 'Z')) {
        node.type = ch;
    } else if (ch == 'i') {
        node.type = 'i';
        node.cond = s[pos++];
        ++pos;  // '('
        node.first = parse_program(s, pos);
        ++pos;  // ')'
        ++pos;  // '('
        node.second = parse_program(s, pos);
        ++pos;  // ')'
    } else {
        node.type = 'u';
        node.cond = s[pos++];
        ++pos;  // '('
        node.first = parse_program(s, pos);
        ++pos;  // ')'
    }
    node.next = parse_program(s, pos);
    return add_node(node);
}

int parse_program(const string& s, int& pos) {
    if (pos >= static_cast<int>(s.size()) || s[pos] == ')') {
        return 0;
    }
    return parse_command_and_rest(s, pos);
}

int state_key(int node_id, int state) {
    return node_id * state_count + state;
}

short lookup_result(int node_id, int state) {
    if (node_id == 0) {
        return static_cast<short>(state);
    }
    return memo[state_key(node_id, state)];
}

short solve_state(int root_node, int root_state) {
    if (root_node == 0) {
        return static_cast<short>(root_state);
    }
    int root_key = state_key(root_node, root_state);
    if (memo[root_key] != UNVISITED) {
        return memo[root_key] == IN_PROGRESS ? INF_STATE : memo[root_key];
    }

    struct Frame {
        int node_id;
        int state;
        int stage;
        short temp;
    };

    vector<Frame> stack;
    stack.push_back({root_node, root_state, 0, 0});
    memo[root_key] = IN_PROGRESS;

    while (!stack.empty()) {
        Frame& frame = stack.back();
        int key = state_key(frame.node_id, frame.state);
        const Node& node = nodes[frame.node_id];

        auto request = [&](int child_node, int child_state, int next_stage) -> bool {
            short value = lookup_result(child_node, child_state);
            if (value == UNVISITED) {
                frame.stage = next_stage;
                memo[state_key(child_node, child_state)] = IN_PROGRESS;
                stack.push_back({child_node, child_state, 0, 0});
                return true;
            }
            if (value == IN_PROGRESS) {
                memo[key] = INF_STATE;
                stack.pop_back();
                return true;
            }
            frame.temp = value;
            frame.stage = next_stage;
            return false;
        };

        if (node.type == 'm') {
            if (frame.stage == 0) {
                if (request(node.next, move_forward_state[frame.state], 1)) {
                    continue;
                }
            }
            frame.temp = lookup_result(node.next, move_forward_state[frame.state]);
            memo[key] = frame.temp;
            stack.pop_back();
            continue;
        }

        if (node.type == 'l') {
            if (frame.stage == 0) {
                if (request(node.next, turn_left_state[frame.state], 1)) {
                    continue;
                }
            }
            frame.temp = lookup_result(node.next, turn_left_state[frame.state]);
            memo[key] = frame.temp;
            stack.pop_back();
            continue;
        }

        if ('A' <= node.type && node.type <= 'Z') {
            if (frame.stage == 0) {
                if (request(proc_root[node.type - 'A'], frame.state, 1)) {
                    continue;
                }
            }
            if (frame.stage == 1) {
                frame.temp = lookup_result(proc_root[node.type - 'A'], frame.state);
                if (frame.temp == INF_STATE) {
                    memo[key] = INF_STATE;
                    stack.pop_back();
                    continue;
                }
                if (request(node.next, frame.temp, 2)) {
                    continue;
                }
            }
            frame.temp = lookup_result(node.next, lookup_result(proc_root[node.type - 'A'], frame.state));
            memo[key] = frame.temp;
            stack.pop_back();
            continue;
        }

        if (node.type == 'i') {
            int branch = check_condition(frame.state, node.cond) ? node.first : node.second;
            if (frame.stage == 0) {
                if (request(branch, frame.state, 1)) {
                    continue;
                }
            }
            if (frame.stage == 1) {
                frame.temp = lookup_result(branch, frame.state);
                if (frame.temp == INF_STATE) {
                    memo[key] = INF_STATE;
                    stack.pop_back();
                    continue;
                }
                if (request(node.next, frame.temp, 2)) {
                    continue;
                }
            }
            frame.temp = lookup_result(node.next, lookup_result(branch, frame.state));
            memo[key] = frame.temp;
            stack.pop_back();
            continue;
        }

        if (frame.stage == 0) {
            if (check_condition(frame.state, node.cond)) {
                if (request(node.next, frame.state, 2)) {
                    continue;
                }
            } else {
                if (request(node.first, frame.state, 1)) {
                    continue;
                }
            }
        }
        if (frame.stage == 1) {
            frame.temp = lookup_result(node.first, frame.state);
            if (frame.temp == INF_STATE) {
                memo[key] = INF_STATE;
                stack.pop_back();
                continue;
            }
            if (request(frame.node_id, frame.temp, 2)) {
                continue;
            }
        }
        if (check_condition(frame.state, node.cond)) {
            frame.temp = lookup_result(node.next, frame.state);
        } else {
            frame.temp = lookup_result(frame.node_id, lookup_result(node.first, frame.state));
        }
        memo[key] = frame.temp;
        stack.pop_back();
    }

    return memo[root_key];
}

void build_transitions() {
    state_count = rows_count * cols_count * 4;
    move_forward_state.resize(state_count);
    turn_left_state.resize(state_count);
    barrier_ahead.resize(state_count);

    const int dr[4] = {-1, 0, 1, 0};
    const int dc[4] = {0, 1, 0, -1};
    for (int r = 0; r < rows_count; ++r) {
        for (int c = 0; c < cols_count; ++c) {
            for (int dir = 0; dir < 4; ++dir) {
                int state = encode_state(r, c, dir);
                turn_left_state[state] = encode_state(r, c, (dir + 3) & 3);

                int nr = r + dr[dir];
                int nc = c + dc[dir];
                bool blocked = nr < 0 || nr >= rows_count || nc < 0 || nc >= cols_count ||
                               grid_cells[nr][nc] == '#';
                barrier_ahead[state] = static_cast<unsigned char>(blocked);
                move_forward_state[state] = blocked ? state : encode_state(nr, nc, dir);
            }
        }
    }
}

void solve() {
    int definition_count, execution_count;
    cin >> rows_count >> cols_count >> definition_count >> execution_count;
    grid_cells.resize(rows_count);
    for (int i = 0; i < rows_count; ++i) {
        cin >> grid_cells[i];
    }

    fill(proc_root, proc_root + 26, 0);
    for (int i = 0; i < definition_count; ++i) {
        string line;
        cin >> line;
        int pos = 2;
        proc_root[line[0] - 'A'] = parse_program(line, pos);
    }

    vector<int> start_state(execution_count);
    query_root.resize(execution_count);
    for (int i = 0; i < execution_count; ++i) {
        int r, c;
        char heading;
        cin >> r >> c >> heading;
        string program;
        cin >> program;

        int dir = 0;
        if (heading == 'e') {
            dir = 1;
        } else if (heading == 's') {
            dir = 2;
        } else if (heading == 'w') {
            dir = 3;
        }
        start_state[i] = encode_state(r - 1, c - 1, dir);

        int pos = 0;
        query_root[i] = parse_program(program, pos);
    }

    build_transitions();
    memo.assign(static_cast<size_t>(nodes.size()) * state_count, UNVISITED);

    const char dir_name[4] = {'n', 'e', 's', 'w'};
    for (int i = 0; i < execution_count; ++i) {
        short result = solve_state(query_root[i], start_state[i]);
        if (result == INF_STATE) {
            cout << "inf\n";
            continue;
        }

        int r, c, dir;
        decode_state(result, r, c, dir);
        cout << (r + 1) << ' ' << (c + 1) << ' ' << dir_name[dir] << '\n';
    }
}

}  // namespace

int main() {
    ios::sync_with_stdio(false);
    cin.tie(nullptr);

    solve();
    return 0;
}

\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{enumitem}

\title{ICPC World Finals 2019\\I. Karel the Robot}
\author{}
\date{}

\begin{document}
\maketitle

\section*{Problem Summary}

We must interpret a small Karel-like language with movement, turning, procedure calls, conditionals, and
``until'' loops on a grid with barriers.
For each start state and top-level program we must either output Karel's final state or determine that the
execution never terminates.

\section*{Key Observations}

\begin{itemize}[leftmargin=*]
    \item The robot configuration is finite: there are only $4rc \le 6400$ possible pairs
    \[
        (\text{position}, \text{heading}).
    \]
    \item The program text is also finite. If we represent every suffix of every parsed program body as a
    node, then execution is always ``at'' one such node.
    \item Therefore the full execution state can be represented as
    \[
        (\text{program node}, \text{robot configuration}),
    \]
    and there are at most $O(rcs)$ such states, where $s$ is the number of program nodes.
    \item The language is deterministic. Hence if DFS evaluation ever revisits the same state while that
    state is still on the recursion stack, the execution has entered a cycle and will never terminate.
\end{itemize}

\section*{Algorithm}

\begin{enumerate}[leftmargin=*]
    \item Parse every procedure body and every query program into a linked representation of program
    suffixes. Each node stores one command and a pointer to the suffix executed afterwards.
    Nested programs inside \texttt{if} and \texttt{until} are parsed recursively and referenced by their root nodes.
    \item Precompute all robot transitions for the $4rc$ configurations:
    turning left, moving forward, and whether there is a barrier ahead.
    \item Let \texttt{solve(node, state)} mean: execute the program suffix rooted at \texttt{node} starting
    from robot configuration \texttt{state}.
    \item Evaluate this function with DFS and memoization.
    \begin{itemize}[leftmargin=*]
        \item For \texttt{m} and \texttt{l}, apply the corresponding transition and continue with \texttt{next}.
        \item For a procedure call, recursively evaluate the procedure body, then continue with \texttt{next}.
        \item For \texttt{i cond (A)(B)}, choose the branch determined by the current state, execute it,
        then continue with \texttt{next}.
        \item For \texttt{u cond (A)}, if the condition is already true, continue with \texttt{next};
        otherwise execute \texttt{A} and then recursively execute the same \texttt{until} node again.
    \end{itemize}
    \item Memoize the result of every state. A special marker \texttt{in progress} is used during DFS;
    touching such a state again means non-termination.
\end{enumerate}

\section*{Correctness Proof}

We prove that the algorithm returns the correct output for every query.

\paragraph{Lemma 1.}
For every parsed program suffix $P$ and robot configuration $s$, the value computed by
\texttt{solve(P, s)} is exactly the result of executing suffix $P$ from state $s$, unless the execution is
infinite, in which case it returns \texttt{inf}.

\paragraph{Proof.}
We inspect the first command of $P$.
If it is \texttt{m} or \texttt{l}, the operational semantics applies one primitive robot action and then
continues with the remaining suffix, which is exactly what the recursion does.
If it is a procedure call, the language semantics executes the procedure body completely and then resumes
with the caller's suffix; the recursive call followed by \texttt{next} matches this exactly.
If it is an \texttt{if}, both the language and the algorithm choose the same branch from the current state,
execute it, and then continue with the suffix.
If it is an \texttt{until}, both either skip the loop when the condition is already true, or execute the body
once and repeat the same \texttt{until} command.
Thus every recursive case follows the language semantics exactly. \qed

\paragraph{Lemma 2.}
If the DFS re-enters a state $(P,s)$ that is already marked \texttt{in progress}, then executing $P$ from $s$
does not terminate.

\paragraph{Proof.}
The language is deterministic, so from a fixed state $(P,s)$ the future execution is uniquely determined.
If the recursion reaches $(P,s)$ again before finishing the first evaluation of $(P,s)$, then the execution
path from $(P,s)$ has returned to the same state and will repeat forever.
Hence termination is impossible. \qed

\paragraph{Lemma 3.}
If \texttt{solve(P, s)} returns a finite robot configuration $t$, then executing $P$ from $s$ terminates in
exactly $t$.

\paragraph{Proof.}
By Lemma 1 each recursive step mirrors the true execution semantics.
By Lemma 2 the only executions declared infinite are genuine cycles.
Therefore any state that is memoized with a finite result must terminate, and the returned configuration is
the actual final configuration. \qed

\paragraph{Theorem.}
For each query, the algorithm outputs \texttt{inf} iff the program never terminates; otherwise it outputs the
correct final position and heading of Karel.

\paragraph{Proof.}
Each query is evaluated as \texttt{solve(root, start\_state)}.
If the answer is \texttt{inf}, Lemma 2 shows the execution is non-terminating.
Otherwise Lemma 3 shows the returned configuration is exactly the true final state.
Thus every printed answer is correct. \qed

\section*{Complexity Analysis}

Let $s$ be the total number of parsed program nodes across all procedures and query programs.
There are $4rc$ robot configurations, so at most $4rcs$ states.
Each state is solved once and each transition does only $O(1)$ extra work.
Therefore the running time is $O(rcs)$ and the memory usage is also $O(rcs)$.

\section*{Implementation Notes}

\begin{itemize}[leftmargin=*]
    \item The parser naturally creates one node for every non-empty program suffix, which is exactly the
    granularity needed for memoization.
    \item Empty programs can appear inside parentheses and are represented by a null node.
    \item Because $4rc \le 6400$, the memo table fits comfortably in memory even when stored for all
    parsed nodes.
\end{itemize}

\end{document}