Package org.smtlib

Class TypeChecker

java.lang.Object

org.smtlib.TypeChecker

All Implemented Interfaces:

IVisitor<ISort>

public class TypeChecker
extends Object
implements IVisitor<ISort>

This class is a visitor that type-checks a formula

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	TypeChecker.Variable

Nested classes/interfaces inherited from interface org.smtlib.IVisitor

IVisitor.TreeVisitor<T>, IVisitor.VisitorException

Field Summary

Fields

Modifier and Type	Field	Description
protected Map<IExpr.ISymbol,TypeChecker.Variable>	currentScope
protected List<Map<IExpr.ISymbol,TypeChecker.Variable>>	parameters
protected IExpr	quantifierBody	The body of the innermost quantifier being checked (the only place a :pattern may appear), or null.
List<IResponse>	result	Compilation of errors

Constructor Summary

Constructors

Constructor	Description
TypeChecker(SymbolTable symTable)	Constructs a formula typechecker from the current symbol table; sorts computed while checking are recorded directly on each IExpr node via IExpr.setSort().

Method Summary

Modifier and Type	Method	Description
protected boolean	badSymbol(IExpr.ISymbol s)	Reports a symbol that is not legal (see SMT.Configuration.isOKSymbol), which only the API (or declare-fun's name) can produce; returns true if it is not legal
static List<IResponse>	check(SymbolTable symTable, IExpr expr)	The main entry point for type-checking an IExpr (expected to be a Bool)
static List<IResponse>	checkAssertion(SymbolTable symTable, IExpr expr)	The main entry point for type-checking an assert expression (expected to be a Bool); unlike check(SymbolTable,IExpr), this checks the expression within a pushed scope that is merged into the enclosing scope on success (or popped on error).
static List<IResponse>	checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)
static List<IResponse>	checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos)
static List<IResponse>	checkFcnRec(SymbolTable symTable, boolean global, IExpr.ISymbol id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)	Type-checks a define-fun-rec command: verifies the symbol is new, validates sorts, pre-adds the function to the symbol table so the body may call it recursively, then checks the body expression.
static List<IResponse>	checkFcnsRec(SymbolTable symTable, boolean global, List<IExpr.IFunctionDeclaration> decls, List<IExpr> bodies)	Type-checks a define-funs-rec command: for each declaration verifies the symbol is new and sorts are valid, pre-adds all functions to the symbol table for mutual recursion, then checks each body expression.
protected boolean	checkPatternTerm(IExpr t)	Checks that a pattern term is binder-free and has no annotations (SMT-LIB 2.7, Section 3.6.5); returns false, recording an error, if it is not.
static List<IResponse>	checkSortAbbreviation(SymbolTable symTable, IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
static List<IResponse>	checkTerm(SymbolTable symTable, IExpr expr)	Type-checks a term of any sort (e.g.
static void	clearSorts(IExpr expr)	Walks the given expression subtree, nulling out the sort recorded on each node (e.g.
protected void	error(String msg, IPos pos)	Utility method for recording an error
protected boolean	noVariables(List<?> list, String binder, IPos pos)	Reports a binder with no variables; returns true if the list is empty
protected String	pr(IExpr e)	Utility method for printing an expression, using the default printer
protected String	pr(ISort e)	Utility method for printing a sort, using the default printer
static ISort.IFcnSort	resolveFcnSort(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos, List<IResponse> errors)	Checks a function signature as checkFcn does, adding any errors to errors; returns the signature with its sorts resolved in the current scope (so a sort parameter in scope becomes its IParameter), or null if there were errors.
ISort	save(IExpr e, ISort s)
protected boolean	shadowsLogic(IExpr.ISymbol s, boolean sort)	Reports a bound variable (sort parameter, if sort is true) with the name of a function (sort) symbol of the logic or its theories, which only --relax allows (SMT-LIB Remark 7); returns true if reported
static List<IResponse>	validate(SMT.Configuration smtConfig, ICommand cmd)	Validates non-syntactic well-formedness of a command (user IDs, duplicate names, list sizes).
static List<IResponse>	validateDatatypeNames(SymbolTable symTable, SMT.Configuration smtConfig, List<IExpr.ISortDeclaration> sortDecls, List<ISort.IDatatype> datatypes)	Checks that constructor and selector names introduced by a datatype group are not already defined (neither in the symbol table nor duplicated within the group).
ISort	visit(ICommand e)
ISort	visit(ICommand.IScript e)
ISort	visit(IExpr.IAsIdentifier e)
ISort	visit(IExpr.IAttribute<?> e)
ISort	visit(IExpr.IAttributedExpr e)
ISort	visit(IExpr.IBinaryLiteral e)
ISort	visit(IExpr.IBinding e)
ISort	visit(IExpr.IConstructor e)
ISort	visit(IExpr.IDecimal e)
ISort	visit(IExpr.IDeclaration e)
ISort	visit(IExpr.IError e)
ISort	visit(IExpr.IExists e)
ISort	visit(IExpr.IFcnExpr e)
ISort	visit(IExpr.IForall e)
ISort	visit(IExpr.IFunctionDeclaration e)
ISort	visit(IExpr.IHexLiteral e)
ISort	visit(IExpr.IKeyword e)
ISort	visit(IExpr.ILambda e)	Type-checks a lambda expression: (lambda (sorted_var+) term), SMT-LIB 2.7ff (the optional HO-Core theory -- see SMT/logics/HO-Core.smt2).
ISort	visit(IExpr.ILet e)
ISort	visit(IExpr.IMatch e)
ISort	visit(IExpr.IMatchCase e)
ISort	visit(IExpr.INumeral e)
ISort	visit(IExpr.IParameterizedIdentifier e)
ISort	visit(IExpr.IPattern e)
ISort	visit(IExpr.ISelector e)
ISort	visit(IExpr.ISortDeclaration e)
ISort	visit(IExpr.IStringLiteral e)
ISort	visit(IExpr.ISymbol e)
ISort	visit(ILogic s)
ISort	visit(IResponse e)
ISort	visit(IResponse.IAssertionsResponse e)
ISort	visit(IResponse.IAssignmentResponse e)
ISort	visit(IResponse.IAttributeList e)
ISort	visit(IResponse.IError e)
ISort	visit(IResponse.IProofResponse e)
ISort	visit(IResponse.IUnsatAssumptionsResponse e)
ISort	visit(IResponse.IUnsatCoreResponse e)
ISort	visit(IResponse.IValueResponse e)
ISort	visit(ISort.IAbbreviation s)
ISort	visit(ISort.IApplication s)
ISort	visit(ISort.IDatatype e)
ISort	visit(ISort.IFamily s)
ISort	visit(ISort.IFcnSort s)
ISort	visit(ISort.IParameter s)
ISort	visit(ITheory s)
ISort	visit(ISexpr.ISeq e)
ISort	visit(ISexpr.IToken<?> e)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.smtlib.IVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Field Details

result

public List<IResponse> result

Compilation of errors

quantifierBody

protected IExpr quantifierBody

The body of the innermost quantifier being checked (the only place a :pattern may appear), or null.

currentScope

protected Map<IExpr.ISymbol,TypeChecker.Variable> currentScope

parameters

protected List<Map<IExpr.ISymbol,TypeChecker.Variable>> parameters

Constructor Details

TypeChecker

public TypeChecker(SymbolTable symTable)

Constructs a formula typechecker from the current symbol table; sorts computed while checking are recorded directly on each IExpr node via IExpr.setSort().

Method Details

visit

public ISort visit(IExpr.IAttribute<?> e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IBinding e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISort.IDatatype e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.ISortDeclaration e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.ISelector e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IConstructor e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IDeclaration e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IFunctionDeclaration e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ICommand.IScript e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ICommand e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IMatchCase e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IPattern e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ILogic s)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ITheory s)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IError e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IAssertionsResponse e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IAssignmentResponse e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IProofResponse e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IValueResponse e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IUnsatCoreResponse e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IUnsatAssumptionsResponse e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IResponse.IAttributeList e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISexpr.ISeq e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISexpr.IToken<?> e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

error

protected void error(String msg,
 IPos pos)

Utility method for recording an error

badSymbol

protected boolean badSymbol(IExpr.ISymbol s)

Reports a symbol that is not legal (see SMT.Configuration.isOKSymbol), which only the API (or declare-fun's name) can produce; returns true if it is not legal

shadowsLogic

protected boolean shadowsLogic(IExpr.ISymbol s,
 boolean sort)

Reports a bound variable (sort parameter, if sort is true) with the name of a function (sort) symbol of the logic or its theories, which only --relax allows (SMT-LIB Remark 7); returns true if reported

noVariables

protected boolean noVariables(List<?> list,
 String binder,
 IPos pos)

Reports a binder with no variables; returns true if the list is empty

pr

protected String pr(IExpr e)

Utility method for printing an expression, using the default printer

pr

protected String pr(ISort e)

Utility method for printing a sort, using the default printer

checkSortAbbreviation

public static List<IResponse> checkSortAbbreviation(SymbolTable symTable,
 IExpr.IIdentifier id,
 List<ISort.IParameter> params,
 ISort expr)

checkFcn

public static List<IResponse> checkFcn(SymbolTable symTable,
 IExpr.IIdentifier id,
 List<ISort> sorts,
 ISort result,
 IPos pos)

resolveFcnSort

public static ISort.IFcnSort resolveFcnSort(SymbolTable symTable,
 IExpr.IIdentifier id,
 List<ISort> sorts,
 ISort result,
 IPos pos,
 List<IResponse> errors)

Checks a function signature as checkFcn does, adding any errors to errors; returns the signature with its sorts resolved in the current scope (so a sort parameter in scope becomes its IParameter), or null if there were errors.

checkFcn

public static List<IResponse> checkFcn(SymbolTable symTable,
 IExpr.IIdentifier id,
 List<IExpr.IDeclaration> params,
 ISort result,
 IExpr expr)

checkFcnRec

public static List<IResponse> checkFcnRec(SymbolTable symTable,
 boolean global,
 IExpr.ISymbol id,
 List<IExpr.IDeclaration> params,
 ISort result,
 IExpr expr)

Type-checks a define-fun-rec command: verifies the symbol is new, validates sorts, pre-adds the function to the symbol table so the body may call it recursively, then checks the body expression. On success the entry's definition is set. Delegates to checkFcnsRec as the N=1 case (a singleton declaration group).

checkFcnsRec

public static List<IResponse> checkFcnsRec(SymbolTable symTable,
 boolean global,
 List<IExpr.IFunctionDeclaration> decls,
 List<IExpr> bodies)

Type-checks a define-funs-rec command: for each declaration verifies the symbol is new and sorts are valid, pre-adds all functions to the symbol table for mutual recursion, then checks each body expression. On success all entries' definitions are set.

check

public static List<IResponse> check(SymbolTable symTable,
 IExpr expr)

The main entry point for type-checking an IExpr (expected to be a Bool)

checkTerm

public static List<IResponse> checkTerm(SymbolTable symTable,
 IExpr expr)

Type-checks a term of any sort (e.g. a get-value term) and checks it against the logic in use, if any.

checkAssertion

public static List<IResponse> checkAssertion(SymbolTable symTable,
 IExpr expr)

The main entry point for type-checking an assert expression (expected to be a Bool); unlike check(SymbolTable,IExpr), this checks the expression within a pushed scope that is merged into the enclosing scope on success (or popped on error).

save

public ISort save(IExpr e,
 ISort s)

clearSorts

public static void clearSorts(IExpr expr)
                       throws IVisitor.VisitorException

Walks the given expression subtree, nulling out the sort recorded on each node (e.g. because it is leaving the live assertion set, on pop or reset-assertions).

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.INumeral e)

Specified by:

visit in interface IVisitor<ISort>

visit

public ISort visit(IExpr.IFcnExpr e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.ISymbol e)

Specified by:

visit in interface IVisitor<ISort>

visit

public ISort visit(IExpr.IDecimal e)

Specified by:

visit in interface IVisitor<ISort>

visit

public ISort visit(IExpr.IBinaryLiteral e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IHexLiteral e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IStringLiteral e)

Specified by:

visit in interface IVisitor<ISort>

visit

public ISort visit(IExpr.IKeyword e)

Specified by:

visit in interface IVisitor<ISort>

visit

public ISort visit(IExpr.IError e)

Specified by:

visit in interface IVisitor<ISort>

visit

public ISort visit(IExpr.IParameterizedIdentifier e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IAsIdentifier e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

checkPatternTerm

protected boolean checkPatternTerm(IExpr t)

Checks that a pattern term is binder-free and has no annotations (SMT-LIB 2.7, Section 3.6.5); returns false, recording an error, if it is not.

visit

public ISort visit(IExpr.IAttributedExpr e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IForall e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IExists e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.ILambda e)
            throws IVisitor.VisitorException

Type-checks a lambda expression: (lambda (sorted_var+) term), SMT-LIB 2.7ff (the optional HO-Core theory -- see SMT/logics/HO-Core.smt2).

Parameter/body scoping is identical to visit(IForall)/visit(IExists) above: push a new scope, type-check each parameter declaration into it (catching duplicate names), then type-check the body in that scope. Unlike a quantifier, though, a lambda's body is not required to be Bool -- it can be any sort -- and the lambda expression's own computed sort is not its body's sort but the function sort mapping its parameters' sorts to its body's sort.

Design decision (see jSMTLIB issue #125): SMT-LIB 2.7 also introduces a (-> sort+ sort) function-sort constructor for exactly this purpose, and that constructor already exists in this codebase -- not as new work for lambda, but as an ordinary theory-declared sort: HO-Core.smt2 declares :sorts ( (-> 2 :right-assoc) ), so -> is a plain 2-ary sort family, resolved through the same generic path as any other declared sort (visit(ISort.IApplication) already has a special case unfolding -> via its :right-assoc attribute when given more than its declared arity of 2 arguments -- see the comment there). So rather than fabricating a placeholder sort (e.g. just the body's sort) or throwing a not-yet-supported error, this builds an (unchecked) (-> paramSort1 ... paramSortN bodySort) sort-application node and runs it through this same type checker, exactly the way makeBitVec()/makeFloatingPoint()/makeReal() above already construct-then-check a sort expression rather than hand-building one. Two honest, non-fabricated outcomes follow directly from reusing that existing machinery, with no new logic of its own:

• If the active logic/theory declares -> (i.e. HO-Core is loaded, as with (set-logic ALL)), the lambda's sort is the real, correctly-computed function sort -- e.g. (-> Int Int) for (lambda ((x Int)) (+ x 1)).
• If it does not, this reports the same "No such sort symbol declared: ->" error that any other undeclared sort symbol would get -- exactly like using any other theory-specific symbol without its theory loaded, not a crash or a silently-wrong sort.

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.ILet e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(IExpr.IMatch e)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISort.IApplication s)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISort.IFamily s)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISort.IParameter s)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISort.IAbbreviation s)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

visit

public ISort visit(ISort.IFcnSort s)
            throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<ISort>

Throws:

IVisitor.VisitorException

validate

public static List<IResponse> validate(SMT.Configuration smtConfig,
 ICommand cmd)

Validates non-syntactic well-formedness of a command (user IDs, duplicate names, list sizes). Returns a list of errors; an empty list means the command is well-formed.

validateDatatypeNames

public static List<IResponse> validateDatatypeNames(SymbolTable symTable,
 SMT.Configuration smtConfig,
 List<IExpr.ISortDeclaration> sortDecls,
 List<ISort.IDatatype> datatypes)

Checks that constructor and selector names introduced by a datatype group are not already defined (neither in the symbol table nor duplicated within the group). Returns any errors found; empty list means all names are fresh.