z3 - 使用 ctx-simplify 策略的奇怪输出

Question

小例子准备如下：

(declare-datatypes () ((Type1 a b c d e g h i f k l m n o p q r s t u v w z)))
(declare-const x Type1)
(declare-const y Type1)
(assert (and (= y x) (or (and (not (= x g)) (not (= x a))) (and (or (not (= x g)) (not (= x q))) (not (= x a))))))
(apply ctx-simplify)

输出是：

(goals
(goal
  (= y x)
  (or (not and) (not (= x a)))
  :precision precise :depth 1)
)

什么(or (not and) (not (= x a)))意思？漏洞？

谢谢你。

Answer 1

感谢您指出了这一点。我同意在打印输出中没有参数的“和”看起来很奇怪。上下文简化器创建一个带有 0 个参数的连词。它被简单地打印为“和”。所以 ctx-simplify 返回的表达式等价于 (not (= xa))。我将更新 ctx-simplify 策略以返回不带空连词的表达式。