Package org.smtlib.impl

Class SMTExpr.Logic

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.SMTExpr.Logic

All Implemented Interfaces:

ILanguage, ILogic, INode, IPos.IPosable

Direct Known Subclasses:

Logic

Enclosing class:

SMTExpr

public static class SMTExpr.Logic
extends Pos.Printable
implements ILogic

Field Summary

Fields

Modifier and Type	Field	Description
protected Map<IExpr.IKeyword,IExpr.IAttribute<?>>	attributes	The logic's attributes — last occurrence wins for duplicate keywords
protected List<IExpr.IAttribute<?>>	attributesList	All logic attributes in source order, preserving duplicates
protected IExpr.ISymbol	logicName	The name of the logic
protected final SMT.Configuration	smtConfig	The configuration this logic instance is scoped to; see issue #22.

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

pos

Constructor Summary

Constructors

Constructor	Description
Logic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)	Creates a logic

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); }
List<IExpr.IAttribute<?>>	attributeList()	The attributes in source order, including repeated keywords
Map<IExpr.IKeyword,IExpr.IAttribute<?>>	attributes()	The attributes, as a Map, keyed by the keyword in the attribute
void	checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)	Checks whether the given function declaration is permitted in the language, throwing an exception if not
void	checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)	Checks whether the given sort declaration is permitted in the language, throwing an exception if not
IExpr.ISymbol	logicName()	The name of the logic
void	validExpression(IExpr expr)	Checks whether the given expression is permitted in the language, throwing an exception if not
IAttributeValue	value(IExpr.IKeyword keyword)	The value of a given attribute

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

Field Details

smtConfig

protected final SMT.Configuration smtConfig

The configuration this logic instance is scoped to; see issue #22.

logicName

protected IExpr.ISymbol logicName

The name of the logic

attributes

protected Map<IExpr.IKeyword,IExpr.IAttribute<?>> attributes

The logic's attributes — last occurrence wins for duplicate keywords

attributesList

protected List<IExpr.IAttribute<?>> attributesList

All logic attributes in source order, preserving duplicates

Constructor Details

Logic

public Logic(SMT.Configuration smtConfig,
 IExpr.ISymbol name,
 Collection<IExpr.IAttribute<?>> attributes)

Creates a logic

Method Details

logicName

public IExpr.ISymbol logicName()

The name of the logic

Specified by:

logicName in interface ILogic

attributes

public Map<IExpr.IKeyword,IExpr.IAttribute<?>> attributes()

The attributes, as a Map, keyed by the keyword in the attribute

Specified by:

attributes in interface ILogic

attributeList

public List<IExpr.IAttribute<?>> attributeList()

Description copied from interface: ILogic

The attributes in source order, including repeated keywords

Specified by:

attributeList in interface ILogic

value

public IAttributeValue value(IExpr.IKeyword keyword)

The value of a given attribute

Specified by:

value in interface ILogic

validExpression

public void validExpression(IExpr expr)
                     throws IVisitor.VisitorException

Description copied from interface: ILanguage

Checks whether the given expression is permitted in the language, throwing an exception if not

Specified by:

validExpression in interface ILanguage

Throws:

IVisitor.VisitorException

checkFcnDeclaration

public void checkFcnDeclaration(IExpr.IIdentifier id,
 List<ISort> argSorts,
 ISort resultSort,
 IExpr definition)
                         throws IVisitor.VisitorException

Description copied from interface: ILanguage

Checks whether the given function declaration is permitted in the language, throwing an exception if not

Specified by:

checkFcnDeclaration in interface ILanguage

Throws:

IVisitor.VisitorException

checkSortDeclaration

public void checkSortDeclaration(IExpr.IIdentifier id,
 List<ISort.IParameter> params,
 ISort expr)
                          throws IVisitor.VisitorException

Description copied from interface: ILanguage

Checks whether the given sort declaration is permitted in the language, throwing an exception if not

Specified by:

checkSortDeclaration in interface ILanguage

Throws:

IVisitor.VisitorException

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