CVC4 Parsing Fehler (die gleiche Formel übergibt Z3)

Question

Die folgenden SMT folumas übergeben Z3 Constraint-Lösung, während CVC4 einen Parsing-Fehler kennzeichnet: "Symbol 'None' zuvor als eine Variable deklariert". Ich habe mit CVC4 1.4 und CVC 1.5 unter Windows getestet. Irgendwelche Vorschläge oder Gedanken?

(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 akzeptiert keine Datentypdefinitionen, bei denen die Namen von Konstruktoren dupliziert werden. Also kann "None" nicht sowohl Enum13, Enum0 und Enum9 sein. Stattdessen könnten Sie eindeutige Namen wie None13, None0, None9 und CVC4 verwenden, die keinen Syntaxfehler ergeben würden.

Btw, nimmt die neueste Version von CVC4 SMT LIB 2.6 standardmäßig, in dem das Format für Datentypen etwas anders ist: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf Um das alte Format verwenden Sie noch --lang verwenden = smt2.5

Hoffnung dies hilft, Andy