Z3:将 Z3py 表达式转换为 SMT-LIB2? [英] Z3: convert Z3py expression to SMT-LIB2?

问题描述

给定 Z3py 中的表达式，我可以将其转换为 SMT-LIB2 语言吗?(所以我可以将此 SMT-LIB2 表达式提供给其他支持 SMT-LIB2 的 SMT 求解器)

Given an expression in Z3py, can I convert that to SMT-LIB2 language? (So I can feed this SMT-LIB2 expression to other SMT solvers that support SMT-LIB2)

如果可以，请举一个例子.

If this is possible, please give one example.

非常感谢.

推荐答案

我们可以使用 C API Z3_benchmark_to_smtlib_string.C API 中的每个函数都可以在 Z3Py 中使用.此函数最初用于转储 SMT 1.0 格式的基准测试，它早于 SMT 2.0.这就是为什么它有一些看起来不必要的参数.现在，默认情况下，它将以 SMT 2.0 格式显示基准.输出不意味着人类可读.我们可以编写如下Python函数，使用起来更加方便:

We can use the C API Z3_benchmark_to_smtlib_string. Every function in the C API is available in Z3Py. This function was initially used to dump benchmarks in SMT 1.0 format, and it predates SMT 2.0. That is why it has some parameters that may seem unnecessary. Now, by default, it will display benchmarks in SMT 2.0 format. The output is not meant to be human readable. We can write the following Python function to make it more convenient to use:

def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

这是一个使用它的小例子(也可以在线这里获得)

Here is a small example using it (also available online here)

a = Int('a')
b = Int('b')
f = And(Or(a > If(b > 0, -b, b) + 1, a <= 0), b > 0)
print toSMT2Benchmark(f, logic="QF_LIA")

这篇关于Z3:将 Z3py 表达式转换为 SMT-LIB2?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！