Package org.smtlib

Class TypeChecker.Variable

java.lang.Object

org.smtlib.TypeChecker.Variable

Enclosing class:

TypeChecker

public static class TypeChecker.Variable
extends Object

Field Summary

Fields

Modifier and Type	Field	Description
boolean	closed	Whether a reference to this variable is itself closed (no free/bound variable reachable through it) -- false for a quantifier- or match-pattern-bound variable (which IS the free variable), true for a let-bound variable whose own defining expression was itself closed when the let was checked, false for one that wasn't (e.g.
IExpr	expression
ISort	sort
IExpr.ISymbol	symbol

Constructor Summary

Constructors

Constructor	Description
Variable(IExpr.ISymbol sym, ISort sort, IExpr expr, boolean closed)

Method Summary

Methods inherited from class java.lang.Object

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

Field Details

symbol

public IExpr.ISymbol symbol

sort

public ISort sort

expression

public IExpr expression

closed

public boolean closed

Whether a reference to this variable is itself closed (no free/bound variable reachable through it) -- false for a quantifier- or match-pattern-bound variable (which IS the free variable), true for a let-bound variable whose own defining expression was itself closed when the let was checked, false for one that wasn't (e.g. (forall ((q Bool)) (let ((r q)) ...)): referencing r is not closed, because r's value is the outer free q). See visit(ISymbol)/visit(ILet).

Constructor Details

Variable

public Variable(IExpr.ISymbol sym,
 ISort sort,
 IExpr expr,
 boolean closed)