Add virtual Solver member functions for opcodes

This enforces stricter compile-time checks of the Solver implementations;
possible cases in the original switch statement could have been easily
forgotten which would have made the maintenance more difficult as new
opcodes are added. This patch fixes this by introducing a virtual member
function in Solver for each possible opcode. As one immediate result, the
semantics of OPCODE_ERROR becomes clearer.