Package org.smtlib.impl

Class SMTExpr

java.lang.Object

org.smtlib.impl.SMTExpr

All Implemented Interfaces:

IAttributeValue, IExpr, INode, IPos.IPosable, IResponse

public abstract class SMTExpr
extends Object
implements IExpr

This class defines a number of subclasses that implement the SMT-LIB abstract AST; they are used by commands and expressions.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	SMTExpr.AsIdentifier	This class represents an SMT as-identifier AST
static class	SMTExpr.Attribute<TT extends IAttributeValue>	Represents an SMT-LIB attribute: a keyword optionally paired with a value.
static class	SMTExpr.AttributedExpr	Represents an SMT-LIB attributed expression ((! expr attrs...)).
static class	SMTExpr.BinaryLiteral	Represents an SMT-LIB binary literal (e.g.
static class	SMTExpr.Binding	Represents a let-binding: a symbol bound to an expression.
static class	SMTExpr.Constructor	Represents a constructor declaration within a datatype, consisting of a name and a list of selectors.
static class	SMTExpr.Datatype	Represents a datatype body: a list of constructors and (for parametric forms) a list of sort parameter symbols.
static class	SMTExpr.Decimal	This class represents an SMT Decimal literal expression or syntax token
static class	SMTExpr.Declaration	Represents a sorted variable declaration (parameter name and its sort), used in forall/exists/define-fun.
static class	SMTExpr.Error	Represents an expression-level error node inserted during parsing to allow error recovery.
static class	SMTExpr.Exists	Represents an SMT-LIB existential quantifier expression.
static class	SMTExpr.FcnExpr	Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
static class	SMTExpr.Forall	Represents an SMT-LIB universal quantifier expression.
static class	SMTExpr.FunctionDeclaration	Represents a function declaration header (name, sorted parameters, result sort), used in define-funs-rec.
static class	SMTExpr.HexLiteral	Represents an SMT-LIB hex literal (e.g.
static class	SMTExpr.Keyword	This class represents an SMT Keyword syntax token
static class	SMTExpr.Lambda	Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
static class	SMTExpr.Let	Represents an SMT-LIB let expression: a list of bindings and a body expression.
static class	SMTExpr.Literal<T>	Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
static class	SMTExpr.Logic
static class	SMTExpr.Match	Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
static class	SMTExpr.MatchCase	Represents a single case in a match expression: a pattern and its result body.
static class	SMTExpr.Numeral	This class represents an SMT Numeral expression or syntax token
static class	SMTExpr.ParameterizedIdentifier	This class represents an SMT parameterized-identifier AST (e.g.
static class	SMTExpr.Pattern	Represents a match pattern: a constructor name applied to zero or more variable symbols.
static class	SMTExpr.PatternTerms	Represents the value of a :pattern attribute: a list of trigger terms.
static class	SMTExpr.Selector	Represents a selector declaration within a datatype constructor.
static class	SMTExpr.SortDeclaration	Represents a sort declaration (symbol and arity) used in declare-datatype and declare-datatypes.
static class	SMTExpr.StringLiteral	This class represents an SMT String literal expression or syntax token
static class	SMTExpr.Symbol	This class represents an SMT Symbol
static class	SMTExpr.Theory

Nested classes/interfaces inherited from interface org.smtlib.IExpr

IExpr.IAsIdentifier, IExpr.IAttribute<TT extends IAttributeValue>, IExpr.IAttributedExpr, IExpr.IBinaryLiteral, IExpr.IBinding, IExpr.IConstructor, IExpr.IDecimal, IExpr.IDeclaration, IExpr.IError, IExpr.IExists, IExpr.IFactory, IExpr.IFcnExpr, IExpr.IForall, IExpr.IFunctionDeclaration, IExpr.IHexLiteral, IExpr.IIdentifier, IExpr.IIndex, IExpr.IKeyword, IExpr.ILambda, IExpr.ILet, IExpr.ILiteral, IExpr.IMatch, IExpr.IMatchCase, IExpr.INumeral, IExpr.IParameterizedIdentifier, IExpr.IPattern, IExpr.IPatternTerms, IExpr.IQualifiedIdentifier, IExpr.ISelector, IExpr.ISortDeclaration, IExpr.IStringLiteral, IExpr.ISymbol

Nested classes/interfaces inherited from interface org.smtlib.IResponse

IResponse.IAssertionsResponse, IResponse.IAssignmentResponse, IResponse.IAttributeList, IResponse.IPair<T1,T2>, IResponse.IProofResponse, IResponse.IUnsatAssumptionsResponse, IResponse.IUnsatCoreResponse, IResponse.IValueResponse

Constructor Summary

Constructors

Constructor	Description
SMTExpr()

Method Summary

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.smtlib.IAttributeValue

isOK

Methods inherited from interface org.smtlib.IExpr

isError, setSort, sort

Methods inherited from interface org.smtlib.INode

accept

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Constructor Details

SMTExpr

public SMTExpr()