Решатель SMT с пользовательскими теориями?

Существует несколько вариантов, учитывая, что наиболее разумные решатели SMT имеют открытый исходный код, вы можете интегрировать теоретические решатели с любыми деталями в зависимости от того, сколько времени и энергии вам нужно потратить.

• OpenSMT http://verify.inf.usi.ch/opensmt был специально создан для поддержки теории подключаемых модулей. интеграция.
• VeriT, Yices и CVC4 имеют открытый исходный код, и вы можете изучить теоретическую интеграцию в этих решателях.
• Z3 имеет открытый исходный код и доступен для использования вами и другими пользователями. Существовал API для режима плагина DPLL (T), но мы удалили его, когда исходный код Z3 стал открытым, а также из-за основного ограничения: он плохо поддерживал построение модели. Внутренние API, используемые для вставки теорий, в принципе изоморфны внешним API. Более старая статья, описывающая различные способы интеграции теорий: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-aplas11.pdf. Я бы сказал, что первый прототип намного проще создать, используя внешний цикл вокруг решателя. Вы получаете пропозициональную модель от решателя, а затем проверяете, соответствует ли она вашей базовой теории. Вы также можете попробовать внутренние API. Для некоторых теорий это довольно просто. См., Например, UTVPI https://github.com/Z3Prover/z3/blob/master/src/smt/theory_utvpi_def.h в качестве образца. Для теории струн это довольно сложно (потому что теория требует существенных рассуждений в частном случае). Модуль z3str3 был интегрирован ранее в этом году https://github.com/Z3Prover/z3/blob/master/src/smt/theory_str.cpp, и разработка все еще продолжается. Это около 10KLOC. Bui Phi Dep использует старую версию Z3 для внешней теоретической интеграции https://github.com/diepbp/FAT. Это также значительный объем кода, опять же, поскольку теории струн и преобразователей требуют довольно небольшой настройки. Для участников, которые готовы реагировать на отчеты об ошибках и запросы пользователей, мы (Z3) очень приветствуем дополнительные вклады в основную ветвь Z3 с теориями и алгоритмами, которые не рассматриваются. В пространстве акцептора / преобразователя струны и дерева довольно много места для маневра.

Опять же, я бы сказал, что для первой версии вы должны довольно далеко продвинуться с внешней интеграцией, когда вы позволите решателю SMT иметь дело с пропозициональным SAT и неинтерпретируемыми функциями (и арифметикой, если вам это нужно). Затем вы можете попросить у решателя модель и добавить аксиомы теории обратно до тех пор, пока пропозициональная модель, которую вы получаете из решающей программы, не согласуется с вашей теорией (или вы не получите UNSAT). Не все задания в модели высказываний будут уместными. Вы можете минимизировать количество рассматриваемых назначений, применив двойное распространение (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/29_niemetz.pdf).