將java布爾表達式轉換爲SMTlib

Question

我嘗試將java布爾表達式轉換爲Z3能夠理解的格式時遇到一些問題。由於項目的一些要求，我無法使用任何其他工具評估表達式。只有標識符可用於表達式中，而不是函數或更復雜的類型。

我也考慮過這種可能性是：

• 使用半熟或類似的工具建立一個解析器。這樣做的缺點是，我只想在將操作員轉換到SMT等效位置並可能添加括號後將其放置在放置操作員的位置，因此，此解決方案和涉及AST處理的工作似乎對我而言過度勞累。而且，我發現定義一個可以適合所有嵌套層次的語法有點複雜。

• 使用詞法分析器或其他類型的工具獲取令牌，然後使用類似於Shunting-yard algorithm的算法對其進行重新排序。在這種情況下，可能需要輸入所有的括號以避免某些問題。

• 使用可以解析表達式並讓其進行編輯的庫。到目前爲止，我還沒有發現任何東西，只能讓你評估表達的工具。

• 使用可以在符號之間直接轉換的東西。我一直在尋找，但我無法找到。儘管如此，這將使我的一天。

我查找過類似的問題，但我還沒有找到任何東西。我會欣賞你可能有的任何想法。提前致謝！

Answer 1

你考慮過TXL嗎？ TXL爲解析文件提供支持，將轉換應用於抽象語法樹並打印結果。它很容易使用，而且它們有很多文檔和大量的語法（包括Java）。

Answer 2

您可以使用免費軟件工具bc2ncf將您的布爾表達式轉換爲CNF（連接範式），而不是SMT。 Z3能夠輸入CNF並解決包含的可滿足性問題。

Z3的命令行語法會不時變化。 前段時間，我用瞭如下的東西：

bc2cnf.exe -v test.bc.txt test.dimacs.txt 

z3.exe /dimacs /v:1 test.dimacs.txt > test.solution.txt