Module Dba_to_smtlib

module Dba_to_smtlib: sig .. end
Convert some DBA structure to Smtlib

exception NoSmtEquivalent
Raised if trying to convert DBA operators that don't have equivalent in smtlib2. The two operators that don't have equivalent are: Dba.LeftRotate and Dba.RightRotate that can take a variable shift value while smtlib2 only support constant
val unary : Dba.unary_op -> Smtlib2.smt_bv_unary
convert a DBA unary operator to a Smtlib unary operator
val binary : Dba.binary_op -> Smtlib2.smt_bv_binary
convert a DBA binary operator to a Smtlib binary operator