org.smtlib.SMT.Configuration

All Implemented Interfaces:: Cloneable, SMT.IConfiguration

Enclosing class:: SMT

public static class SMT.Configuration extends Object implements Cloneable, SMT.IConfiguration

The configuration object holds the values of all of the current options (e.g. command-line settings); it also holds factory objects that are used to create objects for the particular concrete syntax being used; it also holds a few internal state values

Nested Class Summary

Nested Classes

Modifier and Type

Class

Description

static enum

SMT.Configuration.SMTLIB

Enumeration of the supported SMT-LIB versions, in declaration order from oldest to newest.
Field Summary

Fields

Modifier and Type

Field

Description

boolean

abort

If true, command processing in a solver aborts on the first error

String[]

commandExtensionPrefixes

An array of fully-qualified class name prefixes; a command name (with hyphen replaced by underscore) is appended to the prefix to obtain a fully-qualified class name that implements the command.

ICommand.IFactory

commandFactory

The factory to use to create ICommand objects

ICommand.IFinder

commandFinder

A class that implements ICommandFinder, whose one method returns the class object of the class that implements a command with a given name; the algorithm to identify the command class first looks for an entry in the command map above and otherwise uses this default: replace each - in the command name by _, and append the resulting string to the elements of 'commandExtensionPrefixes', looking for the first such class that exists; if relax is false (strict SMT-LIB) then the commands map and all but the initial entry of commandExtensionPrefixes are ignored.

Map<String,Class<? extends ICommand>>

commands

Holds a mapping from command name to the class implementing the command

IPrinter

defaultPrinter

The default printer used to convert AST objects to strings for output.

String

diag

If non-null, the file name (or 'stdout'/'stderr') to use for diagnostic output.

boolean

echo

True if the application is to echo commands as it executes them; only applies in interactiveMode mode

String

executable

The path to the executable for the solver to use

IExpr.IFactory

exprFactory

The factory to use to create IExpr objects

List<String>

files

The files of SMT-LIB commands to process; if null or empty then the standard input is used

int

initialInputBufferSize

Initial capacity in characters for the input reader's internal buffer.

boolean

interactive

This variable records whether we are reading from standard input, in which case the input text is usually already present.

Log

log

The log to use for regular, error, and diagnostic output

String

logfile

The file to which to write the communication, for debugging or reference; null means default

String

logic

This field is set from the command-line; if set, then sets the logic used by the solver, as if the first command were the corresponding set-logic command.

String

logicPath

The path on which to find logic and theory definitions

boolean

noshow

If true, then information about the position of an error is not shown

boolean

nosuccess

This field is set from the command-line and sets the initial state of the :print-success option within a solver.

String

out

If non-null, the file name (or 'stdout'/'stderr') to use for regular output.

boolean

pipeline

If true, commands are sent to the solver without waiting for each response where that is possible (AbstractSolver.sendPipelined), and the responses are read as they arrive: by the command-line tool for file or --text input (--pipeline), and by IScript.execute (AbstractSolver.executePipelined)

int

port

The port to use for socket communications; a port > 0 supersedes any file value, but is ignored if the text option is set.

String

prompt

The prompt to use when needing new input from the user in an interactive mode.

String

prompt2

The prompt to use when in the middle of a command

Properties

props

Properties loaded from the jsmtlib.properties file(s); see readProperties().

boolean

relax

When true, allows some convenience relaxations of the SMTLIB standard; when false, the standard is strictly enforced.

Map<String,SMT.Configuration.SMTLIB>

reservedSince

The version in which a reserved word became reserved, for those not reserved in V2.0

Set<String>

reservedWords

A list of all reserved words

Set<String>

reservedWordsNotCommands

A list of reserved words that are not commands

IResponse.IFactory

responseFactory

The factory to use to create IResponse objects

int

seed

If non-zero, a seed to pass to the solver to initialize its random number generator (--seed, non-negative)

IParser.IFactory

smtFactory

The factory to use to create IParser, IPos, ISource objects

SMT.Configuration.SMTLIB

smtlib

The version of SMT-LIB to be supported; null means the default (most recent version)

String

solvername

The solver to use

int

solverVerbosity

The verbosity level of the SMT solver

ISort.IFactory

sortFactory

The factory to use to create ISort objects

PrintStream

stderr

The PrintStream that "stderr" resolves to for this instance.

PrintStream

stdout

The PrintStream that "stdout" resolves to for this instance.

String[]

strictCommandExtensionPrefixes

boolean

testing

When true, a solver's raw response text is scrubbed of known non-deterministic content (elapsed-time figures, memory usage) before being parsed, replacing each with a fixed placeholder (e.g.

String

text

A string containing the SMT-LIB commands to use; if null the given file is used; if non-null this text is used instead of the content of the file or the input from a port.

