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))

对于此输入，具有“-增量”选项(支持多个查询)的cvc4将提供以下响应：

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

希望这有帮助，安迪