CVC4の誘導データ型のアサーション

Question

私はCVC4で少し実験を試みています。私は次の出力

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

を取得しています。この使用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)) 

。 私はxとyが同じであってはならないと主張しているならば、その値は違うはずですか？ 異なるアサーションの場合も同じです。 CVC4はxとyを2つの異なる「オブジェクト」として扱っているので、出力していますか？

Answer 1

同じ結果は表示されません。これは私がCVC4（http://cvc4.cs.stanford.edu/downloads/）の最新の開発版を取得するメッセージである。この入力に

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

：あなたの例では、いくつかの構文エラーがあります

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

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

、ここでの修正バージョンがあります、オプションでcvc4（複数のクエリを可能にする） "--incremental" は、この応答を与える：

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

、この情報がお役に立てば幸いアンディ