Package org.smtlib.logic

Class QF_AUFBV

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.QF_UF

org.smtlib.logic.QF_AUFBV

All Implemented Interfaces:

ILanguage, ILogic, INode, IPos.IPosable

public class QF_AUFBV
extends QF_UF

This logic does not allow quantifiers; all array terms have sort (Array (_ BitVec i) (_ BitVec j))

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_AUFBV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)

Method Summary

Modifier and Type	Method	Description
protected boolean	allowedArraySort(ISort.IApplication array)	Whether this logic allows the Array sort array, whose own sort is already expanded and which contains no sort parameter
protected String	allowedArraySorts()	The Array sorts this logic allows, as text for error messages, or null if it allows every Array sort.
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

Methods inherited from class org.smtlib.logic.QF_UF

validExpression

Methods inherited from class org.smtlib.logic.Logic

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_AUFBV

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

Method Details

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

Overrides:

checkFcnDeclaration in class QF_UF

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

Overrides:

checkSortDeclaration in class SMTExpr.Logic

Throws:

IVisitor.VisitorException

allowedArraySorts

protected String allowedArraySorts()

Description copied from class: Logic

The Array sorts this logic allows, as text for error messages, or null if it allows every Array sort. A logic restricting Array sorts overrides this and Logic.allowedArraySort(org.smtlib.ISort.IApplication).

Overrides:

allowedArraySorts in class Logic

allowedArraySort

protected boolean allowedArraySort(ISort.IApplication array)

Description copied from class: Logic

Whether this logic allows the Array sort array, whose own sort is already expanded and which contains no sort parameter

Overrides:

allowedArraySort in class Logic