ИСТИНА |
Войти в систему Регистрация |
|
ИПМех РАН |
||
Библиотека позволяет создавать формулы в форме синтаксических деревьев, транслировать их во внешние форматы (языки программирования высокого уровня, языки описания цифровой аппаратуры, а также XML и SMT-LIB), вычислять их значения и осуществлять их символическое упрощение. Также она позволяет решать ограничения при помощи внешних решателей (таких как Z3 и CVC4). Кроме этого библиотека содержит классы для описания битовых векторов и осуществления различных операций над ними, а также классы для генерации псевдослучайных значений различного типа.