У меня есть ряд ограничений, утверждающих биты в BitVec, и мне интересно, что является самым эффективным способом утверждения ограничений для определенного бита в BitVec?z3py: Каков наиболее эффективный способ ограничения бит в BitVec?
Предположим, я хочу утверждать, что 5-й бит в BitVec равен 1, есть ли способ, который более эффективен (меньшее время проверки), чем это?
bitvec = BitVec('bitvec',10)
s.add(Extract(5,5,bitvec)==1)
Из того, что я понимаю, о внутренностях Z3 (от экспериментирования и глядя на источник), это является наиболее эффективным способом.
Как я понимаю, экстракты и конкаты не имеют времени на выполнение решения. Они просто разбивают кусочки на части.
Единственной альтернативой может быть применение операции and для извлечения бит. Но после упрощения это должно превратиться в выписку (что вы можете проверить, выполнив тактику упрощения. Это забавный переписывать).
Это здорово, я попробую применить побитовое и извлечь бит. Благодарю. –