Package org.smtlib.command

Class C_declare_sort

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Command

org.smtlib.command.C_declare_sort

All Implemented Interfaces:

ICommand, ICommand.Ideclare_sort, INode, IPos.IPosable

public class C_declare_sort
extends Command
implements ICommand.Ideclare_sort

Implements the declare-sort command

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 IExpr.INumeral	arity	The arity of the sort symbol
static final String	commandName	The command name
protected IExpr.ISymbol	sortSymbol	The new sort symbol

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_declare_sort(IExpr.ISymbol id, IExpr.INumeral n)	Constructs a new command object

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); }
IExpr.INumeral	arity()	The arity of the sort symbol
String	commandName()	The command name
IResponse	execute(ISolver solver)	Executes the command on the given solver; presumes that the command type-checked successfully.
static C_declare_sort	parse(Parser p)	Parses the arguments of the command, producing a new command instance
IExpr.ISymbol	sortSymbol()	The sort symbol declared by this command

Methods inherited from class org.smtlib.impl.Command

error, setTrailingText, trailingText, write, writeArgs

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

sortSymbol

protected IExpr.ISymbol sortSymbol

The new sort symbol

arity

protected IExpr.INumeral arity

The arity of the sort symbol

Constructor Details

C_declare_sort

public C_declare_sort(IExpr.ISymbol id,
 IExpr.INumeral n)

Constructs a new command object

Method Details

commandName

public String commandName()

The command name

Specified by:

commandName in interface ICommand

Specified by:

commandName in class Command

arity

public IExpr.INumeral arity()

The arity of the sort symbol

Specified by:

arity in interface ICommand.Ideclare_sort

sortSymbol

public IExpr.ISymbol sortSymbol()

The sort symbol declared by this command

Specified by:

sortSymbol in interface ICommand.Ideclare_sort

parse

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

Parses the arguments of the command, producing a new command instance

Throws:

IOException

IParser.ParserException

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