Директива SMTLib2 (get-info all-statistics) отображает несколько чисел, например.
num. conflicts: 4
num. propagations: 0 (binary: 0)
num. qa. inst: 23
Чтобы протестировать различные аксиоматизации и кодировки, я хотел бы знать, какие из этих чисел подходят для объявления того, что один запуск Z3 лучше/эффективнее другого.
Судя по именам, я бы сказал, что num. qa. inst — количество экземпляров квантификатора — это хороший показатель (ниже = лучше), но как насчет других?
Количество экземпляров квантификатора является хорошей мерой для проверки того, создает ли ваша аксиоматизация слишком много экземпляров или нет. Вы также можете использовать QI_PROFILE=true. Он будет производить статистику для каждого квантификатора. Вы можете использовать атрибут :qid, чтобы дать имя квантификатору. Вы также можете использовать DEFAULT_QID=true, и Z3 создаст имя на основе номеров строк. QI_PROFILE_FREQ= будет отображать статистику после создания каждого экземпляра. Эти параметры полезны для обнаружения циклов инстанцирования.
«Число конфликтов» полезно для оценки размера пространства поиска, через которое проходит Z3. Можно сказать, что аксиоматизация «лучше», если размер области поиска меньше.
Привет, Лео
