小编Mat*_*fer的帖子

我正在尝试用zt的smt-lib 2语法编码QBF.运行z3会产生警告

警告:未能找到量词的模式(量词id:k!14)

并且可满足性结果是"未知的".

代码如下:

(declare-fun R (Bool Bool Bool Bool) Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool))
      (forall ((x1 Bool))
        (R x1 x2 x3 y)
      )
    )
  )
)
(check-sat)

我通过重写代码来摆脱警告

(set-option :auto-config false)
(set-option :mbqi false)
(declare-fun R (Bool Bool Bool Bool) Bool)
(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(declare-fun y () Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
  (!
    (exists ((y Bool))
    (!
      (forall ((x1 Bool))
      (!
        (R …