Есть ли способ включить другой файл в smtlib? - PullRequest
0 голосов
/ 06 января 2019

Аналогично #include в C при импорте функций и аксиом, определенных в другом файле. Я не смог найти такую ​​функциональность, описанную в документации SMTLIB или в онлайн-примерах. Есть намеки?

1 Ответ

0 голосов
/ 06 января 2019

SMTLib не имеет возможности #include загружать или импортировать другие файлы. Это может выглядеть как недостаток, но люди редко пишут вручную файлы SMTLib: это почти всегда машина, сгенерированная из языка более высокого уровня, и предполагается, что тот, кто генерирует SMTLib, может просто выплюнуть один большой файл, который включает в себя все, что вам нужно.

Сказав это, я думаю, что будет полезной функцией, чтобы действительно иметь. Стандарт SMTLib постоянно развивается, и такие функции обычно обсуждаются в их списке рассылки:

https://groups.google.com/forum/#!forum/smt-lib

Не стесняйтесь присоединиться к обсуждению и сделать запрос!

...