Package org.smtlib

Class SolverProcess

java.lang.Object
org.smtlib.SolverProcess
public class SolverProcess extends Object
This class implements launching, writing to, and reading responses from a launched process (in particular, solver processes).
Author:
David Cok

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static class 
    SolverProcess.NoResponseException
    Thrown when a command gets literally no response from the solver -- either because the process was already confirmed dead before this command was even written (the pre-write liveness check in send()), or because its output stream closed while listening without ever producing anything on either stream (the forced-EOF check in listen()).
    static class 
    SolverProcess.ProverException
    Wraps an exception thrown because of a failure in the prover
    static class 
    SolverProcess.StreamGobbler
    Continuously drains one of the process's output streams (stdout or stderr) on a dedicated thread, so that a solver writing a large amount of text to one stream can never be blocked by the other stream's OS pipe buffer filling up while this process is busy reading elsewhere -- reading stdout and stderr sequentially in a single thread cannot make that guarantee.

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    protected String[]
    app
    The command-line arguments that launch a new process
    boolean
    badFormat
    Set true by a caller for the duration of a single command whose expected response text may contain literal, non-SMT-LIB unbalanced parentheses (e.g.
    protected Charset
    charset
    The charset used to encode text sent to the process and decode text read back from it
    boolean
    discardErrorOutput
    Set before start() by an adapter whose solver writes only diagnostics to stderr, to discard them
    long
    endDrainMillis
    Once the solver's standard output has ended, how long (ms) to wait at most for its standard error to end too, so that what it wrote there just before exiting (typically an error) is read in full rather than lost to the stderr reader not having caught up
    protected String
    endMarker
    The text that marks the end of the text returned from the process
    protected static final String
    eol
     
    protected SolverProcess.StreamGobbler
    errorOut
     
    long
    errorSettleMillis
    How long (ms) to wait for error-stream text to arrive before concluding a command produced none, and (once some has arrived) how much longer to wait for further stragglers before returning it.
    Writer
    log
    A place (e.g., log file), if non-null, to write all outbound communications for diagnostic purposes
    protected Process
    process
    The Java process object (initialized by start() )
    protected Thread
    shutdownThread
     
    protected SolverProcess.StreamGobbler
    standardOut
     
    protected Writer
    toProcess
    The Writer object that writes to the spawned process (initialized by start() )

  • Constructor Summary

    Constructors
    Constructor
    Description
    SolverProcess(String[] cmd, String endMarker, String logfile)
    Constructs a SolverProcess object, without actually starting the process as yet.
    SolverProcess(String[] cmd, String endMarker, String logfile, Charset charset)
    As SolverProcess(String[], String, String), but explicitly setting the charset used to encode text sent to the process and decode text read back from it.

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    endedAfter(double seconds, long waitMillis)
    Whether the process has ended on its own (not stopped or interrupted here), waiting at most waitMillis for that, after running at least the given number of seconds
    void
    exit()
    Aborts the process; returns immediately if already stopped
    Charset
    getCharset()
    The charset being used to encode text sent to the process and decode text read back from it
    boolean
    hasExited()
    Whether the process was started and has since exited
    void
    interrupt()
    Interrupts the command the solver is running by sending it SIGINT: z3 then abandons the command (check-sat answers unknown) and goes on; most other solvers exit.
    boolean
    isRunning(boolean expectStopped)
    Returns true if the process is still running; this relies on exceptions for control flow and may be a bit expensive.
    String
    listen()
    Listens to the process's standard output until the designated endMarker is read, combined with whatever error output has arrived.
    int
    nextLine()
    The number of the solver input line that the next text sent starts on (lines counted from 1)
    void
    openDiagnosticLine(String text)
    Adds the start of a line of standard-error text, read when pipelining, to the diagnostic output, as an unended line that the next standard-error text read finishes
    boolean
    outputEnded()
    Whether reading has reached the end of standard output: the process has exited or closed it
    String
    readErrorOutput(long waitMillis)
    For pipelined reading: the text that has arrived on standard error, waiting up to waitMillis for some (see StreamGobbler.drain)
    String
    readOutput(long waitMillis)
    For pipelined reading, which, unlike listen(), does not pair the text with one command: the next text the solver wrote on standard output, waiting up to waitMillis for it (not at all if 0; until some arrives or the output ends if negative).
    String
    readRemainingErrorOutput()
    For pipelined reading, once the output has ended: the rest of the text on standard error, up to its end (waiting at most endDrainMillis)
    String
    send(boolean listen, String... args)
    Sends all the given text arguments, then (if listen is true) listens for the designated end marker text
    String
    sendAndListen(String... args)
    Sends all the given text arguments, then listens for the designated end marker text
    void
    sendNoListen(String... args)
    Sends all the given text arguments, but does not wait for a response
    void
    setCmd(String[] cmd)
    Enables changing the command-line; must be called prior to start()
    void
    start(boolean listen)
    Starts the process; if the argument is true, then also listens to its output until a prompt is read.
    void
    stopIfRunning()
    Stops the solver's OS process if it is still running, leaving this object as it is: later sends then fail as "Solver process has already exited", and exit() cleans up.
    String
    takeDiagnosticOutput(boolean all)
    Returns and clears the solver's diagnostic output: standard-error text read with a reply on standard output, which answered instead (see listen()).
    String[]
    unreadOutput()
    The text the solver wrote that has not been read as a response, on stdout and on stderr (in that order): e.g.
    boolean
    waitForEnd(long millis)
    Waits at most millis for the process to end; returns whether it has

    Methods inherited from class java.lang.Object

    clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Field Details

    • errorSettleMillis

      public long errorSettleMillis
      How long (ms) to wait for error-stream text to arrive before concluding a command produced none, and (once some has arrived) how much longer to wait for further stragglers before returning it. There is no OS-level signal tying completeness of stderr to the recognized end marker on stdout, so this is a bounded best-effort wait, not a guarantee; see StreamGobbler.drain() for why even the first check needs this, not just the straggler wait -- it is paid on every command, including ones with no error to find, not only when error text is actually flowing. Kept small rather than 0 because it is paid per command, not per script: see SMT/experiments/error-settle-wait/ for measurements showing z3/cvc5/yices2/smtinterpol write to stderr only rarely under jSMTLIB's launch flags (z3 does so occasionally, for unparseable input), so a larger value buys little extra safety at a real per-command cost on long scripts.

    • endDrainMillis

      public long endDrainMillis
      Once the solver's standard output has ended, how long (ms) to wait at most for its standard error to end too, so that what it wrote there just before exiting (typically an error) is read in full rather than lost to the stderr reader not having caught up

    • badFormat

      public boolean badFormat
      Set true by a caller for the duration of a single command whose expected response text may contain literal, non-SMT-LIB unbalanced parentheses (e.g. some z3 :reason-unknown text), so the end-marker recognizer does not wait forever for parentheses to balance.

    • discardErrorOutput

      public boolean discardErrorOutput
      Set before start() by an adapter whose solver writes only diagnostics to stderr, to discard them

    • eol

      protected static final String eol

    • standardOut

      protected SolverProcess.StreamGobbler standardOut

    • errorOut

      protected SolverProcess.StreamGobbler errorOut

    • app

      protected String[] app
      The command-line arguments that launch a new process

    • charset

      protected Charset charset
      The charset used to encode text sent to the process and decode text read back from it

    • endMarker

      protected String endMarker
      The text that marks the end of the text returned from the process

    • process

      protected volatile Process process
      The Java process object (initialized by start() )

    • toProcess

      protected volatile Writer toProcess
      The Writer object that writes to the spawned process (initialized by start() )

    • log

      public Writer log
      A place (e.g., log file), if non-null, to write all outbound communications for diagnostic purposes

    • shutdownThread

      protected Thread shutdownThread

  • Constructor Details

    • SolverProcess

      public SolverProcess(String[] cmd, String endMarker, String logfile)
      Constructs a SolverProcess object, without actually starting the process as yet.
      Parameters:
      cmd - the command-line that will launch the desired process
      endMarker - text that marks the end of text returned from the process, e.g. the end of the prompt for new input
      logfile - if not null, the name of a file to log communications to, for diagnostic purposes

    • SolverProcess

      public SolverProcess(String[] cmd, String endMarker, String logfile, Charset charset)
      As SolverProcess(String[], String, String), but explicitly setting the charset used to encode text sent to the process and decode text read back from it.
      Parameters:
      charset - the charset to use for the process's stdin/stdout/stderr

  • Method Details

    • getCharset

      public Charset getCharset()
      The charset being used to encode text sent to the process and decode text read back from it

    • setCmd

      public void setCmd(String[] cmd)
      Enables changing the command-line; must be called prior to start()

    • start

      public void start(boolean listen) throws SolverProcess.ProverException
      Starts the process; if the argument is true, then also listens to its output until a prompt is read.
      Parameters:
      listen - true if the process prints banner/greeting text of its own before it is ready to read commands (e.g. a version line, a copyright notice) that must be read and discarded before the first real command is sent, lest it be mistaken for that command's response; listen() blocks until the end marker is recognized, however long the banner actually takes to arrive, so this does not need -- and must not be replaced by -- a fixed delay. Pass false when the process prints nothing until it has consumed its first command (true of every solver currently adapted here; each launches with a quiet/non-interactive flag specifically to suppress any such banner at the source).
      Throws:
      SolverProcess.ProverException - if this SolverProcess has already been started (each instance is single-use; solver adapters construct a fresh SolverProcess per start() rather than reusing one)

    • listen

      public String listen() throws IOException
      Listens to the process's standard output until the designated endMarker is read, combined with whatever error output has arrived. The reply is what the solver wrote on standard output; the error output is returned instead only when standard output holds no reply (it is empty, or it ended with an incomplete one): some solvers write errors there. Error output not returned is kept as diagnostic output (see takeDiagnosticOutput).
      Throws:
      IOException

    • openDiagnosticLine

      public void openDiagnosticLine(String text)
      Adds the start of a line of standard-error text, read when pipelining, to the diagnostic output, as an unended line that the next standard-error text read finishes

    • takeDiagnosticOutput

      public String takeDiagnosticOutput(boolean all)
      Returns and clears the solver's diagnostic output: standard-error text read with a reply on standard output, which answered instead (see listen()). An unended last line is kept until it ends, so that it is logged whole, unless all is true (the solver is being stopped).

    • unreadOutput

      public String[] unreadOutput()
      The text the solver wrote that has not been read as a response, on stdout and on stderr (in that order): e.g. a report it wrote just before exiting on its own, such as when its whole-run time limit ended it between commands. Meant for use after the process has exited, when both streams reach EOF and this returns promptly; it does not wait for a response to a command.

    • endedAfter

      public boolean endedAfter(double seconds, long waitMillis)
      Whether the process has ended on its own (not stopped or interrupted here), waiting at most waitMillis for that, after running at least the given number of seconds

    • interrupt

      public void interrupt()
      Interrupts the command the solver is running by sending it SIGINT: z3 then abandons the command (check-sat answers unknown) and goes on; most other solvers exit. Windows has no such signal, so there the process is ended.

    • isRunning

      public boolean isRunning(boolean expectStopped)
      Returns true if the process is still running; this relies on exceptions for control flow and may be a bit expensive.

    • exit

      public void exit()
      Aborts the process; returns immediately if already stopped

    • hasExited

      public boolean hasExited()
      Whether the process was started and has since exited

    • waitForEnd

      public boolean waitForEnd(long millis)
      Waits at most millis for the process to end; returns whether it has

    • nextLine

      public int nextLine()
      The number of the solver input line that the next text sent starts on (lines counted from 1)

    • send

      public String send(boolean listen, String... args) throws IOException
      Sends all the given text arguments, then (if listen is true) listens for the designated end marker text
      Throws:
      IOException

    • stopIfRunning

      public void stopIfRunning()
      Stops the solver's OS process if it is still running, leaving this object as it is: later sends then fail as "Solver process has already exited", and exit() cleans up.

    • sendAndListen

      public String sendAndListen(String... args) throws IOException
      Sends all the given text arguments, then listens for the designated end marker text
      Throws:
      IOException

    • sendNoListen

      public void sendNoListen(String... args) throws IOException
      Sends all the given text arguments, but does not wait for a response
      Throws:
      IOException

    • outputEnded

      public boolean outputEnded()
      Whether reading has reached the end of standard output: the process has exited or closed it

    • readOutput

      public String readOutput(long waitMillis) throws IOException
      For pipelined reading, which, unlike listen(), does not pair the text with one command: the next text the solver wrote on standard output, waiting up to waitMillis for it (not at all if 0; until some arrives or the output ends if negative). Returns null if none arrived in that time, or if the output has ended (see outputEnded()).
      Throws:
      IOException

    • readErrorOutput

      public String readErrorOutput(long waitMillis) throws IOException
      For pipelined reading: the text that has arrived on standard error, waiting up to waitMillis for some (see StreamGobbler.drain)
      Throws:
      IOException

    • readRemainingErrorOutput

      public String readRemainingErrorOutput() throws IOException
      For pipelined reading, once the output has ended: the rest of the text on standard error, up to its end (waiting at most endDrainMillis)
      Throws:
      IOException