Uses of Interface
org.smtlib.ICommand.Ideclare_datatype

Packages that use ICommand.Ideclare_datatype

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
org.smtlib.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
org.smtlib.solvers	This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.

Uses of ICommand.Ideclare_datatype in org.smtlib

Methods in org.smtlib that return ICommand.Ideclare_datatype

Modifier and Type	Method	Description
ICommand.Ideclare_datatype	ICommand.IFactory.declare_datatype(IExpr.ISortDeclaration sd, ISort.IDatatype d)	Creates a declare-datatype command object.

Methods in org.smtlib with parameters of type ICommand.Ideclare_datatype

Modifier and Type	Method	Description
IResponse	AbstractSolver.declare_datatype(ICommand.Ideclare_datatype cmd)
IResponse	ISolver.declare_datatype(ICommand.Ideclare_datatype cmd)	Declares a new datatype sort; returns success or an SMT error response
T	IVisitor.TreeVisitor.visit(ICommand.Ideclare_datatype e)
default T	IVisitor.visit(ICommand.Ideclare_datatype e)

Uses of ICommand.Ideclare_datatype in org.smtlib.command

Classes in org.smtlib.command that implement ICommand.Ideclare_datatype

Modifier and Type	Class	Description
class	C_declare_datatype	Implements the declare-datatype command

Uses of ICommand.Ideclare_datatype in org.smtlib.impl

Methods in org.smtlib.impl that return ICommand.Ideclare_datatype

Modifier and Type	Method	Description
ICommand.Ideclare_datatype	Factory.declare_datatype(IExpr.ISortDeclaration sd, ISort.IDatatype d)

Uses of ICommand.Ideclare_datatype in org.smtlib.sexpr

Methods in org.smtlib.sexpr with parameters of type ICommand.Ideclare_datatype

Modifier and Type	Method	Description
Void	Printer.visit(ICommand.Ideclare_datatype e)

Uses of ICommand.Ideclare_datatype in org.smtlib.solvers

Methods in org.smtlib.solvers with parameters of type ICommand.Ideclare_datatype

Modifier and Type	Method	Description
IResponse	Solver_bitwuzla.declare_datatype(ICommand.Ideclare_datatype cmd)	Not sent: Bitwuzla exits on it (see above)
IResponse	Solver_simplify.declare_datatype(ICommand.Ideclare_datatype cmd)	Datatypes postdate Simplify (added in SMT-LIB 2.6) and its untyped translation (see the class javadoc: "Simplify has no type definitions") has no way to express a datatype's constructors/selectors.
IResponse	Solver_test.declare_datatype(ICommand.Ideclare_datatype cmd)