h&p     Safe-Inferred"T smtlib-backendsA solver is essentially a wrapper around a solver backend. It also comes an optional queue of commands to send to the backend.A solver can either be in  mode or  mode. In  mode, the queue of commands isn't used and the commands are sent to the backend immediately. In  mode, commands whose output are not strictly necessary for the rest of the computation (typically the ones whose output should just be success) and that are sent through   are not sent to the backend immediately, but rather written on the solver's queue. When a command whose output is actually necessary needs to be sent, the queue is flushed and sent as a batch to the backend. mode should be faster as there usually is a non-negligible constant overhead in sending a command to the backend. But since the commands are sent by batches, a command sent to the solver will only produce an error when the queue is flushed, i.e. when a command with interesting output is sent. You thus probably want to stick with  mode when debugging. Moreover, when commands are sent by batches, only the last command in the batch may produce an output for parsing to work properly. Hence the :print-success option is disabled in 2 mode, and this should not be overriden manually. smtlib-backends$The backend processing the commands. smtlib-backendsAn optional queue to write commands that are to be sent to the solver lazily.smtlib-backendsA boolean-equivalent datatype indicating whether to enable queuing.smtlib-backendsThe type of solver backends. SMTLib2 commands are sent to a backend which processes them and outputs the solver's response.smtlib-backendsSend a command to the backend. While the implementation depends on the backend, this function is usually *not* thread-safe.smtlib-backendsSend a command that doesn't produce any response to the backend. The backend may implement this by not reading the output and leaving it for a later read, or reading the output and discarding it immediately. Hence this method should only be used when the command does not produce any response to be outputted. Again, this function may not be thread-safe.smtlib-backendsPush a command on the solver's queue of commands to evaluate. The command must not produce any output when evaluated, unless it is the last command added before the queue is flushed. For a fixed queue, this function is *not* thread-safe.smtlib-backendsEmpty the queue of commands to evaluate and return its content as a bytestring builder. For a fixed queue, this function is *not* thread-safe.smtlib-backendsCreate a new solver and initialize it with some options so that it behaves correctly for our use. In particular, the "print-success" option is disabled in . mode. This should not be overriden manually. smtlib-backendsHave the solver evaluate a SMT-LIB command. This forces the queued commands to be evaluated as well, but their results are *not* checked for correctness. For a fixed backend, this function is *not* thread-safe. smtlib-backends*A command with no interesting result. In 1 mode, the result is checked for correctness. In  mode, (unless the queue is flushed and evaluated right after) the command must not produce any output when evaluated, and its output is thus in particular not checked for correctness. For a fixed backend, this function is *not* thread-safe. smtlib-backendsForce the content of the queue to be sent to the solver. Only useful in queuing mode, does nothing in non-queuing mode.smtlib-backendswhether to enable  mode (see  for the meaning of this flag)smtlib-backendsthe solver backend        smtlib-backends-0.3-inplaceSMTLIB.BackendsSolver QueuingFlagQueuing NoQueuingBackendsendsend_ initSolvercommandcommand_ flushQueuebackendqueueputflush