package binsec

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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