Uses of Interface
org.smtlib.IExpr.INumeral

Packages that use IExpr.INumeral

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 IExpr.INumeral in org.smtlib

Methods in org.smtlib that return IExpr.INumeral

Modifier and Type	Method	Description
IExpr.INumeral	ICommand.Ideclare_sort.arity()	Returns the arity of the sort.
IExpr.INumeral	IExpr.ISortDeclaration.arity()
IExpr.INumeral	ISort.IFamily.arity()	The arity of the sort symbol
IExpr.INumeral	ICommand.Ipop.number()	Returns the number of scopes to pop.
IExpr.INumeral	ICommand.Ipush.number()	Returns the number of scopes to push.
IExpr.INumeral	IExpr.IFactory.numeral(long v)	Creates an INumeral object; the argument must be non-negative.
IExpr.INumeral	IExpr.IFactory.numeral(String v)	Creates an INumeral object; the argument must be a string of digits.
IExpr.INumeral	IParser.parseNumeral()	Parse an SMT-LIB numeral; return null and log an error response if there is no numeral

Methods in org.smtlib with parameters of type IExpr.INumeral

Modifier and Type	Method	Description
boolean	SymbolTable.addSortDefinition(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes, boolean global)	Adds a new sort family definition, with attributes (e.g.
ISort.IFamily	ISort.IFactory.createSortFamily(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)	Creates a sort family with the given identifier, arity, and attributes (null or empty if none).
ICommand.Ideclare_sort	ICommand.IFactory.declare_sort(IExpr.ISymbol sym, IExpr.INumeral arity)	Creates a declare-sort command object.
ICommand.Ipop	ICommand.IFactory.pop(IExpr.INumeral number)	Creates a pop command object.
ICommand.Ipush	ICommand.IFactory.push(IExpr.INumeral number)	Creates a push command object.
IExpr.ISortDeclaration	IExpr.IFactory.sortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)	Creates a sort declaration (symbol + arity) for use in declare-datatype(s).
T	IVisitor.TreeVisitor.visit(IExpr.INumeral e)
T	IVisitor.visit(IExpr.INumeral e)
ISort	TypeChecker.visit(IExpr.INumeral e)

Uses of IExpr.INumeral in org.smtlib.command

Fields in org.smtlib.command declared as IExpr.INumeral

Modifier and Type	Field	Description
protected IExpr.INumeral	C_declare_sort.arity	The arity of the sort symbol
protected IExpr.INumeral	C_pop.numeral	The (non-negative) number of stack frames to pop
protected IExpr.INumeral	C_push.numeral	The (non-negative) number of stack frames to push

Methods in org.smtlib.command that return IExpr.INumeral

Modifier and Type	Method	Description
IExpr.INumeral	C_declare_sort.arity()	The arity of the sort symbol
IExpr.INumeral	C_pop.number()	The number of assertion set stack items to pop
IExpr.INumeral	C_push.number()	Returns the number of assertion set scopes to push.

Constructors in org.smtlib.command with parameters of type IExpr.INumeral

Modifier	Constructor	Description
	C_declare_sort(IExpr.ISymbol id, IExpr.INumeral n)	Constructs a new command object
	C_pop(IExpr.INumeral n)	Constructs a command instance
	C_push(IExpr.INumeral n)	Constructs a command instance

Uses of IExpr.INumeral in org.smtlib.impl

Classes in org.smtlib.impl that implement IExpr.INumeral

Modifier and Type	Class	Description
static class	SMTExpr.Numeral	This class represents an SMT Numeral expression or syntax token

Fields in org.smtlib.impl declared as IExpr.INumeral

Modifier and Type	Field	Description
protected IExpr.INumeral	SMTExpr.SortDeclaration.arity
protected IExpr.INumeral	Sort.Family.arity

Methods in org.smtlib.impl that return IExpr.INumeral

Modifier and Type	Method	Description
IExpr.INumeral	SMTExpr.SortDeclaration.arity()
IExpr.INumeral	Sort.Family.arity()
IExpr.INumeral	Factory.numeral(String v)
IExpr.INumeral	Response.Factory.numericLiteral(int value)

Methods in org.smtlib.impl with parameters of type IExpr.INumeral

Modifier and Type	Method	Description
Sort.Family	Factory.createSortFamily(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)
ICommand.Ideclare_sort	Factory.declare_sort(IExpr.ISymbol s, IExpr.INumeral n)
ICommand.Ipop	Factory.pop(IExpr.INumeral n)
ICommand.Ipush	Factory.push(IExpr.INumeral n)
IExpr.ISortDeclaration	Factory.sortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)

Constructors in org.smtlib.impl with parameters of type IExpr.INumeral

Modifier	Constructor	Description
	Family(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)	Creates a sort family with the given identifier, arity, and attributes (null or empty if none).
	SortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)	Creates a sort declaration for the given sort name and arity.

Uses of IExpr.INumeral in org.smtlib.sexpr

Methods in org.smtlib.sexpr that return IExpr.INumeral

Modifier and Type	Method	Description
IExpr.INumeral	Parser.parseNumeral()	Parses a numeral, returning null with error messages if an error occurs; if the next token is not a numeral, the token is not consumed,

Methods in org.smtlib.sexpr with parameters of type IExpr.INumeral

Modifier and Type	Method	Description
Void	Printer.visit(IExpr.INumeral e)

Uses of IExpr.INumeral in org.smtlib.solvers

Methods in org.smtlib.solvers with parameters of type IExpr.INumeral

Modifier and Type	Method	Description
String	Solver_simplify.Translator.visit(IExpr.INumeral e)