Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

D

datatype - Variable in class org.smtlib.command.C_declare_datatype

datatype() - Method in class org.smtlib.command.C_declare_datatype

datatype() - Method in interface org.smtlib.ICommand.Ideclare_datatype

Returns the datatype body.

datatype(List<IExpr.IConstructor>, List<IExpr.ISymbol>) - Method in interface org.smtlib.IExpr.IFactory

Creates a datatype declaration; symbols is non-null only for parametric (par) forms.

datatype(List<IExpr.IConstructor>, List<IExpr.ISymbol>) - Method in class org.smtlib.impl.Factory

Datatype(List<IExpr.IConstructor>, List<IExpr.ISymbol>) - Constructor for class org.smtlib.impl.SMTExpr.Datatype

Creates a datatype body; symbols is non-null only for parametric (par) forms.

datatypeConstructors(IExpr.IIdentifier) - Method in class org.smtlib.SymbolTable

The constructors of the datatype sort with the given identifier, or null if no datatype of that name is in scope.

datatypes - Variable in class org.smtlib.command.C_declare_datatypes

The datatype declarations, parallel to sortDeclarations

datatypes() - Method in class org.smtlib.command.C_declare_datatypes

datatypes() - Method in interface org.smtlib.ICommand.Ideclare_datatypes

Returns the list of datatype bodies, parallel to ICommand.Ideclare_datatypes.sortDeclarations().

DATATYPES - Enum constant in enum class org.smtlib.SolverCapabilities.Capability

decimal(String) - Method in interface org.smtlib.IExpr.IFactory

Creates an IDecimal object; the argument must be a string of digits with just one decimal point.

decimal(String) - Method in class org.smtlib.impl.Factory

Decimal(BigDecimal) - Constructor for class org.smtlib.impl.SMTExpr.Decimal

Creates a Decimal literal with the given value.

DECIMAL - Static variable in class org.smtlib.sexpr.Utils

Concrete syntax for the special DECIMAL token

declaration(IExpr.ISymbol, ISort) - Method in interface org.smtlib.IExpr.IFactory

Creates a parameter declaration.

declaration(IExpr.ISymbol, ISort) - Method in class org.smtlib.impl.Factory

Declaration(IExpr.ISymbol, ISort) - Constructor for class org.smtlib.impl.SMTExpr.Declaration

Creates a declaration binding the given symbol to the given sort.

declarations - Variable in class org.smtlib.command.C_define_funs_rec

The list of function declarations (name, parameters, result sort)

declarations() - Method in class org.smtlib.command.C_define_funs_rec

declarations() - Method in interface org.smtlib.ICommand.Idefine_funs_rec

Returns the list of function declarations.

declare_const(ICommand.Ideclare_const) - Method in class org.smtlib.AbstractSolver

declare_const(ICommand.Ideclare_const) - Method in interface org.smtlib.ISolver

Declares a new uninterpreted constant; returns success or an SMT error response

declare_const(ICommand.Ideclare_const) - Method in class org.smtlib.solvers.Solver_simplify

See Solver_test.declare_const(ICommand.Ideclare_const).

declare_const(ICommand.Ideclare_const) - Method in class org.smtlib.solvers.Solver_test

declare_const(ICommand.Ideclare_const) - Method in class org.smtlib.solvers.Solver_z3_4_3

declare_const(IExpr.ISymbol, ISort) - Method in interface org.smtlib.ICommand.IFactory

Creates a declare-const command object.

declare_const(IExpr.ISymbol, ISort) - Method in class org.smtlib.impl.Factory

declare_datatype(ICommand.Ideclare_datatype) - Method in class org.smtlib.AbstractSolver

declare_datatype(ICommand.Ideclare_datatype) - Method in interface org.smtlib.ISolver

Declares a new datatype sort; returns success or an SMT error response

declare_datatype(ICommand.Ideclare_datatype) - Method in class org.smtlib.solvers.Solver_bitwuzla

