使用Z3編碼語言語法並枚舉所有接受的終端（Z3py）

Question

我有一個問題，我想使用Z3進行編程。但是，我不確定最好的辦法是什麼。這裏是我想要編碼和預期輸出的描述。

如果我有一個語言的語法，其中x，y和z都是非端子與 「和」， 「或」 和 「a」 是語言端子：

1. X :: = y「的或」 y

   | y 
   

2. ŷ:: = Z 「和」 z

   | z 
   

3. ž:: = 「一」

我想首先編碼以前的規則，然後我想要生成語法接受的所有可能的終端派生。

最終輸出將是：

一個和一個或一個和

一個或一個

一個和

一個和一個或一個

一個或a和

...

我不知道從哪裏開始。什麼是編碼問題的最佳方式？

任何建議/指導是非常讚賞..

感謝

Answer 1

使用Z3產生的約束系統中所有可能的解決方案的典型方法是將它反覆地「禁止」之前找到解決方案作爲新的（消極）約束。見Leo's answer至this question。