Microsoft Z3命名聲明

Question

我需要在我的z3模型中聲明一些聲明，以便它能夠生成不飽和核心。

我可以手動執行此操作是這樣的：

(assert (! (assertion) :named x)) 

我只需要直接使用.NET API來做到這一點。

有幫助嗎？

Answer 1

Z3不直接通過.NET API支持此操作。取而代之的是，一個布爾常數應被創建（名稱，例如，x），然後可將其用於斷言條件的限制，例如，

solver.AssertAndTrack(constraint, x); 

該約束然後命名x和該常量用於指它在不飽和的核心。 有關Python中的示例，另請參閱此其他question;該策略在.NET API中是相同的，只是函數名稱略有不同。