Package org.smtlib

Interface ICommand

All Superinterfaces:

INode, IPos.IPosable

All Known Subinterfaces:

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.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.Iset_info, ICommand.Iset_logic, ICommand.Iset_option, Iexec, Iwhat

All Known Implementing Classes:

C_assert, C_check_sat, C_check_sat_assuming, C_comment, C_declare_const, C_declare_datatype, C_declare_datatypes, C_declare_fun, C_declare_sort, C_declare_sort_parameter, C_define_const, C_define_fun, C_define_fun_rec, 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, Command

public interface ICommand
extends INode, IPos.IPosable

This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.

Author:

David R. Cok

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static interface	ICommand.Iassert	Interface for the SMT-LIB assert command.
static interface	ICommand.Icheck_sat	Interface for the SMT-LIB check-sat command.
static interface	ICommand.Icheck_sat_assuming	Interface for the SMT-LIB check-sat-assuming command.
static interface	ICommand.Icomment	Interface for a comment pseudo-command: not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand (see issue #115) so that every dispatch path -- execution, typed-visitor traversal, and printing -- treats it uniformly with every other command, rather than falling back on IVisitor's generic visit(ICommand) handling (a reflection-based lookup in Printer's case).
static interface	ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
static interface	ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
static interface	ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
static interface	ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
static interface	ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
static interface	ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
static interface	ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
static interface	ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
static interface	ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
static interface	ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
static interface	ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
static interface	ICommand.Iecho	Interface for the SMT-LIB echo command.
static interface	ICommand.Iexit	Interface for the SMT-LIB exit command.
static interface	ICommand.IFactory	This is the interface to be used by a concrete ICommand factory.
static interface	ICommand.IFinder	This interface defines classes that implement techniques for mapping a command name to a class that implements that command.
static interface	ICommand.Iget_assertions	Interface for the SMT-LIB get-assertions command.
static interface	ICommand.Iget_assignment	Interface for the SMT-LIB get-assignment command.
static interface	ICommand.Iget_info	Interface for the SMT-LIB get-info command.
static interface	ICommand.Iget_model	Interface for the SMT-LIB get-model command (non-standard extension).
static interface	ICommand.Iget_option	Interface for the SMT-LIB get-option command.
static interface	ICommand.Iget_proof	Interface for the SMT-LIB get-proof command.
static interface	ICommand.Iget_unsat_assumptions	Interface for the SMT-LIB get-unsat-assumptions command.
static interface	ICommand.Iget_unsat_core	Interface for the SMT-LIB get-unsat-core command.
static interface	ICommand.Iget_value	Interface for the SMT-LIB get-value command.
static interface	ICommand.Ipop	Interface for the SMT-LIB pop command.
static interface	ICommand.Ipush	Interface for the SMT-LIB push command.
static interface	ICommand.Ireset	Interface for the SMT-LIB reset command.
static interface	ICommand.Ireset_assertions	Interface for the SMT-LIB reset-assertions command.
static interface	ICommand.IScript	Interface to be implemented by all objects representing SMT-LIB scripts.
static interface	ICommand.Iset_info	Interface for the SMT-LIB set-info command.
static interface	ICommand.Iset_logic	Interface for the SMT-LIB set-logic command.
static interface	ICommand.Iset_option	Interface for the SMT-LIB set-option command.

Method Summary

Modifier and Type	Method	Description
String	commandName()	Returns the SMT-LIB name of this command (e.g.
IResponse	execute(ISolver solver)	Executes the command on the given solver; presumes that the command type-checked successfully.

Methods inherited from interface org.smtlib.INode

accept

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Method Details

commandName

String commandName()

Returns the SMT-LIB name of this command (e.g. "assert", "check-sat").

execute

IResponse execute(ISolver solver)

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

Parameters:

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

Returns:

the result of the command