Package org.smtlib.command

Class C_define_fun

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Command

org.smtlib.command.C_define_fun

All Implemented Interfaces:

ICommand, ICommand.Idefine_fun, INode, IPos.IPosable

Direct Known Subclasses:

C_define_const, C_define_fun_rec

public class C_define_fun
extends Command
implements ICommand.Idefine_fun

Implements the define-fun 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 List<IExpr.IDeclaration>	args	The sorts of the arguments of the function being defined
static final String	commandName	The command name
protected IExpr	expression	The defining expression for the function
protected IExpr.ISymbol	fcnName	The name of the function being defined
protected ISort	resultSort	The sort of the result

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_define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expr)	Constructs a command instance

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.
IExpr	expression()	The defining expression for the function
List<IExpr.IDeclaration>	parameters()	The sorts of the arguments of the function being defined
static C_define_fun	parse(Parser p)	Parses the command arguments and creates a command instance
ISort	resultSort()	The result sort
IExpr.ISymbol	symbol()	The name of the function being defined

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

fcnName

protected IExpr.ISymbol fcnName

The name of the function being defined

args

protected List<IExpr.IDeclaration> args

The sorts of the arguments of the function being defined

resultSort

protected ISort resultSort

The sort of the result

expression

protected IExpr expression

The defining expression for the function

Constructor Details

C_define_fun

public C_define_fun(IExpr.ISymbol id,
 List<IExpr.IDeclaration> declarations,
 ISort resultSort,
 IExpr expr)

Constructs a command instance

Method Details

commandName

public String commandName()

The command name

Specified by:

commandName in interface ICommand

Specified by:

commandName in class Command

symbol

public IExpr.ISymbol symbol()

The name of the function being defined

Specified by:

symbol in interface ICommand.Idefine_fun

parameters

public List<IExpr.IDeclaration> parameters()

The sorts of the arguments of the function being defined

Specified by:

parameters in interface ICommand.Idefine_fun

resultSort

public ISort resultSort()

The result sort

Specified by:

resultSort in interface ICommand.Idefine_fun

expression

public IExpr expression()

The defining expression for the function

Specified by:

expression in interface ICommand.Idefine_fun

parse

public static C_define_fun parse(Parser p)
                          throws IParser.ParserException

Parses the command arguments and creates a command instance

Throws:

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