Uses of Class
org.smtlib.impl.Command

Packages that use Command

Package	Description
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.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.

Uses of Command in org.smtlib.command

Subclasses of Command in org.smtlib.command

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 Command in org.smtlib.ext

Subclasses of Command in org.smtlib.ext

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 Command in org.smtlib.sexpr

Methods in org.smtlib.sexpr that return Command

Modifier and Type	Method	Description
Command	Parser.parseCommand()	Parses the next text in the source as a SMT-LIB command; if an error occurs, the error is logged and the method skips through a matching number of right parentheses