Планирам някои експерименти в символно изпълнение на C код, като използвам готов SMT решаващ инструмент и се чудя кой решаващ инструмент да използвам; гледайки напр. участниците в конкурса за SMT и като се вземат само системите с отворен код, се стеснява до Beaver, Boolector, CVC3, OpenSMT, Sateen, Sonolar, STP, Verit; което все още е дълъг списък.
Опитвайки се да го стесня още малко, забелязвам, че някои от системите рекламират способността да обработват аритметика с битов вектор, докато други рекламират само способността да обработват обща аритметика с цели числа. По принцип първото е правилно за C, където променливите са машинни думи, а не неограничени цели числа. Колко голяма е разликата на практика? Какво се случва, ако се опитате да използвате обща система за цели числа за този вид работа? Приложим ли е един от следните сценарии?
Системата с битов вектор е малко по-ефективна, но можете да използвате и двете, без проблем.
Можете да използвате обща система с цели числа с малко корекции.
Общата система за цели числа е добра за int със знак (тъй като резултатът от препълване е недефиниран), но ще даде грешен отговор за unsigned.
Общата система с цели числа просто не е правилна за аритметика с машинни думи и мога да намаля краткия си списък само до онези системи, които осигуряват аритметика с битов вектор.
Нещо друго...?
Опитах се да задам възможно най-конкретен въпрос, но ако някой може да предложи други критерии за стесняване на списъка, това би било чудесно!
