Dba_to_formula (p.binsec.0.6.2.doc.binsec.Binsec.Dba_to

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.t -> Formula.bv_unop

convert a DBA unary operator to a Smtlib unary operator

val binary : 
  Dba.Binary_op.t ->
  [ `Unop of Formula.bv_unop
  | `Bnop of Formula.bv_bnop
  | `Comp of Formula.bv_comp ]

convert a DBA binary operator to a Smtlib binary operator