smt - LANG_AUTO 和 antlr 的 cvc4 错误

Question

我已经根据他们的手册从源代码构建了cvc4。我跑make check的很完美，然后sudo make install。然后，我尝试运行一个适用于 z3 的简单示例：

(declare-const i Int)
(declare-const j Int)

(assert (= i 5))
(assert (= (+ i j) 9))

(check-sat)
(get-value (i j))

但我得到这个错误：

CVC4 Error:
internal error: unhandled language LANG_AUTO in AntlrInput::newInput

我究竟做错了什么？谢谢！

score 0 · Accepted Answer

事实证明我从命令行错误地调用了它。这是有效的：

cvc4 --quiet --produce-models --lang=smt2 ./example.txt

这会产生以下结果：

sat
((i 5) (j 4))

1 回答 1