0
Это следующий вопрос о моем предыдущем вопросе "Is it possible to intrinsically reduce the search space of Function".z3, z3py: Можно ли определить сортировку, которая включает в себя набор целых чисел?
Я думаю, если возможно, что я могу определить сортировку, содержащую набор целых чисел, например целые числа 1-10.
Мою интуицию заключается в том, что для сокращения пространства поиска функции вместо определения функции, сортировка по доменам и сортировка по диапазону которой является IntSort, я хочу определить функцию, сортировка и сортировка по домену которой относится только к набору целые мои интересы.
Пусть
Действительно ли вы используете операции с целыми числами? Если нет, вы можете использовать тип данных для определения конечного перечисления вместо использования неограниченных целых чисел? – Ayrat
еще один трюк: определить функцию-оболочку: 'wrap_func (x): return seek_func (x), если 0
Ayrat
Спасибо, Айрат. Я выполняю ограничения на целые числа. Вы имеете в виду, что мы определяем Enum или DeclareSort? Проблема в том, что сортировка определений в основном представляет собой набор строк, а не целых чисел, и они не могут иметь целые числа в качестве основных элементов. –