我可以使用z3来“简化”smt2 2文件吗？

Question

我想使用一些z3策略来修改".smt2“文件中的表达式。我这样做是为了让其他SMT解决者(cvc、mathsat等)能够从z3战术中受益，即使他们不支持他们。

下面是一个如何通过Z3的Python来实现的示例：

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上询问，这是SMTLib社区中的人订阅的。