首页 文章

Z3 - check-sat-using的参数

提问于
浏览 次
1

抱歉，如果这是一个愚蠢的问题 - 我对使用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”，具有更复杂的非线性数学的变体返回“unknown” .

我认为更复杂的变体可以使用非线性求解器来解决，例如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”？

谢谢你的帮助 .

z3

1 回答

  • 1

    check-sat和check-sat-using的参数不一样 . check-sat采用一系列假设（布尔文字），check-sat-using期望一个应用于当前目标的策略（如'apply'命令），它不需要假设 . apply和check-sat-using之间的区别在于后者应用策略然后检查结果是空目标还是 false 目标 . （有关Z3中目标和战术的更多信息，请参阅strategies tutorial . ）

    对于这个特定的例子，我认为在应用qfnra-nlsat之前将 assum1 置于目标中是最容易的（这意味着如果任何假设发生变化，你将不得不构建一个新的目标） .

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

    (set-logic QF_NRA)

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

    回复于

相关问题