Package org.smtlib.impl

Class Factory

java.lang.Object

org.smtlib.impl.Factory

All Implemented Interfaces:

ICommand.IFactory, IExpr.IFactory, ISort.IFactory

public class Factory
extends Object
implements IExpr.IFactory, ISort.IFactory, ICommand.IFactory

Implements a factory for SMT-LIB expressions using the standard concrete syntax. Instances of these IExpr objects have an IPos element. The various factories are all implemented together in this one class because they use each other mutually; combining them lets them be overridden in a consistent fashion.

Field Summary

Fields

Modifier and Type	Field	Description
protected final SMT.Configuration	smtConfig	The configuration this factory's instances (e.g.

Constructor Summary

Constructors

Constructor	Description
Factory(SMT.Configuration smtConfig)

Method Summary

Modifier and Type	Method	Description
ICommand.Iassert	assertCommand(IExpr expr)	Creates an assert command object, asserting the given expression.
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.
ISort.IApplication	Bool()	Returns the Bool sort.
ICommand.Icheck_sat	check_sat()	Creates a check-sat command object.
ICommand.Icheck_sat_assuming	check_sat_assuming(List<IExpr> terms)	Creates a check-sat-assuming command object.
ICommand.Icomment	comment(String text)	Creates a comment pseudo-command object, carrying the given raw comment text (see ICommand.Icomment).
IExpr.IConstructor	constructor(IExpr.ISymbol symbol, List<IExpr.ISelector> selectors)	Creates a constructor declaration.
ISort.IErrorDefinition	createErrorDefinition(IExpr.IIdentifier id, String errorMessage, IPos pos)	Creates an error-placeholder definition (suppresses cascading errors).
Sort.FcnSort	createFcnSort(ISort[] args, ISort result)	Creates a function sort.
Sort.Abbreviation	createSortAbbreviation(IExpr.IIdentifier identifier, List<ISort.IParameter> params, ISort sortExpr)	Creates a new sort abbreviation.
Sort.Application	createSortExpression(IExpr.IIdentifier sortFamily, List<ISort> exprs)	Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
Sort.Application	createSortExpression(IExpr.IIdentifier sortFamily, ISort... exprs)	Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
Sort.Family	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).
Sort.Parameter	createSortParameter(IExpr.ISymbol symbol)	Creates a parameter for a parameterized sort abbreviation.
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.
ICommand.Ideclare_const	declare_const(IExpr.ISymbol s, ISort r)	Creates a declare-const command object.
ICommand.Ideclare_datatype	declare_datatype(IExpr.ISortDeclaration sd, ISort.IDatatype d)	Creates a declare-datatype command object.
ICommand.Ideclare_datatypes	declare_datatypes(List<IExpr.ISortDeclaration> sds, List<ISort.IDatatype> dts)	Creates a declare-datatypes command object.
ICommand.Ideclare_fun	declare_fun(IExpr.ISymbol id, List<ISort> args, ISort r)	Creates a declare-fun command object.
ICommand.Ideclare_sort	declare_sort(IExpr.ISymbol s, IExpr.INumeral n)	Creates a declare-sort command object.
ICommand.Ideclare_sort_parameter	declare_sort_parameter(IExpr.ISymbol s)	Creates a declare-sort-parameter command object.
ICommand.Idefine_const	define_const(IExpr.ISymbol s, ISort r, IExpr e)	Creates a define-const command object.
ICommand.Idefine_fun	define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> ps, ISort r, IExpr e)	Creates a define-fun command object.
ICommand.Idefine_fun_rec	define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> ps, ISort r, IExpr e)	Creates a define-fun-rec command object.
ICommand.Idefine_funs_rec	define_funs_rec(List<IExpr.IFunctionDeclaration> ds, List<IExpr> bs)	Creates a define-funs-rec command object.
ICommand.Idefine_sort	define_sort(IExpr.ISymbol id, List<ISort.IParameter> ps, ISort e)	Creates a define-sort command object.
ICommand.Iecho	echo(IExpr.IStringLiteral arg)	Creates an echo command object.
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).
ICommand.Iexit	exit()	Creates an exit command object.
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).
ICommand.Iget_assertions	get_assertions()	Creates a get-assertions command object.
ICommand.Iget_assignment	get_assignment()	Creates a get-assignment command object.
ICommand.Iget_info	get_info(IExpr.IKeyword k)	Creates a get-info command object.
ICommand.Iget_model	get_model()	Creates a get-model command object.
ICommand.Iget_option	get_option(IExpr.IKeyword k)	Creates a get-option command object.
ICommand.Iget_proof	get_proof()	Creates a get-proof command object.
ICommand.Iget_unsat_assumptions	get_unsat_assumptions()	Creates a get-unsat-assumptions command object.
ICommand.Iget_unsat_core	get_unsat_core()	Creates a get-unsat-core command object.
ICommand.Iget_value	get_value(List<IExpr> exprs)	Creates a get-value command object.
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).
static void	initFactories(SMT.Configuration config)	Initializes the SMT configuration object for the implementation in org.smtlib.impl - all the appropriate factories, etc.
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.
SMTExpr.Numeral	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.
ICommand.Ipop	pop(IExpr.INumeral n)	Creates a pop command object.
ICommand.Ipush	push(IExpr.INumeral n)	Creates a push command object.
IExpr.IStringLiteral	quotedString(String v)	Creates an IStringLiteral from a string that is SMT-LIB escaped with enclosing quotes.
ICommand.Ireset	reset()	Creates a reset command object.
ICommand.Ireset_assertions	reset_assertions()	Creates a reset-assertions command object.
ICommand.IScript	script()	Creates an empty script, with no filename and no commands, ready to have commands added via ICommand.IScript.add(ICommand).
ICommand.IScript	script(IExpr.IStringLiteral filename, List<ICommand> commands)	Creates a script object containing the given filename or the given set of commands.
IExpr.ISelector	selector(IExpr.ISymbol symbol, ISort sort)	Creates a selector declaration.
ICommand.Iset_info	set_info(IExpr.IKeyword k, IAttributeValue v)	Creates a set-info command object.
ICommand.Iset_logic	set_logic(IExpr.ISymbol s)	Creates a set-logic command object.
ICommand.Iset_option	set_option(IExpr.IKeyword k, IAttributeValue v)	Creates a set-option command object.
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.

