Package org.smtlib

Class SMT

java.lang.Object
org.smtlib.SMT
public class SMT extends Object
This is the main class for the SMT-LIB tool. The tool is invoked as a command-line tool by running main within org.smtlib.SMT. The tool can also be invoked programmatically by calling exec() in a new instance of the SMT class, created with the default constructor. Separate instances of SMT objects can be run independently and in parallel. They are thread-safe (though they all may write to the same standard and error output streams).

To extend this tool, e.g. to use it with other factory objects for a different implementation, or to add configuration options:

  • Create subclasses of SMT, SMT.Configuration
  • The SMT' should set a new object of type SMT.Configuration' in its constructor
  • SMT' can override parseCommandLine, help, usage
  • Create a new main method; the new main should also instantiate the derived SMT and call exec on it
  • SMT.Configuration' can have new options added; it can also instantiate different object factories
  • SMT.Configuration' can also instantiate a derived Utils or Log object
Known rough edges in the above: parseCommandLine, help, and usage are not easy to extend as-is, and replacing the SymbolTable or SolverProcess, or introducing interfaces for Log/Utils, isn't supported by any of the extension points above.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static class 
    SMT.Configuration
    The configuration object holds the values of all of the current options (e.g.
    static interface 
    SMT.IConfiguration
    Marker interface for configuration objects; reserved for future extension.
    static class 
    SMT.InternalException
    This class is used to turn internal bugs that we do not want to try to recover into exceptions that can be reported
    static class 
    SMT.Prompter
    This class is a prompter used when more data is needed from a data source

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    IResponse
    checkSatStatus
    The last check-sat status seen during execution; null if no check-sat has been executed yet.
    IResponse
    lastResponse
    The response from the most recently executed command; used to export results in interactive mode.
    protected boolean
    pipelineInput
    Whether the input being processed may be pipelined (with --pipeline): file and --text input, not the socket or standard input, whose client needs each command's response at once
    SMT.Configuration
    smtConfig
    The set of configuration settings for this instance of the SMT object
    protected ISolver
    solver
     

  • Constructor Summary

    Constructors
    Constructor
    Description
    SMT()
     

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    cleanup()
    Forcibly stops the active solver, if any.
    protected int
    doParser(IParser p)
     
    protected int
    doParser(IParser p, boolean restart)
     
    protected void
    error(String msg)
    Helper function to log a command-line error
    int
    exec()
    Executes, presuming all options (e.g.
    int
    exec(String[] args)
    The method that does all the execution for the main method, here made a non-static method, so that multiple SMT operations can be proceeding independently.
    void
    help()
    Prints a verbose message about command line arguments
    static void
    main(String[] args)
    The main method of the SMT application
    int
    processCommandLine(String[] args, SMT.Configuration options)
    Parses the command-line, setting any option in the given configuration argument.
    String
    resolveExecutableForSolver(String solvername)
    Resolves the executable path startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String) would use for the given solver name (absent an explicit caller-supplied override -- startSolver's own executable parameter takes precedence there, which this standalone method has no equivalent of), without instantiating an adapter or starting anything -- lets a caller check whether the file actually exists before committing to run tests against it (see the test harness's LogicTests#solversFromEnv, which filters the solver list against this up front so a missing binary is one WARNING line instead of a wall of per-file failures).
    static String
    resolveExecutablePath(String exec, String solverDir)
    Resolves the path of a solver executable, whether from the properties (.exec or the solver name) or supplied by the caller: null, or an absolute path: returned unchanged; a relative path with a directory part (e.g.
    ISolver
    startSolver(SMT.Configuration smtConfig, String solvername, String executable)
    Starts the solver with the given name and executable, preset according to the given configuration.
    void
    usage()
    Prints a summary of the command-line arguments

    Methods inherited from class java.lang.Object

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

  • Field Details

    • smtConfig

      public SMT.Configuration smtConfig
      The set of configuration settings for this instance of the SMT object

    • checkSatStatus

      public IResponse checkSatStatus
      The last check-sat status seen during execution; null if no check-sat has been executed yet.

    • pipelineInput

      protected boolean pipelineInput
      Whether the input being processed may be pipelined (with --pipeline): file and --text input, not the socket or standard input, whose client needs each command's response at once

    • solver

      protected ISolver solver

    • lastResponse

      public IResponse lastResponse
      The response from the most recently executed command; used to export results in interactive mode.

  • Constructor Details

    • SMT

      public SMT()

  • Method Details

    • main

      public static void main(String[] args)
      The main method of the SMT application

    • exec

      public int exec(String[] args)
      The method that does all the execution for the main method, here made a non-static method, so that multiple SMT operations can be proceeding independently.
      Parameters:
      args - the command-line arguments
      Returns:
      the exit code to return to the command-line: 0 if every command succeeded (or for --help and --version); 1 for a command-line error, a solver that could not be started, an input file not found, or any command that reported an error; 2 if input could not be read or processing failed outright (an I/O or parser exception, stack overflow, out of memory). Over several files, the highest code wins.

    • exec

      public int exec()
      Executes, presuming all options (e.g. from the command-line) are set in the configuration object

    • doParser

      protected int doParser(IParser p)

    • cleanup

      public void cleanup()
      Forcibly stops the active solver, if any. Safe to call when no solver is running.

    • doParser

      protected int doParser(IParser p, boolean restart)

    • processCommandLine

      public int processCommandLine(String[] args, SMT.Configuration options)
      Parses the command-line, setting any option in the given configuration argument.

    • resolveExecutablePath

      public static String resolveExecutablePath(String exec, String solverDir)
      Resolves the path of a solver executable, whether from the properties (.exec or the solver name) or supplied by the caller:
      • null, or an absolute path: returned unchanged;
      • a relative path with a directory part (e.g. ../bin/z3): relative to the current directory, as a shell would take it; returned as an absolute path;
      • a simple file name (e.g. z3-5.1.0): solverDir/name if that file exists (on Windows, also as name.exe); else the name unchanged if it is found on the PATH, so that the process launch finds it there; else solverDir/name (so an error names the expected file), or the name unchanged if there is no solverDir.
      Pass System.getenv("SMT_SOLVER_DIR") as solverDir in production; pass a literal in tests.

    • resolveExecutableForSolver

      public String resolveExecutableForSolver(String solvername)
      Resolves the executable path startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String) would use for the given solver name (absent an explicit caller-supplied override -- startSolver's own executable parameter takes precedence there, which this standalone method has no equivalent of), without instantiating an adapter or starting anything -- lets a caller check whether the file actually exists before committing to run tests against it (see the test harness's LogicTests#solversFromEnv, which filters the solver list against this up front so a missing binary is one WARNING line instead of a wall of per-file failures). Mirrors the same .exec.<platform> / .exec / bare-name-as-executable resolution order startSolver itself uses for that case, but intentionally not reused *by* startSolver: unlike this method, startSolver still needs a real executable value even for a solver configured via .command (to populate command[0]), where existence-checking a single array element in isolation wouldn't be meaningful -- the two methods' correct behavior genuinely diverges on that case, not just their implementation.

      Returns null for the "test" pseudo-solver (no executable at all -- pure Java) and for a solver configured via a multi-argument .command property, both treated as "don't existence-check this one" by the caller.

    • startSolver

      public ISolver startSolver(SMT.Configuration smtConfig, String solvername, String executable)
      Starts the solver with the given name and executable, preset according to the given configuration. If executable is null, the path is resolved from jsmtlib.properties -- the org.smtlib.solver_<name>.exec.<platform> entry, then org.smtlib.solver_<name>.exec, then the solver name itself. A simple file name is looked for in $SMT_SOLVER_DIR (else on the PATH); a relative path with a directory part is relative to the current directory (see SMT.Configuration.createSolver(java.lang.String, java.lang.String) and resolveExecutablePath(java.lang.String, java.lang.String)).

      This is a thin, CLI-flavored wrapper around SMT.Configuration.createSolver(java.lang.String, java.lang.String): it resolves and constructs the adapter by delegating there, translating a thrown ISolver.CreationException into this method's own error()/usage()/null-return contract (preserved here unchanged for backward compatibility with the CLI's own --solver flag handling and its tests), then itself starts the constructed solver and applies the same response-checking this method has always done.

      Parameters:
      smtConfig - the configuration object to use for solver settings
      solvername - the name of the solver to use
      executable - the executable path
      Returns:
      the ISolver object, or null if errors happened

    • error

      protected void error(String msg)
      Helper function to log a command-line error

    • usage

      public void usage()
      Prints a summary of the command-line arguments

    • help

      public void help()
      Prints a verbose message about command line arguments