Package org.smtlib.logic

Class QF_RDL

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

org.smtlib.logic.QF_RDL

All Implemented Interfaces:

ILanguage, ILogic, INode, IPos.IPosable

public class QF_RDL
extends DifferenceLogic

QF_RDL atoms (QF_RDL.smt2): (op x y), (op (- x y) c), (op (- (+ x ... x) (+ y ... y)) c) with k > 1 occurrences each of x and y, and the extension (op (- x y) (/ c n)); x, y are free constants of sort Real, c is m or (- m), and m, n are numerals with n nonzero. A decimal d or (- d) as c is an error; --relax accepts it with a warning.

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

Method Summary

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

Methods inherited from class org.smtlib.logic.DifferenceLogic

isDifferenceOfSymbols, 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, 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_RDL

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

Method Details

kind

protected String kind()

Description copied from class: DifferenceLogic

"IDL" or "RDL", for error messages

Specified by:

kind in class DifferenceLogic

checkAtom

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

Description copied from class: DifferenceLogic

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

Specified by:

checkAtom in class DifferenceLogic

Throws:

IVisitor.VisitorException

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

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