Package org.smtlib

Class SymbolTable

java.lang.Object
org.smtlib.SymbolTable
public class SymbolTable extends Object
This class manages a symbol table used for storing definitions and looking up ids in expressions. The table maps names to Entry objects that hold information about the defined symbol.

Deliberately a concrete class rather than an interface: there is exactly one implementation, constructed directly by every caller, with no substitutability need to abstract over. See issue #36.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static class 
    SymbolTable.Entry
    An object that holds all the information about the defined symbol (or aliased definition).
    static class 
    SymbolTable.Iterator
    An iterator over all of the Symbols in the symbol scope stack from the top-most scope on down.

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    boolean
    bitVectorTheorySet
    true if the bit-vector theory has been set
    boolean
    floatingPointTheorySet
    true if the FloatingPoint theory has been set
    ILogic
    logicInUse
    The logic that is being used - this value is used to check that expressions, etc., conform to the language restrictions of the current logic.
    boolean
    realsIntsTheorySet
    true if the RealsInts theory is set (which allows implicit promotion of ints to reals)
    SMT.Configuration
    smtConfig
    A reference to the Configuration for this instance of SMT.

  • Constructor Summary

    Constructors
    Constructor
    Description
    SymbolTable(SMT.Configuration smtConfig)
    Constructs an empty symbol table

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    add(SymbolTable.Entry entry, boolean global)
    Adds the given entry to the symbol table.
    boolean
    add(SymbolTable.Entry entry, boolean global, boolean overload)
    Adds the given entry to the symbol table; if overload is false and the identifier in the entry is already in the table, the method returns false (without changing the symbol table); otherwise the entry is added and the method returns true
    void
    addDatatypeConstructors(IExpr.IIdentifier sortName, List<IExpr.ISymbol> ctors, boolean global)
    Records a datatype's constructors, in the frame its sort was added to (global = background, else current).
    void
    addLogicSymbol(IExpr.IIdentifier id, boolean sort)
    Records a function (sort, if sort is true) symbol declared by the logic or one of its theories
    boolean
    addSortDefinition(IExpr.IIdentifier identifier, List<ISort.IParameter> parameters, ISort definition, boolean global)
    Adds a new sort abbreviation definition to the given frame (global = background, else current).
    boolean
    addSortDefinition(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes, boolean global)
    Adds a new sort family definition, with attributes (e.g.
    boolean
    addSortParameter(IExpr.ISymbol symbol, boolean global)
    Adds the given symbol as a sort to the top scope of the sort table; returns false if the given symbol is already in the top scope (and the sort table is unchanged); returns true if the symbol is not already in the top scope.
    String
    ambiguousConstant(IExpr.IIdentifier name)
    Returns an error message if more than one constant (arity 0) named `name` is declared, so that a bare use of it needs an `as` qualifier; otherwise null.
    void
    clear(boolean keepBackground)
    Leaves the background frame and an empty primary frame, the state after set-logic; keepBackground false empties the background frame too.
    static boolean
    containsParameter(ISort sort)
    Whether the sort contains a sort parameter.
    List<IExpr.ISymbol>
    datatypeConstructors(IExpr.IIdentifier sortName)
    The constructors of the datatype sort with the given identifier, or null if no datatype of that name is in scope.
    boolean
    isLogicSymbol(IExpr.ISymbol s, boolean sort)
    Whether the symbol is a function (sort, if sort is true) symbol of the logic or its theories
    SymbolTable.Iterator
    iterator()
    Returns a fresh iterator over the symbol table's contents
    ISort.IFcnSort
    lookup(int arity, IExpr.IIdentifier name)
    Lookup the Symbol with the given identifier and arity, returning its Sort.
    List<SymbolTable.Entry>
    lookup(IExpr.IIdentifier name)
    Lookup the Symbol with the given identifier, returning all of its declared entries (of any arity).
    ISort
    lookup(IExpr.IIdentifier name, List<ISort> argSorts, ISort resultSort, StringBuilder reason)
    Lookup a Symbol with the given name and argument Sorts and result Sort.
    ISort.IFcnSort
    lookupInstance(int arity, IExpr.IIdentifier name, ISort resultSort)
    The signature of the arity-n function name, instantiated so that its result sort is resultSort (a par entry's parameters are bound by unification), or null if there is no such function or its result sort cannot be resultSort.
    ISort.IDefinition
    lookupSort(IExpr.IIdentifier name)
    Looks up the Sort definition with the given name
    void
    merge()
    Combines the top two symbol scopes, removing the current top scope; presumes that there is no shadowing of symbols; the top sort scope is discarded.
    void
    pop()
    Removes the top frame from the symbol table stack.
    void
    push()
    Adds a new empty frame on the top of the symbol table stack.

    Methods inherited from class java.lang.Object

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

  • Field Details

    • bitVectorTheorySet

      public boolean bitVectorTheorySet
      true if the bit-vector theory has been set

    • realsIntsTheorySet

      public boolean realsIntsTheorySet
      true if the RealsInts theory is set (which allows implicit promotion of ints to reals)

    • floatingPointTheorySet

      public boolean floatingPointTheorySet
      true if the FloatingPoint theory has been set

    • logicInUse

      public ILogic logicInUse
      The logic that is being used - this value is used to check that expressions, etc., conform to the language restrictions of the current logic.

    • smtConfig

      public SMT.Configuration smtConfig
      A reference to the Configuration for this instance of SMT.

  • Constructor Details

    • SymbolTable

      public SymbolTable(SMT.Configuration smtConfig)
      Constructs an empty symbol table

  • Method Details

    • iterator

      public SymbolTable.Iterator iterator()
      Returns a fresh iterator over the symbol table's contents

    • clear

      public void clear(boolean keepBackground)
      Leaves the background frame and an empty primary frame, the state after set-logic; keepBackground false empties the background frame too.

    • addLogicSymbol

      public void addLogicSymbol(IExpr.IIdentifier id, boolean sort)
      Records a function (sort, if sort is true) symbol declared by the logic or one of its theories

    • isLogicSymbol

      public boolean isLogicSymbol(IExpr.ISymbol s, boolean sort)
      Whether the symbol is a function (sort, if sort is true) symbol of the logic or its theories

    • push

      public void push()
      Adds a new empty frame on the top of the symbol table stack.

    • addDatatypeConstructors

      public void addDatatypeConstructors(IExpr.IIdentifier sortName, List<IExpr.ISymbol> ctors, boolean global)
      Records a datatype's constructors, in the frame its sort was added to (global = background, else current).

    • datatypeConstructors

      public List<IExpr.ISymbol> datatypeConstructors(IExpr.IIdentifier sortName)
      The constructors of the datatype sort with the given identifier, or null if no datatype of that name is in scope.

    • merge

      public void merge()
      Combines the top two symbol scopes, removing the current top scope; presumes that there is no shadowing of symbols; the top sort scope is discarded.

    • pop

      public void pop()
      Removes the top frame from the symbol table stack. The symbol table must have at least one non-background scope or an InternalException will be thrown.

    • addSortParameter

      public boolean addSortParameter(IExpr.ISymbol symbol, boolean global)
      Adds the given symbol as a sort to the top scope of the sort table; returns false if the given symbol is already in the top scope (and the sort table is unchanged); returns true if the symbol is not already in the top scope.
      Parameters:
      symbol - the symbol to add
      Returns:
      true if successfully added, false if already present

    • addSortDefinition

      public boolean addSortDefinition(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes, boolean global)
      Adds a new sort family definition, with attributes (e.g. :right-assoc; null or empty if none), to the given frame (global = background, else current).
      Parameters:
      identifier - the identifier of the new Sort definition
      arity - the arity of the new Sort definition
      attributes - any attributes declared on the sort symbol (null or empty if none)
      global - if true, add to the background frame; otherwise add to the current frame
      Returns:
      true if successfully added, false if there already is a sort (in any scope) with this identifier

    • addSortDefinition

      public boolean addSortDefinition(IExpr.IIdentifier identifier, List<ISort.IParameter> parameters, ISort definition, boolean global)
      Adds a new sort abbreviation definition to the given frame (global = background, else current).
      Parameters:
      identifier - the name of the new Sort definition
      parameters - the names of the parameters of the Sort abbreviation
      definition - the expression of the Sort abbreviation
      global - if true, add to the background frame; otherwise add to the current frame
      Returns:
      true if successfully added, false if there already is a sort by this name in the target scope

    • lookupSort

      public ISort.IDefinition lookupSort(IExpr.IIdentifier name)
      Looks up the Sort definition with the given name
      Parameters:
      name - the name of the Sort definition to find
      Returns:
      null if not found

    • lookup

      public ISort.IFcnSort lookup(int arity, IExpr.IIdentifier name)
      Lookup the Symbol with the given identifier and arity, returning its Sort.
      Parameters:
      arity - the arity of the Symbol
      name - the name of the Symbol
      Returns:
      null if not found, the Sort of the Symbol if found

    • lookup

      public List<SymbolTable.Entry> lookup(IExpr.IIdentifier name)
      Lookup the Symbol with the given identifier, returning all of its declared entries (of any arity).
      Parameters:
      name - the name of the Symbol
      Returns:
      null if not found, the corresponding List<Entry> from the top-most scope in which the identifier is found

    • lookup

      public ISort lookup(IExpr.IIdentifier name, List<ISort> argSorts, ISort resultSort, StringBuilder reason)
      Lookup a Symbol with the given name and argument Sorts and result Sort.
      Parameters:
      name - the name to find
      argSorts - the Sorts of the arguments
      resultSort - the expected result sort (from an `as` qualifier), or null if none given
      reason - if not null and this call returns null because some candidate(s) were found for `name` but none matched, set to a diagnostic message: the one candidate's own specific reason if there was exactly one, or a generic "no match" message listing the available signatures if there was more than one (overloading is rare, so a pile of per-candidate reasons is more noise than help once there's more than one to explain). Left untouched if `name` has no declared candidates at all, or if a match is found.
      Returns:
      the result Sort of the matching declaration, or null if none matches

    • ambiguousConstant

      public String ambiguousConstant(IExpr.IIdentifier name)
      Returns an error message if more than one constant (arity 0) named `name` is declared, so that a bare use of it needs an `as` qualifier; otherwise null.

    • containsParameter

      public static boolean containsParameter(ISort sort)
      Whether the sort contains a sort parameter.

    • lookupInstance

      public ISort.IFcnSort lookupInstance(int arity, IExpr.IIdentifier name, ISort resultSort)
      The signature of the arity-n function name, instantiated so that its result sort is resultSort (a par entry's parameters are bound by unification), or null if there is no such function or its result sort cannot be resultSort. Used for constructor patterns, whose sort comes from the match scrutinee.

    • add

      public void add(SymbolTable.Entry entry, boolean global)
      Adds the given entry to the symbol table.
      Parameters:
      entry - the Entry to add

    • add

      public boolean add(SymbolTable.Entry entry, boolean global, boolean overload)
      Adds the given entry to the symbol table; if overload is false and the identifier in the entry is already in the table, the method returns false (without changing the symbol table); otherwise the entry is added and the method returns true
      Parameters:
      entry - the Entry to add