Module Smt_bitvectors

module Smt_bitvectors: sig .. end
Types for SMT-LIB bitvectors

type basic_value = [ `Undef of int | `Value of Dba.region * Bitvector.t ] 
type smtBvVarAlt = string * int * basic_value 
type smtBvExprAlt = 
| SmtBvCstAlt of Bitvector.t
| SmtBvVarAlt of smtBvVarAlt
| SmtBvUnaryAlt of Smtlib2.smt_bv_unary * smtBvExprAlt
| SmtBvBinaryAlt of Smtlib2.smt_bv_binary * smtBvExprAlt
* smtBvExprAlt
| SmtBvIteAlt of smtBvExprAlt * smtBvExprAlt
* smtBvExprAlt
| SmtBvUndefAlt of int * int
type condition_env = smtBvExprAlt list 
val smtBvExprAlt_to_smtBvExpr : smtBvExprAlt -> Smtlib2.smt_bv_expr
val is_equal_smtBvExpr : smtBvExprAlt -> smtBvExprAlt -> bool
val smtBvExpr_to_hstring : smtBvExprAlt -> string
val smtBvExpr_to_string : smtBvExprAlt -> string
val gen_undef : int -> smtBvExprAlt
exception Assume_condition of smtBvExprAlt