Я пытаюсь придумать способы улучшить производительность z3 при решении моих задач. Мне известно о документе CAV'06 и технический отчет . Отличаются ли соответствующие части z3 v4.3.1 от того, что описано в этих документах, и если да, то чем? Кроме того, какой стратегии по умолчанию придерживаются в z3 для принятия решения о том, когда проверять непротиворечивость в линейной действительной арифметике атомов теории, соответствующих определенным (и распространяемым) пропозициональным литералам?
Задокументировано ли решение SMT в стиле DPLL(T) в z3 для линейной действительной арифметики?
comment
Основные методы те же. Реализация в Z3 содержит множество расширений, которые были добавлены в ходе экспериментов и бенчмаркинга. Например, он интегрируется с нелинейными ограничениями, имеет режим единичного распространения, а в некоторых случаях использует локальную оптимизацию как часть решения целочисленных задач и генерации моделей, в которых переменные интерфейса по возможности имеют разные значения. Эта последняя функция описана в рабочем документе SMT 2007 по комбинациям теории на основе моделей. Другие функции нигде не описаны, но исходный код доступен на z3.codeplex.com.
- person Nikolaj Bjorner schedule 18.01.2014
Ответы (1)
Линейная арифметика реализована в файлах по адресу src/smt/theory_arith*. См. http://z3.codeplex.com/SourceControl/latest#src/smt/theory_arith_core.h
Что касается бумаги, которую вы указали, идеи используются в реализации. Однако фактический код содержит множество расширений для линейных целых чисел, нелинейной арифметики и генерации доказательств. Если вас интересует только линейная действительная арифметика, вам следует сосредоточиться только на theory_arith.h, theory_arith_core.h. Файл theory_arith_aux.h также содержит полезные функции.
person
Leonardo de Moura
schedule
17.01.2014
Спасибо. Мои задачи SMT LRA имеют произвольную пропозициональную структуру (включая «=›», «или» и т. д. во входных файлах .smt2). Итак, меня интересует LRA, а также взаимодействие между функциями теории LRA, на которые вы указали, и решателем SAT. В частности, я пытаюсь выяснить, являются ли узким местом многочисленные вызовы со слоя SAT к функциям в theory_arith* (в этом случае я хотел бы изменить эту стратегию) ИЛИ это тот случай, когда отдельные вызовы в theory_arith* потребляют относительно много времени (я считаю, что функции, подобные update_and_pivot(), являются хорошими кандидатами на профилирование).
- person user1779685; 18.01.2014
Любое понимание того, как это сделать, было бы очень полезно. Спасибо!
- person user1779685; 18.01.2014
