Я использую z3py, и у меня есть IntVector размера 3. Мне нужно проанализировать каждую цифру в IntVector как одно целое число. Это означает, что если у меня есть IntVector, который имеет такие ограничения:
myIntVector = IntVector('iv', 3)
s = Solver()
s.add(iv[0] == 5)
s.add(iv[1] == 2)
s.add(iv[2] == 6)
….
Мне нужно иметь возможность работать с номером 526 как с сортировкой Int в z3, потому что мне нужно добавить оба ограничения, которые применяются к каждому отдельному члену ограничений IntVector (цифра) И, которые применяются ко всему номер, в данном случае 526. Я не могу сделать что-то вроде:
s.add(iv[0] / iv == 55)
потому что это 2 отдельных типа. iv[0] - это Int, а iv - это IntVector