Z3 - check-sat-using 的参数

Question

抱歉，如果这是一个愚蠢的问题 - 我对使用 Z3（和一般的 SMT）很陌生 - 但我有点难过。

假设我有两个SMT2输入语言的文件，略有不同，总结如下：

(define-fun T ((i Int)) Bool (... - too long to paste completely, but does define $prop)
(assert (T 0))
(declare-fun assum1 () Bool)
(assert (=> assum1 (not (and ($prop 0)))))
(check-sat assum1)

现在，其中之一（更简单的）返回“sat”，具有更复杂非线性数学的变体返回“未知”。

我认为更复杂的变体可以使用非线性求解器（例如 qfnra-nlsat 或其他策略）来求解，但尝试将其与 check-sat-using 一起使用：

(check-sat-using qfnra-nlsat assum1)

返回：

(error "line 246 column 29: invalid command argument, keyword expected")

但是，没有明确命名函数 assum1

(check-sat-using qfnra-nlsat)

运行，但给了我一个“未知”的结果。

所以，我的问题是 - 我如何选择我的求解器并将其专门应用于函数“assum1”？

感谢您的帮助。

Answer 1

check-sat 和 check-sat-using 的参数不同。虽然 check-sat 采用一组假设（布尔文字），但 check-sat-using 期望将一种策略应用于当前目标（如“应用”命令），它不采用假设。 apply 和 check-sat-using 之间的区别在于后者应用策略然后检查结果是空目标还是false 目标。 （有关 Z3 中的目标和战术的更多信息，请参阅strategies tutorial。）

对于这个特定示例，我认为在应用 qfnra-nlsat 之前将assum1 断言到目标中是最简单的（这意味着如果任何假设发生变化，您将必须构建一个新目标）。

如果问题在 QF_NRA 中，默认情况下也会应用 nlsat 策略，但它可能需要明确

(set-logic QF_NRA)

在文件的开头以确保它被应用。