38 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S); 41 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S) 62 "variable number shall be within bounds");
68 out <<
"; SMT 2" <<
"\n";
76 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
85 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
87 out <<
"(set-option :produce-models true)" <<
"\n";
93 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
103 out <<
"; assumptions\n";
117 out <<
"(check-sat)" <<
"\n";
123 out <<
"(get-value (|" <<
id <<
"|))" <<
"\n";
130 out <<
"; end of SMT2 file" <<
"\n";
141 std::size_t number = 0;
142 std::size_t h=pointer_width-1;
151 if(o.id()!=ID_symbol ||
159 out <<
"(assert (implies (= " <<
160 "((_ extract " << h <<
" " << l <<
") ";
162 out <<
") (_ bv" << number <<
" " 164 <<
"(= " <<
id <<
" (_ bv" <<
object_size.to_ulong() <<
" " 165 << size_width <<
"))))\n";
180 if(expr.
id()==ID_symbol)
187 return it->second.value;
189 else if(expr.
id()==ID_nondet_symbol)
196 return it->second.value;
198 else if(expr.
id()==ID_member)
237 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
242 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
253 else if(src.
get_sub().size()==2 &&
258 else if(src.
get_sub().size()==3 &&
261 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
265 else if(src.
get_sub().size()==4 &&
268 if(type.
id()==ID_floatbv)
285 else if(src.
get_sub().size()==4 &&
293 else if(src.
get_sub().size()==4 &&
301 else if(src.
get_sub().size()==4 &&
310 if(type.
id()==ID_signedbv ||
311 type.
id()==ID_unsignedbv ||
312 type.
id()==ID_c_enum ||
313 type.
id()==ID_c_bool)
317 else if(type.
id()==ID_c_enum_tag)
324 else if(type.
id()==ID_fixedbv ||
325 type.
id()==ID_floatbv)
330 else if(type.
id()==ID_integer ||
336 "smt2_convt::parse_literal should not be of unsupported type " +
356 else if(src.
get_sub().size()==2 &&
357 src.
get_sub()[0].get_sub().size()==3 &&
358 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
359 src.
get_sub()[0].get_sub()[1].id()==
"const")
382 return union_exprt(first.get_name(), converted, type);
396 if(components.empty())
404 if(src.
get_sub().size()!=components.size()+1)
407 for(std::size_t i=0; i<components.size(); i++)
422 if(
binary.size()!=total_width)
425 std::size_t offset=0;
427 for(std::size_t i=0; i<components.size(); i++)
429 std::size_t component_width=
boolbv_width(components[i].type());
432 offset + component_width <= total_width,
433 "struct component bits shall be within struct bit vector");
435 std::string component_binary=
437 total_width-offset-component_width, component_width);
442 offset+=component_width;
453 if(type.
id()==ID_signedbv ||
454 type.
id()==ID_unsignedbv ||
455 type.
id()==ID_integer ||
456 type.
id()==ID_rational ||
457 type.
id()==ID_real ||
458 type.
id()==ID_fixedbv ||
459 type.
id()==ID_floatbv)
463 else if(type.
id()==ID_bool)
465 if(src.
id()==ID_1 || src.
id()==ID_true)
467 else if(src.
id()==ID_0 || src.
id()==ID_false)
470 else if(type.
id()==ID_pointer)
476 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
481 ptr.
object = numeric_cast_v<std::size_t>(v / pow);
485 else if(type.
id()==ID_struct)
489 else if(type.
id()==ID_union)
493 else if(type.
id()==ID_array)
505 if(expr.
id()==ID_symbol ||
506 expr.
id()==ID_constant ||
507 expr.
id()==ID_string_constant ||
517 else if(expr.
id()==ID_index)
526 if(array.
type().
id()==ID_pointer)
528 else if(array.
type().
id()==ID_array)
546 address_of_expr.
type());
551 else if(expr.
id()==ID_member)
559 struct_op_type.
id() == ID_struct,
560 "member expression operand shall have struct type");
577 else if(expr.
id()==ID_if)
592 "operand of address of expression should not be of kind " +
618 "failed to get width of byte_update");
625 if(expr.
id()==ID_byte_update_little_endian)
628 upper = lower+value_width-1;
630 else if(expr.
id()==ID_byte_update_big_endian)
633 lower = max-((i+1)*8-1);
650 out <<
" ((_ extract " << lower-1 <<
" 0) ";
660 out <<
"((_ extract " << max <<
" " << (upper+1) <<
") ";
668 out <<
"(concat (concat ";
669 out <<
"((_ extract " << max <<
" " << (upper+1) <<
") ";
673 out <<
") ((_ extract " << (lower-1) <<
" 0) ";
715 else if(expr.
id()==ID_literal)
727 out <<
"; convert\n";
728 out <<
"(define-fun ";
765 for(std::size_t i=0; i<identifier.
size(); i++)
767 char ch=identifier[i];
790 if(type.
id()==ID_floatbv)
795 else if(type.
id()==ID_unsignedbv)
799 else if(type.
id()==ID_c_bool)
803 else if(type.
id()==ID_signedbv)
807 else if(type.
id()==ID_bool)
811 else if(type.
id()==ID_c_enum_tag)
832 if(expr.
id()==ID_symbol)
839 if(expr.
id()==ID_smt2_symbol)
847 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
849 out <<
"(|float_bv." << expr.
id()
865 if(expr.
id()==ID_symbol)
871 else if(expr.
id()==ID_nondet_symbol)
874 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
877 else if(expr.
id()==ID_smt2_symbol)
883 else if(expr.
id()==ID_typecast)
887 else if(expr.
id()==ID_floatbv_typecast)
891 else if(expr.
id()==ID_struct)
895 else if(expr.
id()==ID_union)
899 else if(expr.
id()==ID_constant)
903 else if(expr.
id()==ID_concatenation ||
904 expr.
id()==ID_bitand ||
905 expr.
id()==ID_bitor ||
906 expr.
id()==ID_bitxor ||
907 expr.
id()==ID_bitnand ||
908 expr.
id()==ID_bitnor)
912 "given expression should have at least two operands",
917 if(expr.
id()==ID_concatenation)
919 else if(expr.
id()==ID_bitand)
921 else if(expr.
id()==ID_bitor)
923 else if(expr.
id()==ID_bitxor)
925 else if(expr.
id()==ID_bitnand)
927 else if(expr.
id()==ID_bitnor)
938 else if(expr.
id()==ID_bitnot)
942 if(bitnot_expr.
type().
id() == ID_vector)
953 out <<
"(let ((?vectorop ";
957 out <<
"(mk-" << smt_typename;
964 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
980 else if(expr.
id()==ID_unary_minus)
985 unary_minus_expr.
type().
id() == ID_rational ||
986 unary_minus_expr.
type().
id() == ID_integer ||
987 unary_minus_expr.
type().
id() == ID_real)
993 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1005 else if(unary_minus_expr.
type().
id() == ID_vector)
1009 const std::string &smt_typename =
1016 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1018 out <<
"(let ((?vectorop ";
1022 out <<
"(mk-" << smt_typename;
1029 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1045 else if(expr.
id()==ID_unary_plus)
1050 else if(expr.
id()==ID_sign)
1056 if(op_type.
id()==ID_floatbv)
1060 out <<
"(fp.isNegative ";
1067 else if(op_type.
id()==ID_signedbv)
1073 out <<
" (_ bv0 " << op_width <<
"))";
1078 "sign should not be applied to unsupported type",
1081 else if(expr.
id()==ID_if)
1093 else if(expr.
id()==ID_and ||
1098 expr.
type().
id() == ID_bool,
1099 "logical and, or, and xor expressions should have Boolean type");
1102 "logical and, or, and xor expressions should have at least two operands");
1104 out <<
"(" << expr.
id();
1112 else if(expr.
id()==ID_implies)
1117 implies_expr.
type().
id() == ID_bool,
1118 "implies expression should have Boolean type");
1126 else if(expr.
id()==ID_not)
1131 not_expr.
type().
id() == ID_bool,
1132 "not expression should have Boolean type");
1138 else if(expr.
id() == ID_equal)
1144 "operands of equal expression shall have same type");
1152 else if(expr.
id() == ID_notequal)
1158 "operands of not equal expression shall have same type");
1166 else if(expr.
id()==ID_ieee_float_equal ||
1167 expr.
id()==ID_ieee_float_notequal)
1173 "float equal and not equal expressions must have two operands");
1176 "operands of float equal and not equal expressions shall have same type");
1181 if(expr.
id()==ID_ieee_float_notequal)
1190 if(expr.
id()==ID_ieee_float_notequal)
1196 else if(expr.
id()==ID_le ||
1203 else if(expr.
id()==ID_plus)
1207 else if(expr.
id()==ID_floatbv_plus)
1211 else if(expr.
id()==ID_minus)
1215 else if(expr.
id()==ID_floatbv_minus)
1219 else if(expr.
id()==ID_div)
1223 else if(expr.
id()==ID_floatbv_div)
1227 else if(expr.
id()==ID_mod)
1231 else if(expr.
id()==ID_mult)
1235 else if(expr.
id()==ID_floatbv_mult)
1239 else if(expr.
id()==ID_address_of)
1245 else if(expr.
id()==ID_array_of)
1250 array_of_expr.
type().
id() == ID_array,
1251 "array of expression shall have array type");
1253 defined_expressionst::const_iterator it =
1258 else if(expr.
id()==ID_index)
1262 else if(expr.
id()==ID_ashr ||
1263 expr.
id()==ID_lshr ||
1269 if(type.
id()==ID_unsignedbv ||
1270 type.
id()==ID_signedbv ||
1273 if(shift_expr.
id() == ID_ashr)
1275 else if(shift_expr.
id() == ID_lshr)
1277 else if(shift_expr.
id() == ID_shl)
1306 if(width_op0==width_op1)
1308 else if(width_op0>width_op1)
1310 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1316 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1323 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1330 "unsupported type for " + shift_expr.
id_string() +
": " +
1333 else if(expr.
id()==ID_with)
1337 else if(expr.
id()==ID_update)
1341 else if(expr.
id()==ID_member)
1345 else if(expr.
id()==ID_pointer_offset)
1349 "pointer offset expression shall have one operand");
1352 "operand of pointer offset expression shall be of pointer type");
1354 std::size_t offset_bits=
1359 if(offset_bits>result_width)
1360 offset_bits=result_width;
1363 if(result_width>offset_bits)
1364 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1366 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1370 if(result_width>offset_bits)
1373 else if(expr.
id()==ID_pointer_object)
1377 "pointer object expressions should have one operand");
1381 "pointer object expressions should be of pointer type");
1387 out <<
"((_ zero_extend " << ext <<
") ";
1389 out <<
"((_ extract " 1390 << pointer_width-1 <<
" " 1398 else if(expr.
id()==ID_dynamic_object)
1402 else if(expr.
id()==ID_invalid_pointer)
1406 "invalid pointer expression shall have one operand");
1409 out <<
"(= ((_ extract " 1410 << pointer_width-1 <<
" " 1416 else if(expr.
id()==ID_string_constant)
1422 else if(expr.
id()==ID_extractbit)
1430 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1436 out <<
"(= ((_ extract 0 0) ";
1441 tmp.
op0() = extractbit_expr.
index();
1446 else if(expr.
id()==ID_extractbits)
1454 mp_integer op1_i = numeric_cast_v<mp_integer>(extractbits_expr.
upper());
1455 mp_integer op2_i = numeric_cast_v<mp_integer>(extractbits_expr.
lower());
1458 std::swap(op1_i, op2_i);
1462 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1469 out <<
"(= ((_ extract 0 0) ";
1478 SMT2_TODO(
"smt2: extractbits with non-constant index");
1481 else if(expr.
id()==ID_replication)
1485 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1487 out <<
"((_ repeat " << times <<
") ";
1491 else if(expr.
id()==ID_byte_extract_little_endian ||
1492 expr.
id()==ID_byte_extract_big_endian)
1496 else if(expr.
id()==ID_byte_update_little_endian ||
1497 expr.
id()==ID_byte_update_big_endian)
1501 else if(expr.
id()==ID_width)
1504 expr.
operands().size() == 1,
"width expression should have one operand");
1514 out <<
"(_ bv" << op_width/8
1515 <<
" " << result_width <<
")";
1517 else if(expr.
id()==ID_abs)
1523 if(type.
id()==ID_signedbv)
1527 out <<
"(ite (bvslt ";
1529 out <<
" (_ bv0 " << result_width <<
")) ";
1536 else if(type.
id()==ID_fixedbv)
1540 out <<
"(ite (bvslt ";
1542 out <<
" (_ bv0 " << result_width <<
")) ";
1549 else if(type.
id()==ID_floatbv)
1563 else if(expr.
id()==ID_isnan)
1569 if(op_type.
id()==ID_fixedbv)
1571 else if(op_type.
id()==ID_floatbv)
1575 out <<
"(fp.isNaN ";
1585 else if(expr.
id()==ID_isfinite)
1591 if(op_type.
id()==ID_fixedbv)
1593 else if(op_type.
id()==ID_floatbv)
1599 out <<
"(not (fp.isNaN ";
1603 out <<
"(not (fp.isInf ";
1615 else if(expr.
id()==ID_isinf)
1621 if(op_type.
id()==ID_fixedbv)
1623 else if(op_type.
id()==ID_floatbv)
1627 out <<
"(fp.isInfinite ";
1637 else if(expr.
id()==ID_isnormal)
1643 if(op_type.
id()==ID_fixedbv)
1645 else if(op_type.
id()==ID_floatbv)
1649 out <<
"(fp.isNormal ";
1659 else if(expr.
id()==ID_overflow_plus ||
1660 expr.
id()==ID_overflow_minus)
1664 "overflow plus and overflow minus expressions shall have two operands");
1667 expr.
type().
id() == ID_bool,
1668 "overflow plus and overflow minus expressions shall be of Boolean type");
1670 bool subtract=expr.
id()==ID_overflow_minus;
1674 if(op_type.
id()==ID_signedbv)
1677 out <<
"(let ((?sum (";
1678 out << (subtract?
"bvsub":
"bvadd");
1679 out <<
" ((_ sign_extend 1) ";
1682 out <<
" ((_ sign_extend 1) ";
1686 "((_ extract " << width <<
" " << width <<
") ?sum) " 1687 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1690 else if(op_type.
id()==ID_unsignedbv ||
1691 op_type.
id()==ID_pointer)
1695 out <<
"((_ extract " << width <<
" " << width <<
") ";
1696 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1697 out <<
" ((_ zero_extend 1) ";
1700 out <<
" ((_ zero_extend 1) ";
1708 "overflow check should not be performed on unsupported type",
1711 else if(expr.
id()==ID_overflow_mult)
1715 "overflow mult expression shall have two operands");
1718 expr.
type().
id() == ID_bool,
1719 "overflow mult expression shall be of Boolean type");
1727 if(op_type.id()==ID_signedbv)
1729 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1731 out <<
") ((_ sign_extend " << width <<
") ";
1734 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" " 1736 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" " 1737 << width*2 <<
")))))";
1739 else if(op_type.id()==ID_unsignedbv)
1741 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1743 out <<
") ((_ zero_extend " << width <<
") ";
1745 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1750 "overflow check should not be performed on unsupported type",
1751 op_type.id_string());
1753 else if(expr.
id()==ID_array)
1759 else if(expr.
id()==ID_literal)
1763 else if(expr.
id()==ID_forall ||
1764 expr.
id()==ID_exists)
1770 throw "MathSAT does not support quantifiers";
1772 if(quantifier_expr.
id() == ID_forall)
1774 else if(quantifier_expr.
id() == ID_exists)
1789 else if(expr.
id()==ID_vector)
1794 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1797 size == vector_expr.
operands().size(),
1798 "size indicated by type shall be equal to the number of operands");
1802 const std::string &smt_typename =
datatype_map.at(vector_type);
1804 out <<
"(mk-" << smt_typename;
1818 else if(expr.
id()==ID_object_size)
1822 else if(expr.
id()==ID_let)
1833 else if(expr.
id()==ID_constraint_select_one)
1836 "smt2_convt::convert_expr: `"+expr.
id_string()+
1837 "' is not yet supported");
1839 else if(expr.
id() == ID_bswap)
1845 "operand of byte swap expression shall have same type as the expression");
1848 out <<
"(let ((bswap_op ";
1853 bswap_expr.
type().
id() == ID_signedbv ||
1854 bswap_expr.
type().
id() == ID_unsignedbv)
1856 const std::size_t width =
1863 width % bits_per_byte == 0,
1864 "bit width indicated by type of bswap expression should be a multiple " 1865 "of the number of bits per byte");
1867 const std::size_t bytes = width / bits_per_byte;
1876 for(std::size_t byte = 0; byte < bytes; byte++)
1880 out <<
"(bswap_byte_" << byte <<
' ';
1881 out <<
"((_ extract " << (byte * bits_per_byte + (bits_per_byte - 1))
1882 <<
" " << (byte * bits_per_byte) <<
") bswap_op)";
1891 for(std::size_t byte = 0; byte < bytes; byte++)
1892 out <<
" bswap_byte_" << byte;
1903 else if(expr.
id() == ID_popcount)
1911 "smt2_convt::convert_expr should not be applied to unsupported type",
1920 if(dest_type.
id()==ID_c_enum_tag)
1924 if(src_type.
id()==ID_c_enum_tag)
1927 if(dest_type.
id()==ID_bool)
1930 if(src_type.
id()==ID_signedbv ||
1931 src_type.
id()==ID_unsignedbv ||
1932 src_type.
id()==ID_c_bool ||
1933 src_type.
id()==ID_fixedbv ||
1934 src_type.
id()==ID_pointer ||
1935 src_type.
id()==ID_integer)
1943 else if(src_type.
id()==ID_floatbv)
1947 out <<
"(not (fp.isZero ";
1959 else if(dest_type.
id()==ID_c_bool)
1968 out <<
" (_ bv1 " << to_width <<
")";
1969 out <<
" (_ bv0 " << to_width <<
")";
1972 else if(dest_type.
id()==ID_signedbv ||
1973 dest_type.
id()==ID_unsignedbv ||
1974 dest_type.
id()==ID_c_enum ||
1975 dest_type.
id()==ID_bv)
1979 if(src_type.
id()==ID_signedbv ||
1980 src_type.
id()==ID_unsignedbv ||
1981 src_type.
id()==ID_c_bool ||
1982 src_type.
id()==ID_c_enum ||
1983 src_type.
id()==ID_bv)
1987 if(from_width==to_width)
1989 else if(from_width<to_width)
1991 if(src_type.
id()==ID_signedbv)
1992 out <<
"((_ sign_extend ";
1994 out <<
"((_ zero_extend ";
1996 out << (to_width-from_width)
2003 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2008 else if(src_type.
id()==ID_fixedbv)
2012 std::size_t from_width=fixedbv_type.
get_width();
2019 out <<
"(let ((?tcop ";
2025 if(to_width>from_integer_bits)
2027 out <<
"((_ sign_extend " 2028 << (to_width-from_integer_bits) <<
") ";
2029 out <<
"((_ extract " << (from_width-1) <<
" " 2030 << from_fraction_bits <<
") ";
2036 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2037 <<
" " << from_fraction_bits <<
") ";
2042 out <<
" (ite (and ";
2045 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) " 2046 "(_ bv0 " << from_fraction_bits <<
")))";
2049 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2054 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2058 else if(src_type.
id()==ID_floatbv)
2060 if(dest_type.
id()==ID_bv)
2077 else if(dest_type.
id()==ID_signedbv)
2081 "typecast unexpected "+src_type.
id_string()+
" -> "+
2084 else if(dest_type.
id()==ID_unsignedbv)
2088 "typecast unexpected "+src_type.
id_string()+
" -> "+
2092 else if(src_type.
id()==ID_bool)
2097 if(dest_type.
id()==ID_fixedbv)
2100 out <<
" (concat (_ bv1 " 2103 "(_ bv0 " << spec.
width <<
")";
2107 out <<
" (_ bv1 " << to_width <<
")";
2108 out <<
" (_ bv0 " << to_width <<
")";
2113 else if(src_type.
id()==ID_pointer)
2117 if(from_width<to_width)
2119 out <<
"((_ sign_extend ";
2120 out << (to_width-from_width)
2127 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2132 else if(src_type.
id()==ID_integer)
2137 mp_integer i = numeric_cast_v<mp_integer>(src);
2138 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2141 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2143 else if(src_type.
id()==ID_struct)
2149 "bit vector with of source and destination type shall be equal");
2156 "bit vector with of source and destination type shall be equal");
2160 else if(src_type.
id()==ID_union)
2164 "bit vector with of source and destination type shall be equal");
2167 else if(src_type.
id()==ID_c_bit_field)
2171 if(from_width==to_width)
2182 std::ostringstream e_str;
2183 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2184 <<
" src == " <<
format(src);
2188 else if(dest_type.
id()==ID_fixedbv)
2194 if(src_type.
id()==ID_unsignedbv ||
2195 src_type.
id()==ID_signedbv ||
2196 src_type.
id()==ID_c_enum)
2203 if(from_width==to_integer_bits)
2205 else if(from_width>to_integer_bits)
2208 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2216 from_width < to_integer_bits,
2217 "from_width should be smaller than to_integer_bits as other case " 2218 "have been handled above");
2219 if(dest_type.
id()==ID_unsignedbv)
2221 out <<
"(_ zero_extend " 2222 << (to_integer_bits-from_width) <<
") ";
2228 out <<
"((_ sign_extend " 2229 << (to_integer_bits-from_width) <<
") ";
2235 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2238 else if(src_type.
id()==ID_bool)
2240 out <<
"(concat (concat" 2241 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2247 else if(src_type.
id()==ID_fixedbv)
2252 std::size_t from_width=from_fixedbv_type.
get_width();
2254 out <<
"(let ((?tcop ";
2260 if(to_integer_bits<=from_integer_bits)
2262 out <<
"((_ extract " 2263 << (from_fraction_bits+to_integer_bits-1) <<
" " 2264 << from_fraction_bits
2270 to_integer_bits > from_integer_bits,
2271 "to_integer_bits should be greater than from_integer_bits as the" 2272 "other case has been handled above");
2273 out <<
"((_ sign_extend " 2274 << (to_integer_bits-from_integer_bits)
2276 << (from_width-1) <<
" " 2277 << from_fraction_bits
2283 if(to_fraction_bits<=from_fraction_bits)
2285 out <<
"((_ extract " 2286 << (from_fraction_bits-1) <<
" " 2287 << (from_fraction_bits-to_fraction_bits)
2293 to_fraction_bits > from_fraction_bits,
2294 "to_fraction_bits should be greater than from_fraction_bits as the" 2295 "other case has been handled above");
2296 out <<
"(concat ((_ extract " 2297 << (from_fraction_bits-1) <<
" 0) ";
2300 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2309 else if(dest_type.
id()==ID_pointer)
2313 if(src_type.
id()==ID_pointer)
2318 else if(src_type.
id()==ID_unsignedbv ||
2319 src_type.
id()==ID_signedbv)
2325 if(from_width==to_width)
2327 else if(from_width<to_width)
2329 out <<
"((_ sign_extend " 2330 << (to_width-from_width)
2337 out <<
"((_ extract " << to_width <<
" 0) ";
2345 else if(dest_type.
id()==ID_range)
2349 else if(dest_type.
id()==ID_floatbv)
2357 if(src_type.
id()==ID_bool)
2372 a.
build(significand, exponent);
2380 a.
build(significand, exponent);
2386 else if(src_type.
id()==ID_c_bool)
2395 else if(dest_type.
id()==ID_integer)
2397 if(src_type.
id()==ID_bool)
2406 else if(dest_type.
id()==ID_c_bit_field)
2411 if(from_width==to_width)
2432 if(dest_type.
id()==ID_floatbv)
2434 if(src_type.
id()==ID_floatbv)
2461 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2462 << dst.
get_f() + 1 <<
") ";
2471 else if(src_type.
id()==ID_unsignedbv)
2492 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" " 2493 << dst.
get_f() + 1 <<
") ";
2502 else if(src_type.
id()==ID_signedbv)
2510 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2511 << dst.
get_f() + 1 <<
") ";
2520 else if(src_type.
id()==ID_c_enum_tag)
2536 else if(dest_type.
id()==ID_signedbv)
2541 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2550 else if(dest_type.
id()==ID_unsignedbv)
2555 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2579 components.size() == expr.
operands().size(),
2580 "number of struct components as indicated by the struct type shall be equal" 2581 "to the number of operands of the struct expression");
2583 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2587 const std::string &smt_typename =
datatype_map.at(struct_type);
2590 out <<
"(mk-" << smt_typename;
2593 for(struct_typet::componentst::const_iterator
2594 it=components.begin();
2595 it!=components.end();
2606 if(components.size()==1)
2611 for(std::size_t i=components.size(); i>1; i--)
2628 for(std::size_t i=1; i<components.size(); i++)
2643 out <<
"(let ((?far ";
2651 out <<
"(select ?far ";
2674 total_width != 0,
"failed to get union width for union");
2678 member_width != 0,
"failed to get union member width for union");
2680 if(total_width==member_width)
2688 total_width > member_width,
2689 "total_width should be greater than member_width as member_width can be" 2690 "at most as large as total_width and the other case has been handled " 2694 << (total_width-member_width) <<
") ";
2704 if(expr_type.
id()==ID_unsignedbv ||
2705 expr_type.
id()==ID_signedbv ||
2706 expr_type.
id()==ID_bv ||
2707 expr_type.
id()==ID_c_enum ||
2708 expr_type.
id()==ID_c_enum_tag ||
2709 expr_type.
id()==ID_c_bool ||
2710 expr_type.
id()==ID_incomplete_c_enum ||
2711 expr_type.
id()==ID_c_bit_field)
2717 out <<
"(_ bv" << value
2718 <<
" " << width <<
")";
2720 else if(expr_type.
id()==ID_fixedbv)
2726 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2728 else if(expr_type.
id()==ID_floatbv)
2741 size_t e=floatbv_type.
get_e();
2742 size_t f=floatbv_type.
get_f()+1;
2748 out <<
"((_ to_fp " << e <<
" " << f <<
")" 2754 out <<
"(_ NaN " << e <<
" " << f <<
")";
2759 out <<
"(_ -oo " << e <<
" " << f <<
")";
2761 out <<
"(_ +oo " << e <<
" " << f <<
")";
2771 <<
"#b" << binaryString.substr(0, 1) <<
" " 2772 <<
"#b" << binaryString.substr(1, e) <<
" " 2773 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
2781 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
2784 else if(expr_type.
id()==ID_pointer)
2796 else if(expr_type.
id()==ID_bool)
2805 else if(expr_type.
id()==ID_array)
2811 else if(expr_type.
id()==ID_rational)
2814 size_t pos=value.find(
"/");
2816 if(
pos==std::string::npos)
2817 out << value <<
".0";
2820 out <<
"(/ " << value.substr(0,
pos) <<
".0 " 2821 << value.substr(
pos+1) <<
".0)";
2824 else if(expr_type.
id()==ID_integer)
2834 if(expr.
type().
id()==ID_unsignedbv ||
2835 expr.
type().
id()==ID_signedbv)
2837 if(expr.
type().
id()==ID_unsignedbv)
2853 std::vector<std::size_t> dynamic_objects;
2858 "is_dynamic_object expression should have one operand");
2860 if(dynamic_objects.empty())
2866 out <<
"(let ((?obj ((_ extract " 2867 << pointer_width-1 <<
" " 2872 if(dynamic_objects.size()==1)
2874 out <<
"(= (_ bv" << dynamic_objects.front()
2881 for(
const auto &
object : dynamic_objects)
2882 out <<
" (= (_ bv" <<
object 2898 if(op_type.id()==ID_unsignedbv ||
2899 op_type.id()==ID_pointer ||
2900 op_type.id()==ID_bv)
2903 if(expr.
id()==ID_le)
2905 else if(expr.
id()==ID_lt)
2907 else if(expr.
id()==ID_ge)
2909 else if(expr.
id()==ID_gt)
2918 else if(op_type.id()==ID_signedbv ||
2919 op_type.id()==ID_fixedbv)
2922 if(expr.
id()==ID_le)
2924 else if(expr.
id()==ID_lt)
2926 else if(expr.
id()==ID_ge)
2928 else if(expr.
id()==ID_gt)
2937 else if(op_type.id()==ID_floatbv)
2942 if(expr.
id()==ID_le)
2944 else if(expr.
id()==ID_lt)
2946 else if(expr.
id()==ID_ge)
2948 else if(expr.
id()==ID_gt)
2960 else if(op_type.id()==ID_rational ||
2961 op_type.id()==ID_integer)
2974 "unsupported type for "+expr.
id_string()+
": "+op_type.id_string());
2980 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
2981 expr.
type().
id() == ID_real)
2986 for(
const auto &op : expr.
operands())
2995 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
2996 expr.
type().
id() == ID_fixedbv)
3013 else if(expr.
type().
id() == ID_floatbv)
3020 else if(expr.
type().
id() == ID_pointer)
3026 if(p.
type().
id() != ID_pointer)
3030 p.
type().
id() == ID_pointer,
3031 "one of the operands should have pointer type");
3034 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3040 if(*element_size >= 2)
3057 else if(expr.
type().
id() == ID_vector)
3061 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3067 const std::string &smt_typename =
datatype_map.at(vector_type);
3069 out <<
"(mk-" << smt_typename;
3079 tmp.copy_to_operands(
3112 if(expr.
id()==ID_constant)
3119 out <<
"roundNearestTiesToEven";
3121 out <<
"roundTowardNegative";
3123 out <<
"roundTowardPositive";
3125 out <<
"roundTowardZero";
3129 "Rounding mode should have value 0, 1, 2, or 3",
3137 out <<
"(ite (= (_ bv0 " << width <<
") ";
3139 out <<
") roundNearestTiesToEven ";
3141 out <<
"(ite (= (_ bv1 " << width <<
") ";
3143 out <<
") roundTowardNegative ";
3145 out <<
"(ite (= (_ bv2 " << width <<
") ";
3147 out <<
") roundTowardPositive ";
3150 out <<
"roundTowardZero";
3161 type.
id() == ID_floatbv ||
3162 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv) ||
3163 (type.
id() == ID_vector && type.
subtype().
id() == ID_floatbv));
3167 if(type.
id()==ID_floatbv)
3177 else if(type.
id()==ID_complex)
3181 else if(type.
id()==ID_vector)
3188 "type should not be one of the unsupported types",
3197 if(expr.
type().
id()==ID_integer)
3205 else if(expr.
type().
id()==ID_unsignedbv ||
3206 expr.
type().
id()==ID_signedbv ||
3207 expr.
type().
id()==ID_fixedbv)
3209 if(expr.
op0().
type().
id()==ID_pointer &&
3214 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3216 if(*element_size >= 2)
3221 "bitvector width of operand shall be equal to the bitvector width of " 3230 if(*element_size >= 2)
3243 else if(expr.
type().
id()==ID_floatbv)
3250 else if(expr.
type().
id()==ID_pointer)
3254 else if(expr.
type().
id()==ID_vector)
3258 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3264 const std::string &smt_typename =
datatype_map.at(vector_type);
3266 out <<
"(mk-" << smt_typename;
3276 tmp.copy_to_operands(
3295 expr.
type().
id() == ID_floatbv,
3296 "type of ieee floating point expression shall be floatbv");
3314 if(expr.
type().
id()==ID_unsignedbv ||
3315 expr.
type().
id()==ID_signedbv)
3317 if(expr.
type().
id()==ID_unsignedbv)
3327 else if(expr.
type().
id()==ID_fixedbv)
3332 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3337 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3339 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3345 else if(expr.
type().
id()==ID_floatbv)
3359 expr.
type().
id() == ID_floatbv,
3360 "type of ieee floating point expression shall be floatbv");
3391 "expression should have been converted to a variant with two operands");
3393 if(expr.
type().
id()==ID_unsignedbv ||
3394 expr.
type().
id()==ID_signedbv)
3405 else if(expr.
type().
id()==ID_floatbv)
3412 else if(expr.
type().
id()==ID_fixedbv)
3417 out <<
"((_ extract " 3418 << spec.
width+fraction_bits-1 <<
" " 3419 << fraction_bits <<
") ";
3423 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3427 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3433 else if(expr.
type().
id()==ID_rational ||
3434 expr.
type().
id()==ID_integer ||
3435 expr.
type().
id()==ID_real)
3454 expr.
type().
id() == ID_floatbv,
3455 "type of ieee floating point expression shall be floatbv");
3477 std::size_t s=expr.
operands().size();
3492 "with expression should have been converted to a version with three " 3497 if(expr_type.id()==ID_array)
3521 out <<
"(let ((distance? ";
3522 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3526 if(array_width>index_width)
3528 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3534 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3543 out <<
"(bvlshr (_ bv" <<
power(2, array_width)-1 <<
" " 3544 << array_width <<
") ";
3545 out <<
"distance?) ";
3549 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3551 out <<
") distance?)))";
3554 else if(expr_type.id()==ID_struct)
3561 const irep_idt &component_name=index.
get(ID_component_name);
3565 "struct should have accessed component");
3569 const std::string &smt_typename =
datatype_map.at(expr_type);
3571 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3585 out <<
"(let ((?withop ";
3589 if(m.
width==struct_width)
3598 <<
"((_ extract " << (struct_width-1) <<
" " 3599 << m.
width <<
") ?withop) ";
3608 out <<
"((_ extract " << (m.
offset-1) <<
" 0) ?withop))";
3613 out <<
"(concat (concat " 3614 <<
"((_ extract " << (struct_width-1) <<
" " 3617 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3624 else if(expr_type.id()==ID_union)
3634 total_width != 0,
"failed to get union width for with");
3638 member_width != 0,
"failed to get union member width for with");
3640 if(total_width==member_width)
3647 total_width > member_width,
3648 "total width should be greater than member_width as member_width is at " 3649 "most as large as total_width and the other case has been handled " 3652 out <<
"((_ extract " 3654 <<
" " << member_width <<
") ";
3661 else if(expr_type.id()==ID_bv ||
3662 expr_type.id()==ID_unsignedbv ||
3663 expr_type.id()==ID_signedbv)
3669 total_width != 0,
"failed to get total width");
3676 value_width != 0,
"failed to get value width");
3688 out <<
" (bvnot (bvshl";
3691 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3692 out <<
" (repeat[" << value_width <<
"] bv1[1])";
3714 "with expects struct, union, or array type, but got "+
3722 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
3729 if(array_op_type.
id()==ID_array)
3765 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
3769 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3773 if(array_width>index_width)
3775 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3781 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3791 else if(array_op_type.
id()==ID_vector)
3797 const std::string &smt_typename =
datatype_map.at(vector_type);
3804 SMT2_TODO(
"non-constant index on vectors");
3808 out <<
"(" << smt_typename <<
"." << index_int <<
" ";
3820 false,
"index with unsupported array type: " + array_op_type.
id_string());
3830 if(struct_op_type.
id()==ID_struct)
3836 struct_type.
has_component(name),
"struct should have accessed component");
3840 const std::string &smt_typename =
datatype_map.at(struct_type);
3842 out <<
"(" << smt_typename <<
"." 3855 member_offset.has_value(),
"failed to get struct member offset");
3857 out <<
"((_ extract " << ((*member_offset) * 8 + member_width - 1) <<
" " 3863 else if(struct_op_type.
id()==ID_union)
3867 width != 0,
"failed to get union member width");
3871 out <<
"((_ extract " 3881 "convert_member on an unexpected type "+struct_op_type.
id_string());
3888 if(type.
id()==ID_bool)
3894 else if(type.
id()==ID_vector)
3898 const std::string &smt_typename =
datatype_map.at(type);
3903 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3905 out <<
"(let ((?vflop ";
3913 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
3921 else if(type.
id()==ID_array)
3925 else if(type.
id()==ID_struct)
3929 const std::string &smt_typename =
datatype_map.at(type);
3934 out <<
"(let ((?sflop ";
3942 for(std::size_t i=components.size(); i>1; i--)
3944 out <<
"(concat (" << smt_typename <<
"." 3945 << components[i-1].get_name() <<
" ?sflop)";
3950 out <<
"(" << smt_typename <<
"." 3951 << components[0].get_name() <<
" ?sflop)";
3953 for(std::size_t i=1; i<components.size(); i++)
3961 else if(type.
id()==ID_floatbv)
3965 "floatbv expressions should be flattened when using FPA theory");
3978 if(type.
id() == ID_symbol_type)
3981 if(type.
id()==ID_bool)
3988 else if(type.
id()==ID_vector)
3992 const std::string &smt_typename =
datatype_map.at(type);
3999 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4002 out <<
"(let ((?ufop" << nesting <<
" ";
4007 out <<
"(mk-" << smt_typename;
4009 std::size_t offset=0;
4011 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4015 out <<
"((_ extract " << offset+subtype_width-1 <<
" " 4016 << offset <<
") ?ufop" << nesting <<
")";
4028 else if(type.
id()==ID_struct)
4034 out <<
"(let ((?ufop" << nesting <<
" ";
4039 const std::string &smt_typename =
datatype_map.at(type);
4041 out <<
"(mk-" << smt_typename;
4048 std::size_t offset=0;
4051 for(struct_typet::componentst::const_iterator
4052 it=components.begin();
4053 it!=components.end();
4060 out <<
"((_ extract " << offset+member_width-1 <<
" " 4061 << offset <<
") ?ufop" << nesting <<
")";
4063 offset+=member_width;
4089 if(expr.
id()==ID_and && value)
4096 if(expr.
id()==ID_or && !value)
4103 if(expr.
id()==ID_not)
4113 if(expr.
id() == ID_equal && value)
4117 if(equal_expr.
lhs().
id()==ID_symbol)
4127 id.type=equal_expr.
lhs().
type();
4134 out <<
"; set_to true (equal)\n";
4135 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4154 out <<
"; set_to " << (value?
"true":
"false") <<
"\n" 4180 if(expr.
id()==ID_symbol ||
4181 expr.
id()==ID_nondet_symbol)
4184 if(expr.
type().
id()==ID_code)
4189 if(expr.
id()==ID_symbol)
4192 identifier=
"nondet_"+
4197 if(
id.type.is_nil())
4199 id.type=expr.
type();
4204 out <<
"; find_symbols\n";
4205 out <<
"(declare-fun |" 4212 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)
4269 out <<
"; the following is a substitute for a string" <<
"\n";
4270 out <<
"(declare-fun " <<
id <<
" () ";
4274 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4276 out <<
"(assert (= (select " << id;
4280 out <<
"))" <<
"\n";
4286 else if(expr.
id()==ID_object_size &&
4291 if(op.
type().
id()==ID_pointer)
4297 out <<
"(declare-fun " <<
id <<
" () ";
4307 (expr.
id()==ID_floatbv_plus ||
4308 expr.
id()==ID_floatbv_minus ||
4309 expr.
id()==ID_floatbv_mult ||
4310 expr.
id()==ID_floatbv_div ||
4311 expr.
id()==ID_floatbv_typecast ||
4312 expr.
id()==ID_ieee_float_equal ||
4313 expr.
id()==ID_ieee_float_notequal ||
4314 ((expr.
id()==ID_lt ||
4318 expr.
id()==ID_isnan ||
4319 expr.
id()==ID_isnormal ||
4320 expr.
id()==ID_isfinite ||
4321 expr.
id()==ID_isinf ||
4322 expr.
id()==ID_sign ||
4323 expr.
id()==ID_unary_minus ||
4324 expr.
id()==ID_typecast ||
4325 expr.
id()==ID_abs) &&
4331 if(
bvfp_set.insert(
function).second)
4333 out <<
"; this is a model for " << expr.
id()
4336 <<
"(define-fun " <<
function <<
" (";
4338 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4342 out <<
"(op" << i <<
' ';
4352 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4380 if(expr.
id()==ID_with)
4382 else if(expr.
id()==ID_member)
4391 if(type.
id()==ID_array)
4404 out <<
"(_ BitVec 1)";
4410 else if(type.
id()==ID_bool)
4414 else if(type.
id()==ID_struct)
4424 width != 0,
"failed to get width of struct");
4426 out <<
"(_ BitVec " << width <<
")";
4429 else if(type.
id()==ID_vector)
4441 width != 0,
"failed to get width of vector");
4443 out <<
"(_ BitVec " << width <<
")";
4446 else if(type.
id()==ID_code)
4453 else if(type.
id()==ID_union)
4460 out <<
"(_ BitVec " << width <<
")";
4462 else if(type.
id()==ID_pointer)
4467 else if(type.
id()==ID_bv ||
4468 type.
id()==ID_fixedbv ||
4469 type.
id()==ID_unsignedbv ||
4470 type.
id()==ID_signedbv ||
4471 type.
id()==ID_c_bool)
4476 else if(type.
id()==ID_c_enum)
4482 else if(type.
id()==ID_c_enum_tag)
4486 else if(type.
id()==ID_floatbv)
4491 out <<
"(_ FloatingPoint " 4492 << floatbv_type.
get_e() <<
" " 4493 << floatbv_type.
get_f() + 1 <<
")";
4498 else if(type.
id()==ID_rational ||
4501 else if(type.
id()==ID_integer)
4503 else if(type.
id() == ID_symbol_type)
4505 else if(type.
id()==ID_complex)
4517 width != 0,
"failed to get width of complex");
4519 out <<
"(_ BitVec " << width <<
")";
4522 else if(type.
id()==ID_c_bit_field)
4534 std::set<irep_idt> recstack;
4540 std::set<irep_idt> &recstack)
4542 if(type.
id()==ID_array)
4548 else if(type.
id()==ID_incomplete_array)
4552 else if(type.
id()==ID_complex)
4559 const std::string smt_typename =
4563 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4564 <<
"(mk-" << smt_typename;
4566 out <<
" (" << smt_typename <<
".imag ";
4570 out <<
" (" << smt_typename <<
".real ";
4577 else if(type.
id()==ID_vector)
4586 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4588 const std::string smt_typename =
4592 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4593 <<
"(mk-" << smt_typename;
4597 out <<
" (" << smt_typename <<
"." << i <<
" ";
4605 else if(type.
id()==ID_struct)
4608 bool need_decl=
false;
4612 const std::string smt_typename =
4627 const std::string &smt_typename =
datatype_map.at(type);
4638 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4639 <<
"(mk-" << smt_typename <<
" ";
4643 out <<
"(" << smt_typename <<
"." <<
component.get_name()
4649 out <<
"))))" <<
"\n";
4666 for(struct_union_typet::componentst::const_iterator
4667 it=components.begin();
4668 it!=components.end();
4672 out <<
"(define-fun update-" << smt_typename <<
"." 4674 <<
"((s " << smt_typename <<
") " 4677 out <<
")) " << smt_typename <<
" " 4678 <<
"(mk-" << smt_typename
4681 for(struct_union_typet::componentst::const_iterator
4682 it2=components.begin();
4683 it2!=components.end();
4690 out <<
"(" << smt_typename <<
"." 4691 << it2->get_name() <<
" s) ";
4695 out <<
"))" <<
"\n";
4701 else if(type.
id()==ID_union)
4709 else if(type.
id()==ID_code)
4713 for(
const auto ¶m : parameters)
4718 else if(type.
id()==ID_pointer)
4722 else if(type.
id() == ID_symbol_type)
4727 if(recstack.find(
id)==recstack.end())
4729 recstack.insert(
id);
4738 std::vector<exprt> let_order;
4747 std::vector<exprt> &let_order,
4751 if(i>=let_order.size())
4754 exprt current=let_order[i];
4756 map.
find(current) != map.
end(),
"expression should have been seen already");
4759 return letify_rec(expr, let_order, map, i+1);
4762 map.
find(current)->second.let_symbol,
4770 std::vector<exprt> &let_order)
4789 map.
find(expr) == map.
end(),
"expression should not have been seen yet");
4796 let_order.push_back(expr);
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const irep_idt & get_name() const
void unflatten(wheret, const typet &, unsigned nesting=0)
The type of an expression, extends irept.
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.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
datatype_mapt datatype_map
virtual tvt l_get(literalt l) const
Semantic type conversion.
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 an 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 typet to a signedbv_typet.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an 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 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 an exprt to a div_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
void convert_literal(const literalt)
Evaluates to true if the operand is infinite.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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 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
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
std::vector< componentt > componentst
void convert_update(const exprt &expr)
bool is_false() const
Return whether the expression is a constant representing false.
const_iterator find(const Key &key) const
const irep_idt & get_value() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a 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)
The trinary if-then-else operator.
bool is_true() const
Return whether the expression is a constant representing true.
Evaluates to true if the operand is a normal number.
typet & type()
Return the type of the expression.
void get_dynamic_objects(std::vector< std::size_t > &objects) const
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
void convert_plus(const plus_exprt &expr)
std::string type2id(const typet &) const
A constant literal expression.
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
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
Follow type tag of union type.
bool use_array_theory(const exprt &)
const let_exprt & to_let_expr(const exprt &expr)
Cast an 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 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)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
virtual literalt convert(const exprt &expr)
struct configt::bv_encodingt bv_encoding
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an 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
Evaluates to true if the operand is NaN.
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
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
A reference into the symbol table.
const irep_idt & get_identifier() const
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
void convert_mod(const mod_exprt &expr)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
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)
std::size_t unsafe_string2size_t(const std::string &str, int base)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Union constructor from single element.
API to expression classes.
void convert_index(const index_exprt &expr)
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
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
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an 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 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)
The plus expression Associativity is not specified.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an 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.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
void convert_minus(const minus_exprt &expr)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const_iterator end() const
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Vector constructor from list of elements.
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
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Operator to return the address of an object.
const irep_idt & get_identifier() const
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
The unary minus expression.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Fixed-width bit-vector with signed fixed-point interpretation.
The Boolean constant false.
bool is_constant() const
Return whether the expression is a constant.
std::size_t get_width() const
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an 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 typet to a c_enum_tag_typet.
exprt float_bv(const exprt &src)
bool has_component(const irep_idt &component_name) const
Binary multiplication Associativity is not specified.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::size_t get_f() const
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a 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 an exprt to a popcount_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
exprt lower_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...
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
mstreamt & result() const
virtual exprt get(const exprt &expr) const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a 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 typet to a fixedbv_typet.
const string_constantt & to_string_constant(const exprt &expr)
Evaluates to true if the operand is finite.
void convert_is_dynamic_object(const exprt &expr)
std::size_t get_bits_per_byte() const
Semantic type conversion from/to floating-point formats.
literalt get_literal() const
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
Sign of an expression Predicate is true if _op is negative, false otherwise.
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 an exprt to a union_exprt.
Operator to update elements in structs and arrays.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
void convert_overflow(const exprt &expr)
A base class for quantifier expressions.
static std::string binary(const constant_exprt &src)
irep_idt get_component_name() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
#define UNREACHABLE
This should be used to mark dead code.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
void find_symbols(const exprt &expr)
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
std::size_t no_boolean_variables
void convert_member(const member_exprt &expr)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
exprt parse_rec(const irept &s, const typet &type)
const std::string & id_string() const
#define Forall_operands(it, expr)
bool is_zero() const
Return whether the expression is a constant representing 0.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
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 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 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)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const typet & subtype() const
exprt parse_struct(const irept &s, const struct_typet &type)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
#define UNEXPECTEDCASE(S)
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
void write_footer(std::ostream &)
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 These have two data operands (op0 and op1) and one rounding mode (op2)...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
A base class for shift operators.
smt2_identifierst smt2_identifiers
const irep_idt & get_identifier() const
defined_expressionst defined_expressions
The byte swap expression.
void set(const irep_namet &name, const irep_idt &value)
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
pointer_logict pointer_logic
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
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)