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";
87 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
89 out <<
"(set-option :produce-models true)" <<
"\n";
95 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
105 out <<
"; assumptions\n";
119 out <<
"(check-sat)" <<
"\n";
125 out <<
"(get-value (|" <<
id <<
"|))" <<
"\n";
132 out <<
"; end of SMT2 file" <<
"\n";
139 assert(expr.
id()==ID_object_size);
143 std::size_t number = 0;
144 std::size_t h=pointer_width-1;
153 if(o.id()!=ID_symbol ||
161 out <<
"(assert (implies (= " <<
162 "((_ extract " << h <<
" " << l <<
") ";
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_member)
229 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
234 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
240 PARSERERROR(
"smt2_convt::parse_literal can't parse \""+s+
"\"");
242 else if(src.
get_sub().size()==3 &&
245 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
249 else if(src.
get_sub().size()==4 &&
252 if(type.
id()==ID_floatbv)
269 else if(src.
get_sub().size()==4 &&
277 else if(src.
get_sub().size()==4 &&
285 else if(src.
get_sub().size()==4 &&
294 if(type.
id()==ID_signedbv ||
295 type.
id()==ID_unsignedbv ||
297 type.
id()==ID_c_enum ||
298 type.
id()==ID_c_bool)
302 else if(type.
id()==ID_c_enum_tag)
309 else if(type.
id()==ID_fixedbv ||
310 type.
id()==ID_floatbv)
315 else if(type.
id()==ID_integer ||
338 else if(src.
get_sub().size()==2 &&
339 src.
get_sub()[0].get_sub().size()==3 &&
340 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
341 src.
get_sub()[0].get_sub()[1].id()==
"const")
364 return union_exprt(first.get_name(), converted, type);
378 if(components.empty())
386 if(src.
get_sub().size()!=components.size()+1)
389 for(std::size_t i=0; i<components.size(); i++)
404 if(binary.
size()!=total_width)
407 std::size_t offset=0;
409 for(std::size_t i=0; i<components.size(); i++)
411 std::size_t component_width=
boolbv_width(components[i].type());
413 assert(offset+component_width<=total_width);
414 std::string component_binary=
416 total_width-offset-component_width, component_width);
421 offset+=component_width;
432 if(type.
id()==ID_signedbv ||
433 type.
id()==ID_unsignedbv ||
435 type.
id()==ID_fixedbv ||
436 type.
id()==ID_floatbv)
440 else if(type.
id()==ID_bool)
442 if(src.
id()==ID_1 || src.
id()==ID_true)
444 else if(src.
id()==ID_0 || src.
id()==ID_false)
447 else if(type.
id()==ID_pointer)
463 else if(type.
id()==ID_struct)
467 else if(type.
id()==ID_union)
471 else if(type.
id()==ID_array)
483 if(expr.
id()==ID_symbol ||
484 expr.
id()==ID_constant ||
485 expr.
id()==ID_string_constant ||
493 else if(expr.
id()==ID_index)
503 if(array.
type().
id()==ID_pointer)
505 else if(array.
type().
id()==ID_array)
513 exprt new_index_expr=expr;
523 address_of_expr.
type());
528 else if(expr.
id()==ID_member)
538 if(struct_op_type.
id()==ID_struct)
561 else if(expr.
id()==ID_if)
598 INVALIDEXPR(
"byte_update takes constant as second parameter");
609 if(expr.
id()==ID_byte_update_little_endian)
612 upper = lower+value_width-1;
614 else if(expr.
id()==ID_byte_update_big_endian)
617 lower = max-((i+1)*8-1);
634 out <<
" ((_ extract " << lower-1 <<
" 0) ";
644 out <<
"((_ extract " << max <<
" " << (upper+1) <<
") ";
652 out <<
"(concat (concat ";
653 out <<
"((_ extract " << max <<
" " << (upper+1) <<
") ";
657 out <<
") ((_ extract " << (lower-1) <<
" 0) ";
692 assert(expr.
type().
id()==ID_bool);
700 else if(expr.
id()==ID_literal)
712 out <<
"; convert\n";
713 out <<
"(define-fun ";
750 for(std::size_t i=0; i<identifier.
size(); i++)
752 char ch=identifier[i];
760 result+=std::to_string(ch);
775 if(type.
id()==ID_floatbv)
778 return "f"+std::to_string(spec.
width())+
"_"+std::to_string(spec.
f);
780 else if(type.
id()==ID_unsignedbv)
784 else if(type.
id()==ID_c_bool)
788 else if(type.
id()==ID_signedbv)
792 else if(type.
id()==ID_bool)
796 else if(type.
id()==ID_c_enum_tag)
817 if(expr.
id()==ID_symbol)
824 if(expr.
id()==ID_smt2_symbol)
833 out <<
"(|float_bv." << expr.
id()
849 if(expr.
id()==ID_symbol)
856 else if(expr.
id()==ID_nondet_symbol)
862 else if(expr.
id()==ID_smt2_symbol)
868 else if(expr.
id()==ID_typecast)
872 else if(expr.
id()==ID_floatbv_typecast)
876 else if(expr.
id()==ID_struct)
880 else if(expr.
id()==ID_union)
884 else if(expr.
id()==ID_constant)
888 else if(expr.
id()==ID_concatenation ||
889 expr.
id()==ID_bitand ||
890 expr.
id()==ID_bitor ||
891 expr.
id()==ID_bitxor ||
892 expr.
id()==ID_bitnand ||
893 expr.
id()==ID_bitnor)
899 if(expr.
id()==ID_concatenation)
901 else if(expr.
id()==ID_bitand)
903 else if(expr.
id()==ID_bitor)
905 else if(expr.
id()==ID_bitxor)
907 else if(expr.
id()==ID_bitnand)
909 else if(expr.
id()==ID_bitnor)
920 else if(expr.
id()==ID_bitnot)
924 if(expr.
type().
id()==ID_vector)
930 const std::string smt_typename=
938 INVALIDEXPR(
"failed to convert vector size to constant");
940 out <<
"(let ((?vectorop ";
944 out <<
"(mk-" << smt_typename;
951 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
967 else if(expr.
id()==ID_unary_minus)
971 if(expr.
type().
id()==ID_rational)
977 else if(expr.
type().
id()==ID_floatbv)
989 else if(expr.
type().
id()==ID_vector)
995 const std::string smt_typename=
1003 INVALIDEXPR(
"failed to convert vector size to constant");
1005 out <<
"(let ((?vectorop ";
1009 out <<
"(mk-" << smt_typename;
1016 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1032 else if(expr.
id()==ID_unary_plus)
1038 else if(expr.
id()==ID_sign)
1044 if(op_type.id()==ID_floatbv)
1048 out <<
"(fp.isNegative ";
1055 else if(op_type.id()==ID_signedbv)
1061 out <<
" (_ bv0 " << op_width <<
"))";
1066 else if(expr.
id()==ID_if)
1078 else if(expr.
id()==ID_and ||
1082 assert(expr.
type().
id()==ID_bool);
1085 out <<
"(" << expr.
id();
1093 else if(expr.
id()==ID_implies)
1095 assert(expr.
type().
id()==ID_bool);
1104 else if(expr.
id()==ID_not)
1106 assert(expr.
type().
id()==ID_bool);
1113 else if(expr.
id()==ID_equal ||
1114 expr.
id()==ID_notequal)
1119 if(expr.
id()==ID_notequal)
1136 else if(expr.
id()==ID_ieee_float_equal ||
1137 expr.
id()==ID_ieee_float_notequal)
1147 if(expr.
id()==ID_ieee_float_notequal)
1156 if(expr.
id()==ID_ieee_float_notequal)
1162 else if(expr.
id()==ID_le ||
1169 else if(expr.
id()==ID_plus)
1173 else if(expr.
id()==ID_floatbv_plus)
1177 else if(expr.
id()==ID_minus)
1181 else if(expr.
id()==ID_floatbv_minus)
1185 else if(expr.
id()==ID_div)
1189 else if(expr.
id()==ID_floatbv_div)
1193 else if(expr.
id()==ID_mod)
1197 else if(expr.
id()==ID_mult)
1201 else if(expr.
id()==ID_floatbv_mult)
1205 else if(expr.
id()==ID_address_of)
1208 assert(expr.
type().
id()==ID_pointer);
1211 else if(expr.
id()==ID_array_of)
1213 assert(expr.
type().
id()==ID_array);
1219 else if(expr.
id()==ID_index)
1223 else if(expr.
id()==ID_ashr ||
1224 expr.
id()==ID_lshr ||
1231 if(type.
id()==ID_unsignedbv ||
1232 type.
id()==ID_signedbv ||
1235 if(expr.
id()==ID_ashr)
1237 else if(expr.
id()==ID_lshr)
1239 else if(expr.
id()==ID_shl)
1261 else if(expr.
op1().
type().
id()==ID_signedbv ||
1262 expr.
op1().
type().
id()==ID_unsignedbv ||
1269 if(width_op0==width_op1)
1271 else if(width_op0>width_op1)
1273 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1279 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1286 "unsupported op1 type for "+expr.
id_string()+
": "+
1295 else if(expr.
id()==ID_with)
1299 else if(expr.
id()==ID_update)
1303 else if(expr.
id()==ID_member)
1307 else if(expr.
id()==ID_pointer_offset)
1310 assert(expr.
op0().
type().
id()==ID_pointer);
1315 if(offset_bits>result_width)
1316 offset_bits=result_width;
1319 if(result_width>offset_bits)
1320 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1322 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1326 if(result_width>offset_bits)
1329 else if(expr.
id()==ID_pointer_object)
1332 assert(expr.
op0().
type().
id()==ID_pointer);
1337 out <<
"((_ zero_extend " << ext <<
") ";
1339 out <<
"((_ extract " 1340 << pointer_width-1 <<
" " 1348 else if(expr.
id()==ID_dynamic_object)
1352 else if(expr.
id()==ID_invalid_pointer)
1357 out <<
"(= ((_ extract " 1358 << pointer_width-1 <<
" " 1364 else if(expr.
id()==
"pointer_object_has_type")
1369 SMT2_TODO(
"pointer_object_has_type not implemented");
1371 else if(expr.
id()==ID_string_constant)
1377 else if(expr.
id()==ID_extractbit)
1387 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1393 out <<
"(= ((_ extract 0 0) ";
1403 else if(expr.
id()==ID_extractbits)
1418 std::swap(op1_i, op2_i);
1422 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1429 out <<
"(= ((_ extract 0 0) ";
1438 SMT2_TODO(
"smt2: extractbits with non-constant index");
1441 else if(expr.
id()==ID_replication)
1447 INVALIDEXPR(
"replication takes constant as first parameter");
1449 out <<
"((_ repeat " << times <<
") ";
1453 else if(expr.
id()==ID_byte_extract_little_endian ||
1454 expr.
id()==ID_byte_extract_big_endian)
1458 else if(expr.
id()==ID_byte_update_little_endian ||
1459 expr.
id()==ID_byte_update_big_endian)
1463 else if(expr.
id()==ID_width)
1480 out <<
"(_ bv" << op_width/8
1481 <<
" " << result_width <<
")";
1483 else if(expr.
id()==ID_abs)
1489 if(type.id()==ID_signedbv)
1493 out <<
"(ite (bvslt ";
1495 out <<
" (_ bv0 " << result_width <<
")) ";
1502 else if(type.id()==ID_fixedbv)
1506 out <<
"(ite (bvslt ";
1508 out <<
" (_ bv0 " << result_width <<
")) ";
1515 else if(type.id()==ID_floatbv)
1529 else if(expr.
id()==ID_isnan)
1535 if(op_type.id()==ID_fixedbv)
1537 else if(op_type.id()==ID_floatbv)
1541 out <<
"(fp.isNaN ";
1551 else if(expr.
id()==ID_isfinite)
1558 if(op_type.
id()==ID_fixedbv)
1560 else if(op_type.
id()==ID_floatbv)
1566 out <<
"(not (fp.isNaN ";
1570 out <<
"(not (fp.isInf ";
1582 else if(expr.
id()==ID_isinf)
1589 if(op_type.
id()==ID_fixedbv)
1591 else if(op_type.
id()==ID_floatbv)
1595 out <<
"(fp.isInfinite ";
1605 else if(expr.
id()==ID_isnormal)
1612 if(op_type.
id()==ID_fixedbv)
1614 else if(op_type.
id()==ID_floatbv)
1618 out <<
"(fp.isNormal ";
1628 else if(expr.
id()==ID_overflow_plus ||
1629 expr.
id()==ID_overflow_minus)
1632 assert(expr.
type().
id()==ID_bool);
1634 bool subtract=expr.
id()==ID_overflow_minus;
1638 if(op_type.
id()==ID_signedbv)
1641 out <<
"(let ((?sum (";
1642 out << (subtract?
"bvsub":
"bvadd");
1643 out <<
" ((_ sign_extend 1) ";
1646 out <<
" ((_ sign_extend 1) ";
1650 "((_ extract " << width <<
" " << width <<
") ?sum) " 1651 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1654 else if(op_type.
id()==ID_unsignedbv ||
1655 op_type.
id()==ID_pointer)
1659 out <<
"((_ extract " << width <<
" " << width <<
") ";
1660 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1661 out <<
" ((_ zero_extend 1) ";
1664 out <<
" ((_ zero_extend 1) ";
1672 else if(expr.
id()==ID_overflow_mult)
1682 if(op_type.id()==ID_signedbv)
1684 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1686 out <<
") ((_ sign_extend " << width <<
") ";
1689 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" " 1691 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" " 1692 << width*2 <<
")))))";
1694 else if(op_type.id()==ID_unsignedbv)
1696 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1698 out <<
") ((_ zero_extend " << width <<
") ";
1700 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1703 UNEXPECTEDCASE(
"overflow-* check on unknown type: "+op_type.id_string());
1705 else if(expr.
id()==ID_array)
1711 else if(expr.
id()==ID_literal)
1715 else if(expr.
id()==ID_forall ||
1716 expr.
id()==ID_exists)
1720 throw "MathSAT does not support quantifiers";
1722 if(expr.
id()==ID_forall)
1724 else if(expr.
id()==ID_exists)
1739 else if(expr.
id()==ID_vector)
1745 INVALIDEXPR(
"failed to convert vector size to constant");
1747 assert(size==expr.
operands().size());
1753 const std::string smt_typename=
1756 out <<
"(mk-" << smt_typename;
1770 else if(expr.
id()==ID_object_size)
1774 else if(expr.
id()==ID_let)
1785 else if(expr.
id()==ID_constraint_select_one)
1788 "smt2_convt::convert_expr: `"+expr.
id_string()+
1789 "' is not yet supported");
1793 "smt2_convt::convert_expr: `"+expr.
id_string()+
"' is unsupported");
1802 if(dest_type.
id()==ID_c_enum_tag)
1806 if(src_type.
id()==ID_c_enum_tag)
1809 if(dest_type.
id()==ID_bool)
1812 if(src_type.
id()==ID_signedbv ||
1813 src_type.
id()==ID_unsignedbv ||
1814 src_type.
id()==ID_c_bool ||
1815 src_type.
id()==ID_fixedbv ||
1816 src_type.
id()==ID_pointer)
1824 else if(src_type.
id()==ID_floatbv)
1828 out <<
"(not (fp.isZero ";
1840 else if(dest_type.
id()==ID_c_bool)
1849 out <<
" (_ bv1 " << to_width <<
")";
1850 out <<
" (_ bv0 " << to_width <<
")";
1853 else if(dest_type.
id()==ID_signedbv ||
1854 dest_type.
id()==ID_unsignedbv ||
1855 dest_type.
id()==ID_c_enum ||
1856 dest_type.
id()==ID_bv)
1860 if(src_type.
id()==ID_signedbv ||
1861 src_type.
id()==ID_unsignedbv ||
1862 src_type.
id()==ID_c_bool ||
1863 src_type.
id()==ID_c_enum ||
1864 src_type.
id()==ID_bv)
1868 if(from_width==to_width)
1870 else if(from_width<to_width)
1872 if(src_type.
id()==ID_signedbv)
1873 out <<
"((_ sign_extend ";
1875 out <<
"((_ zero_extend ";
1877 out << (to_width-from_width)
1884 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
1889 else if(src_type.
id()==ID_fixedbv)
1893 std::size_t from_width=fixedbv_type.
get_width();
1900 out <<
"(let ((?tcop ";
1906 if(to_width>from_integer_bits)
1908 out <<
"((_ sign_extend " 1909 << (to_width-from_integer_bits) <<
") ";
1910 out <<
"((_ extract " << (from_width-1) <<
" " 1911 << from_fraction_bits <<
") ";
1917 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
1918 <<
" " << from_fraction_bits <<
") ";
1923 out <<
" (ite (and ";
1926 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) " 1927 "(_ bv0 " << from_fraction_bits <<
")))";
1930 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
1935 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
1939 else if(src_type.
id()==ID_floatbv)
1941 if(dest_type.
id()==ID_bv)
1958 else if(dest_type.
id()==ID_signedbv)
1962 "typecast unexpected "+src_type.
id_string()+
" -> "+
1965 else if(dest_type.
id()==ID_unsignedbv)
1969 "typecast unexpected "+src_type.
id_string()+
" -> "+
1973 else if(src_type.
id()==ID_bool)
1978 if(dest_type.
id()==ID_fixedbv)
1981 out <<
" (concat (_ bv1 " 1984 "(_ bv0 " << spec.
width <<
")";
1988 out <<
" (_ bv1 " << to_width <<
")";
1989 out <<
" (_ bv0 " << to_width <<
")";
1994 else if(src_type.
id()==ID_pointer)
1998 if(from_width<to_width)
2000 out <<
"((_ sign_extend ";
2001 out << (to_width-from_width)
2008 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2013 else if(src_type.
id()==ID_integer)
2016 if(src.is_constant())
2020 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2023 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2025 else if(src_type.
id()==ID_struct)
2038 else if(src_type.
id()==ID_union)
2043 else if(src_type.
id()==ID_c_bit_field)
2047 if(from_width==to_width)
2059 "TODO typecast2 "+src_type.
id_string()+
" -> "+
2063 else if(dest_type.
id()==ID_fixedbv)
2069 if(src_type.
id()==ID_unsignedbv ||
2070 src_type.
id()==ID_signedbv ||
2071 src_type.
id()==ID_c_enum)
2078 if(from_width==to_integer_bits)
2080 else if(from_width>to_integer_bits)
2083 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2090 assert(from_width<to_integer_bits);
2091 if(dest_type.
id()==ID_unsignedbv)
2093 out <<
"(_ zero_extend " 2094 << (to_integer_bits-from_width) <<
") ";
2100 out <<
"((_ sign_extend " 2101 << (to_integer_bits-from_width) <<
") ";
2107 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2110 else if(src_type.
id()==ID_bool)
2112 out <<
"(concat (concat" 2113 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2119 else if(src_type.
id()==ID_fixedbv)
2124 std::size_t from_width=from_fixedbv_type.
get_width();
2126 out <<
"(let ((?tcop ";
2132 if(to_integer_bits<=from_integer_bits)
2134 out <<
"((_ extract " 2135 << (from_fraction_bits+to_integer_bits-1) <<
" " 2136 << from_fraction_bits
2141 assert(to_integer_bits>from_integer_bits);
2142 out <<
"((_ sign_extend " 2143 << (to_integer_bits-from_integer_bits)
2145 << (from_width-1) <<
" " 2146 << from_fraction_bits
2152 if(to_fraction_bits<=from_fraction_bits)
2154 out <<
"((_ extract " 2155 << (from_fraction_bits-1) <<
" " 2156 << (from_fraction_bits-to_fraction_bits)
2161 assert(to_fraction_bits>from_fraction_bits);
2162 out <<
"(concat ((_ extract " 2163 << (from_fraction_bits-1) <<
" 0) ";
2166 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2175 else if(dest_type.
id()==ID_pointer)
2179 if(src_type.
id()==ID_pointer)
2184 else if(src_type.
id()==ID_unsignedbv ||
2185 src_type.
id()==ID_signedbv)
2191 if(from_width==to_width)
2193 else if(from_width<to_width)
2195 out <<
"((_ sign_extend " 2196 << (to_width-from_width)
2203 out <<
"((_ extract " << to_width <<
" 0) ";
2211 else if(dest_type.
id()==ID_range)
2215 else if(dest_type.
id()==ID_floatbv)
2223 if(src_type.
id()==ID_bool)
2238 a.
build(significand, exponent);
2246 a.
build(significand, exponent);
2252 else if(src_type.
id()==ID_c_bool)
2261 else if(dest_type.
id()==ID_c_bit_field)
2266 if(from_width==to_width)
2287 if(dest_type.
id()==ID_floatbv)
2289 if(src_type.
id()==ID_floatbv)
2316 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2317 << dst.
get_f() + 1 <<
") ";
2326 else if(src_type.
id()==ID_unsignedbv)
2347 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" " 2348 << dst.
get_f() + 1 <<
") ";
2357 else if(src_type.
id()==ID_signedbv)
2365 out <<
"((_ to_fp " << dst.
get_e() <<
" " 2366 << dst.
get_f() + 1 <<
") ";
2375 else if(src_type.
id()==ID_c_enum_tag)
2391 else if(dest_type.
id()==ID_signedbv)
2396 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2405 else if(dest_type.
id()==ID_unsignedbv)
2410 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2433 assert(components.size()==expr.
operands().size());
2435 assert(!components.empty());
2440 const std::string smt_typename =
2444 out <<
"(mk-" << smt_typename;
2447 for(struct_typet::componentst::const_iterator
2448 it=components.begin();
2449 it!=components.end();
2460 if(components.size()==1)
2465 for(std::size_t i=components.size(); i>1; i--)
2482 for(std::size_t i=1; i<components.size(); i++)
2496 INVALIDEXPR(
"failed to convert array size for flattening");
2501 out <<
"(let ((?far ";
2509 out <<
"(select ?far ";
2533 INVALIDEXPR(
"failed to get union width for union");
2538 INVALIDEXPR(
"failed to get union member width for union");
2540 if(total_width==member_width)
2547 assert(total_width>member_width);
2550 << (total_width-member_width) <<
") ";
2560 if(expr_type.
id()==ID_unsignedbv ||
2561 expr_type.
id()==ID_signedbv ||
2562 expr_type.
id()==ID_bv ||
2563 expr_type.
id()==ID_c_enum ||
2564 expr_type.
id()==ID_c_enum_tag ||
2565 expr_type.
id()==ID_c_bool ||
2566 expr_type.
id()==ID_incomplete_c_enum ||
2567 expr_type.
id()==ID_c_bit_field)
2573 out <<
"(_ bv" << value
2574 <<
" " << width <<
")";
2576 else if(expr_type.
id()==ID_fixedbv)
2583 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2585 else if(expr_type.
id()==ID_floatbv)
2598 size_t e=floatbv_type.
get_e();
2599 size_t f=floatbv_type.
get_f()+1;
2605 out <<
"((_ to_fp " << e <<
" " << f <<
")" 2611 out <<
"(_ NaN " << e <<
" " << f <<
")";
2616 out <<
"(_ -oo " << e <<
" " << f <<
")";
2618 out <<
"(_ +oo " << e <<
" " << f <<
")";
2628 <<
"#b" << binaryString.substr(0, 1) <<
" " 2629 <<
"#b" << binaryString.substr(1, e) <<
" " 2630 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
2641 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
2644 else if(expr_type.
id()==ID_pointer)
2656 else if(expr_type.
id()==ID_bool)
2665 else if(expr_type.
id()==ID_array)
2671 else if(expr_type.
id()==ID_rational)
2674 size_t pos=value.find(
"/");
2676 if(
pos==std::string::npos)
2677 out << value <<
".0";
2680 out <<
"(/ " << value.substr(0,
pos) <<
".0 " 2681 << value.substr(
pos+1) <<
".0)";
2684 else if(expr_type.
id()==ID_integer)
2696 if(expr.
type().
id()==ID_unsignedbv ||
2697 expr.
type().
id()==ID_signedbv)
2699 if(expr.
type().
id()==ID_unsignedbv)
2715 std::vector<std::size_t> dynamic_objects;
2720 if(dynamic_objects.empty())
2726 out <<
"(let ((?obj ((_ extract " 2727 << pointer_width-1 <<
" " 2732 if(dynamic_objects.size()==1)
2734 out <<
"(= (_ bv" << dynamic_objects.front()
2741 for(
const auto &
object : dynamic_objects)
2742 out <<
" (= (_ bv" <<
object 2758 if(op_type.id()==ID_unsignedbv ||
2759 op_type.id()==ID_pointer ||
2760 op_type.id()==ID_bv)
2763 if(expr.
id()==ID_le)
2765 else if(expr.
id()==ID_lt)
2767 else if(expr.
id()==ID_ge)
2769 else if(expr.
id()==ID_gt)
2778 else if(op_type.id()==ID_signedbv ||
2779 op_type.id()==ID_fixedbv)
2782 if(expr.
id()==ID_le)
2784 else if(expr.
id()==ID_lt)
2786 else if(expr.
id()==ID_ge)
2788 else if(expr.
id()==ID_gt)
2797 else if(op_type.id()==ID_floatbv)
2802 if(expr.
id()==ID_le)
2804 else if(expr.
id()==ID_lt)
2806 else if(expr.
id()==ID_ge)
2808 else if(expr.
id()==ID_gt)
2820 else if(op_type.id()==ID_rational ||
2821 op_type.id()==ID_integer)
2834 "unsupported type for "+expr.
id_string()+
": "+op_type.id_string());
2849 if(expr.
type().
id()==ID_unsignedbv ||
2850 expr.
type().
id()==ID_signedbv ||
2851 expr.
type().
id()==ID_fixedbv)
2861 else if(expr.
type().
id()==ID_floatbv)
2868 else if(expr.
type().
id()==ID_pointer)
2872 if(p.
type().
id()!=ID_pointer)
2875 if(p.
type().
id()!=ID_pointer)
2876 INVALIDEXPR(
"unexpected mixture in pointer arithmetic");
2880 assert(element_size>0);
2890 out <<
" (_ bv" << element_size
2898 else if(expr.
type().
id()==ID_rational)
2906 else if(expr.
type().
id()==ID_vector)
2912 INVALIDEXPR(
"failed to convert vector size to constant");
2920 const std::string smt_typename=
2923 out <<
"(mk-" << smt_typename;
2933 tmp.copy_to_operands(
2971 if(expr.
id()==ID_constant)
2978 out <<
"roundNearestTiesToEven";
2980 out <<
"roundTowardNegative";
2982 out <<
"roundTowardPositive";
2984 out <<
"roundTowardZero";
2987 "Unknown constant rounding mode with value "+
2995 out <<
"(ite (= (_ bv0 " << width <<
") ";
2997 out <<
") roundNearestTiesToEven ";
2999 out <<
"(ite (= (_ bv1 " << width <<
") ";
3001 out <<
") roundTowardNegative ";
3003 out <<
"(ite (= (_ bv2 " << width <<
") ";
3005 out <<
") roundTowardPositive ";
3008 out <<
"roundTowardZero";
3019 assert(type.
id()==ID_floatbv ||
3020 (type.
id()==ID_complex && type.
subtype().
id()==ID_floatbv) ||
3021 (type.
id()==ID_vector && type.
subtype().
id()==ID_floatbv));
3025 if(type.
id()==ID_floatbv)
3035 else if(type.
id()==ID_complex)
3039 else if(type.
id()==ID_vector)
3054 if(expr.
type().
id()==ID_unsignedbv ||
3055 expr.
type().
id()==ID_signedbv ||
3056 expr.
type().
id()==ID_fixedbv)
3058 if(expr.
op0().
type().
id()==ID_pointer &&
3064 assert(element_size>0);
3078 out <<
" (_ bv" << element_size
3090 else if(expr.
type().
id()==ID_floatbv)
3097 else if(expr.
type().
id()==ID_pointer)
3101 else if(expr.
type().
id()==ID_vector)
3107 INVALIDEXPR(
"failed to convert vector size to constant");
3115 const std::string smt_typename=
3118 out <<
"(mk-" << smt_typename;
3128 tmp.copy_to_operands(
3147 assert(expr.
type().
id()==ID_floatbv);
3167 if(expr.
type().
id()==ID_unsignedbv ||
3168 expr.
type().
id()==ID_signedbv)
3170 if(expr.
type().
id()==ID_unsignedbv)
3180 else if(expr.
type().
id()==ID_fixedbv)
3185 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3190 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3192 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3198 else if(expr.
type().
id()==ID_floatbv)
3212 assert(expr.
type().
id()==ID_floatbv);
3245 if(expr.
type().
id()==ID_unsignedbv ||
3246 expr.
type().
id()==ID_signedbv)
3257 else if(expr.
type().
id()==ID_floatbv)
3264 else if(expr.
type().
id()==ID_fixedbv)
3269 out <<
"((_ extract " 3270 << spec.
width+fraction_bits-1 <<
" " 3271 << fraction_bits <<
") ";
3275 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3279 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3285 else if(expr.
type().
id()==ID_rational)
3304 assert(expr.
type().
id()==ID_floatbv);
3328 std::size_t s=expr.
operands().size();
3335 assert(new_with_expr.
operands().size()==3);
3337 new_with_expr.
old()=tmp;
3347 if(expr_type.
id()==ID_array)
3371 out <<
"(let ((distance? ";
3372 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3376 if(array_width>index_width)
3378 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3384 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3393 out <<
"(bvlshr (_ bv" <<
power(2, array_width)-1 <<
" " 3394 << array_width <<
") ";
3395 out <<
"distance?) ";
3399 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3401 out <<
") distance?)))";
3404 else if(expr_type.
id()==ID_struct)
3411 const irep_idt &component_name=index.
get(ID_component_name);
3414 INVALIDEXPR(
"with failed to find component in struct");
3419 const std::string smt_typename=
3422 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3436 out <<
"(let ((?withop ";
3440 if(m.
width==struct_width)
3449 <<
"((_ extract " << (struct_width-1) <<
" " 3450 << m.
width <<
") ?withop) ";
3459 out <<
"((_ extract " << (m.
offset-1) <<
" 0) ?withop))";
3464 out <<
"(concat (concat " 3465 <<
"((_ extract " << (struct_width-1) <<
" " 3468 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3475 else if(expr_type.
id()==ID_union)
3486 INVALIDEXPR(
"failed to get union width for with");
3491 INVALIDEXPR(
"failed to get union member width for with");
3493 if(total_width==member_width)
3499 assert(total_width>member_width);
3501 out <<
"((_ extract " 3503 <<
" " << member_width <<
") ";
3510 else if(expr_type.
id()==ID_bv ||
3511 expr_type.
id()==ID_unsignedbv ||
3512 expr_type.
id()==ID_signedbv)
3538 out <<
" (bvnot (bvshl";
3541 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3542 out <<
" (repeat[" << value_width <<
"] bv1[1])";
3563 "with expects struct, union, or array type, but got "+
3571 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
3580 if(array_op_type.id()==ID_array)
3609 assert(array_width!=0);
3616 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
3620 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3624 if(array_width>index_width)
3626 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3632 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3642 else if(array_op_type.id()==ID_vector)
3649 const std::string smt_typename=
3657 SMT2_TODO(
"non-constant index on vectors");
3661 out <<
"(" << smt_typename <<
"." << index_int <<
" ";
3673 "index with unsupported array type: "+array_op_type.id_string());
3681 const exprt &struct_op=member_expr.struct_op();
3683 const irep_idt &name=member_expr.get_component_name();
3685 if(struct_op_type.
id()==ID_struct)
3696 const std::string smt_typename=
3699 out <<
"(" << smt_typename <<
"." 3711 INVALIDEXPR(
"failed to get struct member offset");
3719 else if(struct_op_type.
id()==ID_union)
3728 out <<
"((_ extract " 3738 "convert_member on an unexpected type "+struct_op_type.
id_string());
3745 if(type.
id()==ID_bool)
3751 else if(type.
id()==ID_vector)
3757 const std::string smt_typename=
3765 INVALIDEXPR(
"failed to convert vector size to constant");
3767 out <<
"(let ((?vflop ";
3775 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
3783 else if(type.
id()==ID_array)
3787 else if(type.
id()==ID_struct)
3793 const std::string smt_typename=
3799 out <<
"(let ((?sflop ";
3807 for(std::size_t i=components.size(); i>1; i--)
3809 out <<
"(concat (" << smt_typename <<
"." 3810 << components[i-1].get_name() <<
" ?sflop)";
3815 out <<
"(" << smt_typename <<
"." 3816 << components[0].get_name() <<
" ?sflop)";
3818 for(std::size_t i=1; i<components.size(); i++)
3826 else if(type.
id()==ID_floatbv)
3829 INVALIDEXPR(
"need to flatten floatbv in FPA theory");
3842 if(type.
id()==ID_symbol)
3845 if(type.
id()==ID_bool)
3852 else if(type.
id()==ID_vector)
3858 const std::string smt_typename=
3868 INVALIDEXPR(
"failed to convert vector size to constant");
3871 out <<
"(let ((?ufop" << nesting <<
" ";
3876 out <<
"(mk-" << smt_typename;
3878 std::size_t offset=0;
3880 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
3884 out <<
"((_ extract " << offset+subtype_width-1 <<
" " 3885 << offset <<
") ?ufop" << nesting <<
")";
3897 else if(type.
id()==ID_struct)
3903 out <<
"(let ((?ufop" << nesting <<
" ";
3910 const std::string smt_typename=
3913 out <<
"(mk-" << smt_typename;
3920 std::size_t offset=0;
3923 for(struct_typet::componentst::const_iterator
3924 it=components.begin();
3925 it!=components.end();
3932 out <<
"((_ extract " << offset+member_width-1 <<
" " 3933 << offset <<
") ?ufop" << nesting <<
")";
3935 offset+=member_width;
3959 if(expr.
id()==ID_and && value)
3966 if(expr.
id()==ID_or && !value)
3973 if(expr.
id()==ID_not)
3981 assert(expr.
type().
id()==ID_bool);
3986 if(expr.
id()==ID_equal && value==
true)
3990 if(equal_expr.
lhs().
id()==ID_symbol)
3999 assert(
id.type.is_nil());
4001 id.type=equal_expr.
lhs().
type();
4008 out <<
"; set_to true (equal)\n";
4009 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4028 out <<
"; set_to " << (value?
"true":
"false") <<
"\n" 4054 if(expr.
id()==ID_symbol ||
4055 expr.
id()==ID_nondet_symbol)
4058 if(expr.
type().
id()==ID_code)
4063 if(expr.
id()==ID_symbol)
4066 identifier=
"nondet_"+
id2string(expr.
get(ID_identifier));
4070 if(
id.type.is_nil())
4072 id.type=expr.
type();
4077 out <<
"; find_symbols\n";
4078 out <<
"(declare-fun |" 4085 else if(expr.
id()==ID_array_of)
4090 out <<
"; the following is a substitute for lambda i. x" <<
"\n";
4091 out <<
"(declare-fun " <<
id <<
" () ";
4096 #if 0 // not really working in any solver yet! 4097 out <<
"(assert (forall ((i ";
4099 out <<
")) (= (select " <<
id <<
" i) ";
4101 out <<
")))" <<
"\n";
4107 else if(expr.
id()==ID_array)
4114 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4115 out <<
"(declare-fun " <<
id <<
" () ";
4119 for(std::size_t i=0; i<expr.
operands().size(); i++)
4121 out <<
"(assert (= (select " <<
id <<
" ";
4125 out <<
"))" <<
"\n";
4131 else if(expr.
id()==ID_string_constant)
4140 out <<
"; the following is a substitute for a string" <<
"\n";
4141 out <<
"(declare-fun " <<
id <<
" () ";
4145 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4147 out <<
"(assert (= (select " << id;
4151 out <<
"))" <<
"\n";
4157 else if(expr.
id()==ID_object_size &&
4162 if(op.
type().
id()==ID_pointer ||
4163 op.
type().
id()==ID_reference)
4168 out <<
"(declare-fun " <<
id <<
" () ";
4178 (expr.
id()==ID_floatbv_plus ||
4179 expr.
id()==ID_floatbv_minus ||
4180 expr.
id()==ID_floatbv_mult ||
4181 expr.
id()==ID_floatbv_div ||
4182 expr.
id()==ID_floatbv_typecast ||
4183 expr.
id()==ID_ieee_float_equal ||
4184 expr.
id()==ID_ieee_float_notequal ||
4185 ((expr.
id()==ID_lt ||
4189 expr.
id()==ID_isnan ||
4190 expr.
id()==ID_isnormal ||
4191 expr.
id()==ID_isfinite ||
4192 expr.
id()==ID_isinf ||
4193 expr.
id()==ID_sign ||
4194 expr.
id()==ID_unary_minus ||
4195 expr.
id()==ID_typecast ||
4196 expr.
id()==ID_abs) &&
4202 if(
bvfp_set.insert(
function).second)
4204 out <<
"; this is a model for " << expr.
id()
4207 <<
"(define-fun " <<
function <<
" (";
4209 for(
unsigned i=0; i<expr.
operands().size(); i++)
4213 out <<
"(op" << i <<
' ';
4223 for(
unsigned i=0; i<tmp1.
operands().size(); i++)
4230 assert(!tmp2.is_nil());
4241 assert(type.
id()==ID_array);
4251 if(expr.
id()==ID_with)
4253 else if(expr.
id()==ID_member)
4262 if(type.
id()==ID_array)
4275 out <<
"(_ BitVec 1)";
4281 else if(type.
id()==ID_bool)
4285 else if(type.
id()==ID_struct)
4299 out <<
"(_ BitVec " << width <<
")";
4302 else if(type.
id()==ID_vector)
4318 out <<
"(_ BitVec " << width <<
")";
4321 else if(type.
id()==ID_code)
4328 else if(type.
id()==ID_union)
4337 out <<
"(_ BitVec " << width <<
")";
4339 else if(type.
id()==ID_pointer ||
4340 type.
id()==ID_reference)
4345 else if(type.
id()==ID_bv ||
4346 type.
id()==ID_fixedbv ||
4347 type.
id()==ID_unsignedbv ||
4348 type.
id()==ID_signedbv ||
4349 type.
id()==ID_c_bool)
4354 else if(type.
id()==ID_c_enum)
4360 else if(type.
id()==ID_c_enum_tag)
4364 else if(type.
id()==ID_floatbv)
4369 out <<
"(_ FloatingPoint " 4370 << floatbv_type.
get_e() <<
" " 4371 << floatbv_type.
get_f() + 1 <<
")";
4376 else if(type.
id()==ID_rational)
4378 else if(type.
id()==ID_integer)
4380 else if(type.
id()==ID_symbol)
4382 else if(type.
id()==ID_complex)
4398 out <<
"(_ BitVec " << width <<
")";
4401 else if(type.
id()==ID_c_bit_field)
4413 std::set<irep_idt> recstack;
4419 std::set<irep_idt> &recstack)
4421 if(type.
id()==ID_array)
4427 else if(type.
id()==ID_incomplete_array)
4431 else if(type.
id()==ID_complex)
4438 std::string smt_typename =
"complex."+std::to_string(
datatype_map.size());
4441 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4442 <<
"(mk-" << smt_typename;
4444 out <<
" (" << smt_typename <<
".imag ";
4448 out <<
" (" << smt_typename <<
".real ";
4455 else if(type.
id()==ID_vector)
4466 INVALIDEXPR(
"failed to convert vector size to constant");
4468 std::string smt_typename =
"vector."+std::to_string(
datatype_map.size());
4471 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4472 <<
"(mk-" << smt_typename;
4476 out <<
" (" << smt_typename <<
"." << i <<
" ";
4484 else if(type.
id()==ID_struct)
4487 bool need_decl=
false;
4491 std::string smt_typename =
"struct."+std::to_string(
datatype_map.size());
4499 for(
const auto &component : components)
4516 out <<
"(declare-datatypes () ((" << smt_typename <<
" " 4517 <<
"(mk-" << smt_typename <<
" ";
4519 for(
const auto &component : components)
4521 out <<
"(" << smt_typename <<
"." << component.get_name()
4527 out <<
"))))" <<
"\n";
4544 for(struct_union_typet::componentst::const_iterator
4545 it=components.begin();
4546 it!=components.end();
4550 out <<
"(define-fun update-" << smt_typename <<
"." 4552 <<
"((s " << smt_typename <<
") " 4555 out <<
")) " << smt_typename <<
" " 4556 <<
"(mk-" << smt_typename
4559 for(struct_union_typet::componentst::const_iterator
4560 it2=components.begin();
4561 it2!=components.end();
4568 out <<
"(" << smt_typename <<
"." 4569 << it2->get_name() <<
" s) ";
4573 out <<
"))" <<
"\n";
4579 else if(type.
id()==ID_union)
4584 for(
const auto &component : components)
4587 else if(type.
id()==ID_code)
4591 for(
const auto ¶m : parameters)
4596 else if(type.
id()==ID_pointer)
4600 else if(type.
id()==ID_symbol)
4605 if(recstack.find(
id)==recstack.end())
4607 recstack.insert(
id);
4616 std::vector<exprt> let_order;
4625 std::vector<exprt> &let_order,
4629 if(i>=let_order.size())
4632 exprt current=let_order[i];
4633 assert(map.find(current)!=map.end());
4635 if(map.find(current)->second.first<
LET_COUNT)
4636 return letify_rec(expr, let_order, map, i+1);
4640 let.
symbol() = map.
find(current)->second.second;
4650 std::vector<exprt> &let_order)
4652 seen_expressionst::iterator it = map.find(expr);
4668 assert(map.find(expr)==map.end());
4673 map.insert(std::make_pair(expr, std::make_pair(1, let)));
4675 let_order.push_back(expr);
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
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
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
exprt size_of_expr(const typet &type, const namespacet &ns)
exprt parse_union(const irept &s, const union_typet &type)
const typet & follow(const typet &src) const
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 mp_integer string2integer(const std::string &n, unsigned base)
static ieee_floatt NaN(const ieee_float_spect &_spec)
virtual resultt dec_solve()
constant_exprt to_expr() const
Fixed-width bit-vector with IEEE floating-point interpretation.
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
const minus_exprt & to_minus_expr(const exprt &expr)
Cast a generic exprt to a minus_exprt.
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)
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
unsigned unsafe_string2unsigned(const std::string &str, int base)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
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::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
void convert_update(const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const irep_idt & get_value() const
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)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
std::unordered_map< exprt, let_count_idt, irep_hash > seen_expressionst
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
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.
exprt letify_rec(exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, unsigned i)
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)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
bool use_array_theory(const exprt &)
static const unsigned LET_COUNT
std::size_t get_invalid_object() const
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 index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const typet & follow_tag(const union_tag_typet &src) const
virtual literalt convert(const exprt &expr)
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 let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
const membert & get_member(const struct_typet &type, const irep_idt &member) const
void define_object_size(const irep_idt &id, const exprt &expr)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
virtual void print_assignment(std::ostream &out) const
The boolean constant true.
defined_expressionst object_sizes
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
division (integer and real)
A reference into the symbol table.
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::pair< unsigned, symbol_exprt > let_count_idt
typet array_index_type() const
union constructor from single element
API to expression classes.
void convert_index(const index_exprt &expr)
boolbv_widtht boolbv_width
const irep_idt & get(const irep_namet &name) const
const exprt & size() const
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
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 mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
constant_exprt parse_literal(const irept &, const typet &type)
array_exprt to_array_expr() const
convert string into array constant
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
array constructor from single element
void convert_minus(const minus_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.
bitvector_typet index_type()
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
std::string floatbv_suffix(const exprt &) const
Operator to return the address of an object.
const irep_idt & get_identifier() const
Fixed-width bit-vector with signed fixed-point interpretation.
The boolean constant false.
std::size_t get_width() const
exprt pointer_expr(const pointert &pointer, const typet &type) const
exprt float_bv(const exprt &src)
bool has_component(const irep_idt &component_name) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
unsigned no_boolean_variables
std::size_t get_f() const
literalt const_literal(bool value)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
virtual exprt get(const exprt &expr) const
void convert_byte_update(const byte_update_exprt &expr)
const string_constantt & to_string_constant(const exprt &expr)
void convert_is_dynamic_object(const exprt &expr)
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_op_exprt.
semantic type conversion from/to floating-point formats
literalt get_literal() const
Base class for all expressions.
std::set< irep_idt > bvfp_set
const exprt & struct_op() const
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Operator to update elements in structs and arrays.
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 plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
void find_symbols(const exprt &expr)
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
void convert_member(const member_exprt &expr)
exprt parse_rec(const irept &s, const typet &type)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
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)
void convert_with(const with_exprt &expr)
Expression to hold a symbol (variable)
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
std::vector< bool > boolean_assignment
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 constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
const typet & subtype() const
exprt parse_struct(const irept &s, const struct_typet &type)
#define UNEXPECTEDCASE(S)
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)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
IEEE floating-point operations.
const irept & find(const irep_namet &name) const
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)
void set_width(std::size_t width)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.