我剛剛開始，我很好奇，如果有一種方法來添加假設。使用（assert ...）並不是我想要的，因爲有時我的應用程序允許假設爲假，因此所有事情都應該可以滿足。我知道我可以使用諸如（斷言（暗示假設結論））的含義，但如果有很多假設，似乎笨拙地將我的所有斷言轉化爲含義。大概我想有一個像是否有一種在Z3中添加假設假設的一般方法？
的交互模型（假設...）
...
（假設...）
（斷言...）
...
（斷言...）
（檢查-SAT）
使用assert暗示是要走的路，沒有assume（參見SMT-LIB手冊，3.9節，http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf）。
如果你想爲假設使用許多斷言，您可能希望使用編程API中的一個，以幫助自動化這個轉換對您：http://z3.codeplex.com/documentation
另外，如果斷言是很簡單，您可以編寫一個腳本，對斷言的字符串表示進行操作以打印具有含義的SMT-LIB公式。
您可能也有興趣：Soft/Hard constraints in Z3