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()==ID_string_constant)
1392 else if(expr.
id()==ID_extractbit)
1402 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1408 out <<
"(= ((_ extract 0 0) ";
1418 else if(expr.
id()==ID_extractbits)
1433 std::swap(op1_i, op2_i);
1437 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1444 out <<
"(= ((_ extract 0 0) ";
1453 SMT2_TODO(
"smt2: extractbits with non-constant index");
1456 else if(expr.
id()==ID_replication)
1462 INVALIDEXPR(
"replication takes constant as first parameter");
1464 out <<
"((_ repeat " << times <<
") ";
1468 else if(expr.
id()==ID_byte_extract_little_endian ||
1469 expr.
id()==ID_byte_extract_big_endian)
1473 else if(expr.
id()==ID_byte_update_little_endian ||
1474 expr.
id()==ID_byte_update_big_endian)
1478 else if(expr.
id()==ID_width)
1495 out <<
"(_ bv" << op_width/8
1496 <<
" " << result_width <<
")";
1498 else if(expr.
id()==ID_abs)
1504 if(type.id()==ID_signedbv)
1508 out <<
"(ite (bvslt ";
1510 out <<
" (_ bv0 " << result_width <<
")) ";
1517 else if(type.id()==ID_fixedbv)
1521 out <<
"(ite (bvslt ";
1523 out <<
" (_ bv0 " << result_width <<
")) ";
1530 else if(type.id()==ID_floatbv)
1544 else if(expr.
id()==ID_isnan)
1550 if(op_type.id()==ID_fixedbv)
1552 else if(op_type.id()==ID_floatbv)
1556 out <<
"(fp.isNaN ";
1566 else if(expr.
id()==ID_isfinite)
1573 if(op_type.
id()==ID_fixedbv)
1575 else if(op_type.
id()==ID_floatbv)
1581 out <<
"(not (fp.isNaN ";
1585 out <<
"(not (fp.isInf ";
1597 else if(expr.
id()==ID_isinf)
1604 if(op_type.
id()==ID_fixedbv)
1606 else if(op_type.
id()==ID_floatbv)
1610 out <<
"(fp.isInfinite ";
1620 else if(expr.
id()==ID_isnormal)
1627 if(op_type.
id()==ID_fixedbv)
1629 else if(op_type.
id()==ID_floatbv)
1633 out <<
"(fp.isNormal ";
1643 else if(expr.
id()==ID_overflow_plus ||
1644 expr.
id()==ID_overflow_minus)
1647 assert(expr.
type().
id()==ID_bool);
1649 bool subtract=expr.
id()==ID_overflow_minus;
1653 if(op_type.
id()==ID_signedbv)
1656 out <<
"(let ((?sum (";
1657 out << (subtract?
"bvsub":
"bvadd");
1658 out <<
" ((_ sign_extend 1) ";
1661 out <<
" ((_ sign_extend 1) ";
1665 "((_ extract " << width <<
" " << width <<
") ?sum) " 1666 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1669 else if(op_type.
id()==ID_unsignedbv ||
1670 op_type.
id()==ID_pointer)
1674 out <<
"((_ extract " << width <<
" " << width <<
") ";
1675 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1676 out <<
" ((_ zero_extend 1) ";
1679 out <<
" ((_ zero_extend 1) ";
1687 else if(expr.
id()==ID_overflow_mult)
1697 if(op_type.id()==ID_signedbv)
1699 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1701 out <<
") ((_ sign_extend " << width <<
") ";
1704 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" " 1706 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" " 1707 << width*2 <<
")))))";
1709 else if(op_type.id()==ID_unsignedbv)
1711 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1713 out <<
") ((_ zero_extend " << width <<
") ";
1715 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1718 UNEXPECTEDCASE(
"overflow-* check on unknown type: "+op_type.id_string());
1720 else if(expr.
id()==ID_array)
1726 else if(expr.
id()==ID_literal)
1730 else if(expr.
id()==ID_forall ||
1731 expr.
id()==ID_exists)
1735 throw "MathSAT does not support quantifiers";
1737 if(expr.
id()==ID_forall)
1739 else if(expr.
id()==ID_exists)
1754 else if(expr.
id()==ID_vector)
1760 INVALIDEXPR(
"failed to convert vector size to constant");
1762 assert(size==expr.
operands().size());
1768 const std::string smt_typename=
1771 out <<
"(mk-" << smt_typename;
1785 else if(expr.
id()==ID_object_size)
1789 else if(expr.
id()==ID_let)
1800 else if(expr.
id()==ID_constraint_select_one)
1803 "smt2_convt::convert_expr: `"+expr.
id_string()+
1804 "' is not yet supported");
1806 else if(expr.
id() == ID_bswap)
1812 INVALIDEXPR(
"bswap gets one operand with same type");
1815 out <<
"(let ((bswap_op ";
1819 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1827 const std::size_t bytes = width / 8;
1836 for(std::size_t byte = 0; byte < bytes; byte++)
1840 out <<
"(bswap_byte_" << byte <<
' ';
1841 out <<
"((_ extract " << (byte * 8 + 7) <<
" " << (byte * 8)
1851 for(std::size_t byte = 0; byte < bytes; byte++)
1852 out <<
" bswap_byte_" << byte;
1863 else if(expr.
id() == ID_popcount)
1870 "smt2_convt::convert_expr: `"+expr.
id_string()+
"' is unsupported");
1879 if(dest_type.
id()==ID_c_enum_tag)
1883 if(src_type.
id()==ID_c_enum_tag)
1886 if(dest_type.
id()==ID_bool)
1889 if(src_type.
id()==ID_signedbv ||
1890 src_type.
id()==ID_unsignedbv ||
1891 src_type.
id()==ID_c_bool ||
1892 src_type.
id()==ID_fixedbv ||
1893 src_type.
id()==ID_pointer ||
1894 src_type.
id()==ID_integer)
1902 else if(src_type.
id()==ID_floatbv)
1906 out <<
"(not (fp.isZero ";
1918 else if(dest_type.
id()==ID_c_bool)
1927 out <<
" (_ bv1 " << to_width <<
")";
1928 out <<
" (_ bv0 " << to_width <<
")";
1931 else if(dest_type.
id()==ID_signedbv ||
1932 dest_type.
id()==ID_unsignedbv ||
1933 dest_type.
id()==ID_c_enum ||
1934 dest_type.
id()==ID_bv)
1938 if(src_type.
id()==ID_signedbv ||
1939 src_type.
id()==ID_unsignedbv ||
1940 src_type.
id()==ID_c_bool ||
1941 src_type.
id()==ID_c_enum ||
1942 src_type.
id()==ID_bv)
1946 if(from_width==to_width)
1948 else if(from_width<to_width)
1950 if(src_type.
id()==ID_signedbv)
1951 out <<
"((_ sign_extend ";
1953 out <<
"((_ zero_extend ";
1955 out << (to_width-from_width)
1962 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
1967 else if(src_type.
id()==ID_fixedbv)
1971 std::size_t from_width=fixedbv_type.
get_width();
1978 out <<
"(let ((?tcop ";
1984 if(to_width>from_integer_bits)
1986 out <<
"((_ sign_extend " 1987 << (to_width-from_integer_bits) <<
") ";
1988 out <<
"((_ extract " << (from_width-1) <<
" " 1989 << from_fraction_bits <<
") ";
1995 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
1996 <<
" " << from_fraction_bits <<
") ";
2001 out <<
" (ite (and ";
2004 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) " 2005 "(_ bv0 " << from_fraction_bits <<
")))";
2008 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2013 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2017 else if(src_type.
id()==ID_floatbv)
2019 if(dest_type.
id()==ID_bv)
2036 else if(dest_type.
id()==ID_signedbv)
2040 "typecast unexpected "+src_type.
id_string()+
" -> "+
2043 else if(dest_type.
id()==ID_unsignedbv)
2047 "typecast unexpected "+src_type.
id_string()+
" -> "+
2051 else if(src_type.
id()==ID_bool)
2056 if(dest_type.
id()==ID_fixedbv)
2059 out <<
" (concat (_ bv1 " 2062 "(_ bv0 " << spec.
width <<
")";
2066 out <<
" (_ bv1 " << to_width <<
")";
2067 out <<
" (_ bv0 " << to_width <<
")";
2072 else if(src_type.
id()==ID_pointer)
2076 if(from_width<to_width)
2078 out <<
"((_ sign_extend ";
2079 out << (to_width-from_width)
2086 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2091 else if(src_type.
id()==ID_integer)
2094 if(src.is_constant())
2098 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2101 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2103 else if(src_type.
id()==ID_struct)
2116 else if(src_type.
id()==ID_union)
2121 else if(src_type.
id()==ID_c_bit_field)
2125 if(from_width==to_width)
2136 std::ostringstream e_str;
2137 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2138 <<
" src == " <<
format(src);
2142 else if(dest_type.
id()==ID_fixedbv)
2148 if(src_type.
id()==ID_unsignedbv ||
2149 src_type.
id()==ID_signedbv ||
2150 src_type.
id()==ID_c_enum)
2157 if(from_width==to_integer_bits)
2159 else if(from_width>to_integer_bits)
2162 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2169 assert(from_width<to_integer_bits);
2170 if(dest_type.
id()==ID_unsignedbv)
2172 out <<
"(_ zero_extend " 2173 << (to_integer_bits-from_width) <<
") ";
2179 out <<
"((_ sign_extend " 2180 << (to_integer_bits-from_width) <<
") ";
2186 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2189 else if(src_type.
id()==ID_bool)
2191 out <<
"(concat (concat" 2192 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2198 else if(src_type.
id()==ID_fixedbv)
2203 std::size_t from_width=from_fixedbv_type.
get_width();
2205 out <<
"(let ((?tcop ";
2211 if(to_integer_bits<=from_integer_bits)
2213 out <<
"((_ extract " 2214 << (from_fraction_bits+to_integer_bits-1) <<
" " 2215 << from_fraction_bits
2220 assert(to_integer_bits>from_integer_bits);
2221 out <<
"((_ sign_extend " 2222 << (to_integer_bits-from_integer_bits)
2224 << (from_width-1) <<
" " 2225 << from_fraction_bits
2231 if(to_fraction_bits<=from_fraction_bits)
2233 out <<
"((_ extract " 2234 << (from_fraction_bits-1) <<
" " 2235 << (from_fraction_bits-to_fraction_bits)
2240 assert(to_fraction_bits>from_fraction_bits);
2241 out <<
"(concat ((_ extract " 2242 << (from_fraction_bits-1) <<
" 0) ";
2245 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2254 else if(dest_type.
id()==ID_pointer)
2258 if(src_type.
id()==ID_pointer)
2263 else if(src_type.
id()==ID_unsignedbv ||
2264 src_type.
id()==ID_signedbv)
2270 if(from_width==to_width)
2272 else if(from_width<to_width)
2274 out <<
"((_ sign_extend " 2275 << (to_width-from_width)
2282 out <<
"((_ extract " << to_width <<
" 0) ";
2290 else if(dest_type.
id()==ID_range)
2294 else if(dest_type.
id()==ID_floatbv)
2302 if(src_type.
id()==ID_bool)
2317 a.
build(significand, exponent);
2325 a.
build(significand, exponent);
2331 else if(src_type.
id()==ID_c_bool)
2340 else if(dest_type.
id()==ID_integer)
2342 if(src_type.
id()==ID_bool)
2351 else if(dest_type.
id()==ID_c_bit_field)
2356 if(from_width==to_width)
2377 if(dest_type.
id()==ID_floatbv)
2379 if(src_type.
id()==ID_floatbv)
2406 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2407 << dst.
get_f() + 1 <<
") ";
2416 else if(src_type.
id()==ID_unsignedbv)
2437 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" " 2438 << dst.
get_f() + 1 <<
") ";
2447 else if(src_type.
id()==ID_signedbv)
2455 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2456 << dst.
get_f() + 1 <<
") ";
2465 else if(src_type.
id()==ID_c_enum_tag)
2481 else if(dest_type.
id()==ID_signedbv)
2486 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2495 else if(dest_type.
id()==ID_unsignedbv)
2500 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2523 assert(components.size()==expr.
operands().size());
2525 assert(!components.empty());
2530 const std::string smt_typename =
2534 out <<
"(mk-" << smt_typename;
2537 for(struct_typet::componentst::const_iterator
2538 it=components.begin();
2539 it!=components.end();
2550 if(components.size()==1)
2555 for(std::size_t i=components.size(); i>1; i--)
2572 for(std::size_t i=1; i<components.size(); i++)
2586 INVALIDEXPR(
"failed to convert array size for flattening");
2591 out <<
"(let ((?far ";
2599 out <<
"(select ?far ";
2623 INVALIDEXPR(
"failed to get union width for union");
2628 INVALIDEXPR(
"failed to get union member width for union");
2630 if(total_width==member_width)
2637 assert(total_width>member_width);
2640 << (total_width-member_width) <<
") ";
2650 if(expr_type.
id()==ID_unsignedbv ||
2651 expr_type.
id()==ID_signedbv ||
2652 expr_type.
id()==ID_bv ||
2653 expr_type.
id()==ID_c_enum ||
2654 expr_type.
id()==ID_c_enum_tag ||
2655 expr_type.
id()==ID_c_bool ||
2656 expr_type.
id()==ID_incomplete_c_enum ||
2657 expr_type.
id()==ID_c_bit_field)
2663 out <<
"(_ bv" << value
2664 <<
" " << width <<
")";
2666 else if(expr_type.
id()==ID_fixedbv)
2673 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2675 else if(expr_type.
id()==ID_floatbv)
2688 size_t e=floatbv_type.
get_e();
2689 size_t f=floatbv_type.
get_f()+1;
2695 out <<
"((_ to_fp " << e <<
" " << f <<
")" 2701 out <<
"(_ NaN " << e <<
" " << f <<
")";
2706 out <<
"(_ -oo " << e <<
" " << f <<
")";
2708 out <<
"(_ +oo " << e <<
" " << f <<
")";
2718 <<
"#b" << binaryString.substr(0, 1) <<
" " 2719 <<
"#b" << binaryString.substr(1, e) <<
" " 2720 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
2731 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
2734 else if(expr_type.
id()==ID_pointer)
2746 else if(expr_type.
id()==ID_bool)
2755 else if(expr_type.
id()==ID_array)
2761 else if(expr_type.
id()==ID_rational)
2764 size_t pos=value.find(
"/");
2766 if(
pos==std::string::npos)
2767 out << value <<
".0";
2770 out <<
"(/ " << value.substr(0,
pos) <<
".0 " 2771 << value.substr(
pos+1) <<
".0)";
2774 else if(expr_type.
id()==ID_integer)
2786 if(expr.
type().
id()==ID_unsignedbv ||
2787 expr.
type().
id()==ID_signedbv)
2789 if(expr.
type().
id()==ID_unsignedbv)
2805 std::vector<std::size_t> dynamic_objects;
2810 if(dynamic_objects.empty())
2816 out <<
"(let ((?obj ((_ extract " 2817 << pointer_width-1 <<
" " 2822 if(dynamic_objects.size()==1)
2824 out <<
"(= (_ bv" << dynamic_objects.front()
2831 for(
const auto &
object : dynamic_objects)
2832 out <<
" (= (_ bv" <<
object 2848 if(op_type.id()==ID_unsignedbv ||
2849 op_type.id()==ID_pointer ||
2850 op_type.id()==ID_bv)
2853 if(expr.
id()==ID_le)
2855 else if(expr.
id()==ID_lt)
2857 else if(expr.
id()==ID_ge)
2859 else if(expr.
id()==ID_gt)
2868 else if(op_type.id()==ID_signedbv ||
2869 op_type.id()==ID_fixedbv)
2872 if(expr.
id()==ID_le)
2874 else if(expr.
id()==ID_lt)
2876 else if(expr.
id()==ID_ge)
2878 else if(expr.
id()==ID_gt)
2887 else if(op_type.id()==ID_floatbv)
2892 if(expr.
id()==ID_le)
2894 else if(expr.
id()==ID_lt)
2896 else if(expr.
id()==ID_ge)
2898 else if(expr.
id()==ID_gt)
2910 else if(op_type.id()==ID_rational ||
2911 op_type.id()==ID_integer)
2924 "unsupported type for "+expr.
id_string()+
": "+op_type.id_string());
2939 if(expr.
type().
id()==ID_rational ||
2940 expr.
type().
id()==ID_integer ||
2941 expr.
type().
id()==ID_real)
2946 for(
const auto &op : expr.
operands())
2954 else if(expr.
type().
id()==ID_unsignedbv ||
2955 expr.
type().
id()==ID_signedbv ||
2956 expr.
type().
id()==ID_fixedbv)
2973 else if(expr.
type().
id()==ID_floatbv)
2980 else if(expr.
type().
id()==ID_pointer)
2986 if(p.
type().
id()!=ID_pointer)
2989 if(p.
type().
id()!=ID_pointer)
2990 INVALIDEXPR(
"unexpected mixture in pointer arithmetic");
3004 out <<
" (_ bv" << element_size
3017 else if(expr.
type().
id()==ID_vector)
3023 INVALIDEXPR(
"failed to convert vector size to constant");
3031 const std::string smt_typename=
3034 out <<
"(mk-" << smt_typename;
3044 tmp.copy_to_operands(
3078 if(expr.
id()==ID_constant)
3085 out <<
"roundNearestTiesToEven";
3087 out <<
"roundTowardNegative";
3089 out <<
"roundTowardPositive";
3091 out <<
"roundTowardZero";
3094 "Unknown constant rounding mode with value "+
3102 out <<
"(ite (= (_ bv0 " << width <<
") ";
3104 out <<
") roundNearestTiesToEven ";
3106 out <<
"(ite (= (_ bv1 " << width <<
") ";
3108 out <<
") roundTowardNegative ";
3110 out <<
"(ite (= (_ bv2 " << width <<
") ";
3112 out <<
") roundTowardPositive ";
3115 out <<
"roundTowardZero";
3126 assert(type.
id()==ID_floatbv ||
3127 (type.
id()==ID_complex && type.
subtype().
id()==ID_floatbv) ||
3128 (type.
id()==ID_vector && type.
subtype().
id()==ID_floatbv));
3132 if(type.
id()==ID_floatbv)
3142 else if(type.
id()==ID_complex)
3146 else if(type.
id()==ID_vector)
3161 if(expr.
type().
id()==ID_integer)
3169 else if(expr.
type().
id()==ID_unsignedbv ||
3170 expr.
type().
id()==ID_signedbv ||
3171 expr.
type().
id()==ID_fixedbv)
3173 if(expr.
op0().
type().
id()==ID_pointer &&
3179 assert(element_size>0);
3193 out <<
" (_ bv" << element_size
3205 else if(expr.
type().
id()==ID_floatbv)
3212 else if(expr.
type().
id()==ID_pointer)
3216 else if(expr.
type().
id()==ID_vector)
3222 INVALIDEXPR(
"failed to convert vector size to constant");
3230 const std::string smt_typename=
3233 out <<
"(mk-" << smt_typename;
3243 tmp.copy_to_operands(
3262 assert(expr.
type().
id()==ID_floatbv);
3282 if(expr.
type().
id()==ID_unsignedbv ||
3283 expr.
type().
id()==ID_signedbv)
3285 if(expr.
type().
id()==ID_unsignedbv)
3295 else if(expr.
type().
id()==ID_fixedbv)
3300 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3305 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3307 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3313 else if(expr.
type().
id()==ID_floatbv)
3327 assert(expr.
type().
id()==ID_floatbv);
3360 if(expr.
type().
id()==ID_unsignedbv ||
3361 expr.
type().
id()==ID_signedbv)
3372 else if(expr.
type().
id()==ID_floatbv)
3379 else if(expr.
type().
id()==ID_fixedbv)
3384 out <<
"((_ extract " 3385 << spec.
width+fraction_bits-1 <<
" " 3386 << fraction_bits <<
") ";
3390 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3394 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3400 else if(expr.
type().
id()==ID_rational ||
3401 expr.
type().
id()==ID_integer ||
3402 expr.
type().
id()==ID_real)
3421 assert(expr.
type().
id()==ID_floatbv);
3445 std::size_t s=expr.
operands().size();
3452 assert(new_with_expr.
operands().size()==3);
3454 new_with_expr.
old()=tmp;
3464 if(expr_type.
id()==ID_array)
3488 out <<
"(let ((distance? ";
3489 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3493 if(array_width>index_width)
3495 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3501 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3510 out <<
"(bvlshr (_ bv" <<
power(2, array_width)-1 <<
" " 3511 << array_width <<
") ";
3512 out <<
"distance?) ";
3516 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3518 out <<
") distance?)))";
3521 else if(expr_type.
id()==ID_struct)
3528 const irep_idt &component_name=index.
get(ID_component_name);
3531 INVALIDEXPR(
"with failed to find component in struct");
3536 const std::string smt_typename=
3539 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3553 out <<
"(let ((?withop ";
3557 if(m.
width==struct_width)
3566 <<
"((_ extract " << (struct_width-1) <<
" " 3567 << m.
width <<
") ?withop) ";
3576 out <<
"((_ extract " << (m.
offset-1) <<
" 0) ?withop))";
3581 out <<
"(concat (concat " 3582 <<
"((_ extract " << (struct_width-1) <<
" " 3585 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3592 else if(expr_type.
id()==ID_union)
3603 INVALIDEXPR(
"failed to get union width for with");
3608 INVALIDEXPR(
"failed to get union member width for with");
3610 if(total_width==member_width)
3616 assert(total_width>member_width);
3618 out <<
"((_ extract " 3620 <<
" " << member_width <<
") ";
3627 else if(expr_type.
id()==ID_bv ||
3628 expr_type.
id()==ID_unsignedbv ||
3629 expr_type.
id()==ID_signedbv)
3657 out <<
" (bvnot (bvshl";
3660 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3661 out <<
" (repeat[" << value_width <<
"] bv1[1])";
3683 "with expects struct, union, or array type, but got "+
3691 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
3700 if(array_op_type.id()==ID_array)
3729 assert(array_width!=0);
3736 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
3740 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3744 if(array_width>index_width)
3746 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3752 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3762 else if(array_op_type.id()==ID_vector)
3769 const std::string smt_typename=
3777 SMT2_TODO(
"non-constant index on vectors");
3781 out <<
"(" << smt_typename <<
"." << index_int <<
" ";
3793 "index with unsupported array type: "+array_op_type.id_string());
3801 const exprt &struct_op=member_expr.struct_op();
3803 const irep_idt &name=member_expr.get_component_name();
3805 if(struct_op_type.
id()==ID_struct)
3816 const std::string smt_typename=
3819 out <<
"(" << smt_typename <<
"." 3831 INVALIDEXPR(
"failed to get struct member offset");
3839 else if(struct_op_type.
id()==ID_union)
3848 out <<
"((_ extract " 3858 "convert_member on an unexpected type "+struct_op_type.
id_string());
3865 if(type.
id()==ID_bool)
3871 else if(type.
id()==ID_vector)
3877 const std::string smt_typename=
3885 INVALIDEXPR(
"failed to convert vector size to constant");
3887 out <<
"(let ((?vflop ";
3895 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
3903 else if(type.
id()==ID_array)
3907 else if(type.
id()==ID_struct)
3913 const std::string smt_typename=
3919 out <<
"(let ((?sflop ";
3927 for(std::size_t i=components.size(); i>1; i--)
3929 out <<
"(concat (" << smt_typename <<
"." 3930 << components[i-1].get_name() <<
" ?sflop)";
3935 out <<
"(" << smt_typename <<
"." 3936 << components[0].get_name() <<
" ?sflop)";
3938 for(std::size_t i=1; i<components.size(); i++)
3946 else if(type.
id()==ID_floatbv)
3949 INVALIDEXPR(
"need to flatten floatbv in FPA theory");
3962 if(type.
id()==ID_symbol)
3965 if(type.
id()==ID_bool)
3972 else if(type.
id()==ID_vector)
3978 const std::string smt_typename=
3988 INVALIDEXPR(
"failed to convert vector size to constant");
3991 out <<
"(let ((?ufop" << nesting <<
" ";
3996 out <<
"(mk-" << smt_typename;
3998 std::size_t offset=0;
4000 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4004 out <<
"((_ extract " << offset+subtype_width-1 <<
" " 4005 << offset <<
") ?ufop" << nesting <<
")";
4017 else if(type.
id()==ID_struct)
4023 out <<
"(let ((?ufop" << nesting <<
" ";
4030 const std::string smt_typename=
4033 out <<
"(mk-" << smt_typename;
4040 std::size_t offset=0;
4043 for(struct_typet::componentst::const_iterator
4044 it=components.begin();
4045 it!=components.end();
4052 out <<
"((_ extract " << offset+member_width-1 <<
" " 4053 << offset <<
") ?ufop" << nesting <<
")";
4055 offset+=member_width;
4079 if(expr.
id()==ID_and && value)
4086 if(expr.
id()==ID_or && !value)
4093 if(expr.
id()==ID_not)
4101 assert(expr.
type().
id()==ID_bool);
4106 if(expr.
id()==ID_equal && value==
true)
4110 if(equal_expr.
lhs().
id()==ID_symbol)
4119 assert(
id.type.is_nil());
4121 id.type=equal_expr.
lhs().
type();
4128 out <<
"; set_to true (equal)\n";
4129 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4148 out <<
"; set_to " << (value?
"true":
"false") <<
"\n" 4174 if(expr.
id()==ID_symbol ||
4175 expr.
id()==ID_nondet_symbol)
4178 if(expr.
type().
id()==ID_code)
4183 if(expr.
id()==ID_symbol)
4186 identifier=
"nondet_"+
4191 if(
id.type.is_nil())
4193 id.type=expr.
type();
4198 out <<
"; find_symbols\n";
4199 out <<
"(declare-fun |" 4206 else if(expr.
id()==ID_array_of)
4211 out <<
"; the following is a substitute for lambda i. x" <<
"\n";
4212 out <<
"(declare-fun " <<
id <<
" () ";
4217 #if 0 // not really working in any solver yet! 4218 out <<
"(assert (forall ((i ";
4220 out <<
")) (= (select " <<
id <<
" i) ";
4222 out <<
")))" <<
"\n";
4228 else if(expr.
id()==ID_array)
4235 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4236 out <<
"(declare-fun " <<
id <<
" () ";
4240 for(std::size_t i=0; i<expr.
operands().size(); i++)
4242 out <<
"(assert (= (select " <<
id <<
" ";
4246 out <<
"))" <<
"\n";
4252 else if(expr.
id()==ID_string_constant)
4261 out <<
"; the following is a substitute for a string" <<
"\n";
4262 out <<
"(declare-fun " <<
id <<
" () ";
4266 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4268 out <<
"(assert (= (select " << id;
4272 out <<
"))" <<
"\n";
4278 else if(expr.
id()==ID_object_size &&
4283 if(op.
type().
id()==ID_pointer)
4288 out <<
"(declare-fun " <<
id <<
" () ";
4298 (expr.
id()==ID_floatbv_plus ||
4299 expr.
id()==ID_floatbv_minus ||
4300 expr.
id()==ID_floatbv_mult ||
4301 expr.
id()==ID_floatbv_div ||
4302 expr.
id()==ID_floatbv_typecast ||
4303 expr.
id()==ID_ieee_float_equal ||
4304 expr.
id()==ID_ieee_float_notequal ||
4305 ((expr.
id()==ID_lt ||
4309 expr.
id()==ID_isnan ||
4310 expr.
id()==ID_isnormal ||
4311 expr.
id()==ID_isfinite ||
4312 expr.
id()==ID_isinf ||
4313 expr.
id()==ID_sign ||
4314 expr.
id()==ID_unary_minus ||
4315 expr.
id()==ID_typecast ||
4316 expr.
id()==ID_abs) &&
4322 if(
bvfp_set.insert(
function).second)
4324 out <<
"; this is a model for " << expr.
id()
4327 <<
"(define-fun " <<
function <<
" (";
4329 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4333 out <<
"(op" << i <<
' ';
4343 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4350 assert(!tmp2.is_nil());
4371 if(expr.
id()==ID_with)
4373 else if(expr.
id()==ID_member)
4382 if(type.
id()==ID_array)
4395 out <<
"(_ BitVec 1)";
4401 else if(type.
id()==ID_bool)
4405 else if(type.
id()==ID_struct)
4419 out <<
"(_ BitVec " << width <<
")";
4422 else if(type.
id()==ID_vector)
4438 out <<
"(_ BitVec " << width <<
")";
4441 else if(type.
id()==ID_code)
4448 else if(type.
id()==ID_union)
4457 out <<
"(_ BitVec " << width <<
")";
4459 else if(type.
id()==ID_pointer)
4464 else if(type.
id()==ID_bv ||
4465 type.
id()==ID_fixedbv ||
4466 type.
id()==ID_unsignedbv ||
4467 type.
id()==ID_signedbv ||
4468 type.
id()==ID_c_bool)
4473 else if(type.
id()==ID_c_enum)
4479 else if(type.
id()==ID_c_enum_tag)
4483 else if(type.
id()==ID_floatbv)
4488 out <<
"(_ FloatingPoint " 4489 << floatbv_type.
get_e() <<
" " 4490 << floatbv_type.
get_f() + 1 <<
")";
4495 else if(type.
id()==ID_rational ||
4498 else if(type.
id()==ID_integer)
4500 else if(type.
id()==ID_symbol)
4502 else if(type.
id()==ID_complex)
4518 out <<
"(_ BitVec " << width <<
")";
4521 else if(type.
id()==ID_c_bit_field)
4533 std::set<irep_idt> recstack;
4539 std::set<irep_idt> &recstack)
4541 if(type.
id()==ID_array)
4547 else if(type.
id()==ID_incomplete_array)
4551 else if(type.
id()==ID_complex)
4561 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4562 <<
"(mk-" << smt_typename;
4564 out <<
" (" << smt_typename <<
".imag ";
4568 out <<
" (" << smt_typename <<
".real ";
4575 else if(type.
id()==ID_vector)
4586 INVALIDEXPR(
"failed to convert vector size to constant");
4591 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4592 <<
"(mk-" << smt_typename;
4596 out <<
" (" << smt_typename <<
"." << i <<
" ";
4604 else if(type.
id()==ID_struct)
4607 bool need_decl=
false;
4619 for(
const auto &component : components)
4636 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4637 <<
"(mk-" << smt_typename <<
" ";
4639 for(
const auto &component : components)
4641 out <<
"(" << smt_typename <<
"." << component.get_name()
4647 out <<
"))))" <<
"\n";
4664 for(struct_union_typet::componentst::const_iterator
4665 it=components.begin();
4666 it!=components.end();
4670 out <<
"(define-fun update-" << smt_typename <<
"." 4672 <<
"((s " << smt_typename <<
") " 4675 out <<
")) " << smt_typename <<
" " 4676 <<
"(mk-" << smt_typename
4679 for(struct_union_typet::componentst::const_iterator
4680 it2=components.begin();
4681 it2!=components.end();
4688 out <<
"(" << smt_typename <<
"." 4689 << it2->get_name() <<
" s) ";
4693 out <<
"))" <<
"\n";
4699 else if(type.
id()==ID_union)
4704 for(
const auto &component : components)
4707 else if(type.
id()==ID_code)
4711 for(
const auto ¶m : parameters)
4716 else if(type.
id()==ID_pointer)
4720 else if(type.
id()==ID_symbol)
4725 if(recstack.find(
id)==recstack.end())
4727 recstack.insert(
id);
4736 std::vector<exprt> let_order;
4745 std::vector<exprt> &let_order,
4749 if(i>=let_order.size())
4752 exprt current=let_order[i];
4753 assert(map.
find(current)!=map.
end());
4756 return letify_rec(expr, let_order, map, i+1);
4760 let.
symbol() = map.
find(current)->second.let_symbol;
4770 std::vector<exprt> &let_order)
4788 assert(map.
find(expr)==map.
end());
4795 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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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)