Как оценить время, затрачиваемое на решение SAT в z3 для SMT?

Question

я профилированный мои проблемы, которые в (псевдо-нелинейном) целом реального фрагмента с использованием профилировщиком дргиХ (статистика here включая граф вызовов) и пытаюсь выделить время, затрачиваемое на два класс:

I) Часть решения SAT (в том числе [чисто] булево распространение и [чисто] логическое определение конфликтной ситуации, обратное смещение, любая другая пропозициональная манипуляция)

II) Часть решения теории (включая проверку согласованности теории, создание теоретических коллизионных предложений и теория распространения).

Действительно ли линии 3280-3346 в smt_context.cpp в пределах bounded_search() составляют верхний уровень цикла DPLL (X)?

Я считаю, что проще всего подытожить время в функциях решателя SAT (поскольку их меньше) , а затем остальное можно рассматривать как время решателя теории. Я пытаюсь выяснить, какие функции я должен рассматривать как подпадающие под класс I выше? Являются ли они smt::context::decide(), smt::context::bcp() в пределах smt::context::propagate()? Любые другие? smt::context: resolve_conflict(), похоже, смешивается с вызовами теории решателя?

Правильно ли это, что smt::context::propagate() является главным образом распространением теории (класс II), за исключением его функции bcp()? Кроме того, smt::context::final_check(), кажется, чисто в классе II.

Любые советы приветствуются. Благодарю.

Answer 1

Вы правы, bcp() и decide() являются частью «SAT solver». Функция final_check() - это просто теория рассуждений. Он выполняет процедуры, которые Z3 «утверждает» слишком «дорого». Процедура resolve_conflict() смешана: она выполняет обучение леме и возвращается. Для генерации новых лемм Z3 использует булевое разрешение (которое находится в «части SAT»). В ряде случаев самая дорогая часть resolve_conflict отбрасывает состояние решателей теории.