Значение (_ bv0 32), (_ bv1 16) ... в тестах SMT2

Question

Я заметил, что это некоторые тесты SMT2, обозначения, такие как (_ bv0 32), (_ bv16 32),... используются как, например, в:

QF_FP / Schanda / искровым / zeros_consistent_2.smt2

http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.rev_xstrcoll_mtime.il.wp.smt2

http://rise4fun.com/Z3/e1s

Тем не менее, это не ссылка на такие символы в декларациях теорий:

http://smtlib.cs.uiowa.edu/theories.shtml

Любой комментарий по этому поводу? В чем их смысл?

Спасибо!

Answer 1

(_ bv0 32) - константа битового вектора, кодирующая значение 0 в 32 битах.

Вы можете найти формальное описание в определении логики в разделе "Константы битвектора" http://smtlib.cs.uiowa.edu/logics-all.shtml