ILogic

All Superinterfaces:: ILanguage, INode

All Known Implementing Classes:: ALL, AUFLIA, AUFLIRA, AUFNIRA, DifferenceLogic, LIA, Logic, LRA, QF_ABV, QF_AUFBV, QF_AUFLIA, QF_AX, QF_BV, QF_EIA, QF_FP, QF_IDL, QF_LIA, QF_LRA, QF_NIA, QF_NRA, QF_RDL, QF_UF, QF_UFBV, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNRA, SMTExpr.Logic, UFLRA, UFNIA

public interface ILogic extends INode, ILanguage

This interface represents a definition of an SMT_LIB logic

Method Summary

Modifier and Type

Method

Description

List<IExpr.IAttribute<?>>

attributeList()

The attributes in source order, including repeated keywords

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

attributes()

The attributes of the logic

IExpr.ISymbol

logicName()

The name of the logic

IAttributeValue

value(IExpr.IKeyword keyword)

The value of an attribute; returns null if the attribute does not exist for this logic.

Methods inherited from interface org.smtlib.ILanguage
checkFcnDeclaration, checkSortDeclaration, validExpression

Methods inherited from interface org.smtlib.INode
accept

Method Details
- logicName
  
  IExpr.ISymbol logicName()
  
  The name of the logic
- attributes
  
  Map<IExpr.IKeyword,IExpr.IAttribute<?>> attributes()
  
  The attributes of the logic
- attributeList
  
  List<IExpr.IAttribute<?>> attributeList()
  
  The attributes in source order, including repeated keywords
- value
  
  IAttributeValue value(IExpr.IKeyword keyword)
  
  The value of an attribute; returns null if the attribute does not exist for this logic.