Ошибка разбора CVC4 (та же формула пропускает Z3)

Question

Следующие разделы SMT проходят решение по ограничению Z3, а CVC4 отмечает ошибку синтаксического анализа: "Символ" None ", ранее объявленный как переменная". Я протестировал с использованием 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 не принимает определения типов данных, в которых имена конструкторов дублируются. Таким образом, "None" не может быть одновременно 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

Надеюсь, это поможет, Энди