Package org.smtlib.logic

Class QF_UFBV

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_UFBV

All Implemented Interfaces:

ILanguage, ILogic, INode, IPos.IPosable

public class QF_UFBV
extends QF_UF

Quantifier-free, with uninterpreted functions and sorts permitted -- identical restrictions to QF_UF, all inherited from it (the bit-vector vs. plain-UF distinction is carried entirely by the bundled theory signature, not by any extra syntactic restriction here).

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

Method Summary

Methods inherited from class org.smtlib.logic.QF_UF

checkFcnDeclaration, validExpression

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, checkSortDeclaration, 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

Methods inherited from interface org.smtlib.ILanguage

checkSortDeclaration

Constructor Details

QF_UFBV

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