我刚刚开始，我很好奇，如果有一种方法来添加假设。使用（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