CVC4 中关于归纳数据类型的断言

Question

我正在尝试使用 CVC4 进行一些实验。

(set-option :produce-models true)
(set-option :produce-assignments true)
(set-logic QF_UFDT)
(declare-datatypes ()
  (Color (Red) (Black))
)
(declare-const x C)
(declare-const y C)
(assert (not (= x y)))
(check-sat)
(get-value (x y))
(assert (distinct x y))
(check-sat)
(get-value (x y))

当我使用 CVC4 运行它时，我得到以下输出

sat
((x R) (y R))
sat
((x R) (y R))

我对此输出的这种行为感到困惑。 如果我断言 x 和 y 不应该相等，它们的值必须不同，对吗？ 不同断言的情况也是如此。 CVC4 是否将 x 和 y 视为两个不同的“对象”并因此给出它给出的输出？

Answer 1

我没有看到相同的结果。这是我从 CVC4 的最新开发版本 (http://cvc4.cs.stanford.edu/downloads/) 中得到的消息：

(error "Parse Error: stack.smt2:5.8: Sequence terminated early by token: 'Color'.

    (Color (Red) (Black))
     ^
")

您的示例中有一些语法错误，这是一个更正的版本：

(set-option :produce-models true)
(set-option :produce-assignments true)
(set-logic QF_UFDT)
(declare-datatypes () (
  (Color (Red) (Black))
))
(declare-const x Color)
(declare-const y Color)
(assert (not (= x y)))
(check-sat)
(get-value (x y))
(assert (distinct x y))
(check-sat)
(get-value (x y))

在此输入上，带有选项“--incremental”（启用多个查询）的 cvc4 给出以下响应：

sat
((x Red) (y Black))
sat
((x Red) (y Black))

希望这会有所帮助， 安迪