此文件是否符合 SMT2.0 标准？

Question

Click to see the file

此文件是否符合 SMT2.0 标准？至少，z3 可以接受它。顺便说一句，“declare-const”和“declare-fun”有什么区别？例如，为了声明一个 Bool 变量，我可以写 declare-const a Bool 或 declare-fun a() Bool。

Answer 1

我无法找到您在帖子中提到的文件，但要回答您关于 declare-const 的问题：

(declare-const a Bool) 

意思和

一样

(declare-fun a () Bool)

declare-const 不是标准 SMT-LIB2 的一部分。 是为了方便Z3添加的命令 手动输入 SMT-LIB2 基准。你可以 始终使用 declare-fun 来兼容 跨求解器。

虽然 Z3 可以处理符合 SMT-LIB2 的文件。 另一方面，Z3 的输入格式还有其他几个扩展 不属于 SMT-LIB2 标准的部分。 提一些：

• 声明数据类型。代数数据类型的声明是 Z3 特定的扩展。

• 策略和求解器。战术的创建、组合和应用是 Z3 特有的。

• declare-rel、declare-var、规则、查询。定点求解器使用这些命令是为了方便将基准作为 Horn 公式输入。