Package org.smtlib.impl

Class Command

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Command

All Implemented Interfaces:

ICommand, INode, IPos.IPosable

Direct Known Subclasses:

C_assert, C_check_sat, C_check_sat_assuming, C_comment, C_declare_datatype, C_declare_datatypes, C_declare_fun, C_declare_sort, C_declare_sort_parameter, C_define_fun, C_define_funs_rec, C_define_sort, C_echo, C_exec, C_exit, C_get_assertions, C_get_assignment, C_get_info, C_get_model, C_get_option, C_get_proof, C_get_unsat_assumptions, C_get_unsat_core, C_get_value, C_pop, C_push, C_reset, C_reset_assertions, C_set_info, C_set_logic, C_set_option, C_what

public abstract class Command
extends Pos.Printable
implements ICommand

This abstract class is the base class for all commands within this implementation.

Nested Class Summary

Nested classes/interfaces inherited from interface org.smtlib.ICommand

ICommand.Iassert, ICommand.Icheck_sat, ICommand.Icheck_sat_assuming, ICommand.Icomment, ICommand.Ideclare_const, ICommand.Ideclare_datatype, ICommand.Ideclare_datatypes, ICommand.Ideclare_fun, ICommand.Ideclare_sort, ICommand.Ideclare_sort_parameter, ICommand.Idefine_const, ICommand.Idefine_fun, ICommand.Idefine_fun_rec, ICommand.Idefine_funs_rec, ICommand.Idefine_sort, ICommand.Iecho, ICommand.Iexit, ICommand.IFactory, ICommand.IFinder, ICommand.Iget_assertions, ICommand.Iget_assignment, ICommand.Iget_info, ICommand.Iget_model, ICommand.Iget_option, ICommand.Iget_proof, ICommand.Iget_unsat_assumptions, ICommand.Iget_unsat_core, ICommand.Iget_value, ICommand.Ipop, ICommand.Ipush, ICommand.Ireset, ICommand.Ireset_assertions, ICommand.IScript, ICommand.Iset_info, ICommand.Iset_logic, ICommand.Iset_option

Field Summary

Fields

Modifier and Type	Field	Description
protected String	trailingText	Whitespace/comment text, if any, that appeared on the same physical source line immediately after this command's closing parenthesis (before the next line terminator) -- typically a trailing "; comment".

Fields inherited from class org.smtlib.impl.Pos.Posable

pos

Constructor Summary

Constructors

Constructor	Description
Command()

Method Summary

Modifier and Type	Method	Description
abstract String	commandName()	The command name
static IParser.ParserException	error(SMT.Configuration smt, String msg, IPos pos)	Creates a ParserException with the given message and position.
void	setTrailingText(String text)	Sets the text captured in trailingText.
String	trailingText()	The text captured in trailingText, or null if this command has none.
void	write(Printer p)	Writes the full command: (commandName() <writeArgs output>), followed by its trailingText (if any) -- see trailingText.
void	writeArgs(Printer p)	Writes the command arguments (everything between the opening parenthesis + command name and the closing parenthesis); called by write(org.smtlib.sexpr.Printer).

Methods inherited from class org.smtlib.impl.Pos.Printable

toString

Methods inherited from class org.smtlib.impl.Pos.Posable

equals, hashCode, pos, setPos

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.smtlib.ICommand

execute

Methods inherited from interface org.smtlib.INode

accept

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Field Details

trailingText

protected String trailingText

Whitespace/comment text, if any, that appeared on the same physical source line immediately after this command's closing parenthesis (before the next line terminator) -- typically a trailing "; comment". Captured separately from a standalone comment (which parses as its own C_comment) so that sending this command to a solver stays exactly one real source line per one sent line, regardless of whether a trailing comment is present. Never forwarded to a solver (see AbstractSolver's command dispatch); printed back out here purely for round-trip/echo fidelity, since it was real text in the original source.

Constructor Details

Command

public Command()

Method Details

trailingText

public String trailingText()

The text captured in trailingText, or null if this command has none.

setTrailingText

public void setTrailingText(String text)

Sets the text captured in trailingText.

commandName

public abstract String commandName()

The command name

Specified by:

commandName in interface ICommand

writeArgs

public void writeArgs(Printer p)
               throws IOException,
IVisitor.VisitorException

Writes the command arguments (everything between the opening parenthesis + command name and the closing parenthesis); called by write(org.smtlib.sexpr.Printer). Extension commands override this; standard commands are printed via the visitor.

Throws:

IOException

IVisitor.VisitorException

write

public void write(Printer p)
           throws IOException,
IVisitor.VisitorException

Writes the full command: (commandName() <writeArgs output>), followed by its trailingText (if any) -- see trailingText.

Throws:

IOException

IVisitor.VisitorException

error

public static IParser.ParserException error(SMT.Configuration smt,
 String msg,
 IPos pos)

Creates a ParserException with the given message and position.