CVC4解析错误(相同的公式传递Z3)

Question

下面的文件通过了Z3约束求解，而CVC4标记了一个解析错误："Symbol 'None‘之前声明为一个变量“。我已经在windows上使用CVC4 1.4和CVC1.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的最新版本默认接受SMTLib2.6，其中数据类型的格式略有不同：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf使用旧格式，您仍然可以使用旧格式--lang=smt2.5

希望这能帮上忙，安迪