Go to the documentation of this file.
41 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
44 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
48 const std::string &_benchmark,
49 const std::string &_notes,
50 const std::string &_logic,
53 : use_FPA_theory(false),
55 use_array_of_bool(false),
59 benchmark(_benchmark),
65 no_boolean_variables(0)
129 "variable number shall be within bounds");
135 out <<
"; SMT 2" <<
"\n";
143 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
152 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
154 out <<
"(set-option :produce-models true)" <<
"\n";
160 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
170 os <<
"; assumptions\n";
192 os <<
"(get-value (|" <<
id <<
"|))"
200 os <<
"; end of SMT2 file"
212 std::size_t number = 0;
213 std::size_t h=pointer_width-1;
218 const typet &type = o.type();
221 numeric_cast<mp_integer>(size_expr.value_or(
nil_exprt()));
224 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
225 !size_expr.has_value() || !
object_size.has_value())
231 out <<
"(assert (implies (= " <<
232 "((_ extract " << h <<
" " << l <<
") ";
235 <<
"(= " <<
id <<
" (_ bv" << *
object_size <<
" " << size_width
251 if(expr.
id()==ID_symbol)
258 return it->second.value;
260 else if(expr.
id()==ID_nondet_symbol)
267 return it->second.value;
269 else if(expr.
id()==ID_member)
277 else if(expr.
id() == ID_literal)
285 else if(expr.
id() == ID_not)
290 else if(op.is_false())
326 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
331 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
342 else if(src.
get_sub().size()==2 &&
347 else if(src.
get_sub().size()==3 &&
350 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
354 else if(src.
get_sub().size()==4 &&
357 if(type.
id()==ID_floatbv)
366 const auto s1_int = numeric_cast_v<mp_integer>(
s1);
367 const auto s2_int = numeric_cast_v<mp_integer>(
s2);
368 const auto s3_int = numeric_cast_v<mp_integer>(s3);
372 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
378 else if(src.
get_sub().size()==4 &&
386 else if(src.
get_sub().size()==4 &&
394 else if(src.
get_sub().size()==4 &&
403 if(type.
id()==ID_signedbv ||
404 type.
id()==ID_unsignedbv ||
405 type.
id()==ID_c_enum ||
406 type.
id()==ID_c_bool)
410 else if(type.
id()==ID_c_enum_tag)
416 result.
type() = type;
419 else if(type.
id()==ID_fixedbv ||
420 type.
id()==ID_floatbv)
425 else if(type.
id()==ID_integer ||
433 "smt2_convt::parse_literal should not be of unsupported type " +
453 else if(src.
get_sub().size()==2 &&
454 src.
get_sub()[0].get_sub().size()==3 &&
455 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
456 src.
get_sub()[0].get_sub()[1].id()==
"const")
490 if(components.empty())
498 if(src.
get_sub().size()!=components.size()+1)
501 for(std::size_t i=0; i<components.size(); i++)
518 std::size_t offset=0;
520 for(std::size_t i=0; i<components.size(); i++)
522 std::size_t component_width=
boolbv_width(components[i].type());
525 offset + component_width <= total_width,
526 "struct component bits shall be within struct bit vector");
528 std::string component_binary=
530 total_width-offset-component_width, component_width);
535 offset+=component_width;
545 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
546 type.
id() == ID_integer || type.
id() == ID_rational ||
547 type.
id() == ID_real || type.
id() == ID_c_enum ||
548 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
549 type.
id() == ID_floatbv)
553 else if(type.
id()==ID_bool)
555 if(src.
id()==ID_1 || src.
id()==ID_true)
557 else if(src.
id()==ID_0 || src.
id()==ID_false)
560 else if(type.
id()==ID_pointer)
566 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
571 ptr.
object = numeric_cast_v<std::size_t>(v / pow);
575 else if(type.
id()==ID_struct)
579 else if(type.
id() == ID_struct_tag)
584 struct_expr.type() = type;
585 return std::move(struct_expr);
587 else if(type.
id()==ID_union)
591 else if(type.
id() == ID_union_tag)
595 union_expr.type() = type;
598 else if(type.
id()==ID_array)
610 if(expr.
id()==ID_symbol ||
611 expr.
id()==ID_constant ||
612 expr.
id()==ID_string_constant ||
622 else if(expr.
id()==ID_index)
631 if(array.
type().
id()==ID_pointer)
633 else if(array.
type().
id()==ID_array)
653 else if(expr.
id()==ID_member)
658 const typet &struct_op_type = struct_op.
type();
661 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
662 "member expression operand shall have struct type");
679 else if(expr.
id()==ID_if)
694 "operand of address of expression should not be of kind " +
708 else if(expr.
id()==ID_literal)
720 out <<
"; convert\n";
721 out <<
"(define-fun ";
733 if(expr.
type().
id() != ID_bool)
784 for(std::size_t i=0; i<identifier.
size(); i++)
786 char ch=identifier[i];
809 if(type.
id()==ID_floatbv)
814 else if(type.
id()==ID_unsignedbv)
818 else if(type.
id()==ID_c_bool)
822 else if(type.
id()==ID_signedbv)
826 else if(type.
id()==ID_bool)
830 else if(type.
id()==ID_c_enum_tag)
834 else if(type.
id() == ID_pointer)
855 if(expr.
id()==ID_symbol)
862 if(expr.
id()==ID_smt2_symbol)
870 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
872 out <<
"(|float_bv." << expr.
id()
888 if(expr.
id()==ID_symbol)
894 else if(expr.
id()==ID_nondet_symbol)
897 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
900 else if(expr.
id()==ID_smt2_symbol)
906 else if(expr.
id()==ID_typecast)
910 else if(expr.
id()==ID_floatbv_typecast)
914 else if(expr.
id()==ID_struct)
918 else if(expr.
id()==ID_union)
922 else if(expr.
id()==ID_constant)
926 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
930 "concatenation over a single operand should have matching types",
935 else if(expr.
id()==ID_concatenation ||
936 expr.
id()==ID_bitand ||
937 expr.
id()==ID_bitor ||
938 expr.
id()==ID_bitxor ||
939 expr.
id()==ID_bitnand ||
940 expr.
id()==ID_bitnor)
944 "given expression should have at least two operands",
949 if(expr.
id()==ID_concatenation)
951 else if(expr.
id()==ID_bitand)
953 else if(expr.
id()==ID_bitor)
955 else if(expr.
id()==ID_bitxor)
957 else if(expr.
id()==ID_bitnand)
959 else if(expr.
id()==ID_bitnor)
970 else if(expr.
id()==ID_bitnot)
974 if(bitnot_expr.
type().
id() == ID_vector)
985 out <<
"(let ((?vectorop ";
989 out <<
"(mk-" << smt_typename;
996 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
1012 else if(expr.
id()==ID_unary_minus)
1017 unary_minus_expr.
type().
id() == ID_rational ||
1018 unary_minus_expr.
type().
id() == ID_integer ||
1019 unary_minus_expr.
type().
id() == ID_real)
1025 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1037 else if(unary_minus_expr.
type().
id() == ID_vector)
1041 const std::string &smt_typename =
1048 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1050 out <<
"(let ((?vectorop ";
1054 out <<
"(mk-" << smt_typename;
1061 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1077 else if(expr.
id()==ID_unary_plus)
1082 else if(expr.
id()==ID_sign)
1088 if(op_type.
id()==ID_floatbv)
1092 out <<
"(fp.isNegative ";
1099 else if(op_type.
id()==ID_signedbv)
1105 out <<
" (_ bv0 " << op_width <<
"))";
1110 "sign should not be applied to unsupported type",
1113 else if(expr.
id()==ID_if)
1125 else if(expr.
id()==ID_and ||
1130 expr.
type().
id() == ID_bool,
1131 "logical and, or, and xor expressions should have Boolean type");
1134 "logical and, or, and xor expressions should have at least two operands");
1136 out <<
"(" << expr.
id();
1144 else if(expr.
id()==ID_implies)
1149 implies_expr.
type().
id() == ID_bool,
1150 "implies expression should have Boolean type");
1158 else if(expr.
id()==ID_not)
1163 not_expr.
type().
id() == ID_bool,
1164 "not expression should have Boolean type");
1170 else if(expr.
id() == ID_equal)
1176 "operands of equal expression shall have same type");
1184 else if(expr.
id() == ID_notequal)
1190 "operands of not equal expression shall have same type");
1198 else if(expr.
id()==ID_ieee_float_equal ||
1199 expr.
id()==ID_ieee_float_notequal)
1206 rel_expr.lhs().type() == rel_expr.rhs().type(),
1207 "operands of float equal and not equal expressions shall have same type");
1212 if(rel_expr.id() == ID_ieee_float_notequal)
1221 if(rel_expr.id() == ID_ieee_float_notequal)
1227 else if(expr.
id()==ID_le ||
1234 else if(expr.
id()==ID_plus)
1238 else if(expr.
id()==ID_floatbv_plus)
1242 else if(expr.
id()==ID_minus)
1246 else if(expr.
id()==ID_floatbv_minus)
1250 else if(expr.
id()==ID_div)
1254 else if(expr.
id()==ID_floatbv_div)
1258 else if(expr.
id()==ID_mod)
1262 else if(expr.
id()==ID_mult)
1266 else if(expr.
id()==ID_floatbv_mult)
1270 else if(expr.
id()==ID_address_of)
1276 else if(expr.
id()==ID_array_of)
1281 array_of_expr.
type().
id() == ID_array,
1282 "array of expression shall have array type");
1284 defined_expressionst::const_iterator it =
1289 else if(expr.
id()==ID_index)
1293 else if(expr.
id()==ID_ashr ||
1294 expr.
id()==ID_lshr ||
1300 if(type.
id()==ID_unsignedbv ||
1301 type.
id()==ID_signedbv ||
1304 if(shift_expr.
id() == ID_ashr)
1306 else if(shift_expr.
id() == ID_lshr)
1308 else if(shift_expr.
id() == ID_shl)
1338 if(width_op0==width_op1)
1340 else if(width_op0>width_op1)
1342 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1348 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1355 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1362 "unsupported type for " + shift_expr.
id_string() +
": " +
1365 else if(expr.
id()==ID_with)
1369 else if(expr.
id()==ID_update)
1373 else if(expr.
id()==ID_member)
1377 else if(expr.
id()==ID_pointer_offset)
1382 op.type().id() == ID_pointer,
1383 "operand of pointer offset expression shall be of pointer type");
1385 std::size_t offset_bits =
1390 if(offset_bits>result_width)
1391 offset_bits=result_width;
1394 if(result_width>offset_bits)
1395 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1397 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1401 if(result_width>offset_bits)
1404 else if(expr.
id()==ID_pointer_object)
1409 op.type().id() == ID_pointer,
1410 "pointer object expressions should be of pointer type");
1416 out <<
"((_ zero_extend " << ext <<
") ";
1418 out <<
"((_ extract "
1419 << pointer_width-1 <<
" "
1427 else if(expr.
id() == ID_is_dynamic_object)
1431 else if(expr.
id() == ID_is_invalid_pointer)
1435 out <<
"(= ((_ extract "
1436 << pointer_width-1 <<
" "
1442 else if(expr.
id()==ID_string_constant)
1448 else if(expr.
id()==ID_extractbit)
1457 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1463 out <<
"(= ((_ extract 0 0) ";
1472 else if(expr.
id()==ID_extractbits)
1486 std::swap(op1_i, op2_i);
1490 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1497 out <<
"(= ((_ extract 0 0) ";
1506 SMT2_TODO(
"smt2: extractbits with non-constant index");
1509 else if(expr.
id()==ID_replication)
1513 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1515 out <<
"((_ repeat " << times <<
") ";
1519 else if(expr.
id()==ID_byte_extract_little_endian ||
1520 expr.
id()==ID_byte_extract_big_endian)
1523 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1525 else if(expr.
id()==ID_byte_update_little_endian ||
1526 expr.
id()==ID_byte_update_big_endian)
1529 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1531 else if(expr.
id()==ID_width)
1539 out <<
"(_ bv" << op_width/8
1540 <<
" " << result_width <<
")";
1542 else if(expr.
id()==ID_abs)
1548 if(type.
id()==ID_signedbv)
1552 out <<
"(ite (bvslt ";
1554 out <<
" (_ bv0 " << result_width <<
")) ";
1561 else if(type.
id()==ID_fixedbv)
1565 out <<
"(ite (bvslt ";
1567 out <<
" (_ bv0 " << result_width <<
")) ";
1574 else if(type.
id()==ID_floatbv)
1588 else if(expr.
id()==ID_isnan)
1594 if(op_type.
id()==ID_fixedbv)
1596 else if(op_type.
id()==ID_floatbv)
1600 out <<
"(fp.isNaN ";
1610 else if(expr.
id()==ID_isfinite)
1616 if(op_type.
id()==ID_fixedbv)
1618 else if(op_type.
id()==ID_floatbv)
1624 out <<
"(not (fp.isNaN ";
1628 out <<
"(not (fp.isInf ";
1640 else if(expr.
id()==ID_isinf)
1646 if(op_type.
id()==ID_fixedbv)
1648 else if(op_type.
id()==ID_floatbv)
1652 out <<
"(fp.isInfinite ";
1662 else if(expr.
id()==ID_isnormal)
1668 if(op_type.
id()==ID_fixedbv)
1670 else if(op_type.
id()==ID_floatbv)
1674 out <<
"(fp.isNormal ";
1684 else if(expr.
id()==ID_overflow_plus ||
1685 expr.
id()==ID_overflow_minus)
1691 expr.
type().
id() == ID_bool,
1692 "overflow plus and overflow minus expressions shall be of Boolean type");
1694 bool subtract=expr.
id()==ID_overflow_minus;
1695 const typet &op_type = op0.type();
1698 if(op_type.
id()==ID_signedbv)
1701 out <<
"(let ((?sum (";
1702 out << (subtract?
"bvsub":
"bvadd");
1703 out <<
" ((_ sign_extend 1) ";
1706 out <<
" ((_ sign_extend 1) ";
1710 "((_ extract " << width <<
" " << width <<
") ?sum) "
1711 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1714 else if(op_type.
id()==ID_unsignedbv ||
1715 op_type.
id()==ID_pointer)
1719 out <<
"((_ extract " << width <<
" " << width <<
") ";
1720 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1721 out <<
" ((_ zero_extend 1) ";
1724 out <<
" ((_ zero_extend 1) ";
1732 "overflow check should not be performed on unsupported type",
1735 else if(expr.
id()==ID_overflow_mult)
1741 expr.
type().
id() == ID_bool,
1742 "overflow mult expression shall be of Boolean type");
1747 const typet &op_type = op0.type();
1750 if(op_type.
id()==ID_signedbv)
1752 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1754 out <<
") ((_ sign_extend " << width <<
") ";
1757 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
1759 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" "
1760 << width*2 <<
")))))";
1762 else if(op_type.
id()==ID_unsignedbv)
1764 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1766 out <<
") ((_ zero_extend " << width <<
") ";
1768 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1773 "overflow check should not be performed on unsupported type",
1776 else if(expr.
id()==ID_array)
1782 else if(expr.
id()==ID_literal)
1786 else if(expr.
id()==ID_forall ||
1787 expr.
id()==ID_exists)
1793 throw "MathSAT does not support quantifiers";
1795 if(quantifier_expr.
id() == ID_forall)
1797 else if(quantifier_expr.
id() == ID_exists)
1812 else if(expr.
id()==ID_vector)
1817 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1820 size == vector_expr.
operands().size(),
1821 "size indicated by type shall be equal to the number of operands");
1825 const std::string &smt_typename =
datatype_map.at(vector_type);
1827 out <<
"(mk-" << smt_typename;
1841 else if(expr.
id()==ID_object_size)
1845 else if(expr.
id()==ID_let)
1848 const auto &variables = let_expr.
variables();
1849 const auto &values = let_expr.
values();
1854 for(
auto &binding :
make_range(variables).zip(values))
1873 else if(expr.
id()==ID_constraint_select_one)
1876 "smt2_convt::convert_expr: '" + expr.
id_string() +
1877 "' is not yet supported");
1879 else if(expr.
id() == ID_bswap)
1885 "operand of byte swap expression shall have same type as the expression");
1888 out <<
"(let ((bswap_op ";
1893 bswap_expr.
type().
id() == ID_signedbv ||
1894 bswap_expr.
type().
id() == ID_unsignedbv)
1896 const std::size_t width =
1903 width % bits_per_byte == 0,
1904 "bit width indicated by type of bswap expression should be a multiple "
1905 "of the number of bits per byte");
1907 const std::size_t bytes = width / bits_per_byte;
1916 for(std::size_t
byte = 0;
byte < bytes;
byte++)
1920 out <<
"(bswap_byte_" <<
byte <<
' ';
1921 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
1922 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
1931 for(std::size_t
byte = 0;
byte < bytes;
byte++)
1932 out <<
" bswap_byte_" <<
byte;
1943 else if(expr.
id() == ID_popcount)
1951 "smt2_convt::convert_expr should not be applied to unsupported type",
1960 if(dest_type.
id()==ID_c_enum_tag)
1964 if(src_type.
id()==ID_c_enum_tag)
1967 if(dest_type.
id()==ID_bool)
1970 if(src_type.
id()==ID_signedbv ||
1971 src_type.
id()==ID_unsignedbv ||
1972 src_type.
id()==ID_c_bool ||
1973 src_type.
id()==ID_fixedbv ||
1974 src_type.
id()==ID_pointer ||
1975 src_type.
id()==ID_integer)
1983 else if(src_type.
id()==ID_floatbv)
1987 out <<
"(not (fp.isZero ";
1999 else if(dest_type.
id()==ID_c_bool)
2008 out <<
" (_ bv1 " << to_width <<
")";
2009 out <<
" (_ bv0 " << to_width <<
")";
2012 else if(dest_type.
id()==ID_signedbv ||
2013 dest_type.
id()==ID_unsignedbv ||
2014 dest_type.
id()==ID_c_enum ||
2015 dest_type.
id()==ID_bv)
2019 if(src_type.
id()==ID_signedbv ||
2020 src_type.
id()==ID_unsignedbv ||
2021 src_type.
id()==ID_c_bool ||
2022 src_type.
id()==ID_c_enum ||
2023 src_type.
id()==ID_bv)
2027 if(from_width==to_width)
2029 else if(from_width<to_width)
2031 if(src_type.
id()==ID_signedbv)
2032 out <<
"((_ sign_extend ";
2034 out <<
"((_ zero_extend ";
2036 out << (to_width-from_width)
2043 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2048 else if(src_type.
id()==ID_fixedbv)
2052 std::size_t from_width=fixedbv_type.
get_width();
2059 out <<
"(let ((?tcop ";
2065 if(to_width>from_integer_bits)
2067 out <<
"((_ sign_extend "
2068 << (to_width-from_integer_bits) <<
") ";
2069 out <<
"((_ extract " << (from_width-1) <<
" "
2070 << from_fraction_bits <<
") ";
2076 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2077 <<
" " << from_fraction_bits <<
") ";
2082 out <<
" (ite (and ";
2085 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2086 "(_ bv0 " << from_fraction_bits <<
")))";
2089 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2094 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2098 else if(src_type.
id()==ID_floatbv)
2100 if(dest_type.
id()==ID_bv)
2117 else if(dest_type.
id()==ID_signedbv)
2121 "typecast unexpected "+src_type.
id_string()+
" -> "+
2124 else if(dest_type.
id()==ID_unsignedbv)
2128 "typecast unexpected "+src_type.
id_string()+
" -> "+
2132 else if(src_type.
id()==ID_bool)
2137 if(dest_type.
id()==ID_fixedbv)
2140 out <<
" (concat (_ bv1 "
2143 "(_ bv0 " << spec.
width <<
")";
2147 out <<
" (_ bv1 " << to_width <<
")";
2148 out <<
" (_ bv0 " << to_width <<
")";
2153 else if(src_type.
id()==ID_pointer)
2157 if(from_width<to_width)
2159 out <<
"((_ sign_extend ";
2160 out << (to_width-from_width)
2167 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2172 else if(src_type.
id()==ID_integer)
2178 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2181 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2184 src_type.
id() == ID_struct ||
2185 src_type.
id() == ID_struct_tag)
2191 "bit vector with of source and destination type shall be equal");
2198 "bit vector with of source and destination type shall be equal");
2203 src_type.
id() == ID_union ||
2204 src_type.
id() == ID_union_tag)
2208 "bit vector with of source and destination type shall be equal");
2211 else if(src_type.
id()==ID_c_bit_field)
2215 if(from_width==to_width)
2226 std::ostringstream e_str;
2227 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2228 <<
" src == " <<
format(src);
2232 else if(dest_type.
id()==ID_fixedbv)
2238 if(src_type.
id()==ID_unsignedbv ||
2239 src_type.
id()==ID_signedbv ||
2240 src_type.
id()==ID_c_enum)
2247 if(from_width==to_integer_bits)
2249 else if(from_width>to_integer_bits)
2252 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2260 from_width < to_integer_bits,
2261 "from_width should be smaller than to_integer_bits as other case "
2262 "have been handled above");
2263 if(dest_type.
id()==ID_unsignedbv)
2265 out <<
"(_ zero_extend "
2266 << (to_integer_bits-from_width) <<
") ";
2272 out <<
"((_ sign_extend "
2273 << (to_integer_bits-from_width) <<
") ";
2279 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2282 else if(src_type.
id()==ID_bool)
2284 out <<
"(concat (concat"
2285 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2291 else if(src_type.
id()==ID_fixedbv)
2296 std::size_t from_width=from_fixedbv_type.
get_width();
2298 out <<
"(let ((?tcop ";
2304 if(to_integer_bits<=from_integer_bits)
2306 out <<
"((_ extract "
2307 << (from_fraction_bits+to_integer_bits-1) <<
" "
2308 << from_fraction_bits
2314 to_integer_bits > from_integer_bits,
2315 "to_integer_bits should be greater than from_integer_bits as the"
2316 "other case has been handled above");
2317 out <<
"((_ sign_extend "
2318 << (to_integer_bits-from_integer_bits)
2320 << (from_width-1) <<
" "
2321 << from_fraction_bits
2327 if(to_fraction_bits<=from_fraction_bits)
2329 out <<
"((_ extract "
2330 << (from_fraction_bits-1) <<
" "
2331 << (from_fraction_bits-to_fraction_bits)
2337 to_fraction_bits > from_fraction_bits,
2338 "to_fraction_bits should be greater than from_fraction_bits as the"
2339 "other case has been handled above");
2340 out <<
"(concat ((_ extract "
2341 << (from_fraction_bits-1) <<
" 0) ";
2344 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2353 else if(dest_type.
id()==ID_pointer)
2357 if(src_type.
id()==ID_pointer)
2363 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2364 src_type.
id() == ID_bv)
2370 if(from_width==to_width)
2372 else if(from_width<to_width)
2374 out <<
"((_ sign_extend "
2375 << (to_width-from_width)
2382 out <<
"((_ extract " << to_width <<
" 0) ";
2390 else if(dest_type.
id()==ID_range)
2394 else if(dest_type.
id()==ID_floatbv)
2403 if(src_type.
id()==ID_bool)
2418 a.
build(significand, exponent);
2426 a.
build(significand, exponent);
2432 else if(src_type.
id()==ID_c_bool)
2438 else if(src_type.
id() == ID_bv)
2447 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2448 << dest_floatbv_type.get_f() + 1 <<
") ";
2458 else if(dest_type.
id()==ID_integer)
2460 if(src_type.
id()==ID_bool)
2469 else if(dest_type.
id()==ID_c_bit_field)
2474 if(from_width==to_width)
2495 if(dest_type.
id()==ID_floatbv)
2497 if(src_type.
id()==ID_floatbv)
2524 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2525 << dst.
get_f() + 1 <<
") ";
2534 else if(src_type.
id()==ID_unsignedbv)
2555 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
2556 << dst.
get_f() + 1 <<
") ";
2565 else if(src_type.
id()==ID_signedbv)
2573 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2574 << dst.
get_f() + 1 <<
") ";
2583 else if(src_type.
id()==ID_c_enum_tag)
2599 else if(dest_type.
id()==ID_signedbv)
2604 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2613 else if(dest_type.
id()==ID_unsignedbv)
2618 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2642 components.size() == expr.
operands().size(),
2643 "number of struct components as indicated by the struct type shall be equal"
2644 "to the number of operands of the struct expression");
2646 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2650 const std::string &smt_typename =
datatype_map.at(struct_type);
2653 out <<
"(mk-" << smt_typename;
2656 for(struct_typet::componentst::const_iterator
2657 it=components.begin();
2658 it!=components.end();
2669 if(components.size()==1)
2674 for(std::size_t i=components.size(); i>1; i--)
2681 if(op.
type().
id() == ID_array)
2691 for(std::size_t i=1; i<components.size(); i++)
2701 const auto &size_expr = array_type.
size();
2707 out <<
"(let ((?far ";
2715 out <<
"(select ?far ";
2736 total_width != 0,
"failed to get union width for union");
2740 member_width != 0,
"failed to get union member width for union");
2742 if(total_width==member_width)
2750 total_width > member_width,
2751 "total_width should be greater than member_width as member_width can be"
2752 "at most as large as total_width and the other case has been handled "
2756 << (total_width-member_width) <<
") ";
2766 if(expr_type.
id()==ID_unsignedbv ||
2767 expr_type.
id()==ID_signedbv ||
2768 expr_type.
id()==ID_bv ||
2769 expr_type.
id()==ID_c_enum ||
2770 expr_type.
id()==ID_c_enum_tag ||
2771 expr_type.
id()==ID_c_bool ||
2772 expr_type.
id()==ID_c_bit_field)
2778 out <<
"(_ bv" << value
2779 <<
" " << width <<
")";
2781 else if(expr_type.
id()==ID_fixedbv)
2787 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2789 else if(expr_type.
id()==ID_floatbv)
2802 size_t e=floatbv_type.
get_e();
2803 size_t f=floatbv_type.
get_f()+1;
2809 out <<
"((_ to_fp " << e <<
" " << f <<
")"
2815 out <<
"(_ NaN " << e <<
" " << f <<
")";
2820 out <<
"(_ -oo " << e <<
" " << f <<
")";
2822 out <<
"(_ +oo " << e <<
" " << f <<
")";
2832 <<
"#b" << binaryString.substr(0, 1) <<
" "
2833 <<
"#b" << binaryString.substr(1, e) <<
" "
2834 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
2842 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
2845 else if(expr_type.
id()==ID_pointer)
2857 else if(expr_type.
id()==ID_bool)
2866 else if(expr_type.
id()==ID_array)
2872 else if(expr_type.
id()==ID_rational)
2875 size_t pos=value.find(
"/");
2877 if(
pos==std::string::npos)
2878 out << value <<
".0";
2881 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
2882 << value.substr(
pos+1) <<
".0)";
2885 else if(expr_type.
id()==ID_integer)
2895 if(expr.
type().
id()==ID_unsignedbv ||
2896 expr.
type().
id()==ID_signedbv)
2898 if(expr.
type().
id()==ID_unsignedbv)
2914 std::vector<std::size_t> dynamic_objects;
2917 if(dynamic_objects.empty())
2923 out <<
"(let ((?obj ((_ extract "
2924 << pointer_width-1 <<
" "
2929 if(dynamic_objects.size()==1)
2931 out <<
"(= (_ bv" << dynamic_objects.front()
2938 for(
const auto &
object : dynamic_objects)
2939 out <<
" (= (_ bv" <<
object
2953 if(op_type.
id()==ID_unsignedbv ||
2954 op_type.
id()==ID_pointer ||
2955 op_type.
id()==ID_bv)
2958 if(expr.
id()==ID_le)
2960 else if(expr.
id()==ID_lt)
2962 else if(expr.
id()==ID_ge)
2964 else if(expr.
id()==ID_gt)
2973 else if(op_type.
id()==ID_signedbv ||
2974 op_type.
id()==ID_fixedbv)
2977 if(expr.
id()==ID_le)
2979 else if(expr.
id()==ID_lt)
2981 else if(expr.
id()==ID_ge)
2983 else if(expr.
id()==ID_gt)
2992 else if(op_type.
id()==ID_floatbv)
2997 if(expr.
id()==ID_le)
2999 else if(expr.
id()==ID_lt)
3001 else if(expr.
id()==ID_ge)
3003 else if(expr.
id()==ID_gt)
3015 else if(op_type.
id()==ID_rational ||
3016 op_type.
id()==ID_integer)
3035 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3036 expr.
type().
id() == ID_real)
3041 for(
const auto &op : expr.
operands())
3050 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3051 expr.
type().
id() == ID_fixedbv)
3068 else if(expr.
type().
id() == ID_floatbv)
3075 else if(expr.
type().
id() == ID_pointer)
3081 if(p.
type().
id() != ID_pointer)
3085 p.
type().
id() == ID_pointer,
3086 "one of the operands should have pointer type");
3089 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3095 if(*element_size >= 2)
3112 else if(expr.
type().
id() == ID_vector)
3116 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3122 const std::string &smt_typename =
datatype_map.at(vector_type);
3124 out <<
"(mk-" << smt_typename;
3133 summands.reserve(expr.
operands().size());
3134 for(
const auto &op : expr.
operands())
3167 if(expr.
id()==ID_constant)
3171 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3174 out <<
"roundNearestTiesToEven";
3176 out <<
"roundTowardNegative";
3178 out <<
"roundTowardPositive";
3180 out <<
"roundTowardZero";
3184 "Rounding mode should have value 0, 1, 2, or 3",
3192 out <<
"(ite (= (_ bv0 " << width <<
") ";
3194 out <<
") roundNearestTiesToEven ";
3196 out <<
"(ite (= (_ bv1 " << width <<
") ";
3198 out <<
") roundTowardNegative ";
3200 out <<
"(ite (= (_ bv2 " << width <<
") ";
3202 out <<
") roundTowardPositive ";
3205 out <<
"roundTowardZero";
3216 type.
id() == ID_floatbv ||
3217 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv) ||
3218 (type.
id() == ID_vector && type.
subtype().
id() == ID_floatbv));
3222 if(type.
id()==ID_floatbv)
3232 else if(type.
id()==ID_complex)
3236 else if(type.
id()==ID_vector)
3243 "type should not be one of the unsupported types",
3252 if(expr.
type().
id()==ID_integer)
3260 else if(expr.
type().
id()==ID_unsignedbv ||
3261 expr.
type().
id()==ID_signedbv ||
3262 expr.
type().
id()==ID_fixedbv)
3264 if(expr.
op0().
type().
id()==ID_pointer &&
3269 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3271 if(*element_size >= 2)
3276 "bitvector width of operand shall be equal to the bitvector width of "
3285 if(*element_size >= 2)
3298 else if(expr.
type().
id()==ID_floatbv)
3305 else if(expr.
type().
id()==ID_pointer)
3309 else if(expr.
type().
id()==ID_vector)
3313 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3319 const std::string &smt_typename =
datatype_map.at(vector_type);
3321 out <<
"(mk-" << smt_typename;
3350 expr.
type().
id() == ID_floatbv,
3351 "type of ieee floating point expression shall be floatbv");
3369 if(expr.
type().
id()==ID_unsignedbv ||
3370 expr.
type().
id()==ID_signedbv)
3372 if(expr.
type().
id()==ID_unsignedbv)
3382 else if(expr.
type().
id()==ID_fixedbv)
3387 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3392 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3394 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3400 else if(expr.
type().
id()==ID_floatbv)
3414 expr.
type().
id() == ID_floatbv,
3415 "type of ieee floating point expression shall be floatbv");
3446 "expression should have been converted to a variant with two operands");
3448 if(expr.
type().
id()==ID_unsignedbv ||
3449 expr.
type().
id()==ID_signedbv)
3460 else if(expr.
type().
id()==ID_floatbv)
3467 else if(expr.
type().
id()==ID_fixedbv)
3472 out <<
"((_ extract "
3473 << spec.
width+fraction_bits-1 <<
" "
3474 << fraction_bits <<
") ";
3478 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3482 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3488 else if(expr.
type().
id()==ID_rational ||
3489 expr.
type().
id()==ID_integer ||
3490 expr.
type().
id()==ID_real)
3509 expr.
type().
id() == ID_floatbv,
3510 "type of ieee floating point expression shall be floatbv");
3532 std::size_t s=expr.
operands().size();
3547 "with expression should have been converted to a version with three "
3552 if(expr_type.
id()==ID_array)
3576 out <<
"(let ((distance? ";
3577 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3581 if(array_width>index_width)
3583 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3589 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3599 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
3601 out <<
"distance?)) ";
3605 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3607 out <<
") distance?)))";
3610 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
3617 const irep_idt &component_name=index.
get(ID_component_name);
3621 "struct should have accessed component");
3625 const std::string &smt_typename =
datatype_map.at(expr_type);
3627 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3641 out <<
"(let ((?withop ";
3645 if(m.
width==struct_width)
3655 <<
"((_ extract " << (struct_width-1) <<
" "
3656 << m.
width <<
") ?withop) ";
3665 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
3670 out <<
"(concat (concat "
3671 <<
"((_ extract " << (struct_width-1) <<
" "
3674 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3681 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
3689 total_width != 0,
"failed to get union width for with");
3693 member_width != 0,
"failed to get union member width for with");
3695 if(total_width==member_width)
3702 total_width > member_width,
3703 "total width should be greater than member_width as member_width is at "
3704 "most as large as total_width and the other case has been handled "
3707 out <<
"((_ extract "
3709 <<
" " << member_width <<
") ";
3716 else if(expr_type.
id()==ID_bv ||
3717 expr_type.
id()==ID_unsignedbv ||
3718 expr_type.
id()==ID_signedbv)
3724 total_width != 0,
"failed to get total width");
3731 value_width != 0,
"failed to get value width");
3743 out <<
" (bvnot (bvshl";
3746 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3747 out <<
" (repeat[" << value_width <<
"] bv1[1])";
3769 "with expects struct, union, or array type, but got "+
3777 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
3784 if(array_op_type.
id()==ID_array)
3820 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
3824 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3828 if(array_width>index_width)
3830 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3836 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3846 else if(array_op_type.
id()==ID_vector)
3852 const std::string &smt_typename =
datatype_map.at(vector_type);
3856 const auto index_int = numeric_cast<mp_integer>(expr.
index());
3857 if(!index_int.has_value())
3859 SMT2_TODO(
"non-constant index on vectors");
3863 out <<
"(" << smt_typename <<
"." << *index_int <<
" ";
3875 false,
"index with unsupported array type: " + array_op_type.
id_string());
3882 const typet &struct_op_type = struct_op.
type();
3885 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
3890 struct_type.
has_component(name),
"struct should have accessed component");
3894 const std::string &smt_typename =
datatype_map.at(struct_type);
3896 out <<
"(" << smt_typename <<
"."
3909 member_offset.has_value(),
"failed to get struct member offset");
3918 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
3922 width != 0,
"failed to get union member width");
3926 out <<
"((_ extract "
3936 "convert_member on an unexpected type "+struct_op_type.
id_string());
3943 if(type.
id()==ID_bool)
3949 else if(type.
id()==ID_vector)
3953 const std::string &smt_typename =
datatype_map.at(type);
3958 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3960 out <<
"(let ((?vflop ";
3968 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
3976 else if(type.
id()==ID_array)
3980 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
3984 const std::string &smt_typename =
datatype_map.at(type);
3989 out <<
"(let ((?sflop ";
3997 for(std::size_t i=components.size(); i>1; i--)
3999 out <<
"(concat (" << smt_typename <<
"."
4000 << components[i-1].get_name() <<
" ?sflop)";
4005 out <<
"(" << smt_typename <<
"."
4006 << components[0].get_name() <<
" ?sflop)";
4008 for(std::size_t i=1; i<components.size(); i++)
4016 else if(type.
id()==ID_floatbv)
4020 "floatbv expressions should be flattened when using FPA theory");
4033 if(type.
id()==ID_bool)
4040 else if(type.
id()==ID_vector)
4044 const std::string &smt_typename =
datatype_map.at(type);
4051 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4054 out <<
"(let ((?ufop" << nesting <<
" ";
4059 out <<
"(mk-" << smt_typename;
4061 std::size_t offset=0;
4063 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4067 out <<
"((_ extract " << offset+subtype_width-1 <<
" "
4068 << offset <<
") ?ufop" << nesting <<
")";
4080 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4086 out <<
"(let ((?ufop" << nesting <<
" ";
4091 const std::string &smt_typename =
datatype_map.at(type);
4093 out <<
"(mk-" << smt_typename;
4100 std::size_t offset=0;
4103 for(struct_typet::componentst::const_iterator
4104 it=components.begin();
4105 it!=components.end();
4112 out <<
"((_ extract " << offset+member_width-1 <<
" "
4113 << offset <<
") ?ufop" << nesting <<
")";
4115 offset+=member_width;
4136 if(expr.
id()==ID_and && value)
4143 if(expr.
id()==ID_or && !value)
4150 if(expr.
id()==ID_not)
4160 if(expr.
id() == ID_equal && value)
4164 if(equal_expr.
lhs().
id()==ID_symbol)
4174 id.type=equal_expr.
lhs().
type();
4181 out <<
"; set_to true (equal)\n";
4182 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4201 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4226 exprt lowered_expr = expr;
4233 it->id() == ID_byte_extract_little_endian ||
4234 it->id() == ID_byte_extract_big_endian)
4239 it->id() == ID_byte_update_little_endian ||
4240 it->id() == ID_byte_update_big_endian)
4246 return lowered_expr;
4263 "lower_byte_operators should remove all byte operators");
4268 return lowered_expr;
4276 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4281 const auto identifier = q_expr.symbol().get_identifier();
4283 id.type = q_expr.symbol().type();
4293 if(expr.
id()==ID_symbol ||
4294 expr.
id()==ID_nondet_symbol)
4297 if(expr.
type().
id()==ID_code)
4302 if(expr.
id()==ID_symbol)
4305 identifier=
"nondet_"+
4310 if(
id.type.is_nil())
4312 id.type=expr.
type();
4317 out <<
"; find_symbols\n";
4318 out <<
"(declare-fun |"
4325 else if(expr.
id()==ID_array_of)
4331 out <<
"; the following is a substitute for lambda i. x" <<
"\n";
4332 out <<
"(declare-fun " <<
id <<
" () ";
4337 #if 0 // not really working in any solver yet!
4338 out <<
"(assert (forall ((i ";
4340 out <<
")) (= (select " <<
id <<
" i) ";
4342 out <<
")))" <<
"\n";
4348 else if(expr.
id()==ID_array)
4355 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4356 out <<
"(declare-fun " <<
id <<
" () ";
4360 for(std::size_t i=0; i<expr.
operands().size(); i++)
4362 out <<
"(assert (= (select " <<
id <<
" ";
4366 out <<
"))" <<
"\n";
4372 else if(expr.
id()==ID_string_constant)
4382 out <<
"; the following is a substitute for a string" <<
"\n";
4383 out <<
"(declare-fun " <<
id <<
" () ";
4387 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4389 out <<
"(assert (= (select " << id;
4393 out <<
"))" <<
"\n";
4399 else if(expr.
id() == ID_object_size)
4403 if(op.
type().
id()==ID_pointer)
4409 out <<
"(declare-fun " <<
id <<
" () ";
4420 (expr.
id() == ID_floatbv_plus ||
4421 expr.
id() == ID_floatbv_minus ||
4422 expr.
id() == ID_floatbv_mult ||
4423 expr.
id() == ID_floatbv_div ||
4424 expr.
id() == ID_floatbv_typecast ||
4425 expr.
id() == ID_ieee_float_equal ||
4426 expr.
id() == ID_ieee_float_notequal ||
4427 ((expr.
id() == ID_lt ||
4428 expr.
id() == ID_gt ||
4429 expr.
id() == ID_le ||
4430 expr.
id() == ID_ge ||
4431 expr.
id() == ID_isnan ||
4432 expr.
id() == ID_isnormal ||
4433 expr.
id() == ID_isfinite ||
4434 expr.
id() == ID_isinf ||
4435 expr.
id() == ID_sign ||
4436 expr.
id() == ID_unary_minus ||
4437 expr.
id() == ID_typecast ||
4438 expr.
id() == ID_abs) &&
4445 if(
bvfp_set.insert(
function).second)
4447 out <<
"; this is a model for " << expr.
id() <<
" : "
4450 <<
"(define-fun " <<
function <<
" (";
4452 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4456 out <<
"(op" << i <<
' ';
4466 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4493 if(expr.
id()==ID_with)
4495 else if(expr.
id()==ID_member)
4504 if(type.
id()==ID_array)
4517 out <<
"(_ BitVec 1)";
4523 else if(type.
id()==ID_bool)
4527 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4537 width != 0,
"failed to get width of struct");
4539 out <<
"(_ BitVec " << width <<
")";
4542 else if(type.
id()==ID_vector)
4552 width != 0,
"failed to get width of vector");
4554 out <<
"(_ BitVec " << width <<
")";
4557 else if(type.
id()==ID_code)
4564 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
4569 out <<
"(_ BitVec " << width <<
")";
4571 else if(type.
id()==ID_pointer)
4576 else if(type.
id()==ID_bv ||
4577 type.
id()==ID_fixedbv ||
4578 type.
id()==ID_unsignedbv ||
4579 type.
id()==ID_signedbv ||
4580 type.
id()==ID_c_bool)
4585 else if(type.
id()==ID_c_enum)
4591 else if(type.
id()==ID_c_enum_tag)
4595 else if(type.
id()==ID_floatbv)
4600 out <<
"(_ FloatingPoint "
4601 << floatbv_type.
get_e() <<
" "
4602 << floatbv_type.
get_f() + 1 <<
")";
4607 else if(type.
id()==ID_rational ||
4610 else if(type.
id()==ID_integer)
4612 else if(type.
id()==ID_complex)
4622 width != 0,
"failed to get width of complex");
4624 out <<
"(_ BitVec " << width <<
")";
4627 else if(type.
id()==ID_c_bit_field)
4639 std::set<irep_idt> recstack;
4645 std::set<irep_idt> &recstack)
4647 if(type.
id()==ID_array)
4653 else if(type.
id()==ID_complex)
4660 const std::string smt_typename =
4664 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4665 <<
"(mk-" << smt_typename;
4667 out <<
" (" << smt_typename <<
".imag ";
4671 out <<
" (" << smt_typename <<
".real ";
4678 else if(type.
id()==ID_vector)
4687 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4689 const std::string smt_typename =
4693 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4694 <<
"(mk-" << smt_typename;
4698 out <<
" (" << smt_typename <<
"." << i <<
" ";
4706 else if(type.
id() == ID_struct)
4709 bool need_decl=
false;
4713 const std::string smt_typename =
4728 const std::string &smt_typename =
datatype_map.at(type);
4739 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4740 <<
"(mk-" << smt_typename <<
" ";
4744 out <<
"(" << smt_typename <<
"." <<
component.get_name()
4750 out <<
"))))" <<
"\n";
4767 for(struct_union_typet::componentst::const_iterator
4768 it=components.begin();
4769 it!=components.end();
4773 out <<
"(define-fun update-" << smt_typename <<
"."
4775 <<
"((s " << smt_typename <<
") "
4778 out <<
")) " << smt_typename <<
" "
4779 <<
"(mk-" << smt_typename
4782 for(struct_union_typet::componentst::const_iterator
4783 it2=components.begin();
4784 it2!=components.end();
4791 out <<
"(" << smt_typename <<
"."
4792 << it2->get_name() <<
" s) ";
4796 out <<
"))" <<
"\n";
4802 else if(type.
id() == ID_union)
4810 else if(type.
id()==ID_code)
4814 for(
const auto ¶m : parameters)
4819 else if(type.
id()==ID_pointer)
4823 else if(type.
id() == ID_struct_tag)
4826 const irep_idt &
id = struct_tag.get_identifier();
4828 if(recstack.find(
id) == recstack.end())
4830 recstack.insert(
id);
4834 else if(type.
id() == ID_union_tag)
4837 const irep_idt &
id = union_tag.get_identifier();
4839 if(recstack.find(
id) == recstack.end())
4841 recstack.insert(
id);
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Operator to update elements in structs and arrays.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
void convert_typecast(const typecast_exprt &expr)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#define UNEXPECTEDCASE(S)
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
void get_dynamic_objects(std::vector< std::size_t > &objects) const
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
literalt get_literal() const
const typet & subtype() const
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
struct configt::bv_encodingt bv_encoding
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
depth_iteratort depth_begin()
exprt float_bv(const exprt &src)
void convert_type(const typet &)
const irep_idt & get_identifier() const
#define CHECK_RETURN(CONDITION)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
The type of an expression, extends irept.
std::vector< parametert > parameterst
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void pop() override
Currently, only implements a single stack element (no nested contexts)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
datatype_mapt datatype_map
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
exprt parse_array(const irept &s, const array_typet &type)
bool use_array_theory(const exprt &)
void convert_floatbv(const exprt &expr)
std::size_t get_f() const
literalt convert(const exprt &expr)
The trinary if-then-else operator.
bool has_byte_operator(const exprt &src)
Fixed-width bit-vector with IEEE floating-point interpretation.
const mp_integer string2integer(const std::string &n, unsigned base)
std::size_t add_object(const exprt &expr)
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
std::size_t get_fraction_bits() const
void convert_update(const exprt &expr)
Union constructor from single element.
const string_constantt & to_string_constant(const exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
void convert_plus(const plus_exprt &expr)
The plus expression Associativity is not specified.
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
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...
Base class for all expressions.
std::vector< componentt > componentst
Generic base class for unary expressions.
void convert_expr(const exprt &)
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
std::size_t get_bits_per_byte() const
void convert_constant(const constant_exprt &expr)
Sign of an expression Predicate is true if _op is negative, false otherwise.
const array_typet & type() const
void convert_literal(const literalt)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
A base class for quantifier expressions.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Vector constructor from list of elements.
bool is_true() const
Return whether the expression is a constant representing true.
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
bitvector_typet index_type()
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
std::string type2id(const typet &) const
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Evaluates to true if the operand is finite.
void convert_is_dynamic_object(const unary_exprt &)
bool is_false() const
Return whether the expression is a constant representing false.
Fixed-width bit-vector with unsigned binary interpretation.
void convert_index(const index_exprt &expr)
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
#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...
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Struct constructor from list of elements.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
typet & type()
Return the type of the expression.
hash_numbering< exprt, irep_hash > objects
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
std::size_t number_of_solver_calls
void convert_mult(const mult_exprt &expr)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::string convert_identifier(const irep_idt &identifier)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
void push() override
Unimplemented.
constant_exprt parse_literal(const irept &, const typet &type)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
std::size_t width() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
const irep_idt & get_name() const
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
void convert_relation(const binary_relation_exprt &)
Semantic type conversion from/to floating-point formats.
identifier_mapt identifier_map
#define forall_operands(it, expr)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
void convert_mod(const mod_exprt &expr)
const exprt & struct_op() const
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
Array constructor from single element.
const irep_idt & get_identifier() const
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
const std::string & id_string() const
literalt const_literal(bool value)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Binary multiplication Associativity is not specified.
std::size_t get_e() const
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
void convert_struct(const struct_exprt &expr)
pointer_typet pointer_type(const typet &subtype)
The unary minus expression.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool has_component(const irep_idt &component_name) const
exprt object_size(const exprt &pointer)
const irep_idt & id() const
void define_object_size(const irep_idt &id, const exprt &expr)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
defined_expressionst object_sizes
Ranges: pair of begin and end iterators, which can be initialized from containers,...
std::vector< exprt > operandst
std::set< irep_idt > bvfp_set
The Boolean constant false.
void convert_div(const div_exprt &expr)
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const constant_exprt & size() const
void convert_minus(const minus_exprt &expr)
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
resultt
Result of running the decision procedure.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
boolbv_widtht boolbv_width
Fixed-width bit-vector with signed fixed-point interpretation.
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
std::size_t get_width() const
Bit-wise negation of bit-vectors.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
bool is_zero() const
Return whether the expression is a constant representing 0.
void convert_with(const with_exprt &expr)
Extract member of struct or union.
Deprecated expression utility functions.
A base class for shift operators.
array_exprt to_array_expr() const
convert string into array constant
Structure type, corresponds to C style structs.
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.
Forward depth-first search iterators These iterators' copy operations are expensive,...
std::size_t get_fraction_bits() const
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void write_footer(std::ostream &)
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const irep_idt & get(const irep_namet &name) const
exprt parse_rec(const irept &s, const typet &type)
Evaluates to true if the operand is infinite.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
resultt dec_solve() override
Run the decision procedure to solve the problem.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
std::string floatbv_suffix(const exprt &) const
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
int solver(std::istream &in)
std::vector< exprt > assumptions
std::size_t get_integer_bits() const
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
bool is_constant() const
Return whether the expression is a constant.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
A base class for relations, i.e., binary predicates whose two operands have the same type.
struct_exprt parse_struct(const irept &s, const struct_typet &type)
std::size_t no_boolean_variables
void convert_union(const union_exprt &expr)
static std::string binary(const constant_exprt &src)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
std::size_t get_invalid_object() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
pointer_logict pointer_logic
std::size_t unsafe_string2size_t(const std::string &str, int base)
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
The byte swap expression.
irep_idt get_component_name() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
tvt l_get(literalt l) const
constant_exprt to_expr() const
void find_symbols(const exprt &expr)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const std::string integer2binary(const mp_integer &n, std::size_t width)
std::vector< bool > boolean_assignment
Operator to return the address of an object.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
static ieee_floatt NaN(const ieee_float_spect &_spec)
The Boolean constant true.
A constant literal expression.
depth_iteratort depth_end()
bool is_true(const literalt &l)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
exprt & where()
convenience accessor for binding().where()
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
void set_value(const irep_idt &value)
void unflatten(wheret, const typet &, unsigned nesting=0)
const irep_idt & get_value() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const membert & get_member(const struct_typet &type, const irep_idt &member) const
exprt parse_union(const irept &s, const union_typet &type)
ranget< iteratort > make_range(iteratort begin, iteratort end)
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
void flatten2bv(const exprt &)
Evaluates to true if the operand is a normal number.
smt2_identifierst smt2_identifiers
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
Evaluates to true if the operand is NaN.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
API to expression classes for 'mathematical' expressions.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void build(const mp_integer &exp, const mp_integer &frac)
void convert_member(const member_exprt &expr)
defined_expressionst defined_expressions