ITheory

All Superinterfaces:: INode

All Known Implementing Classes:: SMTExpr.Theory

public interface ITheory extends INode

This interface represents a definition of an SMT-LIB theory

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 (keyword-value pairs) of the theory.

IExpr.ISymbol

theoryName()

The name of the theory

IAttributeValue

value(IExpr.IKeyword keyword)

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

default List<IAttributeValue>

values(IExpr.IKeyword keyword)

All values for a given attribute keyword (handles multiple occurrences of the same keyword).

Methods inherited from interface org.smtlib.INode
accept

Method Details
- theoryName
  
  IExpr.ISymbol theoryName()
  
  The name of the theory
- attributes
  
  Map<IExpr.IKeyword,IExpr.IAttribute<?>> attributes()
  
  The attributes (keyword-value pairs) of the theory.
- 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 theory
- values
  
  default List<IAttributeValue> values(IExpr.IKeyword keyword)
  
  All values for a given attribute keyword (handles multiple occurrences of the same keyword). Returns an empty list if the keyword is not present.