Uses of Interface
org.smtlib.ICommand

Packages that use ICommand

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.ext	This package contains commands that are extensions to SMT-LIB.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
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 ICommand in org.smtlib

Subinterfaces of ICommand in org.smtlib

Modifier and Type	Interface	Description
static interface	ICommand.Iassert	Interface for the SMT-LIB assert command.
static interface	ICommand.Icheck_sat	Interface for the SMT-LIB check-sat command.
static interface	ICommand.Icheck_sat_assuming	Interface for the SMT-LIB check-sat-assuming command.
static interface	ICommand.Icomment	Interface for a comment pseudo-command: not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand (see issue #115) so that every dispatch path -- execution, typed-visitor traversal, and printing -- treats it uniformly with every other command, rather than falling back on IVisitor's generic visit(ICommand) handling (a reflection-based lookup in Printer's case).
static interface	ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
static interface	ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
static interface	ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
static interface	ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
static interface	ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
static interface	ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
static interface	ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
static interface	ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
static interface	ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
static interface	ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
static interface	ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
static interface	ICommand.Iecho	Interface for the SMT-LIB echo command.
static interface	ICommand.Iexit	Interface for the SMT-LIB exit command.
static interface	ICommand.Iget_assertions	Interface for the SMT-LIB get-assertions command.
static interface	ICommand.Iget_assignment	Interface for the SMT-LIB get-assignment command.
static interface	ICommand.Iget_info	Interface for the SMT-LIB get-info command.
static interface	ICommand.Iget_model	Interface for the SMT-LIB get-model command (non-standard extension).
static interface	ICommand.Iget_option	Interface for the SMT-LIB get-option command.
static interface	ICommand.Iget_proof	Interface for the SMT-LIB get-proof command.
static interface	ICommand.Iget_unsat_assumptions	Interface for the SMT-LIB get-unsat-assumptions command.
static interface	ICommand.Iget_unsat_core	Interface for the SMT-LIB get-unsat-core command.
static interface	ICommand.Iget_value	Interface for the SMT-LIB get-value command.
static interface	ICommand.Ipop	Interface for the SMT-LIB pop command.
static interface	ICommand.Ipush	Interface for the SMT-LIB push command.
static interface	ICommand.Ireset	Interface for the SMT-LIB reset command.
static interface	ICommand.Ireset_assertions	Interface for the SMT-LIB reset-assertions command.
static interface	ICommand.Iset_info	Interface for the SMT-LIB set-info command.
static interface	ICommand.Iset_logic	Interface for the SMT-LIB set-logic command.
static interface	ICommand.Iset_option	Interface for the SMT-LIB set-option command.

Fields in org.smtlib with type parameters of type ICommand

Modifier and Type	Field	Description
Map<String,Class<? extends ICommand>>	SMT.Configuration.commands	Holds a mapping from command name to the class implementing the command

Methods in org.smtlib that return ICommand

Modifier and Type	Method	Description
ICommand	IParser.parseCommand()	Parses an SMT-LIB command, if the parser is looking at text representing a valid SMT-LIB command; returns null and logs errors if the text is not a valid command.

Methods in org.smtlib that return types with arguments of type ICommand

Modifier and Type	Method	Description
List<ICommand>	ICommand.IScript.commands()
Class<? extends ICommand>	ICommand.IFinder.findCommand(String name)	This method finds a class that implements the ICommand interface for the given class name

Methods in org.smtlib with parameters of type ICommand

Modifier and Type	Method	Description
void	ICommand.IScript.add(ICommand command)	Adds a command to the end of the script's command list.
protected String	AbstractSolver.correctResponse(ICommand cmd, String response)	The solver's raw response to cmd (sent by sendCommand and waited for), corrected where the solver departs from SMT-LIB; an adapter overrides this to patch a specific non-conforming response
IResponse	AbstractSolver.execute(ICommand cmd)	Once the solver process has exited, every command but exit (and a comment, which has no response) answers AbstractSolver.exitedResponse(), including those an adapter answers itself or checks with its own queries
default IResponse	ISolver.execute(ICommand command)	Executes the command on this solver
boolean	AbstractSolver.pipelines(ICommand cmd)	Whether AbstractSolver.sendPipelined(ICommand) may send the command without waiting for its response.
protected IResponse	AbstractSolver.sendChange(AbstractSolver.StackChange kind, ICommand cmd)	Sends a command that changes the assertion stack, recording it (see recordChange)
protected IResponse	AbstractSolver.sendCommand(ICommand cmd)	Translates the given command and sends it to the solver process, returning the parsed response.
IResponse	AbstractSolver.sendPipelined(ICommand cmd)	Executes a command for which AbstractSolver.pipelines(ICommand) is true, sending it to the solver without waiting for the response.
protected static AbstractSolver.Shape	AbstractSolver.shapeOf(ICommand cmd)	The kind of response cmd has
static int	Utils.sourceLine(ICommand cmd)	The line of its source on which the command starts (counted from 1), or 0 if it has no source position
static List<IResponse>	TypeChecker.validate(SMT.Configuration smtConfig, ICommand cmd)	Validates non-syntactic well-formedness of a command (user IDs, duplicate names, list sizes).
T	IVisitor.TreeVisitor.visit(ICommand e)
T	IVisitor.visit(ICommand e)
ISort	TypeChecker.visit(ICommand e)

Method parameters in org.smtlib with type arguments of type ICommand

Modifier and Type	Method	Description
IResponse	AbstractSolver.executePipelined(List<ICommand> commands)	Executes the commands in order, as a script does: returns the first error, or else the last command's response.
ICommand.IScript	ICommand.IFactory.script(IExpr.IStringLiteral filename, List<ICommand> commands)	Creates a script object containing the given filename or the given set of commands.

Uses of ICommand in org.smtlib.command

Classes in org.smtlib.command that implement ICommand

Modifier and Type	Class	Description
class	C_assert	Implements the assert command
class	C_check_sat	Implements the check-sat command
class	C_check_sat_assuming	Implements the check-sat-assuming command
class	C_comment	A synthetic pseudo-command representing a comment that appeared immediately before a real command in a script -- not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand.Icomment (see issue #115) rather than a generic ICommand, so execution, typed-visitor traversal, and printing all dispatch to it the same way every other command does, with no reflection-based or generic-fallback special case.
class	C_declare_const	Implements the declare-const command (syntactic sugar for declare-fun with no argument sorts)
class	C_declare_datatype	Implements the declare-datatype command
class	C_declare_datatypes	Implements the declare-datatypes command
class	C_declare_fun	Implements the declare-fun command
class	C_declare_sort	Implements the declare-sort command
class	C_declare_sort_parameter	Implements the declare-sort-parameter command
class	C_define_const	Implements the define-const command: syntactic sugar for define-fun with no parameters
class	C_define_fun	Implements the define-fun command
class	C_define_fun_rec	Implements the define-fun-rec command (recursive function definition); syntactically identical to define-fun (see C_define_fun), differing only in the dispatch target -- shares that class's fields, accessors, and constructor.
class	C_define_funs_rec	Implements the define-funs-rec command
class	C_define_sort	Implements the define-sort command
class	C_echo	Implements the echo command
class	C_exit	Implements the exit command
class	C_get_assertions	Implements the get-assertions command
class	C_get_assignment	Implements the get-assignment command
class	C_get_info	Implements the get-info command.
class	C_get_model	Implements the get-model command
class	C_get_option	Implements the get-option command
class	C_get_proof	Implements the get-proof command
class	C_get_unsat_assumptions	Implements the get-unsat-assumptions command
class	C_get_unsat_core	Implements the get-unsat-core command
class	C_get_value	Implements the get-value command
class	C_pop	Implements the pop command
class	C_push	Implements the push command
class	C_reset	Implements the reset command
class	C_reset_assertions	Implements the reset-assertions command
class	C_set_info	Implements the set-info command
class	C_set_logic	Implements the set-logic command.
class	C_set_option	Implements the set-option command

Uses of ICommand in org.smtlib.ext

Subinterfaces of ICommand in org.smtlib.ext

Modifier and Type	Interface	Description
interface	Iexec	Interface for the SMT-LIB exec command (non-standard extension).
interface	Iwhat	Interface for the SMT-LIB what command (non-standard extension).

Classes in org.smtlib.ext that implement ICommand

Modifier and Type	Class	Description
class	C_exec	Implements the non-standard exec command
class	C_what	Implements the non-standard what command.

Uses of ICommand in org.smtlib.impl

Classes in org.smtlib.impl that implement ICommand

Modifier and Type	Class	Description
class	Command	This abstract class is the base class for all commands within this implementation.

Fields in org.smtlib.impl with type parameters of type ICommand

Modifier and Type	Field	Description
protected List<ICommand>	Script.commands	The list of commands

Methods in org.smtlib.impl that return types with arguments of type ICommand

Modifier and Type	Method	Description
List<ICommand>	Script.commands()	Returns a reference to the internal list

Methods in org.smtlib.impl with parameters of type ICommand

Modifier and Type	Method	Description
void	Script.add(ICommand command)	Adds a command to the end of the script

Method parameters in org.smtlib.impl with type arguments of type ICommand

Modifier and Type	Method	Description
ICommand.IScript	Factory.script(IExpr.IStringLiteral filename, List<ICommand> commands)

Constructor parameters in org.smtlib.impl with type arguments of type ICommand

Modifier	Constructor	Description
	Script(IExpr.IStringLiteral filename, List<ICommand> list)	Constructs the script with the given list of commands, hijacking the list itself

Uses of ICommand in org.smtlib.sexpr

Methods in org.smtlib.sexpr with parameters of type ICommand

Modifier and Type	Method	Description
protected Void	Printer.printCommand(ICommand e)	Prints a no-argument command: (commandName()).
protected Void	Printer.printCommand(ICommand e, Printer.PrintArgs args)	Prints (commandName() args) — the space between name and args is emitted here, so the args lambda should not prepend one.
Void	Printer.visit(ICommand e)	Fallback for extension command types not covered by a specific visit method; uses reflection to invoke write(Printer) on the command object.

Uses of ICommand in org.smtlib.solvers

Methods in org.smtlib.solvers with parameters of type ICommand

Modifier and Type	Method	Description
IResponse	Solver_test.execute(ICommand cmd)	Once exited, every command but exit (and a comment) answers as a process-based solver's would
boolean	Solver_simplify.pipelines(ICommand cmd)	Never pipelined: commands are executed here, not sent to a process
boolean	Solver_z3_4_3.pipelines(ICommand cmd)	Never pipelined: this adapter sends and corrects commands by its own means
IResponse	Solver_z3_4_3.sendCommand(ICommand cmd)
String	Solver_simplify.Translator.visit(ICommand e)