问题描述
我正在使用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是什么类型，有什么方法可以定义未声明的变量并通过求解约束来获得该变量的预期结果
解决方法
简短答案：否
SMTLib（z3和许多其他SMT求解器接受的语言）是种类繁多的一阶逻辑。这意味着每个变量在声明期间都必须具有已知的类型。类型可以是语言支持的基本类型之一（Int，Real，Bool等），也可以是用户定义的类型，可以通过{{1 }}或declare-datatype构造。
有关详细信息，请参见语言定义：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
如果您要对“动态”类型的语言（例如Lisp，Python等）建模，则通常的技巧是声明变量可以属于的类型的并集，并在解释时进行相应的切换这种语言。但是直接在SMTLib中这样做可能很冗长且容易出错，最好使用Java，C，Haskell，Scala等高级接口（例如z3py或任何高级语言绑定到z3）但是，在上述任何一种编码中，您都需要确保正确存储和更改类型，SMTLib的基础语言将保持强类型，如上面我链接的标准所述。