Uses of Class
org.smtlib.SMT.Configuration

Packages that use SMT.Configuration

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
org.smtlib.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
org.smtlib.logic	This package contains implementations of classes that implement the constraints of individual logics.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
org.smtlib.solvers	This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.

Uses of SMT.Configuration in org.smtlib

Fields in org.smtlib declared as SMT.Configuration

Modifier and Type	Field	Description
protected SMT.Configuration	AbstractSolver.smtConfig	SMT configuration — set by each concrete subclass constructor.
protected SMT.Configuration	CharSequenceSocket.smtConfig	The configuration for this instance of SMT
SMT.Configuration	SMT.Prompter.smtConfig
SMT.Configuration	SMT.smtConfig	The set of configuration settings for this instance of the SMT object
SMT.Configuration	SymbolTable.smtConfig	A reference to the Configuration for this instance of SMT.
protected SMT.Configuration	Utils.smtConfig	A reference to the configuration being used for this instance of Utils.

Methods in org.smtlib that return SMT.Configuration

Modifier and Type	Method	Description
SMT.Configuration	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).
SMT.Configuration	AbstractSolver.smt()
SMT.Configuration	IParser.smt()	Returns the configuration with which the parser was instantiated.
SMT.Configuration	ISolver.smt()	Returns the configuration object with which the solver is initialized

Methods in org.smtlib with parameters of type SMT.Configuration

Modifier and Type	Method	Description
IResponse	AbstractSolver.checkPrintSuccess(SMT.Configuration smtConfig, IExpr.IKeyword key, IAttributeValue value)	Answers a set-option of :print-success locally (it is never sent), else returns null
IParser	IParser.IFactory.createParser(SMT.Configuration smtConfig, ISource source)	Creates a parser that reads and parses concrete syntax from the given source
IPrinter	IParser.IFactory.createPrinter(SMT.Configuration smtConfig, Writer w)	Creates a printer
ISource	IParser.IFactory.createSource(SMT.Configuration smtConfig, File file)	Creates a character source from the given file
ISource	IParser.IFactory.createSource(SMT.Configuration smtConfig, InputStream file, Object location)	Creates a character source from the given stream
static String	Log.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.
int	SMT.processCommandLine(String[] args, SMT.Configuration options)	Parses the command-line, setting any option in the given configuration argument.
static String	Utils.produceAssertionsKey(SMT.Configuration smtConfig)	Returns the name of the option that gates get-assertions -- renamed from :interactive-mode to :produce-assertions in SMT-LIB 2.5.
ISolver	SMT.startSolver(SMT.Configuration smtConfig, String solvername, String executable)	Starts the solver with the given name and executable, preset according to the given configuration.
IResponse	AbstractSolver.successOrEmpty(SMT.Configuration smtConfig)
static List<IResponse>	TypeChecker.validate(SMT.Configuration smtConfig, ICommand cmd)	Validates non-syntactic well-formedness of a command (user IDs, duplicate names, list sizes).
static List<IResponse>	TypeChecker.validateDatatypeNames(SymbolTable symTable, SMT.Configuration smtConfig, List<IExpr.ISortDeclaration> sortDecls, List<ISort.IDatatype> datatypes)	Checks that constructor and selector names introduced by a datatype group are not already defined (neither in the symbol table nor duplicated within the group).

Constructors in org.smtlib with parameters of type SMT.Configuration

Modifier	Constructor	Description
	CharSequenceSocket(SMT.Configuration smtConfig, ServerSocket serverSocket, int initialSize, int sizeIncrease, double sizeMultiple)	Constructor for a new instance
	Log(SMT.Configuration smtConfig)	Constructs a Log based on the given configuration, adding a StandardListener
	Prompter(SMT.Configuration smtConfig)	Creates a prompter object - the object knows how to prompt for input based on current settings and state
	SymbolTable(SMT.Configuration smtConfig)	Constructs an empty symbol table
	Utils(SMT.Configuration smtConfig)	Creates a Utils instance for the given configuration

