Package org.smtlib

Interface IExpr.IFactory

All Known Implementing Classes:

Factory

Enclosing interface:

IExpr

public static interface IExpr.IFactory

The interface defining the factory type for producing objects of various subtypes of IExpr; the IPos argument is an optional argument giving information about the textual position of an expression.

Method Summary

Modifier and Type	Method	Description
IExpr.IAttribute<?>	attribute(IExpr.IKeyword k)	Creates an attribute with just a keyword and no attribute value.
<T extends IAttributeValue> IExpr.IAttribute<T>	attribute(IExpr.IKeyword k, T value)	Creates an attribute with a keyword and a value.
IExpr.IAttributedExpr	attributedExpr(IExpr e, List<IExpr.IAttribute<?>> attributes)	Creates an attributed expression (an expression with a positive number of attributes).
<T extends IAttributeValue> IExpr.IAttributedExpr	attributedExpr(IExpr e, IExpr.IKeyword key, T value)	Creates an attributed expression with just one attribute.
IExpr.IBinaryLiteral	binary(String v)	Creates an IBinaryLiteral from a string of 0 and 1 digits.
IExpr.IBinding	binding(IExpr.ISymbol symbol, IExpr expr)	Creates a binding for a Let expression.
IExpr.IConstructor	constructor(IExpr.ISymbol symbol, List<IExpr.ISelector> selectors)	Creates a constructor declaration.
ISort.IDatatype	datatype(List<IExpr.IConstructor> constructors, List<IExpr.ISymbol> symbols)	Creates a datatype declaration; symbols is non-null only for parametric (par) forms.
IExpr.IDecimal	decimal(String v)	Creates an IDecimal object; the argument must be a string of digits with just one decimal point.
IExpr.IDeclaration	declaration(IExpr.ISymbol symbol, ISort sort)	Creates a parameter declaration.
IExpr.IError	error(String text)	Creates an error expression.
IExpr.IExists	exists(List<IExpr.IDeclaration> params, IExpr e)	Creates an Exists expression.
IExpr.IExists	exists(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)	Creates an Exists expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
IExpr.IFcnExpr	fcn(IExpr.IQualifiedIdentifier id, List<IExpr> args)	Creates a function expression (perhaps with an empty argument list).
IExpr.IFcnExpr	fcn(IExpr.IQualifiedIdentifier id, IExpr... args)	Creates a function expression (perhaps with an empty argument list).
IExpr.IForall	forall(List<IExpr.IDeclaration> params, IExpr e)	Creates a Forall expression.
IExpr.IForall	forall(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)	Creates a Forall expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
IExpr.IFunctionDeclaration	functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration (used in define-funs-rec).
IExpr.IHexLiteral	hex(String v)	Creates an IHexLiteral object from a string of hex digits (either case).
IExpr.IAsIdentifier	id(IExpr.IIdentifier identifier, ISort qualifier)	Creates an 'as' identifier from an identifier and a sort qualifier.
IExpr.IParameterizedIdentifier	id(IExpr.ISymbol symbol, List<IExpr.IIndex> indices)	Creates a parameterized identifier from a symbol and a non-empty list of indices (each INumeral or ISymbol).
IExpr.IKeyword	keyword(String v)	Creates an IKeyword object from a canonical string representation.
IExpr.ILambda	lambda(List<IExpr.IDeclaration> params, IExpr e)	Creates a Lambda expression (SMT-LIB 2.7ff, HO-Core theory).
IExpr.ILet	let(List<IExpr.IBinding> bindings, IExpr e)	Creates a Let expression.
IExpr.IMatch	match(IExpr expr, List<IExpr.IMatchCase> cases)	Creates a match expression.
IExpr.IMatchCase	matchCase(IExpr.IPattern pattern, IExpr body)	Creates a single match case.
IExpr.INumeral	numeral(long v)	Creates an INumeral object; the argument must be non-negative.
IExpr.INumeral	numeral(String v)	Creates an INumeral object; the argument must be a string of digits.
IExpr.IPattern	pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)	Creates a match pattern.
IExpr.IPatternTerms	patternTerms(List<IExpr> terms)	Creates the value of a :pattern attribute: the given terms as one (multi-)pattern.
IExpr.IStringLiteral	quotedString(String v)	Creates an IStringLiteral from a string that is SMT-LIB escaped with enclosing quotes.
IExpr.ISelector	selector(IExpr.ISymbol symbol, ISort sort)	Creates a selector declaration.
IExpr.ISortDeclaration	sortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)	Creates a sort declaration (symbol + arity) for use in declare-datatype(s).
IExpr.ISymbol	symbol(String v)	Creates an ISymbol object from a canonical String representation of the symbol.
IExpr.IStringLiteral	unquotedString(String v)	Creates an IStringLiteral from a pure character string with no SMT-LIB escapes or enclosing quotes.

Method Details

numeral

IExpr.INumeral numeral(String v)

Creates an INumeral object; the argument must be a string of digits.

numeral

IExpr.INumeral numeral(long v)