Not sent: Bitwuzla exits on it (see above)

declare_datatype(ICommand.Ideclare_datatype) - Method in class org.smtlib.solvers.Solver_simplify

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.

declare_datatype(ICommand.Ideclare_datatype) - Method in class org.smtlib.solvers.Solver_test

declare_datatype(IExpr.ISortDeclaration, ISort.IDatatype) - Method in interface org.smtlib.ICommand.IFactory

Creates a declare-datatype command object.

declare_datatype(IExpr.ISortDeclaration, ISort.IDatatype) - Method in class org.smtlib.impl.Factory

DECLARE_DATATYPE - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

declare_datatypes(List<IExpr.ISortDeclaration>, List<ISort.IDatatype>) - Method in interface org.smtlib.ICommand.IFactory

Creates a declare-datatypes command object.

declare_datatypes(List<IExpr.ISortDeclaration>, List<ISort.IDatatype>) - Method in class org.smtlib.impl.Factory

declare_datatypes(ICommand.Ideclare_datatypes) - Method in class org.smtlib.AbstractSolver

declare_datatypes(ICommand.Ideclare_datatypes) - Method in interface org.smtlib.ISolver

Declares mutually recursive datatype sorts; returns success or an SMT error response

declare_datatypes(ICommand.Ideclare_datatypes) - Method in class org.smtlib.solvers.Solver_bitwuzla

Not sent: Bitwuzla exits on it (see above)

declare_datatypes(ICommand.Ideclare_datatypes) - Method in class org.smtlib.solvers.Solver_simplify

See Solver_simplify.declare_datatype(org.smtlib.ICommand.Ideclare_datatype).

declare_datatypes(ICommand.Ideclare_datatypes) - Method in class org.smtlib.solvers.Solver_test

declare_fun(ICommand.Ideclare_fun) - Method in class org.smtlib.AbstractSolver

declare_fun(ICommand.Ideclare_fun) - Method in interface org.smtlib.ISolver

Declares a new uninterpreted function (or constant); returns success or an SMT error response

declare_fun(ICommand.Ideclare_fun) - Method in class org.smtlib.solvers.Solver_simplify

declare_fun(ICommand.Ideclare_fun) - Method in class org.smtlib.solvers.Solver_test

declare_fun(ICommand.Ideclare_fun) - Method in class org.smtlib.solvers.Solver_z3_4_3

declare_fun(IExpr.ISymbol, List<ISort>, ISort) - Method in interface org.smtlib.ICommand.IFactory

Creates a declare-fun command object.

declare_fun(IExpr.ISymbol, List<ISort>, ISort) - Method in class org.smtlib.impl.Factory

DECLARE_FUN - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

declare_sort(ICommand.Ideclare_sort) - Method in class org.smtlib.AbstractSolver

declare_sort(ICommand.Ideclare_sort) - Method in interface org.smtlib.ISolver

Declares a new uninterpreted sort; returns success or an SMT error response

declare_sort(ICommand.Ideclare_sort) - Method in class org.smtlib.solvers.Solver_simplify

See Solver_test.declare_sort(ICommand.Ideclare_sort).

declare_sort(ICommand.Ideclare_sort) - Method in class org.smtlib.solvers.Solver_test

declare_sort(ICommand.Ideclare_sort) - Method in class org.smtlib.solvers.Solver_z3_4_3

declare_sort(IExpr.ISymbol, IExpr.INumeral) - Method in interface org.smtlib.ICommand.IFactory

Creates a declare-sort command object.

declare_sort(IExpr.ISymbol, IExpr.INumeral) - Method in class org.smtlib.impl.Factory

DECLARE_SORT - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

declare_sort_parameter(ICommand.Ideclare_sort_parameter) - Method in class org.smtlib.AbstractSolver

declare_sort_parameter(ICommand.Ideclare_sort_parameter) - Method in interface org.smtlib.ISolver

