CVC4 最多期望运算符 'ITE' 有 3 个参数，结果发现有 5 个

Question

将以下文件输入cvc4时，出现如下错误：

(error "Parse Error: <stdin>:11.221: Expecting at most 3 arguments for operator 'ITE', found 5")

文件 test.txt 是：

(declare-fun start!1 () Bool)

(assert start!1)

(declare-fun lt!2 () String)

(declare-datatypes () ( (JValue!1 (JInt!1 (v!75 (_ BitVec 32))) (JString!1 (v!76 String))) ))

(declare-fun a!0 () JValue!1)

(assert (=> start!1 (not (= lt!2 (ite false "" (ite (and (is-JString!1 a!0) (= (v!76 a!0) "")) """""" (ite (and (is-JInt!1 a!0) (= (v!75 a!0) #x00000000)) "0" (ite (and (is-JString!1 a!0) (= (v!76 a!0) "a")) """a""" lt!2))))))))

命令行：

cat test.txt | cvc4.exe

Answer 1

我需要为格式添加选项 --lang smt2.5 以使用新标准支持双引号转义。

所以：

cat test.txt | cvc4.exe --lang smt2.5

CVC4 最多期望运算符 'ITE' 有 3 个参数，结果发现有 5 个

CVC4 Expecting at most 3 arguments for operator 'ITE', found 5

cvc4