Мне интересно, влияют ли большие целочисленные значения на производительность SMT. Иногда мне приходится работать с большими значениями. В основном я выполняю арифметические операции (в основном сложение и умножение) на них (т. Е. Разные целочисленные члены) и необходимо сравнить полученное значение со связями (т. Е. Некоторым другим целочисленным членом).Влияют ли переменные с большими целыми значениями на производительность SMT?
Большие целые числа и/или рациональные значения в задаче ввода не являются определяющим показателем твердости. Z3 может генерировать большие числа внутри, даже если вход содержит только малые числа. Я наблюдал много примеров, когда Z3 тратит много времени на обработку больших рациональных чисел. Много времени тратится на вычисление GCD числителя и знаменателя. Каждое вычисление GCD занимает относительно небольшое количество времени, но на жестких задачах Z3 будет выполнять миллионы. Заметим, что Z3 использует рациональные числа для решения задач с чистым целым числом, поскольку использует алгоритм Simplex для решения линейной арифметики. Если вы разместите свой пример, я могу дать вам более точный ответ.