39 #define PARSERERROR(S) throw S 42 #define INVALIDEXPR(S) throw "Invalid expression: " S 46 #define UNEXPECTEDCASE(S) throw "Unexpected case: " S 49 #define SMT2_TODO(S) throw "TODO: " S 73 out <<
"; SMT 2" <<
"\n";
86 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
88 out <<
"(set-option :produce-models true)" <<
"\n";
94 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
104 out <<
"; assumptions\n";
118 out <<
"(check-sat)" <<
"\n";
124 out <<
"(get-value (|" <<
id <<
"|))" <<
"\n";
131 out <<
"; end of SMT2 file" <<
"\n";
138 assert(expr.
id()==ID_object_size);
142 std::size_t number = 0;
143 std::size_t h=pointer_width-1;
152 if(o.id()!=ID_symbol ||
160 out <<
"(assert (implies (= " <<
161 "((_ extract " << h <<
" " << l <<
") ";
163 out <<
") (_ bv" << number <<
" " 165 <<
"(= " <<
id <<
" (_ bv" <<
object_size.to_ulong() <<
" " 166 << size_width <<
"))))\n";
181 if(expr.
id()==ID_symbol)
188 return it->second.value;
190 else if(expr.
id()==ID_nondet_symbol)
197 return it->second.value;
199 else if(expr.
id()==ID_member)
238 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
243 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
254 else if(src.
get_sub().size()==2 &&
259 else if(src.
get_sub().size()==3 &&
262 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
266 else if(src.
get_sub().size()==4 &&
269 if(type.
id()==ID_floatbv)
286 else if(src.
get_sub().size()==4 &&
294 else if(src.
get_sub().size()==4 &&
302 else if(src.
get_sub().size()==4 &&
311 if(type.
id()==ID_signedbv ||
312 type.
id()==ID_unsignedbv ||
314 type.
id()==ID_c_enum ||
315 type.
id()==ID_c_bool)
319 else if(type.
id()==ID_c_enum_tag)
326 else if(type.
id()==ID_fixedbv ||
327 type.
id()==ID_floatbv)
332 else if(type.
id()==ID_integer ||
355 else if(src.
get_sub().size()==2 &&
356 src.
get_sub()[0].get_sub().size()==3 &&
357 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
358 src.
get_sub()[0].get_sub()[1].id()==
"const")
381 return union_exprt(first.get_name(), converted, type);
395 if(components.empty())
403 if(src.
get_sub().size()!=components.size()+1)
406 for(std::size_t i=0; i<components.size(); i++)
421 if(binary.
size()!=total_width)
424 std::size_t offset=0;
426 for(std::size_t i=0; i<components.size(); i++)
428 std::size_t component_width=
boolbv_width(components[i].type());
430 assert(offset+component_width<=total_width);
431 std::string component_binary=
433 total_width-offset-component_width, component_width);
438 offset+=component_width;
449 if(type.
id()==ID_signedbv ||
450 type.
id()==ID_unsignedbv ||
451 type.
id()==ID_integer ||
452 type.
id()==ID_rational ||
453 type.
id()==ID_real ||
455 type.
id()==ID_fixedbv ||
456 type.
id()==ID_floatbv)
460 else if(type.
id()==ID_bool)
462 if(src.
id()==ID_1 || src.
id()==ID_true)
464 else if(src.
id()==ID_0 || src.
id()==ID_false)
467 else if(type.
id()==ID_pointer)
483 else if(type.
id()==ID_struct)
487 else if(type.
id()==ID_union)
491 else if(type.
id()==ID_array)
503 if(expr.
id()==ID_symbol ||
504 expr.
id()==ID_constant ||
505 expr.
id()==ID_string_constant ||
515 else if(expr.
id()==ID_index)
525 if(array.
type().
id()==ID_pointer)
527 else if(array.
type().
id()==ID_array)
535 exprt new_index_expr=expr;
545 address_of_expr.
type());
550 else if(expr.
id()==ID_member)
560 if(struct_op_type.
id()==ID_struct)
582 else if(expr.
id()==ID_if)
619 INVALIDEXPR(
"byte_update takes constant as second parameter");
630 if(expr.
id()==ID_byte_update_little_endian)
633 upper = lower+value_width-1;
635 else if(expr.
id()==ID_byte_update_big_endian)
638 lower = max-((i+1)*8-1);
655 out <<
" ((_ extract " << lower-1 <<
" 0) ";
665 out <<
"((_ extract " << max <<
" " << (upper+1) <<
") ";
673 out <<
"(concat (concat ";
674 out <<
"((_ extract " << max <<
" " << (upper+1) <<
") ";
678 out <<
") ((_ extract " << (lower-1) <<
" 0) ";
712 assert(expr.
type().
id()==ID_bool);
720 else if(expr.
id()==ID_literal)
732 out <<
"; convert\n";
733 out <<
"(define-fun ";
770 for(std::size_t i=0; i<identifier.
size(); i++)
772 char ch=identifier[i];
795 if(type.
id()==ID_floatbv)
800 else if(type.
id()==ID_unsignedbv)
804 else if(type.
id()==ID_c_bool)
808 else if(type.
id()==ID_signedbv)
812 else if(type.
id()==ID_bool)
816 else if(type.
id()==ID_c_enum_tag)
837 if(expr.
id()==ID_symbol)
844 if(expr.
id()==ID_smt2_symbol)
853 out <<
"(|float_bv." << expr.
id()
869 if(expr.
id()==ID_symbol)
875 else if(expr.
id()==ID_nondet_symbol)
881 else if(expr.
id()==ID_smt2_symbol)
887 else if(expr.
id()==ID_typecast)
891 else if(expr.
id()==ID_floatbv_typecast)
895 else if(expr.
id()==ID_struct)
899 else if(expr.
id()==ID_union)
903 else if(expr.
id()==ID_constant)
907 else if(expr.
id()==ID_concatenation ||
908 expr.
id()==ID_bitand ||
909 expr.
id()==ID_bitor ||
910 expr.
id()==ID_bitxor ||
911 expr.
id()==ID_bitnand ||
912 expr.
id()==ID_bitnor)
918 if(expr.
id()==ID_concatenation)
920 else if(expr.
id()==ID_bitand)
922 else if(expr.
id()==ID_bitor)
924 else if(expr.
id()==ID_bitxor)
926 else if(expr.
id()==ID_bitnand)
928 else if(expr.
id()==ID_bitnor)
939 else if(expr.
id()==ID_bitnot)
943 if(expr.
type().
id()==ID_vector)
949 const std::string smt_typename=
957 INVALIDEXPR(
"failed to convert vector size to constant");
959 out <<
"(let ((?vectorop ";
963 out <<
"(mk-" << smt_typename;
970 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
986 else if(expr.
id()==ID_unary_minus)
990 if(expr.
type().
id()==ID_rational ||
991 expr.
type().
id()==ID_integer ||
992 expr.
type().
id()==ID_real)
998 else if(expr.
type().
id()==ID_floatbv)
1010 else if(expr.
type().
id()==ID_vector)
1016 const std::string smt_typename=
1024 INVALIDEXPR(
"failed to convert vector size to constant");
1026 out <<
"(let ((?vectorop ";
1030 out <<
"(mk-" << smt_typename;
1037 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1053 else if(expr.
id()==ID_unary_plus)
1059 else if(expr.
id()==ID_sign)
1065 if(op_type.id()==ID_floatbv)
1069 out <<
"(fp.isNegative ";
1076 else if(op_type.id()==ID_signedbv)
1082 out <<
" (_ bv0 " << op_width <<
"))";
1087 else if(expr.
id()==ID_if)
1099 else if(expr.
id()==ID_and ||
1103 assert(expr.
type().
id()==ID_bool);
1106 out <<
"(" << expr.
id();
1114 else if(expr.
id()==ID_implies)
1116 assert(expr.
type().
id()==ID_bool);
1125 else if(expr.
id()==ID_not)
1127 assert(expr.
type().
id()==ID_bool);
1134 else if(expr.
id()==ID_equal ||
1135 expr.
id()==ID_notequal)
1140 if(expr.
id()==ID_notequal)
1157 else if(expr.
id()==ID_ieee_float_equal ||
1158 expr.
id()==ID_ieee_float_notequal)
1168 if(expr.
id()==ID_ieee_float_notequal)
1177 if(expr.
id()==ID_ieee_float_notequal)
1183 else if(expr.
id()==ID_le ||
1190 else if(expr.
id()==ID_plus)
1194 else if(expr.
id()==ID_floatbv_plus)
1198 else if(expr.
id()==ID_minus)
1202 else if(expr.
id()==ID_floatbv_minus)
1206 else if(expr.
id()==ID_div)
1210 else if(expr.
id()==ID_floatbv_div)
1214 else if(expr.
id()==ID_mod)
1218 else if(expr.
id()==ID_mult)
1222 else if(expr.
id()==ID_floatbv_mult)
1226 else if(expr.
id()==ID_address_of)
1229 assert(expr.
type().
id()==ID_pointer);
1232 else if(expr.
id()==ID_array_of)
1234 assert(expr.
type().
id()==ID_array);
1240 else if(expr.
id()==ID_index)
1244 else if(expr.
id()==ID_ashr ||
1245 expr.
id()==ID_lshr ||
1252 if(type.
id()==ID_unsignedbv ||
1253 type.
id()==ID_signedbv ||
1256 if(expr.
id()==ID_ashr)
1258 else if(expr.
id()==ID_lshr)
1260 else if(expr.
id()==ID_shl)
1282 else if(expr.
op1().
type().
id()==ID_signedbv ||
1283 expr.
op1().
type().
id()==ID_unsignedbv ||
1290 if(width_op0==width_op1)
1292 else if(width_op0>width_op1)
1294 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1300 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1307 "unsupported op1 type for "+expr.
id_string()+
": "+
1316 else if(expr.
id()==ID_with)
1320 else if(expr.
id()==ID_update)
1324 else if(expr.
id()==ID_member)
1328 else if(expr.
id()==ID_pointer_offset)
1331 assert(expr.
op0().
type().
id()==ID_pointer);
1332 std::size_t offset_bits=
1337 if(offset_bits>result_width)
1338 offset_bits=result_width;
1341 if(result_width>offset_bits)
1342 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1344 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1348 if(result_width>offset_bits)
1351 else if(expr.
id()==ID_pointer_object)
1354 assert(expr.
op0().
type().
id()==ID_pointer);
1359 out <<
"((_ zero_extend " << ext <<
") ";
1361 out <<
"((_ extract " 1362 << pointer_width-1 <<
" " 1370 else if(expr.
id()==ID_dynamic_object)
1374 else if(expr.
id()==ID_invalid_pointer)
1379 out <<
"(= ((_ extract " 1380 << pointer_width-1 <<
" " 1386 else if(expr.
id()==
"pointer_object_has_type")
1391 SMT2_TODO(
"pointer_object_has_type not implemented");
1393 else if(expr.
id()==ID_string_constant)
1399 else if(expr.
id()==ID_extractbit)
1409 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1415 out <<
"(= ((_ extract 0 0) ";
1425 else if(expr.
id()==ID_extractbits)
1440 std::swap(op1_i, op2_i);
1444 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1451 out <<
"(= ((_ extract 0 0) ";
1460 SMT2_TODO(
"smt2: extractbits with non-constant index");
1463 else if(expr.
id()==ID_replication)
1469 INVALIDEXPR(
"replication takes constant as first parameter");
1471 out <<
"((_ repeat " << times <<
") ";
1475 else if(expr.
id()==ID_byte_extract_little_endian ||
1476 expr.
id()==ID_byte_extract_big_endian)
1480 else if(expr.
id()==ID_byte_update_little_endian ||
1481 expr.
id()==ID_byte_update_big_endian)
1485 else if(expr.
id()==ID_width)
1502 out <<
"(_ bv" << op_width/8
1503 <<
" " << result_width <<
")";
1505 else if(expr.
id()==ID_abs)
1511 if(type.id()==ID_signedbv)
1515 out <<
"(ite (bvslt ";
1517 out <<
" (_ bv0 " << result_width <<
")) ";
1524 else if(type.id()==ID_fixedbv)
1528 out <<
"(ite (bvslt ";
1530 out <<
" (_ bv0 " << result_width <<
")) ";
1537 else if(type.id()==ID_floatbv)
1551 else if(expr.
id()==ID_isnan)
1557 if(op_type.id()==ID_fixedbv)
1559 else if(op_type.id()==ID_floatbv)
1563 out <<
"(fp.isNaN ";
1573 else if(expr.
id()==ID_isfinite)
1580 if(op_type.
id()==ID_fixedbv)
1582 else if(op_type.
id()==ID_floatbv)
1588 out <<
"(not (fp.isNaN ";
1592 out <<
"(not (fp.isInf ";
1604 else if(expr.
id()==ID_isinf)
1611 if(op_type.
id()==ID_fixedbv)
1613 else if(op_type.
id()==ID_floatbv)
1617 out <<
"(fp.isInfinite ";
1627 else if(expr.
id()==ID_isnormal)
1634 if(op_type.
id()==ID_fixedbv)
1636 else if(op_type.
id()==ID_floatbv)
1640 out <<
"(fp.isNormal ";
1650 else if(expr.
id()==ID_overflow_plus ||
1651 expr.
id()==ID_overflow_minus)
1654 assert(expr.
type().
id()==ID_bool);
1656 bool subtract=expr.
id()==ID_overflow_minus;
1660 if(op_type.
id()==ID_signedbv)
1663 out <<
"(let ((?sum (";
1664 out << (subtract?
"bvsub":
"bvadd");
1665 out <<
" ((_ sign_extend 1) ";
1668 out <<
" ((_ sign_extend 1) ";
1672 "((_ extract " << width <<
" " << width <<
") ?sum) " 1673 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1676 else if(op_type.
id()==ID_unsignedbv ||
1677 op_type.
id()==ID_pointer)
1681 out <<
"((_ extract " << width <<
" " << width <<
") ";
1682 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1683 out <<
" ((_ zero_extend 1) ";
1686 out <<
" ((_ zero_extend 1) ";
1694 else if(expr.
id()==ID_overflow_mult)
1704 if(op_type.id()==ID_signedbv)
1706 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1708 out <<
") ((_ sign_extend " << width <<
") ";
1711 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" " 1713 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" " 1714 << width*2 <<
")))))";
1716 else if(op_type.id()==ID_unsignedbv)
1718 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1720 out <<
") ((_ zero_extend " << width <<
") ";
1722 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1725 UNEXPECTEDCASE(
"overflow-* check on unknown type: "+op_type.id_string());
1727 else if(expr.
id()==ID_array)
1733 else if(expr.
id()==ID_literal)
1737 else if(expr.
id()==ID_forall ||
1738 expr.
id()==ID_exists)
1742 throw "MathSAT does not support quantifiers";
1744 if(expr.
id()==ID_forall)
1746 else if(expr.
id()==ID_exists)
1761 else if(expr.
id()==ID_vector)
1767 INVALIDEXPR(
"failed to convert vector size to constant");
1769 assert(size==expr.
operands().size());
1775 const std::string smt_typename=
1778 out <<
"(mk-" << smt_typename;
1792 else if(expr.
id()==ID_object_size)
1796 else if(expr.
id()==ID_let)
1807 else if(expr.
id()==ID_constraint_select_one)
1810 "smt2_convt::convert_expr: `"+expr.
id_string()+
1811 "' is not yet supported");
1813 else if(expr.
id() == ID_bswap)
1819 INVALIDEXPR(
"bswap gets one operand with same type");
1822 out <<
"(let ((bswap_op ";
1826 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1834 const std::size_t bytes = width / 8;
1843 for(std::size_t byte = 0; byte < bytes; byte++)
1847 out <<
"(bswap_byte_" << byte <<
' ';
1848 out <<
"((_ extract " << (byte * 8 + 7) <<
" " << (byte * 8)
1858 for(std::size_t byte = 0; byte < bytes; byte++)
1859 out <<
" bswap_byte_" << byte;
1870 else if(expr.
id() == ID_popcount)
1877 "smt2_convt::convert_expr: `"+expr.
id_string()+
"' is unsupported");
1886 if(dest_type.
id()==ID_c_enum_tag)
1890 if(src_type.
id()==ID_c_enum_tag)
1893 if(dest_type.
id()==ID_bool)
1896 if(src_type.
id()==ID_signedbv ||
1897 src_type.
id()==ID_unsignedbv ||
1898 src_type.
id()==ID_c_bool ||
1899 src_type.
id()==ID_fixedbv ||
1900 src_type.
id()==ID_pointer ||
1901 src_type.
id()==ID_integer)
1909 else if(src_type.
id()==ID_floatbv)
1913 out <<
"(not (fp.isZero ";
1925 else if(dest_type.
id()==ID_c_bool)
1934 out <<
" (_ bv1 " << to_width <<
")";
1935 out <<
" (_ bv0 " << to_width <<
")";
1938 else if(dest_type.
id()==ID_signedbv ||
1939 dest_type.
id()==ID_unsignedbv ||
1940 dest_type.
id()==ID_c_enum ||
1941 dest_type.
id()==ID_bv)
1945 if(src_type.
id()==ID_signedbv ||
1946 src_type.
id()==ID_unsignedbv ||
1947 src_type.
id()==ID_c_bool ||
1948 src_type.
id()==ID_c_enum ||
1949 src_type.
id()==ID_bv)
1953 if(from_width==to_width)
1955 else if(from_width<to_width)
1957 if(src_type.
id()==ID_signedbv)
1958 out <<
"((_ sign_extend ";
1960 out <<
"((_ zero_extend ";
1962 out << (to_width-from_width)
1969 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
1974 else if(src_type.
id()==ID_fixedbv)
1978 std::size_t from_width=fixedbv_type.
get_width();
1985 out <<
"(let ((?tcop ";
1991 if(to_width>from_integer_bits)
1993 out <<
"((_ sign_extend " 1994 << (to_width-from_integer_bits) <<
") ";
1995 out <<
"((_ extract " << (from_width-1) <<
" " 1996 << from_fraction_bits <<
") ";
2002 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2003 <<
" " << from_fraction_bits <<
") ";
2008 out <<
" (ite (and ";
2011 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) " 2012 "(_ bv0 " << from_fraction_bits <<
")))";
2015 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2020 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2024 else if(src_type.
id()==ID_floatbv)
2026 if(dest_type.
id()==ID_bv)
2043 else if(dest_type.
id()==ID_signedbv)
2047 "typecast unexpected "+src_type.
id_string()+
" -> "+
2050 else if(dest_type.
id()==ID_unsignedbv)
2054 "typecast unexpected "+src_type.
id_string()+
" -> "+
2058 else if(src_type.
id()==ID_bool)
2063 if(dest_type.
id()==ID_fixedbv)
2066 out <<
" (concat (_ bv1 " 2069 "(_ bv0 " << spec.
width <<
")";
2073 out <<
" (_ bv1 " << to_width <<
")";
2074 out <<
" (_ bv0 " << to_width <<
")";
2079 else if(src_type.
id()==ID_pointer)
2083 if(from_width<to_width)
2085 out <<
"((_ sign_extend ";
2086 out << (to_width-from_width)
2093 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2098 else if(src_type.
id()==ID_integer)
2101 if(src.is_constant())
2105 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2108 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2110 else if(src_type.
id()==ID_struct)
2123 else if(src_type.
id()==ID_union)
2128 else if(src_type.
id()==ID_c_bit_field)
2132 if(from_width==to_width)
2143 std::ostringstream e_str;
2144 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2145 <<
" src == " <<
format(src);
2149 else if(dest_type.
id()==ID_fixedbv)
2155 if(src_type.
id()==ID_unsignedbv ||
2156 src_type.
id()==ID_signedbv ||
2157 src_type.
id()==ID_c_enum)
2164 if(from_width==to_integer_bits)
2166 else if(from_width>to_integer_bits)
2169 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2176 assert(from_width<to_integer_bits);
2177 if(dest_type.
id()==ID_unsignedbv)
2179 out <<
"(_ zero_extend " 2180 << (to_integer_bits-from_width) <<
") ";
2186 out <<
"((_ sign_extend " 2187 << (to_integer_bits-from_width) <<
") ";
2193 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2196 else if(src_type.
id()==ID_bool)
2198 out <<
"(concat (concat" 2199 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2205 else if(src_type.
id()==ID_fixedbv)
2210 std::size_t from_width=from_fixedbv_type.
get_width();
2212 out <<
"(let ((?tcop ";
2218 if(to_integer_bits<=from_integer_bits)
2220 out <<
"((_ extract " 2221 << (from_fraction_bits+to_integer_bits-1) <<
" " 2222 << from_fraction_bits
2227 assert(to_integer_bits>from_integer_bits);
2228 out <<
"((_ sign_extend " 2229 << (to_integer_bits-from_integer_bits)
2231 << (from_width-1) <<
" " 2232 << from_fraction_bits
2238 if(to_fraction_bits<=from_fraction_bits)
2240 out <<
"((_ extract " 2241 << (from_fraction_bits-1) <<
" " 2242 << (from_fraction_bits-to_fraction_bits)
2247 assert(to_fraction_bits>from_fraction_bits);
2248 out <<
"(concat ((_ extract " 2249 << (from_fraction_bits-1) <<
" 0) ";
2252 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2261 else if(dest_type.
id()==ID_pointer)
2265 if(src_type.
id()==ID_pointer)
2270 else if(src_type.
id()==ID_unsignedbv ||
2271 src_type.
id()==ID_signedbv)
2277 if(from_width==to_width)
2279 else if(from_width<to_width)
2281 out <<
"((_ sign_extend " 2282 << (to_width-from_width)
2289 out <<
"((_ extract " << to_width <<
" 0) ";
2297 else if(dest_type.
id()==ID_range)
2301 else if(dest_type.
id()==ID_floatbv)
2309 if(src_type.
id()==ID_bool)
2324 a.
build(significand, exponent);
2332 a.
build(significand, exponent);
2338 else if(src_type.
id()==ID_c_bool)
2347 else if(dest_type.
id()==ID_integer)
2349 if(src_type.
id()==ID_bool)
2358 else if(dest_type.
id()==ID_c_bit_field)
2363 if(from_width==to_width)
2384 if(dest_type.
id()==ID_floatbv)
2386 if(src_type.
id()==ID_floatbv)
2413 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2414 << dst.
get_f() + 1 <<
") ";
2423 else if(src_type.
id()==ID_unsignedbv)
2444 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" " 2445 << dst.
get_f() + 1 <<
") ";
2454 else if(src_type.
id()==ID_signedbv)
2462 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2463 << dst.
get_f() + 1 <<
") ";
2472 else if(src_type.
id()==ID_c_enum_tag)
2488 else if(dest_type.
id()==ID_signedbv)
2493 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2502 else if(dest_type.
id()==ID_unsignedbv)
2507 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2530 assert(components.size()==expr.
operands().size());
2532 assert(!components.empty());
2537 const std::string smt_typename =
2541 out <<
"(mk-" << smt_typename;
2544 for(struct_typet::componentst::const_iterator
2545 it=components.begin();
2546 it!=components.end();
2557 if(components.size()==1)
2562 for(std::size_t i=components.size(); i>1; i--)
2579 for(std::size_t i=1; i<components.size(); i++)
2593 INVALIDEXPR(
"failed to convert array size for flattening");
2598 out <<
"(let ((?far ";
2606 out <<
"(select ?far ";
2630 INVALIDEXPR(
"failed to get union width for union");
2635 INVALIDEXPR(
"failed to get union member width for union");
2637 if(total_width==member_width)
2644 assert(total_width>member_width);
2647 << (total_width-member_width) <<
") ";
2657 if(expr_type.
id()==ID_unsignedbv ||
2658 expr_type.
id()==ID_signedbv ||
2659 expr_type.
id()==ID_bv ||
2660 expr_type.
id()==ID_c_enum ||
2661 expr_type.
id()==ID_c_enum_tag ||
2662 expr_type.
id()==ID_c_bool ||
2663 expr_type.
id()==ID_incomplete_c_enum ||
2664 expr_type.
id()==ID_c_bit_field)
2670 out <<
"(_ bv" << value
2671 <<
" " << width <<
")";
2673 else if(expr_type.
id()==ID_fixedbv)
2680 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2682 else if(expr_type.
id()==ID_floatbv)
2695 size_t e=floatbv_type.
get_e();
2696 size_t f=floatbv_type.
get_f()+1;
2702 out <<
"((_ to_fp " << e <<
" " << f <<
")" 2708 out <<
"(_ NaN " << e <<
" " << f <<
")";
2713 out <<
"(_ -oo " << e <<
" " << f <<
")";
2715 out <<
"(_ +oo " << e <<
" " << f <<
")";
2725 <<
"#b" << binaryString.substr(0, 1) <<
" " 2726 <<
"#b" << binaryString.substr(1, e) <<
" " 2727 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
2738 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
2741 else if(expr_type.
id()==ID_pointer)
2753 else if(expr_type.
id()==ID_bool)
2762 else if(expr_type.
id()==ID_array)
2768 else if(expr_type.
id()==ID_rational)
2771 size_t pos=value.find(
"/");
2773 if(
pos==std::string::npos)
2774 out << value <<
".0";
2777 out <<
"(/ " << value.substr(0,
pos) <<
".0 " 2778 << value.substr(
pos+1) <<
".0)";
2781 else if(expr_type.
id()==ID_integer)
2793 if(expr.
type().
id()==ID_unsignedbv ||
2794 expr.
type().
id()==ID_signedbv)
2796 if(expr.
type().
id()==ID_unsignedbv)
2812 std::vector<std::size_t> dynamic_objects;
2817 if(dynamic_objects.empty())
2823 out <<
"(let ((?obj ((_ extract " 2824 << pointer_width-1 <<
" " 2829 if(dynamic_objects.size()==1)
2831 out <<
"(= (_ bv" << dynamic_objects.front()
2838 for(
const auto &
object : dynamic_objects)
2839 out <<
" (= (_ bv" <<
object 2855 if(op_type.id()==ID_unsignedbv ||
2856 op_type.id()==ID_pointer ||
2857 op_type.id()==ID_bv)
2860 if(expr.
id()==ID_le)
2862 else if(expr.
id()==ID_lt)
2864 else if(expr.
id()==ID_ge)
2866 else if(expr.
id()==ID_gt)
2875 else if(op_type.id()==ID_signedbv ||
2876 op_type.id()==ID_fixedbv)
2879 if(expr.
id()==ID_le)
2881 else if(expr.
id()==ID_lt)
2883 else if(expr.
id()==ID_ge)
2885 else if(expr.
id()==ID_gt)
2894 else if(op_type.id()==ID_floatbv)
2899 if(expr.
id()==ID_le)
2901 else if(expr.
id()==ID_lt)
2903 else if(expr.
id()==ID_ge)
2905 else if(expr.
id()==ID_gt)
2917 else if(op_type.id()==ID_rational ||
2918 op_type.id()==ID_integer)
2931 "unsupported type for "+expr.
id_string()+
": "+op_type.id_string());
2946 if(expr.
type().
id()==ID_rational ||
2947 expr.
type().
id()==ID_integer ||
2948 expr.
type().
id()==ID_real)
2953 for(
const auto &op : expr.
operands())
2961 else if(expr.
type().
id()==ID_unsignedbv ||
2962 expr.
type().
id()==ID_signedbv ||
2963 expr.
type().
id()==ID_fixedbv)
2980 else if(expr.
type().
id()==ID_floatbv)
2987 else if(expr.
type().
id()==ID_pointer)
2993 if(p.
type().
id()!=ID_pointer)
2996 if(p.
type().
id()!=ID_pointer)
2997 INVALIDEXPR(
"unexpected mixture in pointer arithmetic");
3011 out <<
" (_ bv" << element_size
3024 else if(expr.
type().
id()==ID_vector)
3030 INVALIDEXPR(
"failed to convert vector size to constant");
3038 const std::string smt_typename=
3041 out <<
"(mk-" << smt_typename;
3051 tmp.copy_to_operands(
3085 if(expr.
id()==ID_constant)
3092 out <<
"roundNearestTiesToEven";
3094 out <<
"roundTowardNegative";
3096 out <<
"roundTowardPositive";
3098 out <<
"roundTowardZero";
3101 "Unknown constant rounding mode with value "+
3109 out <<
"(ite (= (_ bv0 " << width <<
") ";
3111 out <<
") roundNearestTiesToEven ";
3113 out <<
"(ite (= (_ bv1 " << width <<
") ";
3115 out <<
") roundTowardNegative ";
3117 out <<
"(ite (= (_ bv2 " << width <<
") ";
3119 out <<
") roundTowardPositive ";
3122 out <<
"roundTowardZero";
3133 assert(type.
id()==ID_floatbv ||
3134 (type.
id()==ID_complex && type.
subtype().
id()==ID_floatbv) ||
3135 (type.
id()==ID_vector && type.
subtype().
id()==ID_floatbv));
3139 if(type.
id()==ID_floatbv)
3149 else if(type.
id()==ID_complex)
3153 else if(type.
id()==ID_vector)
3168 if(expr.
type().
id()==ID_integer)
3176 else if(expr.
type().
id()==ID_unsignedbv ||
3177 expr.
type().
id()==ID_signedbv ||
3178 expr.
type().
id()==ID_fixedbv)
3180 if(expr.
op0().
type().
id()==ID_pointer &&
3186 assert(element_size>0);
3200 out <<
" (_ bv" << element_size
3212 else if(expr.
type().
id()==ID_floatbv)
3219 else if(expr.
type().
id()==ID_pointer)
3223 else if(expr.
type().
id()==ID_vector)
3229 INVALIDEXPR(
"failed to convert vector size to constant");
3237 const std::string smt_typename=
3240 out <<
"(mk-" << smt_typename;
3250 tmp.copy_to_operands(
3269 assert(expr.
type().
id()==ID_floatbv);
3289 if(expr.
type().
id()==ID_unsignedbv ||
3290 expr.
type().
id()==ID_signedbv)
3292 if(expr.
type().
id()==ID_unsignedbv)
3302 else if(expr.
type().
id()==ID_fixedbv)
3307 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3312 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3314 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3320 else if(expr.
type().
id()==ID_floatbv)
3334 assert(expr.
type().
id()==ID_floatbv);
3367 if(expr.
type().
id()==ID_unsignedbv ||
3368 expr.
type().
id()==ID_signedbv)
3379 else if(expr.
type().
id()==ID_floatbv)
3386 else if(expr.
type().
id()==ID_fixedbv)
3391 out <<
"((_ extract " 3392 << spec.
width+fraction_bits-1 <<
" " 3393 << fraction_bits <<
") ";
3397 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3401 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3407 else if(expr.
type().
id()==ID_rational ||
3408 expr.
type().
id()==ID_integer ||
3409 expr.
type().
id()==ID_real)
3428 assert(expr.
type().
id()==ID_floatbv);
3452 std::size_t s=expr.
operands().size();
3459 assert(new_with_expr.
operands().size()==3);
3461 new_with_expr.
old()=tmp;
3471 if(expr_type.
id()==ID_array)
3495 out <<
"(let ((distance? ";
3496 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3500 if(array_width>index_width)
3502 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3508 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3517 out <<
"(bvlshr (_ bv" <<
power(2, array_width)-1 <<
" " 3518 << array_width <<
") ";
3519 out <<
"distance?) ";
3523 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3525 out <<
") distance?)))";
3528 else if(expr_type.
id()==ID_struct)
3535 const irep_idt &component_name=index.
get(ID_component_name);
3538 INVALIDEXPR(
"with failed to find component in struct");
3543 const std::string smt_typename=
3546 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3560 out <<
"(let ((?withop ";
3564 if(m.
width==struct_width)
3573 <<
"((_ extract " << (struct_width-1) <<
" " 3574 << m.
width <<
") ?withop) ";
3583 out <<
"((_ extract " << (m.
offset-1) <<
" 0) ?withop))";
3588 out <<
"(concat (concat " 3589 <<
"((_ extract " << (struct_width-1) <<
" " 3592 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3599 else if(expr_type.
id()==ID_union)
3610 INVALIDEXPR(
"failed to get union width for with");
3615 INVALIDEXPR(
"failed to get union member width for with");
3617 if(total_width==member_width)
3623 assert(total_width>member_width);
3625 out <<
"((_ extract " 3627 <<
" " << member_width <<
") ";
3634 else if(expr_type.
id()==ID_bv ||
3635 expr_type.
id()==ID_unsignedbv ||
3636 expr_type.
id()==ID_signedbv)
3664 out <<
" (bvnot (bvshl";
3667 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3668 out <<
" (repeat[" << value_width <<
"] bv1[1])";
3690 "with expects struct, union, or array type, but got "+
3698 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
3707 if(array_op_type.id()==ID_array)
3736 assert(array_width!=0);
3743 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
3747 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3751 if(array_width>index_width)
3753 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3759 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3769 else if(array_op_type.id()==ID_vector)
3776 const std::string smt_typename=
3784 SMT2_TODO(
"non-constant index on vectors");
3788 out <<
"(" << smt_typename <<
"." << index_int <<
" ";
3800 "index with unsupported array type: "+array_op_type.id_string());
3808 const exprt &struct_op=member_expr.struct_op();
3810 const irep_idt &name=member_expr.get_component_name();
3812 if(struct_op_type.
id()==ID_struct)
3823 const std::string smt_typename=
3826 out <<
"(" << smt_typename <<
"." 3838 INVALIDEXPR(
"failed to get struct member offset");
3846 else if(struct_op_type.
id()==ID_union)
3855 out <<
"((_ extract " 3865 "convert_member on an unexpected type "+struct_op_type.
id_string());
3872 if(type.
id()==ID_bool)
3878 else if(type.
id()==ID_vector)
3884 const std::string smt_typename=
3892 INVALIDEXPR(
"failed to convert vector size to constant");
3894 out <<
"(let ((?vflop ";
3902 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
3910 else if(type.
id()==ID_array)
3914 else if(type.
id()==ID_struct)
3920 const std::string smt_typename=
3926 out <<
"(let ((?sflop ";
3934 for(std::size_t i=components.size(); i>1; i--)
3936 out <<
"(concat (" << smt_typename <<
"." 3937 << components[i-1].get_name() <<
" ?sflop)";
3942 out <<
"(" << smt_typename <<
"." 3943 << components[0].get_name() <<
" ?sflop)";
3945 for(std::size_t i=1; i<components.size(); i++)
3953 else if(type.
id()==ID_floatbv)
3956 INVALIDEXPR(
"need to flatten floatbv in FPA theory");
3969 if(type.
id()==ID_symbol)
3972 if(type.
id()==ID_bool)
3979 else if(type.
id()==ID_vector)
3985 const std::string smt_typename=
3995 INVALIDEXPR(
"failed to convert vector size to constant");
3998 out <<
"(let ((?ufop" << nesting <<
" ";
4003 out <<
"(mk-" << smt_typename;
4005 std::size_t offset=0;
4007 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4011 out <<
"((_ extract " << offset+subtype_width-1 <<
" " 4012 << offset <<
") ?ufop" << nesting <<
")";
4024 else if(type.
id()==ID_struct)
4030 out <<
"(let ((?ufop" << nesting <<
" ";
4037 const std::string smt_typename=
4040 out <<
"(mk-" << smt_typename;
4047 std::size_t offset=0;
4050 for(struct_typet::componentst::const_iterator
4051 it=components.begin();
4052 it!=components.end();
4059 out <<
"((_ extract " << offset+member_width-1 <<
" " 4060 << offset <<
") ?ufop" << nesting <<
")";
4062 offset+=member_width;
4086 if(expr.
id()==ID_and && value)
4093 if(expr.
id()==ID_or && !value)
4100 if(expr.
id()==ID_not)
4108 assert(expr.
type().
id()==ID_bool);
4113 if(expr.
id()==ID_equal && value==
true)
4117 if(equal_expr.
lhs().
id()==ID_symbol)
4126 assert(
id.type.is_nil());
4128 id.type=equal_expr.
lhs().
type();
4135 out <<
"; set_to true (equal)\n";
4136 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4155 out <<
"; set_to " << (value?
"true":
"false") <<
"\n" 4181 if(expr.
id()==ID_symbol ||
4182 expr.
id()==ID_nondet_symbol)
4185 if(expr.
type().
id()==ID_code)
4190 if(expr.
id()==ID_symbol)
4193 identifier=
"nondet_"+
4198 if(
id.type.is_nil())
4200 id.type=expr.
type();
4205 out <<
"; find_symbols\n";
4206 out <<
"(declare-fun |" 4213 else if(expr.
id()==ID_array_of)
4218 out <<
"; the following is a substitute for lambda i. x" <<
"\n";
4219 out <<
"(declare-fun " <<
id <<
" () ";
4224 #if 0 // not really working in any solver yet! 4225 out <<
"(assert (forall ((i ";
4227 out <<
")) (= (select " <<
id <<
" i) ";
4229 out <<
")))" <<
"\n";
4235 else if(expr.
id()==ID_array)
4242 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4243 out <<
"(declare-fun " <<
id <<
" () ";
4247 for(std::size_t i=0; i<expr.
operands().size(); i++)
4249 out <<
"(assert (= (select " <<
id <<
" ";
4253 out <<
"))" <<
"\n";
4259 else if(expr.
id()==ID_string_constant)
4268 out <<
"; the following is a substitute for a string" <<
"\n";
4269 out <<
"(declare-fun " <<
id <<
" () ";
4273 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4275 out <<
"(assert (= (select " << id;
4279 out <<
"))" <<
"\n";
4285 else if(expr.
id()==ID_object_size &&
4290 if(op.
type().
id()==ID_pointer)
4295 out <<
"(declare-fun " <<
id <<
" () ";
4305 (expr.
id()==ID_floatbv_plus ||
4306 expr.
id()==ID_floatbv_minus ||
4307 expr.
id()==ID_floatbv_mult ||
4308 expr.
id()==ID_floatbv_div ||
4309 expr.
id()==ID_floatbv_typecast ||
4310 expr.
id()==ID_ieee_float_equal ||
4311 expr.
id()==ID_ieee_float_notequal ||
4312 ((expr.
id()==ID_lt ||
4316 expr.
id()==ID_isnan ||
4317 expr.
id()==ID_isnormal ||
4318 expr.
id()==ID_isfinite ||
4319 expr.
id()==ID_isinf ||
4320 expr.
id()==ID_sign ||
4321 expr.
id()==ID_unary_minus ||
4322 expr.
id()==ID_typecast ||
4323 expr.
id()==ID_abs) &&
4329 if(
bvfp_set.insert(
function).second)
4331 out <<
"; this is a model for " << expr.
id()
4334 <<
"(define-fun " <<
function <<
" (";
4336 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4340 out <<
"(op" << i <<
' ';
4350 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4357 assert(!tmp2.is_nil());
4378 if(expr.
id()==ID_with)
4380 else if(expr.
id()==ID_member)
4389 if(type.
id()==ID_array)
4402 out <<
"(_ BitVec 1)";
4408 else if(type.
id()==ID_bool)
4412 else if(type.
id()==ID_struct)
4426 out <<
"(_ BitVec " << width <<
")";
4429 else if(type.
id()==ID_vector)
4445 out <<
"(_ BitVec " << width <<
")";
4448 else if(type.
id()==ID_code)
4455 else if(type.
id()==ID_union)
4464 out <<
"(_ BitVec " << width <<
")";
4466 else if(type.
id()==ID_pointer)
4471 else if(type.
id()==ID_bv ||
4472 type.
id()==ID_fixedbv ||
4473 type.
id()==ID_unsignedbv ||
4474 type.
id()==ID_signedbv ||
4475 type.
id()==ID_c_bool)
4480 else if(type.
id()==ID_c_enum)
4486 else if(type.
id()==ID_c_enum_tag)
4490 else if(type.
id()==ID_floatbv)
4495 out <<
"(_ FloatingPoint " 4496 << floatbv_type.
get_e() <<
" " 4497 << floatbv_type.
get_f() + 1 <<
")";
4502 else if(type.
id()==ID_rational ||
4505 else if(type.
id()==ID_integer)
4507 else if(type.
id()==ID_symbol)
4509 else if(type.
id()==ID_complex)
4525 out <<
"(_ BitVec " << width <<
")";
4528 else if(type.
id()==ID_c_bit_field)
4540 std::set<irep_idt> recstack;
4546 std::set<irep_idt> &recstack)
4548 if(type.
id()==ID_array)
4554 else if(type.
id()==ID_incomplete_array)
4558 else if(type.
id()==ID_complex)
4568 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4569 <<
"(mk-" << smt_typename;
4571 out <<
" (" << smt_typename <<
".imag ";
4575 out <<
" (" << smt_typename <<
".real ";
4582 else if(type.
id()==ID_vector)
4593 INVALIDEXPR(
"failed to convert vector size to constant");
4598 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4599 <<
"(mk-" << smt_typename;
4603 out <<
" (" << smt_typename <<
"." << i <<
" ";
4611 else if(type.
id()==ID_struct)
4614 bool need_decl=
false;
4626 for(
const auto &component : components)
4643 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4644 <<
"(mk-" << smt_typename <<
" ";
4646 for(
const auto &component : components)
4648 out <<
"(" << smt_typename <<
"." << component.get_name()
4654 out <<
"))))" <<
"\n";
4671 for(struct_union_typet::componentst::const_iterator
4672 it=components.begin();
4673 it!=components.end();
4677 out <<
"(define-fun update-" << smt_typename <<
"." 4679 <<
"((s " << smt_typename <<
") " 4682 out <<
")) " << smt_typename <<
" " 4683 <<
"(mk-" << smt_typename
4686 for(struct_union_typet::componentst::const_iterator
4687 it2=components.begin();
4688 it2!=components.end();
4695 out <<
"(" << smt_typename <<
"." 4696 << it2->get_name() <<
" s) ";
4700 out <<
"))" <<
"\n";
4706 else if(type.
id()==ID_union)
4711 for(
const auto &component : components)
4714 else if(type.
id()==ID_code)
4718 for(
const auto ¶m : parameters)
4723 else if(type.
id()==ID_pointer)
4727 else if(type.
id()==ID_symbol)
4732 if(recstack.find(
id)==recstack.end())
4734 recstack.insert(
id);
4743 std::vector<exprt> let_order;
4752 std::vector<exprt> &let_order,
4756 if(i>=let_order.size())
4759 exprt current=let_order[i];
4760 assert(map.
find(current)!=map.
end());
4763 return letify_rec(expr, let_order, map, i+1);
4767 let.
symbol() = map.
find(current)->second.let_symbol;
4777 std::vector<exprt> &let_order)
4795 assert(map.
find(expr)==map.
end());
4802 let_order.push_back(expr);
const irep_idt & get_name() const
void unflatten(wheret, const typet &, unsigned nesting=0)
The type of an expression.
std::size_t get_e() const
exprt size_of_expr(const typet &type, const namespacet &ns)
exprt parse_union(const irept &s, const union_typet &type)
Fixed-width bit-vector with unsigned binary interpretation.
datatype_mapt datatype_map
virtual tvt l_get(literalt l) const
std::size_t get_fraction_bits() const
void flatten2bv(const exprt &)
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
exprt parse_array(const irept &s, const array_typet &type)
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
exprt letify(exprt &expr)
const minus_exprt & to_minus_expr(const exprt &expr)
Cast a generic exprt to a minus_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
static ieee_floatt NaN(const ieee_float_spect &_spec)
virtual resultt dec_solve()
constant_exprt to_expr() const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Fixed-width bit-vector with IEEE floating-point interpretation.
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
void convert_literal(const literalt)
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
Deprecated expression utility functions.
void convert_typecast(const typecast_exprt &expr)
void build(const mp_integer &exp, const mp_integer &frac)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
void convert_expr(const exprt &)
std::size_t get_integer_bits() const
void convert_constant(const constant_exprt &expr)
const irep_idt & get_identifier() const
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::vector< componentt > componentst
void convert_update(const exprt &expr)
const_iterator find(const Key &key) const
const irep_idt & get_value() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
std::vector< parametert > parameterst
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
const componentst & components() const
void convert_floatbv(const exprt &expr)
exprt flatten_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
void get_dynamic_objects(std::vector< std::size_t > &objects) const
void convert_plus(const plus_exprt &expr)
std::string type2id(const typet &) const
A constant literal expression.
#define CHECK_RETURN(CONDITION)
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
identifier_mapt identifier_map
void convert_type(const typet &)
#define forall_literals(it, bv)
const typet & follow_tag(const union_tag_typet &) const
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
bool use_array_theory(const exprt &)
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
std::size_t get_invalid_object() const
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Extract member of struct or union.
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt substitute_let(exprt &expr, const seen_expressionst &map)
virtual literalt convert(const exprt &expr)
struct configt::bv_encodingt bv_encoding
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_op_exprt.
void convert_mult(const mult_exprt &expr)
void convert_relation(const exprt &expr)
exprt object_size(const exprt &pointer)
const irep_idt & id() const
const membert & get_member(const struct_typet &type, const irep_idt &member) const
void define_object_size(const irep_idt &id, const exprt &expr)
virtual void print_assignment(std::ostream &out) const
The boolean constant true.
defined_expressionst object_sizes
typename mapt::iterator iterator
division (integer and real)
A reference into the symbol table.
const irep_idt & get_identifier() const
void convert_mod(const mod_exprt &expr)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
std::size_t get_fraction_bits() const
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
void convert_div(const div_exprt &expr)
A constant-size array type.
std::size_t unsafe_string2size_t(const std::string &str, int base)
union constructor from single element
API to expression classes.
void convert_index(const index_exprt &expr)
boolbv_widtht boolbv_width
exprt letify_rec(exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, std::size_t i)
const irep_idt & get(const irep_namet &name) const
const exprt & size() const
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
const exprt & size() const
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
std::string convert_identifier(const irep_idt &identifier)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
constant_exprt parse_literal(const irept &, const typet &type)
array_exprt to_array_expr() const
convert string into array constant
array constructor from single element
void convert_minus(const minus_exprt &expr)
const typet & follow(const typet &) const
const_iterator end() const
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
std::string floatbv_suffix(const exprt &) const
Operator to return the address of an object.
const irep_idt & get_identifier() const
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Fixed-width bit-vector with signed fixed-point interpretation.
The boolean constant false.
std::size_t get_width() const
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
exprt float_bv(const exprt &src)
bool has_component(const irep_idt &component_name) const
std::size_t get_f() const
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
literalt const_literal(bool value)
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast a generic exprt to a popcount_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
mstreamt & result() const
virtual exprt get(const exprt &expr) const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
void convert_byte_update(const byte_update_exprt &expr)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
const string_constantt & to_string_constant(const exprt &expr)
void convert_is_dynamic_object(const exprt &expr)
semantic type conversion from/to floating-point formats
literalt get_literal() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
std::set< irep_idt > bvfp_set
const exprt & struct_op() const
const parameterst & parameters() const
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Operator to update elements in structs and arrays.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
void convert_overflow(const exprt &expr)
irep_idt get_component_name() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
void find_symbols(const exprt &expr)
std::size_t no_boolean_variables
void convert_member(const member_exprt &expr)
exprt parse_rec(const irept &s, const typet &type)
const std::string & id_string() const
#define Forall_operands(it, expr)
void convert_union(const union_exprt &expr)
virtual void set_to(const exprt &expr, bool value)
static const std::size_t LET_COUNT
void convert_with(const with_exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Expression to hold a symbol (variable)
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
std::vector< bool > boolean_assignment
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
std::size_t width() const
void convert_byte_extract(const byte_extract_exprt &expr)
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
exprt parse_struct(const irept &s, const struct_typet &type)
#define DATA_INVARIANT(CONDITION, REASON)
#define UNEXPECTEDCASE(S)
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast a generic exprt to a nondet_symbol_exprt.
void write_footer(std::ostream &)
fixed-width bit-vector without numerical interpretation
Bit-wise negation of bit-vectors.
struct constructor from list of elements
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::size_t add_object(const exprt &expr)
IEEE floating-point operations.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
smt2_identifierst smt2_identifiers
const irep_idt & get_identifier() const
defined_expressionst defined_expressions
void set(const irep_namet &name, const irep_idt &value)
const componentt & get_component(const irep_idt &component_name) const
pointer_logict pointer_logic
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
void collect_bindings(exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
std::pair< iterator, bool > insert(const value_type &value)