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

【问题标题】：strange output using ctx-simplify tactic使用 ctx-simplify 策略的奇怪输出
【发布时间】：2013-04-23 10:52:05
【问题描述】：

下面准备小例子：

(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))) 是什么意思？错误？

谢谢。

【问题讨论】：

标签： z3

【解决方案1】：

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

【讨论】：