file - CVC4 无法打开 SMT2 格式的文件

Question

我正在尝试使用CVC4对函数执行语法引导合成。首先，我正在关注CVC4 Getting Started，我的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

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