非零元未解释排序的含义、SMT-LIB用法及Z3 C API实现

SMT-LIB中的参数化未解释排序 #

SMT-LIB支持通过arity参数声明参数化的未解释排序，示例如下：

(declare-sort MySort 2)

声明后，使用该排序时必须传入对应数量的排序参数，比如声明常量：

(declare-const x (MySort Int Real))

常见疑问解答 #

1. (MySort X Y)的实例是否完全独立？ #

是的，每一组不同参数组合生成的排序实例都是完全独立的未解释排序。比如(MySort Int Real)和(MySort Real Int)、(MySort Bool Bool)，这些排序互相没有关联，Z3不会在它们之间建立任何隐式关系。

2. 无法声明参数化函数时，该特性的用途是什么？ #

即便不能直接声明参数化函数，这个特性依然有不少实用场景：

• 模拟简单泛型结构：比如用(Pair A B)表示一对A、B类型的值，虽然不能写通用的fst函数，但可以针对具体实例声明函数，比如(declare-fun fst_Int_Real ((Pair Int Real)) Int)处理特定Pair实例。
• 区分不同语境的同类概念：比如用(Id User)和(Id Product)分别表示用户ID和商品ID，避免不同类型ID被意外混淆，提升公式的类型安全性。
• 模块化建模：用参数化排序定义通用结构模板，在不同模块中实例化不同参数，保持模型的清晰性。

Z3 C API实现参数化未解释排序 #

Z3的C API没有直接提供带arity的未解释排序创建函数，但可以通过**排序构造器（sort constructor）**模拟该特性，步骤如下：

1. 创建排序构造器：使用Z3_mk_sort_constructor函数，指定构造器名称和参数数量（即arity）。
2. 实例化排序构造器：调用Z3_mk_apply_sort函数，传入构造器和对应参数排序，得到具体实例排序。

示例代码片段：

// 创建上下文
Z3_context ctx = Z3_mk_context(Z3_mk_config());

// 创建arity为2的排序构造器MySort
Z3_symbol name = Z3_mk_string_symbol(ctx, "MySort");
Z3_sort_constructor sc = Z3_mk_sort_constructor(ctx, name, 2, NULL, NULL);

// 获取Int和Real排序
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort real_sort = Z3_mk_real_sort(ctx);

// 实例化(MySort Int Real)排序
Z3_sort my_sort_instance = Z3_mk_apply_sort(ctx, sc, 2, (Z3_sort[]){int_sort, real_sort});

// 用实例排序声明常量
Z3_symbol x_name = Z3_mk_string_symbol(ctx, "x");
Z3_func_decl x = Z3_mk_const(ctx, x_name, my_sort_instance);

// 清理资源
Z3_del_context(ctx);

注意：排序构造器本身不是一个可直接使用的排序，必须通过Z3_mk_apply_sort实例化后才能作为排序使用，这和SMT-LIB中(declare-sort MySort 2)的语义完全对应。

内容的提问来源于stack exchange，提问作者Nicola Gigante