Package org.smtlib

Class Log

java.lang.Object
org.smtlib.Log
public class Log extends Object
This class is used as a collection point for all output. The SMTLIB defines two output streams - regular output and diagnostic output, normally assigned to standard out and stderr. The SMT out stream contains all standard SMT-LIB responses (including errors); the SMT diag stream is for user-defined debugging or other information.
Author:
David Cok

  • Field Details

    • numErrors

      public int numErrors
      Number of errors logged since last clear

    • listeners

      protected List<Log.IListener> listeners
      The list of listeners to send log messages to

  • Constructor Details

    • Log

      public Log(SMT.Configuration smtConfig)
      Constructs a Log based on the given configuration, adding a StandardListener

  • Method Details

    • getOut

      public PrintStream getOut()
      Returns the current regular-output stream.

    • getDiag

      public PrintStream getDiag()
      Returns the current diagnostic stream.

    • setChannels

      public void setChannels(PrintStream out, PrintStream diag)
      Points both output channels at the given streams -- the one point through which every change to these two channels happens. Never opens a new stream: callers construct whatever they want a channel to point at (including smtConfig.stdout/stderr for the standard streams) and hand it in here, and this Log never closes a stream supplied this way -- ownership of it stays with the caller. (To point a channel at a named file, with this Log itself managing that file's lifecycle, use setRegularOutputChannel(String)/setDiagnosticOutputChannel(String) instead -- SMT-LIB's :regular-output-channel/:diagnostic-output-channel commands should go through those, not this method, directly.)

      Does close a stream this Log previously opened for a file, if it's being replaced here and isn't also the other channel's current value (guards the case where both channels were pointed at the same file).

    • setRegularOutputChannel

      public void setRegularOutputChannel(String spec) throws IOException
      Points the regular-output channel at "stdout", "stderr", or -- for any other value -- opens (in append mode) the file so named, per :regular-output-channel's SMT-LIB semantics. If the channel was previously pointed at a file this Log opened itself (and that file isn't also the current diagnostic channel), closes it first. Throws IOException if a named file can't be opened; the channel is left unchanged in that case -- the caller (AbstractSolver/Solver_test's set_option) is responsible for turning that into the appropriate SMT-LIB error response.
      Throws:
      IOException

    • setDiagnosticOutputChannel

      public void setDiagnosticOutputChannel(String spec) throws IOException
      The diag sibling of setRegularOutputChannel(String).
      Throws:
      IOException

    • hold

      public void hold(Log.IPendingOutput output)
      Holds a place in the output for content not yet known: until it is printed (see flush()), later logging calls are held behind it, so that output stays in order.

    • flush

      public void flush()
      Logs held output, in order, up to the first pending output that is not yet ready

    • unheld

      public <T> T unheld(Supplier<T> computation)
      Returns the computation's result, logging what it logs at once rather than holding it (e.g. while a solver's response is parsed, which an adapter may do with the channels redirected)

    • discardHeld

      public void discardHeld()
      Discards held output, e.g. when a run is aborted at an error in a pending response

    • isHolding

      public boolean isHolding()
      Whether output is held (see hold(IPendingOutput))

    • logOut

      public void logOut(IResponse r)
      Prints the argument on the regular output stream and to any listeners

    • logOut

      public void logOut(String message)
      Prints the argument on the regular output stream, with a line termination added, and notifies any listeners.

    • logOutNoln

      public void logOutNoln(String message)
      Prints the argument on the regular output stream with no newline appended, and notifies any listeners.

    • logError

      public IResponse.IError logError(IResponse.IError r)
      Reports the error to any listeners, returning the input.

    • logError

      public void logError(String r)
      Reports the error to any listeners.

    • logDiag

      public void logDiag(String message)
      Prints the argument to any listeners (adds a line terminator).

    • indent

      public void indent(String prompt)
      Sends the call to any listeners.

    • addListener

      public void addListener(Log.IListener listener)
      Adds a listener

    • clearListeners

      public void clearListeners()
      Clears all listeners

    • removeListener

      public boolean removeListener(Log.IListener listener)
      Removes a listener (found by using object equality ==)
      Parameters:
      listener - the listener to add
      Returns:
      true if the argument was in the list

    • locationIndication

      public static String locationIndication(IPos pos, String prompt, SMT.Configuration smtConfig)
      Creates a two-line, compiler-style caret diagnostic pointing at the given position; the returned value does not have a final line termination.

      In non-interactive mode, the first line is the source text line containing pos (if the error is more than 150 characters into a long line, that line is instead shown starting 20 characters before the error, prefixed with "... "; if the visible portion would still run past 150 characters, it is cut off there and suffixed with "...\n"). The second line reproduces the leading whitespace/tabs up to the error's start column -- matched against the prompt's width instead, in interactive mode -- followed by one ^ per character spanning pos's start-to-end range.

      Parameters:
      pos - the position to indicate
      prompt - the prompt with which to begin each line
      smtConfig - the current configuration
      Returns:
      a canonical string representation of the location