title: Encoding a language grammar and Enumerating all accepted terminals using Z3 (Z3py)
body: <p>I have a problem that I want to formulate using Z3. However, I not sure what is the best way to do that. Here is a description of what I want to encode and the anticipated output.</p>
  
  <p>If I have a language grammar where x, y and z are non-terminals and "and", "or" and "a" are the language terminals:</p>
  
  <ol>
  <li><p>x ::= y "or" y </p>
  
  <pre><code>   | y  
  </code></pre></li>
  <li><p>y ::= z "and" z </p>
  
  <pre><code>  | z 
  </code></pre></li>
  <li>z ::= "a"</li>
  </ol>
  
  <p>I want first to encode the previous rules and then I want to generate All possible terminal derivations that are accepted by the grammar.</p>
  
  <p>The ultimate output would be : </p>
  
  <p>a and a or a and a </p>
  
  <p>a or a</p>
  
  <p>a and a </p>
  
  <p>a and a or a </p>
  
  <p>a or a and a </p>
  
  <p>...</p>
  
  <p>I do not know where to start. What is the best way to encode the problem?</p>
  
  <p>Any suggestion/guidance is very appreciated..</p>
  
  <p>Thanks     </p>