Uses of SMT.Configuration in org.smtlib.command

Methods in org.smtlib.command with parameters of type SMT.Configuration

Modifier and Type	Method	Description
IResponse.IError	C_set_option.checkOptionType(SMT.Configuration smtConfig, IExpr.IKeyword keyword, IAttributeValue t)	This method checks that the value for the given keyword has the correct type, when the keyword is used as the key for an SMT-LIB option.

Uses of SMT.Configuration in org.smtlib.impl

Fields in org.smtlib.impl declared as SMT.Configuration

Modifier and Type	Field	Description
protected final SMT.Configuration	Factory.smtConfig	The configuration this factory's instances (e.g.
protected final SMT.Configuration	SMTExpr.Logic.smtConfig	The configuration this logic instance is scoped to; see issue #22.

Methods in org.smtlib.impl with parameters of type SMT.Configuration

Modifier and Type	Method	Description
static IParser.ParserException	Command.error(SMT.Configuration smt, String msg, IPos pos)	Creates a ParserException with the given message and position.
static void	Factory.initFactories(SMT.Configuration config)	Initializes the SMT configuration object for the implementation in org.smtlib.impl - all the appropriate factories, etc.

Constructors in org.smtlib.impl with parameters of type SMT.Configuration

Modifier	Constructor	Description
	Factory(SMT.Configuration smtConfig)
	Factory(SMT.Configuration smtConfig)
	Logic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)	Creates a logic
	Source(SMT.Configuration smtConfig, File f)	Creates a Source from a File; for these objects, the location is the file path (a String)
	Source(SMT.Configuration smtConfig, InputStream f, Object location)	Creates a Source from a File
	StringLiteral(SMT.Configuration smtConfig, String value, boolean quoted)	Creates a string literal.

Uses of SMT.Configuration in org.smtlib.logic

Constructors in org.smtlib.logic with parameters of type SMT.Configuration

