z3Py: Cast BoolRef zu einem Bit BitVecRef

Question

Ist es möglich, BoolRef zu einem ein Bit langen BitVecRef in z3Py zu werfen? In meinem Entwurf ist es erforderlich, dass ein BitVecRef von einem Vergleich zwischen zwei anderen BitVecRef zurückgegeben wird. Dies wäre ähnlich wie ein Python bool zu einem int Casting. Hier ist ein Beispiel für seine Verwendung:

bv1, bv2, added = z3.BitVecs('bv1 bv2 added', 4) 
res = z3.BitVec('res', 1) 
s = z3.Solver() 
s.add(res == (bv1 < bv2)) 
s.add(added == added + z3.ZeroExt(3, res)) 

Dies wäre ideal, aber die Art der (bv1 < bv2) ist Boolref, und es wirft einen „Art Konflikt“ Fehler. Gibt es eine Möglichkeit, das Ergebnis von (bv1 < bv2) so zu übertragen, dass res gleichgesetzt werden kann?

Answer 1

Bit-Vektoren können nicht automatisch in Boolean umgewandelt werden. Die übliche Vorgehensweise besteht darin, sie in einzuwickeln if-then-elses, zum Beispiel in diesem Beispiel statt

s.add(res == (bv1 < bv2)) 

wir

c = If(bv1 < bv2, BitVecVal(1, 1), BitVecVal(0, 1)) 
s.add(res == c) 

sagen können,