为 Z3 和/或 SMT(v2.6) 建模通用数据类型
Modelling generic datatypes for Z3 and or SMT(v2.6)
我想在 SMT v2.6 中模拟通用数据类型的行为。我使用 Z3 作为约束求解器。我基于 official example，按照以下方式将通用列表建模为参数化数据类型：
(declare-datatypes (T) ((MyList nelem (cons (hd T) (tl MyList)))))
我希望列表在数据类型方面是通用的。稍后，我想通过以下方式声明常量：
(declare-const x (MyList Int))
(declare-const y (MyList Real))
但是，现在我想在通用数据类型 MyList 上定义函数（例如，长度操作、空操作......），以便它们可重复用于所有 T的。你知道我怎样才能做到这一点吗？我确实尝试过类似的东西：
(declare-sort K)
(define-fun isEmpty ((in (MyList K))) Bool
(= in nelem)
)
但这给了我一条错误信息；我想，为了让这个例子工作，Z3 需要做一些类型推断。
如果你能给我一个提示就太好了。
SMT-Lib 不允许多态的用户定义函数。 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 4.1.5 节指出：
Well-sortedness checks, required for commands that use sorts or terms,
are always done with respect to the current signature. It is an error
to declare or define a symbol that is already in the current
signature. This implies in particular that, contrary to theory
function symbols, user-defined function symbols cannot be overloaded.
在脚注 29 中进一步扩展：
The motivation for not overloading user-defined symbols is to simplify
their processing by a solver. This restriction is significant only for
users who want to extend the signature of the theory used by a script
with a new polymorphic function symbol—i.e., one whose rank would
contain parametric sorts if it was a theory symbol. For instance,
users who want to declare a “reverse” function on arbitrary lists,
must define a different reverse function symbol for each (concrete)
list sort used in the script. This restriction might be removed in
future versions.
因此，正如您所怀疑的，您无法在用户级别定义 "polymorphic" 函数。但正如脚注所示，此限制将来可能会被取消，这很可能会随着 SMT 求解器的更广泛部署而发生。然而，确切的时间可能会发生，这是任何人的猜测。
我想在 SMT v2.6 中模拟通用数据类型的行为。我使用 Z3 作为约束求解器。我基于 official example，按照以下方式将通用列表建模为参数化数据类型：
(declare-datatypes (T) ((MyList nelem (cons (hd T) (tl MyList)))))
我希望列表在数据类型方面是通用的。稍后，我想通过以下方式声明常量：
(declare-const x (MyList Int))
(declare-const y (MyList Real))
但是，现在我想在通用数据类型 MyList 上定义函数（例如，长度操作、空操作......），以便它们可重复用于所有 T的。你知道我怎样才能做到这一点吗？我确实尝试过类似的东西：
(declare-sort K)
(define-fun isEmpty ((in (MyList K))) Bool
(= in nelem)
)
但这给了我一条错误信息；我想，为了让这个例子工作，Z3 需要做一些类型推断。
如果你能给我一个提示就太好了。
SMT-Lib 不允许多态的用户定义函数。 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 4.1.5 节指出：
Well-sortedness checks, required for commands that use sorts or terms, are always done with respect to the current signature. It is an error to declare or define a symbol that is already in the current signature. This implies in particular that, contrary to theory function symbols, user-defined function symbols cannot be overloaded.
在脚注 29 中进一步扩展：
The motivation for not overloading user-defined symbols is to simplify their processing by a solver. This restriction is significant only for users who want to extend the signature of the theory used by a script with a new polymorphic function symbol—i.e., one whose rank would contain parametric sorts if it was a theory symbol. For instance, users who want to declare a “reverse” function on arbitrary lists, must define a different reverse function symbol for each (concrete) list sort used in the script. This restriction might be removed in future versions.
因此，正如您所怀疑的，您无法在用户级别定义 "polymorphic" 函数。但正如脚注所示，此限制将来可能会被取消，这很可能会随着 SMT 求解器的更广泛部署而发生。然而，确切的时间可能会发生，这是任何人的猜测。