a'un 8 bitlik bir değer olan 254 bir tam sayı olduğunu varsayalım. a işaretli bir tamsayıysa, aslında -2 olarak kabul edilir. Aksine, a imzasız ise, 254 kalır.BitVector ile işaretli tamsayı nasıl modellenir?
Bu imzalı/imzasız tamsayı sorununu Z3 ile BitVector teorisi ile modellemeye çalışıyorum, ancak BitVector buna izin vermiyor gibi görünüyor. Bu doğru mu? Öyleyse Z3py'de nasıl modelleme hakkında bir fikrin var mı?
Çok teşekkürler.
Z3 imzalı ve imzasız yorumlarıyla API'leri vardır. Örneğin, C API'sinde, Z3_mk_bvslt imzasız olandan daha az ve Z3_mk_bvult imzalı oluşturur. Z3Py'de, imzalı olanlar kullanılarak <, <=, aşırı yüklendi. İmzasız olan a < b'u oluşturmak için ULT(a,b)'u kullanmamız gerekiyor. ULE (<=), ULT (<), UGE (>=), UGT (>), UDiv (işaretsiz bölme), URem (işaretsiz kalan): Burada işaretsiz operatörler listesi aşağıdadır. Daha fazla bilgiyi burada bulabilirsiniz:
http://research.microsoft.com/en-us/um/redmond/projects/z3/namespacez3py.html
Bu bit vektör değerlerinin bir işaret taşımadığını gözlemlemekte haklısınız. Diğer taraftan, bit-vektör işlemlerinin ve ilişkilerinin imzalı sürümleri vardır. SO imzalı veya imzasız bir karşılaştırmaya (daha az imzalı/imzasız olarak imzalanmış) veya imzalı veya imzasız bir işleme (imzalı bölüm/imzasız bölüm) geçirerek, aynı bit-vektör varlıklarını imzalı veya imzasız bir sayı olarak ele alabilirsiniz. Diğer aritmetik işlemler, imzalı ve imzasız varlıklar üzerinde aynı şekilde çalışır. Örneğin ekleme, imzalı veya imzasız olarak yorumlamak isteyip istemediğiniz gibi bitleri de aynı şekilde hareket ettirir.
Z3 SMT-LIB2 teorilerin kurallarını izler ve bu kapsamlı belgeleri bulabilirsiniz: http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2
Mükemmel cevap her zaman olduğu gibi! Teşekkürler Leo! – user311703