Declares a new sort parameter (polymorphic sort variable); returns success or an SMT error response

declare_sort_parameter(ICommand.Ideclare_sort_parameter) - Method in class org.smtlib.solvers.Solver_bitwuzla

Not sent: Bitwuzla exits on it (see above)

declare_sort_parameter(ICommand.Ideclare_sort_parameter) - Method in class org.smtlib.solvers.Solver_simplify

See Solver_test.declare_sort_parameter(ICommand.Ideclare_sort_parameter).

declare_sort_parameter(ICommand.Ideclare_sort_parameter) - Method in class org.smtlib.solvers.Solver_test

declare_sort_parameter(IExpr.ISymbol) - Method in interface org.smtlib.ICommand.IFactory

Creates a declare-sort-parameter command object.

declare_sort_parameter(IExpr.ISymbol) - Method in class org.smtlib.impl.Factory

DECLARE_SORT_PARAMETER - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

defaultPrinter - Variable in class org.smtlib.SMT.Configuration

The default printer used to convert AST objects to strings for output.

defaults - Variable in class org.smtlib.Utils

The set of default values for all standard options

define_const(ICommand.Idefine_const) - Method in class org.smtlib.AbstractSolver

define_const(ICommand.Idefine_const) - Method in interface org.smtlib.ISolver

Defines a named constant — syntactic sugar for define-fun with no parameters; returns success or an SMT error response

define_const(ICommand.Idefine_const) - Method in class org.smtlib.solvers.Solver_simplify

See Solver_test.define_const(ICommand.Idefine_const).

define_const(ICommand.Idefine_const) - Method in class org.smtlib.solvers.Solver_test

define_const(IExpr.ISymbol, ISort, IExpr) - Method in interface org.smtlib.ICommand.IFactory

Creates a define-const command object.

define_const(IExpr.ISymbol, ISort, IExpr) - Method in class org.smtlib.impl.Factory

define_fun(ICommand.Idefine_fun) - Method in class org.smtlib.AbstractSolver

define_fun(ICommand.Idefine_fun) - Method in interface org.smtlib.ISolver

Defines a named function or constant; returns success or an SMT error response

define_fun(ICommand.Idefine_fun) - Method in class org.smtlib.solvers.Solver_simplify

define_fun(ICommand.Idefine_fun) - Method in class org.smtlib.solvers.Solver_test

define_fun(ICommand.Idefine_fun) - Method in class org.smtlib.solvers.Solver_z3_4_3

define_fun(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort, IExpr) - Method in interface org.smtlib.ICommand.IFactory

Creates a define-fun command object.

define_fun(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort, IExpr) - Method in class org.smtlib.impl.Factory

DEFINE_FUN - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

define_fun_rec(ICommand.Idefine_fun_rec) - Method in class org.smtlib.AbstractSolver

define_fun_rec(ICommand.Idefine_fun_rec) - Method in interface org.smtlib.ISolver

Defines a named recursive function; returns success or an SMT error response

define_fun_rec(ICommand.Idefine_fun_rec) - Method in class org.smtlib.solvers.Solver_bitwuzla

Not sent: Bitwuzla exits on it (see above)

define_fun_rec(ICommand.Idefine_fun_rec) - Method in class org.smtlib.solvers.Solver_simplify

Recursive function definitions postdate Simplify (added in SMT-LIB 2.6) and its axiom-based translation (see Solver_simplify.define_fun(org.smtlib.ICommand.Idefine_fun)/Solver_simplify.declare_fun(org.smtlib.ICommand.Ideclare_fun)) has no way to express recursion.

define_fun_rec(ICommand.Idefine_fun_rec) - Method in class org.smtlib.solvers.Solver_test

define_fun_rec(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort, IExpr) - Method in interface org.smtlib.ICommand.IFactory

Creates a define-fun-rec command object.

