Request for Z3 SMT-LIB Grammar Specification

[eitanturok]

I'm looking for a formal grammar specification that defines Z3's syntax. My goal is to use this grammar with structured generation techniques to ensure my language model produces valid Z3 code.

I've searched for existing resources but haven't found a complete solution. Both GitHub issue #31 and this Stack Overflow post provide partial information but lack comprehensive grammar definitions.

Could someone point me to:

• An official or community-maintained grammar specification for Z3
• Alternative approaches for constraining LLM output to valid Z3 syntax
• Documentation that might contain the grammar rules

I'd appreciate any guidance.

[NikolajBjorner]

Z3 uses a mild extension of https://smt-lib.org/language.shtml
For other features, the easiest nowadays would be to throw AI at the z3guide documentation pages to generate a grammar with commands it supports.