Кодогенерация по литералам

[TonitaN]

Теперь уже можно реализовывать последний этап преобразования - кодогенерацию. Поскольку подразумевается, что все формулы модели приведены к КНФ (а значит, и вся модель описывается с помощью КНФ), можно генерировать код, рассчитывая, что формула имеет вид либо (AND F1 ... Fn), либо (OR L1 ... Ln), где Fi --- это дизъюнкты, а Li --- литералы. В этой заявке рассматривается преобразование только последних в Рефал-форму. Желательно это делать в двух формах --- перевод в базисный Рефал и перевод в расширенный Рефал. Сейчас сосредоточимся только на расширенном. Отличия для базисного Рефала будут только в форме функций (на это будет отдельная заявка), всё остальное абсолютно такое же. Для каждой переменной, определённой в блоке declare_fun, порождаем соответствующее имя е-переменной. Определим convert([VarName]) = e.[VarName'], где [VarName'] получается из [VarName] заменой всех символов, кроме латинских букв, цифр, знаков подчёркивания и дефисов, на буквенные идентификаторы.

1. Если существуют литералы вида (= S1 S2), заводим функцию Equal следующего содержания.

   Equal { 
       (e.1)(e.1) = True;
       (e.1)(e.2) = False;
   }

   Тогда convert( (= S1 S2) ) = <Equal (convert(S1)) (convert(S2))>. Аргументы заключены в структурные скобки.

2. Если существуют литералы вида (not (= S1 S2)), заводим функцию Inequal следующего содержания.

   Inequal { 
       (e.1)(e.1) = False;
       (e.1)(e.2) = True;
   }

   Тогда convert( (not (= S1 S2)) ) = <Inequal (convert(S1)) (convert(S2))>.

3. Если существуют литералы вида (str.contains S1 [Const]), заводим функцию Infix_[Const] (с уникальным именем и содержанием для всех различных констант [Const]).

   Infix_[Const] { 
       e.1 [Const] e.2 = True;
       e.Z = False;
   }

   Тогда convert( (str.contains S1 [Const]) ) = <Infix_[Const] convert(S1)>. В названии функции [Const] не закавычен, в аргументе [Const] пишем как 'Const' (апострофы вместо двойных кавычек в smt). Если в [Const] есть символы кроме латинских букв и цифр, экранируем их в имени функции --- заменяем на уникальный буквенный идентификатор и выделяем знаками подчёркивания. Если в [Const] есть апострофы или бэкслеш --- экранируем их бэкслешем в теле функции.

4. Если существуют литералы вида (not (str.contains S1 [Const])), заводим функцию No_[Const] (с уникальным именем и содержанием для всех различных констант [Const]).

   No_[Const] { 
       e.1 [Const] e.2 = False;
       e.Z = True;
   }

   Тогда convert( (not (str.contains S1 [Const])) ) = <No_[Const] convert(S1)>. Экранирование и кодировка та же, что в пункте 3.

5. Если существует вызов (str.replace_all S1 [Const1] [Const2]), тогда заводим функцию Repl_[Const1]_[Const2] (уникальную для каждой пары [Const1]+[Const2]).

   Repl_[Const1]_[Const2] { 
       e.1 [Const1] e.2 = e.1 [Const2] <Repl_[Const1]_[Const2] e.2>;
       e.Z = e.Z;
   }

   Тогда convert( (str.replace_all S1 [Const1] [Const2]) ) = <Repl_[Const1]_[Const2] convert(S1)>. Замечания про экранирование те же, что в пункте 3.

6. C конкатенацией без проблем: convert (str.++ S1 F1) = S1 convert(F1).
7. convert ([const]) = 'screen_const([const])', где [const] --- это токен "константа", а screen_const --- экранирование апострофа и бэкслэша с помощью бэкслэша (как в п.3).

Это базовый алгоритм кодогенерации, в котором самое сложное --- это экранировать символы в именах. У него будет одна оптимизация, связанная с особыми дизъюнктами в КНФ --- теми, в которых есть как минимум два литерала вида либо (str.contains S P), либо (not (str.contains S Q)) (где строки P и Q могут быть разными, а вот первый аргумент, S, один и тот же). Но эта оптимизация будет описана уже в следующей заявке по кодогенерации.

[TonitaN]

Я никого не прикрепляю к этой заявке, но поскольку @StepanBog будет загружен резолюциями ещё достаточно долго, похоже, что кодогенерацию придётся делать @ylyxa . Если решите иначе --- тоже ок.

[Mazdaywik]

Даже при кодогенерации код лучше форматировать по-человечески:

Equal {
    (e.1)(e.1) = True;
    (e.1)(e.2) = False;
}

Inequal {
    (e.1)(e.1) = False;
    (e.1)(e.2) = True;
}

Infix_[Const] {
    e.1 [Const] e.2 = True;
    e.Z = False;
}

No_[Const] {
    e.1 [Const] e.2 = False;
    e.Z = True;
}

Repl_[Const1]_[Const2] {
    e.1 [Const1] e.2 = e.1 [Const2] <Repl_[Const1]_[Const2] e.2>;
    e.Z = e.Z;
}

https://github.com/bmstu-iu9/refal-5-lambda/blob/master/doc/style-guide.md

[TonitaN]

@Mazdaywik , спасибо!

[TonitaN]

@ylyxa, придётся прикрепить вас к заявкам по кодогенерации. Если будет неохота делать оптимизации (расшаривание аргумента в заявке #8 ), не делайте, это не повлияет на оценку, на вас и так много заданий.