z3 - 为 Z3 和/或 SMT(v2.6) 建模通用数据类型

Question

我想在 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 需要做一些类型推断。

如果你能给我一个提示就太好了。

Answer 1

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.

在 Footnote-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.

因此，正如您所怀疑的，您不能在用户级别定义“多态”函数。但正如脚注所示，此限制将来可能会被取消，这很可能会随着 SMT 求解器的更广泛部署而发生。然而，这究竟会在什么时候发生，是任何人的猜测。