Считать корректными только объявленные переменные

TonitaN commented 3 years ago

Синтаксический анализатор должен учитывать, что если переменная в утверждении типа (assert... ) не объявлена с помощью (declare-fun [Name]( ) String), то такая переменная синтаксически некорректна. Пример отрицательного теста:

(set-logic QF_SLIA)
(set-option :strings-exp true)
(declare-fun x1 () String)
(assert (str.contains x "A"))
(check-sat)
(get-model)

TonitaN commented 3 years ago

Будем считать, что за синтаксический разбор от парсера до построения синтаксического дерева ответственный исполнитель @ylyxa , а за построение КНФ — @StepanBog .

ylyxa commented 3 years ago

Уже реализовано (parser.py, строки 90-92).

Mazdaywik commented 3 years ago

@ylyxa, если в описание коммита добавить #1, то ссылка на коммит добавится между комментариями в заявку. Тогда можно будет (а) по описанию коммита узнать, какие проблемы он решает, (б) в заявке сразу найти связанные с ней коммиты.

Чтобы сослаться на кусок кода, нужно сделать следующее:

Открыть файл: https://github.com/bmstu-iu9/SMT-to-REF/blob/main/Parser.py
Нажать латинскую клавишу y, тогда в URL страницы появится хеш коммита: https://github.com/bmstu-iu9/SMT-to-REF/blob/55a2ea393442f37c5e844efaa0c3ec7598c07c13/Parser.py
Выбрать строки: кликнуть на 90, нажать Shift и кликнуть на 92. Номера строк добавятся к ссылке как anchor: https://github.com/bmstu-iu9/SMT-to-REF/blob/55a2ea393442f37c5e844efaa0c3ec7598c07c13/Parser.py#L90-L92
Вставить эту ссылку в комментарий, она отобразится как листинг: https://github.com/bmstu-iu9/SMT-to-REF/blob/55a2ea393442f37c5e844efaa0c3ec7598c07c13/Parser.py#L90-L92

ylyxa commented 3 years ago

Насчет листингов - учту, насчет ссылки на заявку - в коммите указана соседняя заявка #2.

Mazdaywik commented 3 years ago

Нажимать клавишу y обязательно — чтобы вставился листинг, нужна прямая ссылка на коммит.

bmstu-iu9 / SMT-to-REF

Считать корректными только объявленные переменные #1