Methods inherited from class java.lang.Object

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

Field Details

smtConfig

protected final SMT.Configuration smtConfig

The configuration this factory's instances (e.g. StringLiteral) are scoped to; see issue #22.

Constructor Details

Factory

public Factory(SMT.Configuration smtConfig)

Method Details

initFactories

public static void initFactories(SMT.Configuration config)

Initializes the SMT configuration object for the implementation in org.smtlib.impl - all the appropriate factories, etc.

Parameters:

config - the configuration object to initialize

createSortFamily

public Sort.Family createSortFamily(IExpr.IIdentifier identifier,
 IExpr.INumeral arity,
 List<IExpr.IAttribute<?>> attributes)

Description copied from interface: ISort.IFactory

Creates a sort family with the given identifier, arity, and attributes (null or empty if none).

Specified by:

createSortFamily in interface ISort.IFactory

createSortParameter

public Sort.Parameter createSortParameter(IExpr.ISymbol symbol)

Description copied from interface: ISort.IFactory

Creates a parameter for a parameterized sort abbreviation.

Specified by:

createSortParameter in interface ISort.IFactory

createSortExpression

public Sort.Application createSortExpression(IExpr.IIdentifier sortFamily,
 List<ISort> exprs)

Description copied from interface: ISort.IFactory

Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.

Specified by:

createSortExpression in interface ISort.IFactory

createSortExpression

public Sort.Application createSortExpression(IExpr.IIdentifier sortFamily,
 ISort... exprs)

Description copied from interface: ISort.IFactory

Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.

Specified by:

createSortExpression in interface ISort.IFactory

createSortAbbreviation

public Sort.Abbreviation createSortAbbreviation(IExpr.IIdentifier identifier,
 List<ISort.IParameter> params,
 ISort sortExpr)

Description copied from interface: ISort.IFactory

Creates a new sort abbreviation.

Specified by:

createSortAbbreviation in interface ISort.IFactory

createFcnSort

public Sort.FcnSort createFcnSort(ISort[] args,
 ISort result)

Description copied from interface: ISort.IFactory

Creates a function sort.

Specified by:

createFcnSort in interface ISort.IFactory

createErrorDefinition

public ISort.IErrorDefinition createErrorDefinition(IExpr.IIdentifier id,
 String errorMessage,
 IPos pos)

Description copied from interface: ISort.IFactory

Creates an error-placeholder definition (suppresses cascading errors).

Specified by:

createErrorDefinition in interface ISort.IFactory

Bool

public ISort.IApplication Bool()

Description copied from interface: ISort.IFactory

Returns the Bool sort.

Specified by:

