h*H    0.4 Safe-Inferred"smtlib-backendsA solver is essentially a wrapper around a solver backend. It also comes an optional queue of commands to send to the backend. smtlib-backends$The backend processing the commands. smtlib-backendsAn optional queue to write commands that are to be sent to the solver lazily.smtlib-backends Whether to enable queuing for a .smtlib-backendsIn  mode, the  has no queue and commands are sent to the backend immediately.In this mode, the option :print-success is enabled by  to monitor that commands are being accepted by the SMT solver.smtlib-backendsIn  mode, commands whose output is not strictly necessary for the rest of the computation (typically the ones whose output should just be success) are not sent to the backend immediately, but rather written on the solver's queue.It is the responsibility of the caller to identify these commands and sent them through the   call.When a command is sent whose output is actually necessary, 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. When commands are sent in batches, a command sent to the solver will only produce an error when it is later sent to the backend. Therefore, you probably want to stick with  mode when debugging.For parsing to work properly, at most one of the commands in the batch can produce an output. Hence the :print-success" option should not be enabled in  mode.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.Concurrent calls to different solvers are thread-safe, but not concurrent calls on the same solver or the same backend.Only one command must be given per invocation, or the multiple commands must together produce the output of one command only. 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.Concurrent calls to different solvers are thread-safe, but not concurrent calls on the same solver or the same backend.Only one command must be given per invocation, or the multiple commands must together produce the output of one command only. 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  modesmtlib-backendsthe solver backend        *smtlib-backends-0.4-1LWy8GYbBpmJ04ckPQzUngSMTLIB.Backendssmtlib-backendsSolver QueuingFlag NoQueuingQueuingBackendsendsend_ initSolvercommandcommand_ flushQueuebackendqueueputflush