double

timeout

The soft, per-query timeout, in seconds (fractional allowed), set via -t/--timeout; <=0 means no timeout.

double

timeoutTotal

The whole-run (solver-process-lifetime) timeout, in seconds (fractional allowed), set via -T/--timeout-total; <=0 means no timeout.

boolean

topLevel

Encodes an aspect of current parser state so that we know what kind of prompt to use.

Utils

utils

The utils object to use for utility methods

int

verbose

True to emit diagnostic output through the SMT-LIB diagnostic channel
Constructor Summary

Constructors

Constructor

Description

Configuration()

Creates a default configuration, initialized from org.smtlib.impl
Method Summary

Modifier and Type

Method

Description

boolean

atLeastVersion(SMT.Configuration.SMTLIB version)

Returns true if the configured version is at least the given version.

SMT.Configuration

clone()

Makes an independent copy of the configuration: a shallow, reference-copying field-for-field clone (via super.clone()) is not enough on its own, since several fields are mutable containers or hold a back-reference to this Configuration -- left reference-copied, mutating one of those through the clone would silently mutate the original too, contradicting this class's own "Separate instances of SMT objects can be run independently and in parallel" design goal (see the class Javadoc).

ISolver

createSolver(String solvername, String executable)

Resolves the given solver name and executable to a concrete ISolver adapter instance, applying the same name/executable/adapter resolution jsmtlib.properties supports as SMT.startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String) -- platform-specific .adapter/.exec overrides checked before their bare counterparts, the Solver_<name> naming convention, the z3-specific Solver_z3_recent fallback for an unrecognized z3 variant, the generic Solver_smt fallback, the "test" pseudo-solver special case, and %exec% command-array placeholder substitution -- but, unlike startSolver, this method does not start the solver and does not do any CLI-flavored error()/usage() reporting: any resolution or construction failure is reported as a thrown ISolver.CreationException instead, leaving it to the caller to start the returned solver (via ISolver.start()) and decide how to report a creation failure.

boolean

isOKKeyword(String value)

True if the string (including the colon) is a legal keyword: a colon followed by a simple symbol, that is, letters, digits and the characters ~!@$%^&*_-+=<>.?/, not starting with a digit and not a reserved word.

boolean

isOKString(String value)

True if the string, as the (unescaped) value of a string literal, is legal in the configured SMT-LIB version: printable and white-space characters only, those beyond ASCII only from V2.5 on

boolean

isOKSymbol(String value)

True if the string, as the value of a symbol (without enclosing bars), is a legal symbol in the configured SMT-LIB version: not a reserved word (|let| is the same symbol as let), without | or \, and of printable and white-space characters only, those beyond ASCII only from V2.5 on

boolean

isReservedWord(String word)

True if the word is reserved in the configured SMT-LIB version; with --relax, command names are not

boolean

isVersion(SMT.Configuration.SMTLIB version)

Returns true if the configured version equals the given version.

Properties

readProperties()

Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details
- reservedWordsNotCommands
  
  public Set<String> reservedWordsNotCommands
  
  A list of reserved words that are not commands
- reservedWords
  
  public Set<String> reservedWords
  
  A list of all reserved words
- reservedSince
  
  public Map<String,SMT.Configuration.SMTLIB> reservedSince
  
  The version in which a reserved word became reserved, for those not reserved in V2.0
- smtlib
  
  public SMT.Configuration.SMTLIB smtlib
  
  The version of SMT-LIB to be supported; null means the default (most recent version)
- verbose
  
  public int verbose
  
  True to emit diagnostic output through the SMT-LIB diagnostic channel
- solverVerbosity
  
  public int solverVerbosity
  
  The verbosity level of the SMT solver
- timeout
  
  public double timeout
  
  The soft, per-query timeout, in seconds (fractional allowed), set via -t/--timeout; <=0 means no timeout. See timeoutTotal for the whole-run counterpart. jSMTLIB expresses both values in seconds regardless of solver; each solver adapter translates them into whatever unit, flag, and scope (per-query vs. whole-run) that solver's own binary actually supports -- see the per-adapter comments where timeout/timeoutTotal are read.
- timeoutTotal
  
  public double timeoutTotal
  
  The whole-run (solver-process-lifetime) timeout, in seconds (fractional allowed), set via -T/--timeout-total; <=0 means no timeout. See timeout for the per-query counterpart and the general unit/translation note there.
- nosuccess
  
  public boolean nosuccess
  
  This field is set from the command-line and sets the initial state of the :print-success option within a solver.
- abort
  
  public boolean abort
  
  If true, command processing in a solver aborts on the first error
- echo
  
  public boolean echo
  
  True if the application is to echo commands as it executes them; only applies in interactiveMode mode
