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

В зависимости от вашей операционной системы, просто разрешите доступ на чтение, и проблема должна исчезнуть go.