Я использую инициализированный массив и выполняю серию операций с 3 хранилищами, за которыми следует выбор, при котором возвращенное значение FIXED (которое будет обозначено как V_A ниже) этим выбором повторно используется в качестве индекса для следующего хранилища.
Я инициализирую ~ 400 индексов в массиве, объявленном следующим образом:
(declare-fun my_array0 () (Array (_ BitVec 30) (_ BitVec 32)))
При инициализации ~ 400 индексов с помощью оператора, указанного ниже, время проверки составляет ~ 30 секунд с Z3.
(= (select my_array0 ((_ extract 31 2) (_ bv0123456 32))) a_fixed_value_var)
Когда я изменяю способ инициализации массива ТОЛЬКО для индекса I_A, содержащего V_A, и я заменяю его оператором ниже, время проверки изменяется на ~ 1 сек.
(= my_array1 (store my_array0 ((_ extract 31 2) (_ bv`I_A index` 32)) `V_A`))
И проверкавремя меняется, когда я перемещаю этот оператор вверх или вниз по серии выбора (инициализируя массив): ~ 10 секунд, когда оператор находится близко к вершине серии выборов (как объявлено в файле), до ~ 0,1 секунды, когда оператор являетсяблизко к нижней части серии выбора.
Кто-нибудь имеет представление о том, почему проверка отличаетсяКак много, и, может быть, как это смягчить?
(я сейчас решаю проблему, но у меня все еще есть файл smt длиной ~ 10 тыс. строк для прохождения.)