Package org.smtlib.logic

Class DifferenceLogic

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

All Implemented Interfaces:

ILanguage, ILogic, INode, IPos.IPosable

Direct Known Subclasses:

QF_IDL, QF_RDL

public abstract class DifferenceLogic
extends Logic

Common base for the difference logics QF_IDL and QF_RDL. Their :language allows closed quantifier-free formulas built with the Core connectives over Bool atoms and restricted arithmetic atoms (op a b), where op is <, <=, >, >=, = or distinct. A subclass checks the shape of each arithmetic atom.

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

Method Summary

Modifier and Type	Method	Description
protected abstract void	checkAtom(IExpr.IFcnExpr atom, IExpr lhs, IExpr rhs)	Checks the arguments of a binary arithmetic atom (op lhs rhs).
protected static boolean	isDifferenceOfSymbols(IExpr e)	True for (- x y) with x and y symbols
protected abstract String	kind()	"IDL" or "RDL", for error messages
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.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, checkFcnDeclaration, 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

checkFcnDeclaration, checkSortDeclaration

Constructor Details

DifferenceLogic

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

Method Details

kind

protected abstract String kind()

"IDL" or "RDL", for error messages

checkAtom

protected abstract void checkAtom(IExpr.IFcnExpr atom,
 IExpr lhs,
 IExpr rhs)
                           throws IVisitor.VisitorException

Checks the arguments of a binary arithmetic atom (op lhs rhs).

Throws:

IVisitor.VisitorException

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 SMTExpr.Logic

Throws:

IVisitor.VisitorException

isDifferenceOfSymbols

protected static boolean isDifferenceOfSymbols(IExpr e)

True for (- x y) with x and y symbols