CVC4の解析エラー（同じ数式がZ3に合格）

Question

次のSMTフォルマは、CVC4が解析エラーのフラグを立てている間にZ3制約を解決します： "以前に変数として宣言された"私はCVC4 1.4とCVC 1.5の両方をWindows上で使ってテストしました。どのような提案や考え？

(set-logic ALL) 
(declare-datatypes() ((Enum13 (Green) (Yellow) (None)))) 
(declare-datatypes() ((Enum0 (True) (False) (None)))) 
(declare-datatypes() ((Enum9 (Star_3) (Star_2) (Star_1) (None)))) 
(declare-fun Decomp 
      (Enum9 Enum13 Enum0) 
      Enum13) 
(declare-fun var_36() Enum0) 
(declare-fun var_37() Enum13) 
(declare-fun var_71() Enum9) 
(declare-fun var_38() Enum13) 
(declare-fun var_31() Real) 
(assert (and true 
    true 
    true 
    (= var_38 
     (Decomp var_71 var_37 var_36)))) 
(assert (>= var_31 0.0)) 
(assert (<= var_31 700.0)) 
(check-sat) 

Answer 1

CVC4はコンストラクタの名前が重複するデータ型定義を受け入れません。したがって、「なし」はEnum13、Enum0、およびEnum9の両方になることはできません。代わりに、None13、None0、None9、CVC4などの一意の名前を使用すると、構文エラーが発生しません。

データ型の形式は少し異なる場合ところで、CVC4の最新バージョンは、デフォルトではSMT LIB 2.6を受け入れ：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf あなたはまだ--lang = smt2.5

希望を使用することができ、古い形式を使用するにはこれは役に立ちます。 Andy