define_fun_rec(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort, IExpr) - Method in class org.smtlib.impl.Factory

DEFINE_FUN_REC - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

define_funs_rec(List<IExpr.IFunctionDeclaration>, List<IExpr>) - Method in interface org.smtlib.ICommand.IFactory

Creates a define-funs-rec command object.

define_funs_rec(List<IExpr.IFunctionDeclaration>, List<IExpr>) - Method in class org.smtlib.impl.Factory

define_funs_rec(ICommand.Idefine_funs_rec) - Method in class org.smtlib.AbstractSolver

define_funs_rec(ICommand.Idefine_funs_rec) - Method in interface org.smtlib.ISolver

Defines a group of mutually recursive functions; returns success or an SMT error response

define_funs_rec(ICommand.Idefine_funs_rec) - Method in class org.smtlib.solvers.Solver_bitwuzla

Not sent: Bitwuzla exits on it (see above)

define_funs_rec(ICommand.Idefine_funs_rec) - Method in class org.smtlib.solvers.Solver_simplify

See Solver_simplify.define_fun_rec(org.smtlib.ICommand.Idefine_fun_rec).

define_funs_rec(ICommand.Idefine_funs_rec) - Method in class org.smtlib.solvers.Solver_test

define_sort(ICommand.Idefine_sort) - Method in class org.smtlib.AbstractSolver

define_sort(ICommand.Idefine_sort) - Method in interface org.smtlib.ISolver

Defines a sort abbreviation; returns success or an SMT error response

define_sort(ICommand.Idefine_sort) - Method in class org.smtlib.solvers.Solver_simplify

See Solver_test.define_sort(ICommand.Idefine_sort).

define_sort(ICommand.Idefine_sort) - Method in class org.smtlib.solvers.Solver_test

define_sort(ICommand.Idefine_sort) - Method in class org.smtlib.solvers.Solver_z3_4_3

define_sort(IExpr.ISymbol, List<ISort.IParameter>, ISort) - Method in interface org.smtlib.ICommand.IFactory

Creates a define-sort command object.

define_sort(IExpr.ISymbol, List<ISort.IParameter>, ISort) - Method in class org.smtlib.impl.Factory

DEFINE_SORT - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

definition - Variable in class org.smtlib.impl.Sort.Application

Reference to definition; filled in during type-checking

definition - Variable in class org.smtlib.SymbolTable.Entry

The definition of the symbol, if any

definition() - Method in class org.smtlib.impl.Sort.Application

definition() - Method in interface org.smtlib.ISort.IApplication

The definition of the family identifier, valid after the sort expression has been type-checked.

definition(ISort.IDefinition) - Method in class org.smtlib.impl.Sort.Application

definition(ISort.IDefinition) - Method in interface org.smtlib.ISort.IApplication

Sets and returns the value of definition() for this object to the value that is the argument

diag - Variable in class org.smtlib.SMT.Configuration

If non-null, the file name (or 'stdout'/'stderr') to use for diagnostic output.

DIAGNOSTIC_OUTPUT_CHANNEL - Static variable in class org.smtlib.Utils

The string designating an option item

DifferenceLogic - Class in org.smtlib.logic

Common base for the difference logics QF_IDL and QF_RDL.

DifferenceLogic(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.DifferenceLogic

discardErrorOutput - Variable in class org.smtlib.SolverProcess

Set before start() by an adapter whose solver writes only diagnostics to stderr, to discard them

discardHeld() - Method in class org.smtlib.Log

Discards held output, e.g.

DISTINCT - Static variable in class org.smtlib.Utils

DIV - Static variable in class org.smtlib.Utils

doParser(IParser) - Method in class org.smtlib.SMT

doParser(IParser, boolean) - Method in class org.smtlib.SMT

Driver - Class in org.smtlib

The Driver class is a client that can send commands to the SMT application acting as a server.

Driver() - Constructor for class org.smtlib.Driver

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form