declare-const是啥意思

`declare-const` 是 SMT-LIB 语言中的一个命令，用于声明一个常量。与 `declare-fun` 命令不同的是，`declare-const` 声明的常量没有参数，只有一个返回类型。

语法如下：

(declare-const <const_name> <type>)

其中 `<const_name>` 是常量的名称，`<type>` 是常量的类型。

例如，声明一个布尔类型的常量 `b`：

(declare-const b Bool)

声明一个整数类型的常量 `n`：

(declare-const n Int)

和 `declare-fun` 命令一样，`declare-const` 命令也是用于描述 SMT 问题的，可以与其他 SMT 命令结合使用来描述约束条件和求解问题。