Bool in interface ISort.IFactory

script

public ICommand.IScript script()

Description copied from interface: ICommand.IFactory

Creates an empty script, with no filename and no commands, ready to have commands added via ICommand.IScript.add(ICommand).

Specified by:

script in interface ICommand.IFactory

script

public ICommand.IScript script(IExpr.IStringLiteral filename,
 List<ICommand> commands)

Description copied from interface: ICommand.IFactory

Creates a script object containing the given filename or the given set of commands.

Specified by:

script in interface ICommand.IFactory

assertCommand

public ICommand.Iassert assertCommand(IExpr expr)

Description copied from interface: ICommand.IFactory

Creates an assert command object, asserting the given expression.

Specified by:

assertCommand in interface ICommand.IFactory

check_sat

public ICommand.Icheck_sat check_sat()

Description copied from interface: ICommand.IFactory

Creates a check-sat command object.

Specified by:

check_sat in interface ICommand.IFactory

check_sat_assuming

public ICommand.Icheck_sat_assuming check_sat_assuming(List<IExpr> terms)

Description copied from interface: ICommand.IFactory

Creates a check-sat-assuming command object.

Specified by:

check_sat_assuming in interface ICommand.IFactory

declare_const

public ICommand.Ideclare_const declare_const(IExpr.ISymbol s,
 ISort r)

Description copied from interface: ICommand.IFactory

Creates a declare-const command object.

Specified by:

declare_const in interface ICommand.IFactory

declare_datatype

public ICommand.Ideclare_datatype declare_datatype(IExpr.ISortDeclaration sd,
 ISort.IDatatype d)

Description copied from interface: ICommand.IFactory

Creates a declare-datatype command object.

Specified by:

declare_datatype in interface ICommand.IFactory

declare_datatypes

public ICommand.Ideclare_datatypes declare_datatypes(List<IExpr.ISortDeclaration> sds,
 List<ISort.IDatatype> dts)

Description copied from interface: ICommand.IFactory

Creates a declare-datatypes command object.

Specified by:

declare_datatypes in interface ICommand.IFactory

declare_fun

public ICommand.Ideclare_fun declare_fun(IExpr.ISymbol id,
 List<ISort> args,
 ISort r)

Description copied from interface: ICommand.IFactory

Creates a declare-fun command object.

Specified by:

declare_fun in interface ICommand.IFactory

declare_sort

public ICommand.Ideclare_sort declare_sort(IExpr.ISymbol s,
 IExpr.INumeral n)

Description copied from interface: ICommand.IFactory

Creates a declare-sort command object.

Specified by:

declare_sort in interface ICommand.IFactory

declare_sort_parameter

public ICommand.Ideclare_sort_parameter declare_sort_parameter(IExpr.ISymbol s)

Description copied from interface: ICommand.IFactory

Creates a declare-sort-parameter command object.

Specified by:

declare_sort_parameter in interface ICommand.IFactory

define_const

public ICommand.Idefine_const define_const(IExpr.ISymbol s,
 ISort r,
 IExpr e)

Description copied from interface: ICommand.IFactory

Creates a define-const command object.

Specified by:

define_const in interface ICommand.IFactory

define_fun

public ICommand.Idefine_fun define_fun(IExpr.ISymbol id,
 List<IExpr.IDeclaration> ps,
 ISort r,
 IExpr e)

Description copied from interface: ICommand.IFactory

Creates a define-fun command object.

Specified by:

define_fun in interface ICommand.IFactory

define_fun_rec

public ICommand.Idefine_fun_rec define_fun_rec(IExpr.ISymbol id,
 List<IExpr.IDeclaration> ps,
 ISort r,
 IExpr e)

Description copied from interface: ICommand.IFactory

Creates a define-fun-rec command object.

Specified by:

define_fun_rec in interface ICommand.IFactory

define_funs_rec

public ICommand.Idefine_funs_rec define_funs_rec(List<IExpr.IFunctionDeclaration> ds,
 List<IExpr> bs)

Description copied from interface: ICommand.IFactory

Creates a define-funs-rec command object.

Specified by:

define_funs_rec in interface ICommand.IFactory

define_sort

public ICommand.Idefine_sort define_sort(IExpr.ISymbol id,
 List<ISort.IParameter> ps,
 ISort e)

Description copied from interface: ICommand.IFactory

Creates a define-sort command object.

Specified by:

define_sort in interface ICommand.IFactory

echo

public ICommand.Iecho echo(IExpr.IStringLiteral arg)

