CVC4解析错误（同样的公式通过Z3）

Question

以下 SMT 公式通过 Z3 约束求解，而 CVC4 标记解析错误：“符号‘无’以前声明为变量”。我已经在 Windows 上同时使用 CVC4 1.4 和 CVC 1.5 进行了测试。有什么建议或想法吗？

(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

希望这会有所帮助， 安迪