Какая статистика указывает на эффективную работу Z3?

Question

Директива SMTLib2 (get-info all-statistics) отображает несколько цифр, например,

num. conflicts:     4
num. propagations:  0 (binary: 0)
num. qa. inst:      23

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

Догадываясь по именам, я бы сказал, что num. qa. inst - число экземпляров квантификатора - является хорошим показателем (ниже = лучше), но как насчет других?

Answer 1

Количество экземпляров квантификатора является хорошей мерой для проверки, производит ли ваша аксиоматизация слишком много экземпляров или нет.Вы также можете использовать QI_PROFILE = true.Он будет производить статистику для каждого квантификатора.Вы можете использовать атрибут: qid, чтобы дать имя квантификатору.Вы также можете использовать DEFAULT_QID = true, и Z3 создаст имя на основе номеров строк.QI_PROFILE_FREQ = будет отображать статистику после генерации каждого экземпляра.Эти параметры полезны для обнаружения циклов создания экземпляров.

«число конфликтов» полезно для оценки размера пространства поиска, пройденного Z3.Мы можем сказать, что аксиоматизация «лучше», если размер пространства поиска меньше.

Ура, Лев