Package org.smtlib.ext

Class C_what

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Command

org.smtlib.ext.C_what

All Implemented Interfaces:

Iwhat, ICommand, INode, IPos.IPosable

public class C_what
extends Command
implements Iwhat

Implements the non-standard what command. This command takes an arbitrary number of arguments, all Symbols, and prints the Sort of each one; if there are no arguments, the command prints all of the defined ids. FIXME - the output is not in SExpr form.

Author:

David R. Cok

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
static final String	commandName	The command name
protected List<IExpr.IIdentifier>	ids	The ids that are the arguments of the command

Fields inherited from class org.smtlib.impl.Command

trailingText

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

pos

Constructor Summary

Constructors

Constructor	Description
C_what(List<IExpr.IIdentifier> ids)	Constructs a command instance for the given identifiers.

Method Summary

Modifier and Type	Method	Description
<T> T	accept(IVisitor<T> v)	The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }
String	commandName()	The command name
IResponse	execute(ISolver solver)	Executes the command on the given solver; presumes that the command type-checked successfully.
List<IExpr.IIdentifier>	ids()	The ids that are the arguments of the command
static C_what	parse(Parser p)	Parses the input concrete S-expression syntax to produce a command instance
void	writeArgs(Printer p)	Writes the command arguments (everything between the opening parenthesis + command name and the closing parenthesis); called by Command.write(org.smtlib.sexpr.Printer).

Methods inherited from class org.smtlib.impl.Command

error, setTrailingText, trailingText, write

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.IPos.IPosable

pos, setPos

Field Details

commandName

public static final String commandName

The command name

See Also:

• Constant Field Values

ids

protected List<IExpr.IIdentifier> ids

The ids that are the arguments of the command

Constructor Details

C_what

public C_what(List<IExpr.IIdentifier> ids)

Constructs a command instance for the given identifiers.

Method Details

commandName

public String commandName()

The command name

Specified by:

commandName in interface ICommand

Specified by:

commandName in class Command

ids

public List<IExpr.IIdentifier> ids()

The ids that are the arguments of the command

Specified by:

ids in interface Iwhat

parse

public static C_what parse(Parser p)
                    throws IOException,
IParser.ParserException

Parses the input concrete S-expression syntax to produce a command instance

Throws:

IOException

IParser.ParserException

writeArgs

public void writeArgs(Printer p)
               throws IOException

Description copied from class: Command

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

Overrides:

writeArgs in class Command

Throws:

IOException

execute

public IResponse execute(ISolver solver)

Description copied from interface: ICommand

Executes the command on the given solver; presumes that the command type-checked successfully.

Specified by:

execute in interface ICommand

Parameters:

solver - the instance of the solver to use (note that solvers have state)

Returns:

the result of the command

accept

public <T> T accept(IVisitor<T> v)
             throws IVisitor.VisitorException

Description copied from interface: INode

The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }

Specified by:

accept in interface INode

Type Parameters:

T - the return type desired from the visit methods

Parameters:

v - the visitor class

Returns:

the value returned by the visit method

Throws:

IVisitor.VisitorException