我刚刚开始，我很好奇是否有办法添加假设。使用 (assert ...) 不是我想要的，因为我的应用程序有时允许假设是错误的，因此一切都应该变得令人满意。我知道我可以只使用诸如（断言（暗示假设结论））之类的含义，但是如果有很多假设，将我的所有断言都转换为含义似乎很笨拙。大致我想要一个交互模型
（认为 ...）
...
（认为 ...）
（断言...）
...
（断言...）
（检查周六）
问问题
189 次
1 回答
1
使用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 公式。
您可能还对此感兴趣：Z3 中的软/硬约束
于 2013-09-23T12:03:48.887 回答