关于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与选项 “--incremental”（使多个查询），给出了这样的回应：

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

希望这有助于 安迪