SMT-решатели для арифметики битовых векторов
Я планирую несколько экспериментов по символьному выполнению кода C, используя стандартный решатель SMT, и задаюсь вопросом, какой решатель использовать; глядя, например, участники конкурса SMT, и принимая только системы с открытым исходным кодом, сужают его до Beaver, Boolector, CVC3, OpenSMT, Sateen, Sonolar, STP, Verit; это все еще длинный список.
Пытаясь сузить его немного дальше, я замечаю, что некоторые из систем рекламируют возможность обработки арифметики битовых векторов, тогда как другие рекламируют только возможность обработки общей арифметики целых чисел. В принципе, первое верно для языка C, где переменные - это машинные слова, а не неограниченные целые числа. Насколько это заметно на практике? Что произойдет, если вы попытаетесь использовать общую целочисленную систему для такой работы? Применяется ли один из следующих сценариев?
Битовая векторная система немного более эффективна, но вы можете использовать любой, без проблем.
Вы можете использовать общую целочисленную систему с небольшой настройкой.
Общая Целочисленная система подходит для знакового int (поскольку результат переполнения не определен), но даст неправильный ответ для беззнакового.
Общая целочисленная система просто не подходит для арифметики машинных слов, и я могу сократить свой короткий список до только те системы, которые обеспечивают арифметику битовых векторов.
Что-то еще ...?
Я попытался задать как можно более конкретный вопрос, но если кто-нибудь может предложить какие-либо другие критерии для сужения списка, это