Uses of Interface
org.smtlib.ICommand.Ideclare_const
Packages that use ICommand.Ideclare_const
Package
Description
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.
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.
This package is an implementation of the interfaces defined in org.smtlib.
This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
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_const in org.smtlib
Methods in org.smtlib that return ICommand.Ideclare_constModifier and TypeMethodDescriptionICommand.IFactory.declare_const(IExpr.ISymbol symbol, ISort resultSort) Creates a declare-const command object.Methods in org.smtlib with parameters of type ICommand.Ideclare_constModifier and TypeMethodDescriptionAbstractSolver.declare_const(ICommand.Ideclare_const cmd) ISolver.declare_const(ICommand.Ideclare_const cmd) Declares a new uninterpreted constant; returns success or an SMT error responseIVisitor.TreeVisitor.visit(ICommand.Ideclare_const e) default TIVisitor.visit(ICommand.Ideclare_const e) -
Uses of ICommand.Ideclare_const in org.smtlib.command
Classes in org.smtlib.command that implement ICommand.Ideclare_constModifier and TypeClassDescriptionclassImplements the declare-const command (syntactic sugar for declare-fun with no argument sorts) -
Uses of ICommand.Ideclare_const in org.smtlib.impl
Methods in org.smtlib.impl that return ICommand.Ideclare_const -
Uses of ICommand.Ideclare_const in org.smtlib.sexpr
Methods in org.smtlib.sexpr with parameters of type ICommand.Ideclare_const -
Uses of ICommand.Ideclare_const in org.smtlib.solvers
Methods in org.smtlib.solvers with parameters of type ICommand.Ideclare_constModifier and TypeMethodDescriptionSolver_simplify.declare_const(ICommand.Ideclare_const cmd) Solver_test.declare_const(ICommand.Ideclare_const cmd) Solver_z3_4_3.declare_const(ICommand.Ideclare_const cmd)