CVC4 无法打开 SMT2 格式的文件答案

【问题标题】：CVC4 cannot open file in SMT2 formatCVC4 无法打开 SMT2 格式的文件
【发布时间】：2020-03-25 03:38:07
【问题描述】：

我正在尝试使用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

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

【问题讨论】：

您是否检查了文件的读取权限？

标签： file synthesis cvc4

【解决方案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

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

【讨论】：