Package org.smtlib

Interface ILanguage

All Known Subinterfaces:

ILogic

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 ILanguage

This interface represents the functionality of an SMT-LIB language - the combination of one or more theories and various restrictions on the permitted expressions. The various checks for permitted expressions and declarations may refer to the current state of the symbol table.

Author:

David Cok

Method Summary

Modifier and Type	Method	Description
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
void	validExpression(IExpr expression)	Checks whether the given expression is permitted in the language, throwing an exception if not

Method Details

validExpression

void validExpression(IExpr expression)
              throws IVisitor.VisitorException

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

Throws:

IVisitor.VisitorException

checkFcnDeclaration

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

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

Throws:

IVisitor.VisitorException

checkSortDeclaration

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

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

Throws:

IVisitor.VisitorException