Связь между arith.nl.rounds и final-checks

Есть ли какая-либо связь между параметром конфигурации smt.arith.nl.rounds и значением статистики final-checks (или это просто совпадение, что в описании первого упоминаются "окончательные проверки")?

Я запускал 64-разрядные сборки Windows Z3 4.3.2 (официальная загрузка) и Z3 4.4 0ab54b9e0c33 в программе SMTLIB, и в обоих случаях сообщаемое число final-checks (около 10 000), по-видимому, не зависит от того, какое значение я выберу для smt.arith.nl.rounds (я пробовал 1, 64, 128, ..., 1024 и 4096).


person Malte Schwerhoff    schedule 22.01.2015    source источник


Ответы (1)


У всех теорий есть окончательные проверки, но smt.arith.nl.rounds предназначен только для решателя нелинейных арифметических операций (старый, не NLSAT). Может быть много окончательных проверок, ни одна из которых не связана с нелинейной арифметикой, или они используют другие методы для решения этих частей.

person Christoph Wintersteiger    schedule 27.01.2015