module Primop_gen : PRIMOP_GENval smt_cval : Jib.cval -> Smt_exp.smt_exp check_writerConvert a Jib IR cval into an SMT expression
val int_size : Jib.ctyp -> intval bv_size : Jib.ctyp -> intval generic_vector_length : Jib.ctyp -> intval wf_lbits : Smt_exp.smt_exp -> Smt_exp.smt_expval smt_conversion :
into:Jib.ctyp ->
from:Jib.ctyp ->
Smt_exp.smt_exp ->
Smt_exp.smt_exp check_writerCreate an SMT expression that converts an expression of the jib type from into an SMT expression for the jib type into. Note that this function assumes that the input is of the correct type.
val builtin :
?allow_io:bool ->
?undefined:undefined_mode ->
string ->
(Jib.cval list -> Jib.ctyp -> Smt_exp.smt_exp check_writer) optionCompile a call to a Sail builtin function into an SMT expression implementing that call. Returns None if that builtin is unsupported by this module.