Package org.smtlib.logic

Class QF_LIA

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.SMTExpr.Logic

org.smtlib.logic.Logic

org.smtlib.logic.LIA

org.smtlib.logic.QF_LIA

All Implemented Interfaces:

ILanguage, ILogic, INode, IPos.IPosable

public class QF_LIA
extends LIA

Field Summary

Fields inherited from class org.smtlib.impl.SMTExpr.Logic

attributes, attributesList, logicName, smtConfig

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

pos

Constructor Summary

Constructors

Constructor	Description
QF_LIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)

Method Summary

Modifier and Type	Method	Description
void	validExpression(IExpr expression)	Checks whether the given expression is permitted in the language, throwing an exception if not

Methods inherited from class org.smtlib.logic.LIA

checkFcnDeclaration, checkSortDeclaration

Methods inherited from class org.smtlib.logic.Logic

allowedArraySort, allowedArraySorts, checkArraySorts, checkArraySorts, checkBoundArraySorts, isBitVecArray, isBitVecSort, isFreeConstant, isInteger, isLinearInteger, isLinearReal, isRealConst, noExponentiation, noFunctions, nonCoefficients, noQuantifiers, noSorts, restrictionError, sameSort, sortApp

Methods inherited from class org.smtlib.impl.SMTExpr.Logic

accept, attributeList, attributes, logicName, value

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

Constructor Details

QF_LIA

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

Method Details

validExpression

public void validExpression(IExpr expression)
                     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

Overrides:

validExpression in class LIA

Throws:

IVisitor.VisitorException