Как интерпретировать статистику Z3

Question

Я получаю следующую статистику в Z3.

(:added-eqs   24529 
:binary-propagations 43837 
:bv-bit2core   7115 
:bv-conflicts   156 
:bv-diseqs   10395 
:bv-dynamic-diseqs 10028 
:bv->core-eq   10401 
:conflicts   409 
:decisions   4840 
:del-clause   84926 
:final-checks   2 
:max-generation  4 
:memory    5.69 
:minimized-lits  467 
:mk-clause   88358 
:propagations   90195 
:quant-instantiations 3388 
:restarts    3 
:time     0.83) 

Я хотел бы знать, какие показатели используются для каждой строки результата.

Вы можете мне помочь?

Answer 1

Отказ от ответственности: У меня такое чувство, что интерпретация статистики по праву является довольно искусством и что разработчики Z3, вероятно, единственные, кто действительно знает, как это сделать. Во всяком случае, вот что я знаю ... или считаю:

quant-instantiations указывает количество экземпляров-кванторов. Чем меньше экземпляров, тем лучше, но вы, конечно, не хотите, чтобы ваши шаблоны/триггеры были слишком строгими, потому что Z3 не сможет ничего доказать.

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

Похожие вопросы:

• Z3 statistics: what does time measure?
• Z3 real arithmetic and statistics
• Which statistics indicate an efficient run of Z3?