74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
z3::expr GetAsInt( const Z3Val& zv )
{
return GetAsInt( zv.expr, zv.type );
}
z3::expr Coerce( const Z3Val& val, const Z3Val& to )
{
if( to.expr.is_int() )
return GetAsInt( val.expr, to.type );
else if( to.expr.is_bv() )
return GetAsBitVec( val.expr, to.type );
else
return val.expr;
}
template< typename I, typename F >
optional< Z3Val > BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
{
auto operand = BuildZ3ExprFromValue( b, instr.operand() );
if( !operand )
|
>
>
>
>
>
|
|
|
|
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
z3::expr GetAsInt( const Z3Val& zv )
{
return GetAsInt( zv.expr, zv.type );
}
z3::expr Coerce( const Z3Val& val, const Z3Val& to )
{
return Coerce( val.expr, to );
}
z3::expr Coerce( const z3::expr& expr, const Z3Val& to )
{
if( to.expr.is_int() )
return GetAsInt( expr, to.type );
else if( to.expr.is_bv() )
return GetAsBitVec( expr, to.type );
else
return expr;
}
template< typename I, typename F >
optional< Z3Val > BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
{
auto operand = BuildZ3ExprFromValue( b, instr.operand() );
if( !operand )
|