z3py：来自 (check-sat ...) 语句的假设

Question

有没有办法将 SMT2 公式的 (check-sat ...) 语句中的假设传递给求解器？

考虑以下存储在 ex.smt2 中的示例公式：

# cat ex.smt2 
(declare-fun p () Bool)
(assert (not p))
(check-sat p)

如预期的那样，在其上运行 z3 会产生 unsat。现在，我想通过 z3py 接口用假设 (p) 来解决：

In [30]: ctx = z3.Context()
In [31]: s = z3.Solver(ctx=ctx)
In [32]: f = z3.parse_smt2_file("ex.smt2", ctx=ctx)
In [33]: s.add(f)
In [34]: s.check()
Out[34]: sat

是否有一个 API 可以从解析器中获取假设（即本例中的 (p)）？或者更好的是，只是告诉求解器使用从输入文件中读取的假设来求解？

Answer 1

不，没有这样的 API。 parse_smt2_file API 非常简单，只提供对输入文件中断言的访问。扩展此 API 已在 TODO 列表中，但目前没有人致力于此。