- pipeline
  
  public boolean pipeline
  
  If true, commands are sent to the solver without waiting for each response where that is possible (AbstractSolver.sendPipelined), and the responses are read as they arrive: by the command-line tool for file or --text input (--pipeline), and by IScript.execute (AbstractSolver.executePipelined)
- logic
  
  public String logic
  
  This field is set from the command-line; if set, then sets the logic used by the solver, as if the first command were the corresponding set-logic command.
- solvername
  
  public String solvername
  
  The solver to use
- executable
  
  public String executable
  
  The path to the executable for the solver to use
- logfile
  
  public String logfile
  
  The file to which to write the communication, for debugging or reference; null means default
- files
  
  public List<String> files
  
  The files of SMT-LIB commands to process; if null or empty then the standard input is used
- text
  
  public String text
  
  A string containing the SMT-LIB commands to use; if null the given file is used; if non-null this text is used instead of the content of the file or the input from a port. A typical use is when the SMT text is generated rather than read.
- noshow
  
  public boolean noshow
  
  If true, then information about the position of an error is not shown
- seed
  
  public int seed
  
  If non-zero, a seed to pass to the solver to initialize its random number generator (--seed, non-negative)
- out
  
  public String out
  
  If non-null, the file name (or 'stdout'/'stderr') to use for regular output.
- diag
  
  public String diag
  
  If non-null, the file name (or 'stdout'/'stderr') to use for diagnostic output.
- port
  
  public int port
  
  The port to use for socket communications; a port > 0 supersedes any file value, but is ignored if the text option is set.
- log
  
  public Log log
  
  The log to use for regular, error, and diagnostic output
- props
  
  public Properties props
  
  Properties loaded from the jsmtlib.properties file(s); see readProperties().
- stdout
  
  public PrintStream stdout
  
  The PrintStream that "stdout" resolves to for this instance. Defaults to System.out; in-process callers (e.g. JUnit tests) set this to a per-test stream so that set_option(:regular-output-channel "stdout") does not escape the capture.
- stderr
  
  public PrintStream stderr
  
  The PrintStream that "stderr" resolves to for this instance. Defaults to System.err; in-process callers (e.g. JUnit tests) set this to a per-test stream so that set_option(:diagnostic-output-channel "stderr") does not escape the capture.
- utils
  
  public Utils utils
  
  The utils object to use for utility methods
- relax
  
  public boolean relax
  
  When true, allows some convenience relaxations of the SMTLIB standard; when false, the standard is strictly enforced.
- testing
  
  public boolean testing
  
  When true, a solver's raw response text is scrubbed of known non-deterministic content (elapsed-time figures, memory usage) before being parsed, replacing each with a fixed placeholder (e.g. TIME, VALUE) so that otherwise-identical output is byte-for-byte reproducible across runs and machines. Off by default -- this is a testing aid, not a normal end-user option. Currently applied only within AbstractSolver.get_info(IExpr.IKeyword), the one place this instability has actually been observed (cvc5's :all-statistics response, and :memory/ :max-memory figures on several solvers).
- commandExtensionPrefixes
  
  public String[] commandExtensionPrefixes
  
  An array of fully-qualified class name prefixes; a command name (with hyphen replaced by underscore) is appended to the prefix to obtain a fully-qualified class name that implements the command.
- strictCommandExtensionPrefixes
  
  public String[] strictCommandExtensionPrefixes
- logicPath
  
  public String logicPath
  
  The path on which to find logic and theory definitions
- prompt
  
  public String prompt
  
  The prompt to use when needing new input from the user in an interactive mode.
- prompt2
  
  public String prompt2
  
  The prompt to use when in the middle of a command
- sortFactory
  
  public ISort.IFactory sortFactory
  
  The factory to use to create ISort objects
- responseFactory
  
  public IResponse.IFactory responseFactory
  
  The factory to use to create IResponse objects
- exprFactory
  
  public IExpr.IFactory exprFactory
  
  The factory to use to create IExpr objects
- commandFactory
  
  public ICommand.IFactory commandFactory
  
  The factory to use to create ICommand objects
- smtFactory
  
  public IParser.IFactory smtFactory
  
  The factory to use to create IParser, IPos, ISource objects
- defaultPrinter
  
  public IPrinter defaultPrinter
  
  The default printer used to convert AST objects to strings for output.
- initialInputBufferSize
  
  public int initialInputBufferSize
  
  Initial capacity in characters for the input reader's internal buffer.
- commands
  
  public Map<String,Class<? extends ICommand>> commands
  
  Holds a mapping from command name to the class implementing the command
- commandFinder
  
  public ICommand.IFinder commandFinder
  
  A class that implements ICommandFinder, whose one method returns the class object of the class that implements a command with a given name; the algorithm to identify the command class first looks for an entry in the command map above and otherwise uses this default: replace each - in the command name by _, and append the resulting string to the elements of 'commandExtensionPrefixes', looking for the first such class that exists; if relax is false (strict SMT-LIB) then the commands map and all but the initial entry of commandExtensionPrefixes are ignored.