Modifier	Constructor	Description
	ALL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	AUFLIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	AUFLIRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	AUFNIRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	DifferenceLogic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	LIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	Logic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	LRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_ABV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_AUFBV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_AUFLIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_AX(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_BV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_EIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_FP(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_IDL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_LIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_LRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_NIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_NRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_RDL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UF(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFBV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFIDL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFLIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFLRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFNRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	UFLRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	UFNIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)

Uses of SMT.Configuration in org.smtlib.sexpr

Fields in org.smtlib.sexpr declared as SMT.Configuration

Modifier and Type	Field	Description
protected final SMT.Configuration	Printer.smtConfig	The Configuration whose rules (e.g.

Methods in org.smtlib.sexpr that return SMT.Configuration

Modifier and Type	Method	Description
SMT.Configuration	Parser.smt()	Returns a handle to the parent SMTConfig object, in order to see command-line options etc.

Methods in org.smtlib.sexpr with parameters of type SMT.Configuration

Modifier and Type	Method	Description
Parser	Factory.createParser(SMT.Configuration smtConfig, ISource source)
IPrinter	Factory.createPrinter(SMT.Configuration smtConfig, Writer w)
Pos.Source	Factory.createSource(SMT.Configuration smtConfig, File file)
Pos.Source	Factory.createSource(SMT.Configuration smtConfig, InputStream file, Object location)
static void	Factory.initFactories(SMT.Configuration config)	This method will initialize the factories and default printer in the configuration with appropriate objects from this implementation; it should be called as part of initial set up of the configuration.
static <T extends INode> void	Printer.WithLines.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.WithLines.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> String	Printer.write(SMT.Configuration smtConfig, T e)	Writes the given expression and outputs as a String, following the given Configuration's rules (e.g.

Constructors in org.smtlib.sexpr with parameters of type SMT.Configuration

Modifier	Constructor	Description
	Lexer(SMT.Configuration smtConfig, ISource src)	Creates a Lexer using an SMT configuration object and a source for characters
	Parser(SMT.Configuration smtConfig, ISource src)	Creates a Parser using an SMT configuration object and a source for characters; ordinarily use a factory to obtain a parser.
	Printer(SMT.Configuration smtConfig, Writer w)	Creates a printer object that follows the given Configuration's rules.
	WithLines(SMT.Configuration smtConfig, Writer w)	Creates a printer object that follows the given Configuration's rules.

Uses of SMT.Configuration in org.smtlib.solvers

Fields in org.smtlib.solvers declared as SMT.Configuration

Modifier and Type	Field	Description
protected SMT.Configuration	Solver_test.smtConfig	A reference to the configuration used by this SMT instance.

Methods in org.smtlib.solvers that return SMT.Configuration

Modifier and Type	Method	Description
SMT.Configuration	Solver_test.smt()	Returns the reference to the configuration currently in use.

Methods in org.smtlib.solvers with parameters of type SMT.Configuration

Modifier and Type	Method	Description
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> String	Printer.write(SMT.Configuration smtConfig, T e)	Writes the given expression and outputs as a String, following the given Configuration's rules.

Constructors in org.smtlib.solvers with parameters of type SMT.Configuration

Modifier	Constructor	Description
	Printer(SMT.Configuration smtConfig, Writer w)	Creates a printer object that follows the given Configuration's rules.
	Solver_altergo(SMT.Configuration smtConfig, String executable)	Creates an instance of the solver
	Solver_altergo(SMT.Configuration smtConfig, String[] command)	Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
	Solver_bitwuzla(SMT.Configuration smtConfig, String executable)	Creates an instance of the solver
	Solver_bitwuzla(SMT.Configuration smtConfig, String[] command)	Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
	Solver_cvc5(SMT.Configuration smtConfig, String executable)	Creates an instance of the solver
	Solver_cvc5(SMT.Configuration smtConfig, String[] command)	Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
	Solver_simplify(SMT.Configuration smtConfig, String executable)	Constructor with standard signature for invocation through reflection
	Solver_simplify(SMT.Configuration smtConfig, String[] command)	Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
	Solver_smt(SMT.Configuration smtConfig, String executable)	Creates an instance of the adapter
	Solver_smt(SMT.Configuration smtConfig, String[] args)
	Solver_smtinterpol(SMT.Configuration smtConfig, String[] command)	Creates an instance of the solver.
	Solver_test(SMT.Configuration smtConfig, String exec)	Constructor for an instance of this test solver class; the second argument is ignored - it is present just for uniformity with other solvers, for which that argument is a path to the relevant executable.
	Solver_yices2(SMT.Configuration smtConfig, String command)	Creates an instance of the yices2 solver
	Solver_yices2(SMT.Configuration smtConfig, String[] command)	Creates an instance of the yices2 solver
	Solver_yices2_2_6(SMT.Configuration smtConfig, String command)
	Solver_yices2_2_6(SMT.Configuration smtConfig, String[] command)
	Solver_z3_4_3(SMT.Configuration smtConfig, String executable)	Creates an instance of the Z3 solver
	Solver_z3_4_3(SMT.Configuration smtConfig, String[] command)	Creates an instance of the Z3 solver
	Solver_z3_4_3_2(SMT.Configuration smtConfig, String executable)
	Solver_z3_4_3_2(SMT.Configuration smtConfig, String[] command)	Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
	Solver_z3_4_5(SMT.Configuration smtConfig, String executable)
	Solver_z3_4_5(SMT.Configuration smtConfig, String[] command)
	Solver_z3_recent(SMT.Configuration smtConfig, String executable)	Creates an instance of the solver
	Solver_z3_recent(SMT.Configuration smtConfig, String[] command)	Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
	Translator(SMT.Configuration smtConfig)
	Translator(SMT.Configuration smtConfig, boolean allLogic)