z3 - 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

No, there is no such API. The parse_smt2_file API is very simple, and only provides access to the assertions in the input file. Extending this API is in the TODO list, but nobody is currently working on that.