我可以将Z3仅用于“简化” SMT2文件

Question

我想使用一些Z3策略来修改“ .smt2”文件中的表达式。 我正在这样做，以便其他SMT垫圈（CVC，Mathsat等）可以从Z3策略中受益，即使它们不支持它们。

这是一个可以通过Z3的Python API完成的示例：

def simplify_smt2_file(file_path: str) -> str:
    tactics = ("simplify", "solve-eqs", "propagate-values", "simplify")
    query = z3.parse_smt2_file(file_path)
    goal = z3.Goal()
    goal.add(query)
    simplified = z3.Then(*tactics)(goal).as_expr()
    solver = z3.SolverFor("NIA")
    solver.add(simplified)
    return solver.sexpr()

但是，我不需要使用Python。有没有办法通过Z3的SMT2接口进行操作？

Answer 1

据我所知，使用Smtlib界面没有简单的方法来执行此操作。如果您一定会使用Smtlib，则必须从字面上运行Z3，解析输出并将其馈回其他求解器。

请随时在 https://groups.google.com/g/smt-lib < /a>，由Smtlib社区中的人们订阅。