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

希望這有助於 安迪