Creates an INumeral object; the argument must be non-negative.

decimal

IExpr.IDecimal decimal(String v)

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

unquotedString

IExpr.IStringLiteral unquotedString(String v)

Creates an IStringLiteral from a pure character string with no SMT-LIB escapes or enclosing quotes.

quotedString

IExpr.IStringLiteral quotedString(String v)

Creates an IStringLiteral from a string that is SMT-LIB escaped with enclosing quotes.

keyword

IExpr.IKeyword keyword(String v)

Creates an IKeyword object from a canonical string representation.

binary

IExpr.IBinaryLiteral binary(String v)

Creates an IBinaryLiteral from a string of 0 and 1 digits.

hex

IExpr.IHexLiteral hex(String v)

Creates an IHexLiteral object from a string of hex digits (either case).

symbol

IExpr.ISymbol symbol(String v)

Creates an ISymbol object from a canonical String representation of the symbol.

attribute

IExpr.IAttribute<?> attribute(IExpr.IKeyword k)

Creates an attribute with just a keyword and no attribute value.

attribute

<T extends IAttributeValue> IExpr.IAttribute<T> attribute(IExpr.IKeyword k,
 T value)

Creates an attribute with a keyword and a value.

attributedExpr

IExpr.IAttributedExpr attributedExpr(IExpr e,
 List<IExpr.IAttribute<?>> attributes)

Creates an attributed expression (an expression with a positive number of attributes).

attributedExpr

<T extends IAttributeValue> IExpr.IAttributedExpr attributedExpr(IExpr e,
 IExpr.IKeyword key,
 T value)

Creates an attributed expression with just one attribute.

patternTerms

IExpr.IPatternTerms patternTerms(List<IExpr> terms)

Creates the value of a :pattern attribute: the given terms as one (multi-)pattern.

fcn

IExpr.IFcnExpr fcn(IExpr.IQualifiedIdentifier id,
 List<IExpr> args)

Creates a function expression (perhaps with an empty argument list).

fcn

IExpr.IFcnExpr fcn(IExpr.IQualifiedIdentifier id,
 IExpr... args)

Creates a function expression (perhaps with an empty argument list).

id

IExpr.IParameterizedIdentifier id(IExpr.ISymbol symbol,
 List<IExpr.IIndex> indices)

Creates a parameterized identifier from a symbol and a non-empty list of indices (each INumeral or ISymbol).

id

IExpr.IAsIdentifier id(IExpr.IIdentifier identifier,
 ISort qualifier)

Creates an 'as' identifier from an identifier and a sort qualifier.

let

IExpr.ILet let(List<IExpr.IBinding> bindings,
 IExpr e)

Creates a Let expression.

binding

IExpr.IBinding binding(IExpr.ISymbol symbol,
 IExpr expr)

Creates a binding for a Let expression.

declaration

IExpr.IDeclaration declaration(IExpr.ISymbol symbol,
 ISort sort)

Creates a parameter declaration.

forall

IExpr.IForall forall(List<IExpr.IDeclaration> params,
 IExpr e)

Creates a Forall expression.

forall

IExpr.IForall forall(List<IExpr.IDeclaration> params,
 IExpr e,
 List<IExpr> patterns)

Creates a Forall expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).

exists

IExpr.IExists exists(List<IExpr.IDeclaration> params,
 IExpr e)

Creates an Exists expression.

exists

IExpr.IExists exists(List<IExpr.IDeclaration> params,
 IExpr e,
 List<IExpr> patterns)

Creates an Exists expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).

lambda

IExpr.ILambda lambda(List<IExpr.IDeclaration> params,
 IExpr e)

Creates a Lambda expression (SMT-LIB 2.7ff, HO-Core theory).

error

IExpr.IError error(String text)

Creates an error expression.

sortDeclaration

IExpr.ISortDeclaration sortDeclaration(IExpr.ISymbol symbol,
 IExpr.INumeral arity)

Creates a sort declaration (symbol + arity) for use in declare-datatype(s).

selector

IExpr.ISelector selector(IExpr.ISymbol symbol,
 ISort sort)

Creates a selector declaration.

constructor

IExpr.IConstructor constructor(IExpr.ISymbol symbol,
 List<IExpr.ISelector> selectors)

Creates a constructor declaration.

datatype

ISort.IDatatype datatype(List<IExpr.IConstructor> constructors,
 List<IExpr.ISymbol> symbols)

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

functionDeclaration

IExpr.IFunctionDeclaration functionDeclaration(IExpr.ISymbol symbol,
 List<IExpr.IDeclaration> parameters,
 ISort sort)

Creates a function declaration (used in define-funs-rec).

pattern

IExpr.IPattern pattern(IExpr.ISymbol constructor,
 List<IExpr.ISymbol> params)

Creates a match pattern.

matchCase

IExpr.IMatchCase matchCase(IExpr.IPattern pattern,
 IExpr body)

Creates a single match case.

match

IExpr.IMatch match(IExpr expr,
 List<IExpr.IMatchCase> cases)

Creates a match expression.