如何在 Z3 Solver 中定义未声明的类型答案

【问题标题】：How to define un-declared type in Z3 Solver如何在 Z3 Solver 中定义未声明的类型
【发布时间】：2020-10-26 14:29:39
【问题描述】：

我正在使用SMT Solver Z3 来解决约束。例如：

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)

// SAT

但是，如果我们不知道变量a的类型是什么，有没有办法定义未声明的变量并通过解决约束得到该变量的预期结果

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

简短回答：不。

SMTLib（z3 和许多其他 SMT 求解器接受的语言）是一个多排序的一阶逻辑。这意味着每个变量在其声明期间都必须具有已知类型。该类型可以是语言支持的基本类型之一（Int、Real、Bool 等），也可以是用户定义的类型，通过 declare-datatype 或 declare-sort 构造。

详见语言定义：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

如果您尝试对“动态”类型语言（如 Lisp、Python 等）进行建模，那么通常的技巧是声明变量可以属于的类型联合，并在您解释时相应地切换那种语言。但是直接在 SMTLib 中这样做可能相当冗长且容易出错，您最好使用 z3py 之类的高级接口或任何与 z3 的高级语言绑定，如 Java、C、Haskell、Scala 等. 但是在任何这些编码中，您需要确保正确存储和更改类型，SMTLib 的基础语言将保持强类型，如我上面链接的标准中所述。

【讨论】：