1

以下 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)
4

1 回答 1

0

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

希望这会有所帮助，安迪

于 2017-08-22T17:01:54.533 回答