CVC4无法以SMT2格式打开文件

Question

我试图使用CVC4对一个函数执行语法指导的综合。首先，我跟踪CVC4入门，我的example.smt2文件如下所示：

(set-logic ALL)
(declare-fun x () Int)
(assert (= (+ x x) (* x 2)))
(check-sat)

当我在目录中的命令行中运行cvc4 example.smt2时，不应该出现基于上面链接的教程的问题。但是，我得到了以下错误：

(error "Couldn't open file: example.smt2")

请注意，此错误与文件不存在的情况不同。例如，当我运行cvc4 exampl.doesnotexist时，会发生以下错误：

CVC4 Error:
Couldn't open file: exampl.doesnotexist

这是不同的。我到处查这个，却找不到答案。有什么想法吗？

Answer 1

如果您没有读取文件的权限，您将得到这个错误：

$ cat example.smt2
(set-logic ALL)
(declare-fun x () Int)
(assert (= (+ x x) (* x 2)))
(check-sat)
$ cvc4 example.smt2
sat
$ chmod u-r example.smt2
$ cvc4 example.smt2
(error "Couldn't open file: example.smt2")
$ cat example.smt2
cat: example.smt2: Permission denied
$ chmod u+r example.smt2
$ cat example.smt2
(set-logic ALL)
(declare-fun x () Int)
(assert (= (+ x x) (* x 2)))
(check-sat)
$ cvc4 example.smt2
sat

根据您的操作系统，只需允许读取访问，问题就会消失。