Package org.smtlib.impl

Class SMTExpr.Pattern

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.SMTExpr.Pattern

All Implemented Interfaces:

IExpr.IPattern, INode, IPos.IPosable

Enclosing class:

SMTExpr

public static class SMTExpr.Pattern
extends Pos.Printable
implements IExpr.IPattern

Represents a match pattern: a constructor name applied to zero or more variable symbols.

Field Summary

Fields

Modifier and Type	Field	Description
protected IExpr.ISymbol	constructor
protected boolean	emptyParentheses	Whether the pattern was written as (c), in parentheses with no variables
protected List<IExpr.ISymbol>	params

Fields inherited from class org.smtlib.impl.Pos.Posable

pos

Constructor Summary

Constructors

Constructor	Description
Pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)	Creates a pattern from the given constructor symbol and variable list.
Pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params, boolean parenthesized)	Creates a pattern that is written in parentheses even if it has no variables, as (c)

Method Summary

Modifier and Type	Method	Description
<T> T	accept(IVisitor<T> v)	The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }
IExpr.ISymbol	constructor()
List<IExpr.ISymbol>	params()
boolean	parenthesized()	True if written in parentheses; (c), with no variables, is not SMT-LIB but is parsed (with an error) so that type checking reports it as well

Methods inherited from class org.smtlib.impl.Pos.Printable

toString

Methods inherited from class org.smtlib.impl.Pos.Posable

equals, hashCode, pos, setPos

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Field Details

constructor

protected IExpr.ISymbol constructor

params

protected List<IExpr.ISymbol> params

emptyParentheses

protected boolean emptyParentheses

Whether the pattern was written as (c), in parentheses with no variables

Constructor Details

Pattern

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

Creates a pattern from the given constructor symbol and variable list.

Pattern

public Pattern(IExpr.ISymbol constructor,
 List<IExpr.ISymbol> params,
 boolean parenthesized)

Creates a pattern that is written in parentheses even if it has no variables, as (c)

Method Details

constructor

public IExpr.ISymbol constructor()

Specified by:

constructor in interface IExpr.IPattern

params

public List<IExpr.ISymbol> params()

Specified by:

params in interface IExpr.IPattern

parenthesized

public boolean parenthesized()

Description copied from interface: IExpr.IPattern

True if written in parentheses; (c), with no variables, is not SMT-LIB but is parsed (with an error) so that type checking reports it as well

Specified by:

parenthesized in interface IExpr.IPattern

accept

public <T> T accept(IVisitor<T> v)
             throws IVisitor.VisitorException

Description copied from interface: INode

The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }

Specified by:

accept in interface INode

Type Parameters:

T - the return type desired from the visit methods

Parameters:

v - the visitor class

Returns:

the value returned by the visit method

Throws:

IVisitor.VisitorException