Description copied from interface: ICommand.IFactory

Creates an echo command object.

Specified by:

echo in interface ICommand.IFactory

comment

public ICommand.Icomment comment(String text)

Description copied from interface: ICommand.IFactory

Creates a comment pseudo-command object, carrying the given raw comment text (see ICommand.Icomment).

Specified by:

comment in interface ICommand.IFactory

exit

public ICommand.Iexit exit()

Description copied from interface: ICommand.IFactory

Creates an exit command object.

Specified by:

exit in interface ICommand.IFactory

get_assertions

public ICommand.Iget_assertions get_assertions()

Description copied from interface: ICommand.IFactory

Creates a get-assertions command object.

Specified by:

get_assertions in interface ICommand.IFactory

get_assignment

public ICommand.Iget_assignment get_assignment()

Description copied from interface: ICommand.IFactory

Creates a get-assignment command object.

Specified by:

get_assignment in interface ICommand.IFactory

get_info

public ICommand.Iget_info get_info(IExpr.IKeyword k)

Description copied from interface: ICommand.IFactory

Creates a get-info command object.

Specified by:

get_info in interface ICommand.IFactory

get_model

public ICommand.Iget_model get_model()

Description copied from interface: ICommand.IFactory

Creates a get-model command object.

Specified by:

get_model in interface ICommand.IFactory

get_option

public ICommand.Iget_option get_option(IExpr.IKeyword k)

Description copied from interface: ICommand.IFactory

Creates a get-option command object.

Specified by:

get_option in interface ICommand.IFactory

get_proof

public ICommand.Iget_proof get_proof()

Description copied from interface: ICommand.IFactory

Creates a get-proof command object.

Specified by:

get_proof in interface ICommand.IFactory

get_unsat_assumptions

public ICommand.Iget_unsat_assumptions get_unsat_assumptions()

Description copied from interface: ICommand.IFactory

Creates a get-unsat-assumptions command object.

Specified by:

get_unsat_assumptions in interface ICommand.IFactory

get_unsat_core

public ICommand.Iget_unsat_core get_unsat_core()

Description copied from interface: ICommand.IFactory

Creates a get-unsat-core command object.

Specified by:

get_unsat_core in interface ICommand.IFactory

get_value

public ICommand.Iget_value get_value(List<IExpr> exprs)

Description copied from interface: ICommand.IFactory

Creates a get-value command object.

Specified by:

get_value in interface ICommand.IFactory

push

public ICommand.Ipush push(IExpr.INumeral n)

Description copied from interface: ICommand.IFactory

Creates a push command object.

Specified by:

push in interface ICommand.IFactory

pop

public ICommand.Ipop pop(IExpr.INumeral n)

Description copied from interface: ICommand.IFactory

Creates a pop command object.

Specified by:

pop in interface ICommand.IFactory

reset

public ICommand.Ireset reset()

Description copied from interface: ICommand.IFactory

Creates a reset command object.

Specified by:

reset in interface ICommand.IFactory

reset_assertions

public ICommand.Ireset_assertions reset_assertions()

Description copied from interface: ICommand.IFactory

Creates a reset-assertions command object.

Specified by:

reset_assertions in interface ICommand.IFactory

set_logic

public ICommand.Iset_logic set_logic(IExpr.ISymbol s)

Description copied from interface: ICommand.IFactory

Creates a set-logic command object.

Specified by:

set_logic in interface ICommand.IFactory

set_info

public ICommand.Iset_info set_info(IExpr.IKeyword k,
 IAttributeValue v)

Description copied from interface: ICommand.IFactory

Creates a set-info command object.

Specified by:

set_info in interface ICommand.IFactory

set_option

public ICommand.Iset_option set_option(IExpr.IKeyword k,
 IAttributeValue v)

Description copied from interface: ICommand.IFactory

Creates a set-option command object.

Specified by:

set_option in interface ICommand.IFactory

numeral

public IExpr.INumeral numeral(String v)

Description copied from interface: IExpr.IFactory

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

Specified by:

numeral in interface IExpr.IFactory

numeral

public SMTExpr.Numeral numeral(long v)

Description copied from interface: IExpr.IFactory

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

Specified by:

numeral in interface IExpr.IFactory

decimal

public IExpr.IDecimal decimal(String v)

Description copied from interface: IExpr.IFactory

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

Specified by:

decimal in interface IExpr.IFactory

unquotedString

public IExpr.IStringLiteral unquotedString(String v)

Description copied from interface: IExpr.IFactory

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

