search

SemGuS-git / Semgus-Parser

Library and tool for parsing SemGuS specifications
MIT License
4 stars 1 forks source link

Lift some restrictions on symbol naming #19

Closed kjcjohnson closed 3 years ago

kjcjohnson commented 3 years ago

We want to be able to support symbols like 0.Syn in certain positions in the grammar, despite them not being SMT-LIB2 conformant. To this end, we should:

  1. Allow reading these symbols
  2. Add new properties to the SymbolToken record, whether a symbol is 1) SMT-LIB2-compliant, 2) internally-reserved (starting with . or @, per SMT-LIB2), and 3) an SMT-LIB2 reserved word.
  3. Ensure that all symbols used in relations and constraints are SMT-LIB2-compliant, while allowing non-compliant symbols in other positions.