0

我想使用 muZ 将 z3 用于 BMC。也许我遗漏了有关查询可满足性定义的一些内容。但是，在以下情况下，我有一个不可满足的查询示例（即，返回“false”），但是当添加一个额外的约束（有效地给出令人满意的分配）时，会返回一个有效的分配。

是否有任何文档有助于理解 z3 的 muZ 语言扩展的确切语义？

谢谢和最好的问候！！

使用 Z3 版本 4.3.2 执行以下 .smt2 文件会导致以下结果：

formula undetermined in model: (= (head query!0_0_n) (state c1 1))
sat
false
sat
(let ((a!1 (insert (state c1 1) (insert (state c2 0) (insert (state c1 0) nil))))
      (a!2 (TransClosure (insert (state c2 0) (insert (state c1 0) nil)))))
  (and (TransClosure a!1) a!2 (TransClosure (insert (state c1 0) nil))))

对应的 .smt2 文件是：

;; Application of z3Mu for BMC of EFSM
;; Behavior of EFSM is defined recursively as a predicate over finite sequences (Lists) of states

;; Declaration of state space
(declare-datatypes () ((Control c1 c2)))
(declare-datatypes () ((State (state (cstate Control) (var Int)))))

;; Definition of transition relation and initial state
(declare-rel Trans (State State))
(declare-var pre State) 
(declare-var post State)
(rule (=> (and (= (cstate pre) c1) (= (cstate post) c2) (= (+ (var pre) 0) (var post))) (Trans post pre)))
(rule (=> (and (= (cstate pre) c2) (= (cstate post) c1) (= (+ (var pre) 1) (var post))) (Trans post pre)))

;; Definition of fixed-point closure
(declare-var init State)
(declare-var trace (List State))

(declare-rel Init (State))
(rule (Init (state c1 0)))

(declare-rel TransClosure ((List State)))
(rule (=> (and (Trans (head trace) (head (tail trace))) (TransClosure (tail trace)))
      (TransClosure trace)))
(rule (=> (Init init) (TransClosure (insert init nil))))


;; Query for a witness which is satifiable in three steps
;; Query without explicit witness construction fails
(query (and (= (head trace) (state c1 1))
            (TransClosure trace)
            )
  :print-answer true)
;; Same query with explicit witness succeeds
(query (and (= (head trace) (state c1 1))
            (TransClosure trace)
            (= trace (insert (state c1 1) (insert (state c2 0) (insert (state c1 0) nil))))
            )
 :print-answer true)
4

1 回答 1

0

“模型中的公式未确定”消息表明 Z3 中存在错误。错误是 Z3 按原样接受输入而没有抱怨。它应该在使用 PDR 后端引擎时拒绝该示例。PDR 后端引擎支持算术、布尔值和非优化的位向量，以及一些对代数数据类型的支持。它不支持代数数据类型的访问器（头、尾），我现在添加了一个检查，在调用搜索之前报告错误并指出使用不受支持的访问器。Z3 的不稳定分支包含修复。

可以仅使用“插入”而不是“头”“尾”来重写您的示例。例如用“s1”替换（head t），用“（insert st）”替换其他地方的“t”。

您可以将 SMT-LIB2 中的纯 Horn 子句与 (set-logic HORN) 命令一起使用来调用可用的 Horn 子句求解器之一，或者您可以使用定点扩展语法，它对声明变量有一些便利。有几个后端。主要有： - 'datalog'：基于哈希表的 Datalog 求解器。关系必须在有限域变量上 - “pdr”：关系必须在布尔、算术、位向量和/或代数数据类型上。- 'bmc'：有界模型检查对应于转换关系的喇叭子句的展开。其他引擎也存在，但这些是需要考虑的主要引擎。

SMT-LIB2 中 HORN 子句的语义与 SMT-LIB2 语义相同。没有特殊的语义，但是 Horn 求解器将只能处理对应于 Horn 子句的公式的合取。您的示例可以仅使用 Horn 子句表示：每个规则都是一个暗示，并且查询对应于一个否定子句（否定查询并将其与其他子句一起断言。当结果子句集不可满足时，查询是可行；当结果子句集是可满足的，则查询是不可行的）。

于 2013-09-23T19:48:36.123 回答