Specified by:

unquotedString in interface IExpr.IFactory

quotedString

public IExpr.IStringLiteral quotedString(String v)

Description copied from interface: IExpr.IFactory

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

Specified by:

quotedString in interface IExpr.IFactory

keyword

public IExpr.IKeyword keyword(String v)

Description copied from interface: IExpr.IFactory

Creates an IKeyword object from a canonical string representation.

Specified by:

keyword in interface IExpr.IFactory

binary

public IExpr.IBinaryLiteral binary(String v)

Description copied from interface: IExpr.IFactory

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

Specified by:

binary in interface IExpr.IFactory

hex

public IExpr.IHexLiteral hex(String v)

Description copied from interface: IExpr.IFactory

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

Specified by:

hex in interface IExpr.IFactory

symbol

public IExpr.ISymbol symbol(String v)

Description copied from interface: IExpr.IFactory

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

Specified by:

symbol in interface IExpr.IFactory

attribute

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

Description copied from interface: IExpr.IFactory

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

Specified by:

attribute in interface IExpr.IFactory

attribute

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

Description copied from interface: IExpr.IFactory

Creates an attribute with a keyword and a value.

Specified by:

attribute in interface IExpr.IFactory

attributedExpr

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

Description copied from interface: IExpr.IFactory

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

Specified by:

attributedExpr in interface IExpr.IFactory

patternTerms

public IExpr.IPatternTerms patternTerms(List<IExpr> terms)

Description copied from interface: IExpr.IFactory

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

Specified by:

patternTerms in interface IExpr.IFactory

attributedExpr

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

Description copied from interface: IExpr.IFactory

Creates an attributed expression with just one attribute.

Specified by:

attributedExpr in interface IExpr.IFactory

fcn

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

Description copied from interface: IExpr.IFactory

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

Specified by:

fcn in interface IExpr.IFactory

fcn

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

Description copied from interface: IExpr.IFactory

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

Specified by:

fcn in interface IExpr.IFactory

id

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

Description copied from interface: IExpr.IFactory

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

Specified by:

id in interface IExpr.IFactory

id

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

Description copied from interface: IExpr.IFactory

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

Specified by:

id in interface IExpr.IFactory

let

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

Description copied from interface: IExpr.IFactory

Creates a Let expression.

Specified by:

let in interface IExpr.IFactory

binding

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

Description copied from interface: IExpr.IFactory

Creates a binding for a Let expression.

Specified by:

binding in interface IExpr.IFactory

declaration

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

Description copied from interface: IExpr.IFactory

Creates a parameter declaration.

Specified by:

declaration in interface IExpr.IFactory

forall

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

Description copied from interface: IExpr.IFactory

Creates a Forall expression.

Specified by:

forall in interface IExpr.IFactory

forall

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

Description copied from interface: IExpr.IFactory

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

Specified by:

forall in interface IExpr.IFactory

exists

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

Description copied from interface: IExpr.IFactory

Creates an Exists expression.

Specified by:

exists in interface IExpr.IFactory

exists

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

Description copied from interface: IExpr.IFactory

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

Specified by:

exists in interface IExpr.IFactory

lambda

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

Description copied from interface: IExpr.IFactory

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

Specified by:

lambda in interface IExpr.IFactory

error

public IExpr.IError error(String text)

Description copied from interface: IExpr.IFactory

Creates an error expression.

Specified by:

error in interface IExpr.IFactory

sortDeclaration

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

Description copied from interface: IExpr.IFactory

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

Specified by:

sortDeclaration in interface IExpr.IFactory

selector

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

Description copied from interface: IExpr.IFactory

Creates a selector declaration.

Specified by:

selector in interface IExpr.IFactory

constructor

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

Description copied from interface: IExpr.IFactory

Creates a constructor declaration.

Specified by:

constructor in interface IExpr.IFactory

datatype

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

Description copied from interface: IExpr.IFactory

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

Specified by:

datatype in interface IExpr.IFactory

functionDeclaration

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

Description copied from interface: IExpr.IFactory

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

Specified by:

functionDeclaration in interface IExpr.IFactory

pattern

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

Description copied from interface: IExpr.IFactory

Creates a match pattern.

Specified by:

pattern in interface IExpr.IFactory

matchCase

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

Description copied from interface: IExpr.IFactory

Creates a single match case.

Specified by:

matchCase in interface IExpr.IFactory

match

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

Description copied from interface: IExpr.IFactory

Creates a match expression.

Specified by:

match in interface IExpr.IFactory