將c＃語句轉換爲z3格式

Question

我正在用c＃編寫代碼。

在代碼中有各種IF條件。我想將這些條件傳遞給z3約束求解器，並檢查它的可滿足性並獲得可以保證它的值。 （我在我的代碼中進一步使用這些值）

如果我在代碼中使用IF條件並在z3語法中編寫其等效聲明，那麼它工作正常。但我想泛化的意思是在c＃中聲明一個語句，我想用z3語法生成它的相應語句。

無論如何我能做到嗎？

Answer 1

C＃語言不提供必要的掛鉤，因此您可以在運行時檢測到if語句的存在。你無法察覺的東西不能告訴Z3。

您可以使用Roslyn將包含C＃代碼的字符串解析爲AST並將其轉換爲Z3。對於簡單的情況可能並不難。這爲循環控制流程打破了。你可以使它適用於常見的非循環結構，如變量，運算符，if,switch。