- interactive
  
  public boolean interactive
  
  This variable records whether we are reading from standard input, in which case the input text is usually already present. If this field is true, then we prompt when we need additional input and we do not need to echo back an invalid command.
- topLevel
  
  public boolean topLevel
  
  Encodes an aspect of current parser state so that we know what kind of prompt to use.
Constructor Details
- Configuration
  
  public Configuration()
  
  Creates a default configuration, initialized from org.smtlib.impl
Method Details
- clone
  
  public SMT.Configuration clone() throws CloneNotSupportedException
  
  Makes an independent copy of the configuration: a shallow, reference-copying field-for-field clone (via super.clone()) is not enough on its own, since several fields are mutable containers or hold a back-reference to this Configuration -- left reference-copied, mutating one of those through the clone would silently mutate the original too, contradicting this class's own "Separate instances of SMT objects can be run independently and in parallel" design goal (see the class Javadoc). commands/reservedWords/reservedWordsNotCommands/utils/log are each given their own fresh copy below for exactly this reason.
  
  Overrides:
  
  clone in class Object
  
  Throws:
  
  CloneNotSupportedException
- isReservedWord
  
  public boolean isReservedWord(String word)
  
  True if the word is reserved in the configured SMT-LIB version; with --relax, command names are not
- isOKSymbol
  
  public boolean isOKSymbol(String value)
  
  True if the string, as the value of a symbol (without enclosing bars), is a legal symbol in the configured SMT-LIB version: not a reserved word (|let| is the same symbol as let), without | or \, and of printable and white-space characters only, those beyond ASCII only from V2.5 on
- isOKKeyword
  
  public boolean isOKKeyword(String value)
  
  True if the string (including the colon) is a legal keyword: a colon followed by a simple symbol, that is, letters, digits and the characters ~!@$%^&*_-+=<>.?/, not starting with a digit and not a reserved word. The standard's example :56 contradicts this (#185).
- isOKString
  
  public boolean isOKString(String value)
  
  True if the string, as the (unescaped) value of a string literal, is legal in the configured SMT-LIB version: printable and white-space characters only, those beyond ASCII only from V2.5 on
- isVersion
  
  public boolean isVersion(SMT.Configuration.SMTLIB version)
  
  Returns true if the configured version equals the given version.
- atLeastVersion
  
  public boolean atLeastVersion(SMT.Configuration.SMTLIB version)
  
  Returns true if the configured version is at least the given version. Uses enum declaration order: V20 < V25 < V26 < V27.
- readProperties
  
  public Properties readProperties()
- createSolver
  
  public ISolver createSolver(String solvername, String executable) throws ISolver.CreationException
  
  Resolves the given solver name and executable to a concrete ISolver adapter instance, applying the same name/executable/adapter resolution jsmtlib.properties supports as SMT.startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String) -- platform-specific .adapter/.exec overrides checked before their bare counterparts, the Solver_<name> naming convention, the z3-specific Solver_z3_recent fallback for an unrecognized z3 variant, the generic Solver_smt fallback, the "test" pseudo-solver special case, and %exec% command-array placeholder substitution -- but, unlike startSolver, this method does not start the solver and does not do any CLI-flavored error()/usage() reporting: any resolution or construction failure is reported as a thrown ISolver.CreationException instead, leaving it to the caller to start the returned solver (via ISolver.start()) and decide how to report a creation failure.
  
  Parameters:
  
  solvername - the name of the solver to use
  
  executable - the executable path, or null to resolve one from jsmtlib.properties or (absent any properties entry) from the solver name itself
  
  Returns:
  
  a constructed, not-yet-started ISolver adapter instance
  
  Throws:
  
  ISolver.CreationException - if the adapter class or its constructor cannot be resolved, or construction otherwise fails

Class SMT.Configuration

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Details

reservedWordsNotCommands

reservedWords

reservedSince

smtlib

verbose

solverVerbosity

timeout

timeoutTotal

nosuccess

abort

echo

pipeline

logic

solvername

executable

logfile

files

text

noshow

seed

out

diag

port

log

props

stdout

stderr

utils

relax

testing

commandExtensionPrefixes

strictCommandExtensionPrefixes

logicPath

prompt

prompt2

sortFactory

responseFactory

exprFactory

commandFactory

smtFactory

defaultPrinter

initialInputBufferSize

commands

commandFinder

interactive

topLevel

Constructor Details

Configuration

Method Details

clone

isReservedWord

isOKSymbol

isOKKeyword

isOKString

isVersion

atLeastVersion

readProperties

createSolver