Package org.smtlib.logic

Class Logic

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.SMTExpr.Logic

org.smtlib.logic.Logic

All Implemented Interfaces:

ILanguage, ILogic, INode, IPos.IPosable

Direct Known Subclasses:

ALL, AUFLIA, AUFLIRA, AUFNIRA, DifferenceLogic, LIA, LRA, QF_AUFLIA, QF_AX, QF_BV, QF_EIA, QF_FP, QF_NIA, QF_NRA, QF_UF, QF_UFIDL, UFNIA

public abstract class Logic
extends SMTExpr.Logic
implements ILanguage

Common base for this package's per-logic syntactic-restriction classes (QF_IDL, LRA, QF_UF, etc). Each subclass overrides ILanguage.validExpression(org.smtlib.IExpr), ILanguage.checkFcnDeclaration(org.smtlib.IExpr.IIdentifier, java.util.List<org.smtlib.ISort>, org.smtlib.ISort, org.smtlib.IExpr), and ILanguage.checkSortDeclaration(org.smtlib.IExpr.IIdentifier, java.util.List<org.smtlib.ISort.IParameter>, org.smtlib.ISort) to reject whatever its own logic's SMT-LIB-mandated grammar forbids (quantifiers, uninterpreted functions, nonlinear arithmetic, unrestricted sorts, ...); this class supplies the shared helpers those overrides call (noQuantifiers, noFunctions, noSorts, checkArraySort, isLinearReal, ...).

Extends SMTExpr.Logic (the plain, unrestricted ILogic implementation sexpr.Parser falls back to when no subclass exists for a given logic name -- see issue #46) rather than depending only on the bare ILogic interface, so that a subclass which doesn't override one of the three hooks above still gets that hook's already-permissive default (an empty/no-op override) for free, instead of every subclass having to restate "permit everything" explicitly.

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
Logic(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.
protected void	checkArraySorts(List<ISort> argSorts, ISort resultSort, IExpr.IIdentifier id)	Checks the Array sorts in a function's argument and result sorts
protected void	checkArraySorts(ISort sort, IPos pos)	Checks every Array sort within sort, expanding abbreviations, against allowedArraySort(org.smtlib.ISort.IApplication).
protected void	checkBoundArraySorts(IExpr expression)	Checks the Array sorts of the variables bound by quantifiers in expression
protected static boolean	isBitVecArray(ISort.IApplication array)	Whether array is (Array (_ BitVec i) (_ BitVec j)), as QF_ABV and QF_AUFBV require
protected static boolean	isBitVecSort(ISort sort)	Whether sort, with abbreviations expanded, is a (_ BitVec n) sort
boolean	isFreeConstant(IExpr expr)
boolean	isInteger(IExpr expr)
boolean	isLinearInteger(IExpr expr)
boolean	isLinearReal(IExpr expr)
boolean	isRealConst(IExpr expr)
void	noExponentiation(IExpr expression)
void	noFunctions(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
protected static List<IExpr>	nonCoefficients(IExpr.IFcnExpr e, Predicate<IExpr> isCoefficient)	The arguments of an application (of * or /) that are not coefficients.
void	noQuantifiers(IExpr expression)
void	noSorts(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
protected IVisitor.VisitorException	restrictionError(String message, IExpr e)	Builds a VisitorException for a restriction violation (e.g.
protected static boolean	sameSort(ISort sort, ISort allowed)	Whether sort, with abbreviations expanded, is structurally the same as allowed
protected ISort	sortApp(String name, ISort... params)	Creates the sort expression name(params...), e.g.

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

accept, attributeList, attributes, checkFcnDeclaration, checkSortDeclaration, logicName, validExpression, 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, validExpression

Constructor Details

Logic

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

Method Details

noQuantifiers

public void noQuantifiers(IExpr expression)
                   throws IVisitor.VisitorException

Throws:

IVisitor.VisitorException

noExponentiation

public void noExponentiation(IExpr expression)
                      throws IVisitor.VisitorException

Throws:

IVisitor.VisitorException

noFunctions

public void noFunctions(IExpr.IIdentifier id,
 List<ISort> argSorts,
 ISort resultSort,
 IExpr definition)
                 throws IVisitor.VisitorException

Throws:

IVisitor.VisitorException

noSorts

public void noSorts(IExpr.IIdentifier id,
 List<ISort.IParameter> params,
 ISort expr)
             throws IVisitor.VisitorException

Throws:

IVisitor.VisitorException

restrictionError

protected IVisitor.VisitorException restrictionError(String message,
 IExpr e)

Builds a VisitorException for a restriction violation (e.g. QF_IDL/QF_RDL's difference-logic shape, LRA's linearity check) whose message includes the offending expression's own printed text, not just an abstract description of the rule it broke -- several subclasses' checks used to throw the bare message alone, each with its own "// FIXME" noting the expression text was meant to be included but wasn't.

sortApp

protected ISort sortApp(String name,
 ISort... params)

Creates the sort expression name(params...), e.g. sortApp("Array", intSort, intSort) for (Array Int Int). Used to build canonical sorts for structural comparison (via ISort.equalsNoExpand(org.smtlib.ISort)), rather than comparing printed text.

allowedArraySorts

protected String allowedArraySorts()

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 allowedArraySort(org.smtlib.ISort.IApplication).

allowedArraySort

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

checkArraySorts

protected void checkArraySorts(ISort sort,
 IPos pos)
                        throws IVisitor.VisitorException

Checks every Array sort within sort, expanding abbreviations, against allowedArraySort(org.smtlib.ISort.IApplication). An Array sort containing a sort parameter is skipped: it is checked where the parameterized abbreviation is instantiated.

Throws:

IVisitor.VisitorException

checkArraySorts

protected void checkArraySorts(List<ISort> argSorts,
 ISort resultSort,
 IExpr.IIdentifier id)
                        throws IVisitor.VisitorException

Checks the Array sorts in a function's argument and result sorts

Throws:

IVisitor.VisitorException

checkBoundArraySorts

protected void checkBoundArraySorts(IExpr expression)
                             throws IVisitor.VisitorException

Checks the Array sorts of the variables bound by quantifiers in expression

Throws:

IVisitor.VisitorException

sameSort

protected static boolean sameSort(ISort sort,
 ISort allowed)

Whether sort, with abbreviations expanded, is structurally the same as allowed

isBitVecArray

protected static boolean isBitVecArray(ISort.IApplication array)

Whether array is (Array (_ BitVec i) (_ BitVec j)), as QF_ABV and QF_AUFBV require

isBitVecSort

protected static boolean isBitVecSort(ISort sort)

Whether sort, with abbreviations expanded, is a (_ BitVec n) sort

isInteger

public boolean isInteger(IExpr expr)

isFreeConstant

public boolean isFreeConstant(IExpr expr)

nonCoefficients

protected static List<IExpr> nonCoefficients(IExpr.IFcnExpr e,
 Predicate<IExpr> isCoefficient)

The arguments of an application (of * or /) that are not coefficients. A product, of any arity, is linear when at most one of its factors is not a coefficient.

isLinearInteger

public boolean isLinearInteger(IExpr expr)

isLinearReal

public boolean isLinearReal(IExpr expr)

isRealConst

public boolean isRealConst(IExpr expr)