43 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
46 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
50 const std::string &_benchmark,
51 const std::string &_notes,
52 const std::string &_logic,
55 : use_FPA_theory(false),
57 use_array_of_bool(false),
61 benchmark(_benchmark),
67 no_boolean_variables(0)
131 "variable number shall be within bounds");
137 out <<
"; SMT 2" <<
"\n";
145 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
154 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
156 out <<
"(set-option :produce-models true)" <<
"\n";
162 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
172 os <<
"; assumptions\n";
194 os <<
"(get-value (|" <<
id <<
"|))"
202 os <<
"; end of SMT2 file"
214 std::size_t number = 0;
215 std::size_t h=pointer_width-1;
220 const typet &type = o.type();
223 numeric_cast<mp_integer>(size_expr.value_or(
nil_exprt()));
226 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
227 !size_expr.has_value() || !
object_size.has_value())
233 out <<
"(assert (implies (= " <<
234 "((_ extract " << h <<
" " << l <<
") ";
237 <<
"(= " <<
id <<
" (_ bv" << *
object_size <<
" " << size_width
253 if(expr.
id()==ID_symbol)
260 return it->second.value;
262 else if(expr.
id()==ID_nondet_symbol)
269 return it->second.value;
271 else if(expr.
id()==ID_member)
279 else if(expr.
id() == ID_literal)
287 else if(expr.
id() == ID_not)
292 else if(op.is_false())
328 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
333 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
344 else if(src.
get_sub().size()==2 &&
349 else if(src.
get_sub().size()==3 &&
352 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
356 else if(src.
get_sub().size()==4 &&
359 if(type.
id()==ID_floatbv)
368 const auto s1_int = numeric_cast_v<mp_integer>(
s1);
369 const auto s2_int = numeric_cast_v<mp_integer>(
s2);
370 const auto s3_int = numeric_cast_v<mp_integer>(s3);
374 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
380 else if(src.
get_sub().size()==4 &&
388 else if(src.
get_sub().size()==4 &&
396 else if(src.
get_sub().size()==4 &&
405 if(type.
id()==ID_signedbv ||
406 type.
id()==ID_unsignedbv ||
407 type.
id()==ID_c_enum ||
408 type.
id()==ID_c_bool)
412 else if(type.
id()==ID_c_enum_tag)
418 result.
type() = type;
421 else if(type.
id()==ID_fixedbv ||
422 type.
id()==ID_floatbv)
427 else if(type.
id()==ID_integer ||
435 "smt2_convt::parse_literal should not be of unsupported type " +
455 else if(src.
get_sub().size()==2 &&
456 src.
get_sub()[0].get_sub().size()==3 &&
457 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
458 src.
get_sub()[0].get_sub()[1].id()==
"const")
492 if(components.empty())
500 if(src.
get_sub().size()!=components.size()+1)
503 for(std::size_t i=0; i<components.size(); i++)
520 std::size_t offset=0;
522 for(std::size_t i=0; i<components.size(); i++)
524 std::size_t component_width=
boolbv_width(components[i].type());
527 offset + component_width <= total_width,
528 "struct component bits shall be within struct bit vector");
530 std::string component_binary=
532 total_width-offset-component_width, component_width);
537 offset+=component_width;
547 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
548 type.
id() == ID_integer || type.
id() == ID_rational ||
549 type.
id() == ID_real || type.
id() == ID_c_enum ||
550 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
551 type.
id() == ID_floatbv)
555 else if(type.
id()==ID_bool)
557 if(src.
id()==ID_1 || src.
id()==ID_true)
559 else if(src.
id()==ID_0 || src.
id()==ID_false)
562 else if(type.
id()==ID_pointer)
568 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
573 ptr.
object = numeric_cast_v<std::size_t>(v / pow);
577 else if(type.
id()==ID_struct)
581 else if(type.
id() == ID_struct_tag)
586 struct_expr.type() = type;
587 return std::move(struct_expr);
589 else if(type.
id()==ID_union)
593 else if(type.
id() == ID_union_tag)
597 union_expr.type() = type;
600 else if(type.
id()==ID_array)
612 if(expr.
id()==ID_symbol ||
613 expr.
id()==ID_constant ||
614 expr.
id()==ID_string_constant ||
624 else if(expr.
id()==ID_index)
633 if(array.
type().
id()==ID_pointer)
635 else if(array.
type().
id()==ID_array)
655 else if(expr.
id()==ID_member)
660 const typet &struct_op_type = struct_op.
type();
663 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
664 "member expression operand shall have struct type");
681 else if(expr.
id()==ID_if)
696 "operand of address of expression should not be of kind " +
710 else if(expr.
id()==ID_literal)
722 out <<
"; convert\n";
723 out <<
"(define-fun ";
735 if(expr.
type().
id() != ID_bool)
786 for(std::size_t i=0; i<identifier.
size(); i++)
788 char ch=identifier[i];
811 if(type.
id()==ID_floatbv)
816 else if(type.
id()==ID_unsignedbv)
820 else if(type.
id()==ID_c_bool)
824 else if(type.
id()==ID_signedbv)
828 else if(type.
id()==ID_bool)
832 else if(type.
id()==ID_c_enum_tag)
836 else if(type.
id() == ID_pointer)
857 if(expr.
id()==ID_symbol)
864 if(expr.
id()==ID_smt2_symbol)
872 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
874 out <<
"(|float_bv." << expr.
id()
890 if(expr.
id()==ID_symbol)
896 else if(expr.
id()==ID_nondet_symbol)
899 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
902 else if(expr.
id()==ID_smt2_symbol)
908 else if(expr.
id()==ID_typecast)
912 else if(expr.
id()==ID_floatbv_typecast)
916 else if(expr.
id()==ID_struct)
920 else if(expr.
id()==ID_union)
924 else if(expr.
id()==ID_constant)
928 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
932 "concatenation over a single operand should have matching types",
937 else if(expr.
id()==ID_concatenation ||
938 expr.
id()==ID_bitand ||
939 expr.
id()==ID_bitor ||
940 expr.
id()==ID_bitxor ||
941 expr.
id()==ID_bitnand ||
942 expr.
id()==ID_bitnor)
946 "given expression should have at least two operands",
951 if(expr.
id()==ID_concatenation)
953 else if(expr.
id()==ID_bitand)
955 else if(expr.
id()==ID_bitor)
957 else if(expr.
id()==ID_bitxor)
959 else if(expr.
id()==ID_bitnand)
961 else if(expr.
id()==ID_bitnor)
972 else if(expr.
id()==ID_bitnot)
976 if(bitnot_expr.
type().
id() == ID_vector)
987 out <<
"(let ((?vectorop ";
991 out <<
"(mk-" << smt_typename;
998 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
1014 else if(expr.
id()==ID_unary_minus)
1019 unary_minus_expr.
type().
id() == ID_rational ||
1020 unary_minus_expr.
type().
id() == ID_integer ||
1021 unary_minus_expr.
type().
id() == ID_real)
1027 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1039 else if(unary_minus_expr.
type().
id() == ID_vector)
1043 const std::string &smt_typename =
1050 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1052 out <<
"(let ((?vectorop ";
1056 out <<
"(mk-" << smt_typename;
1063 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1079 else if(expr.
id()==ID_unary_plus)
1084 else if(expr.
id()==ID_sign)
1090 if(op_type.
id()==ID_floatbv)
1094 out <<
"(fp.isNegative ";
1101 else if(op_type.
id()==ID_signedbv)
1107 out <<
" (_ bv0 " << op_width <<
"))";
1112 "sign should not be applied to unsupported type",
1115 else if(expr.
id()==ID_if)
1127 else if(expr.
id()==ID_and ||
1132 expr.
type().
id() == ID_bool,
1133 "logical and, or, and xor expressions should have Boolean type");
1136 "logical and, or, and xor expressions should have at least two operands");
1138 out <<
"(" << expr.
id();
1146 else if(expr.
id()==ID_implies)
1151 implies_expr.
type().
id() == ID_bool,
1152 "implies expression should have Boolean type");
1160 else if(expr.
id()==ID_not)
1165 not_expr.
type().
id() == ID_bool,
1166 "not expression should have Boolean type");
1172 else if(expr.
id() == ID_equal)
1178 "operands of equal expression shall have same type");
1186 else if(expr.
id() == ID_notequal)
1192 "operands of not equal expression shall have same type");
1200 else if(expr.
id()==ID_ieee_float_equal ||
1201 expr.
id()==ID_ieee_float_notequal)
1208 rel_expr.lhs().type() == rel_expr.rhs().type(),
1209 "operands of float equal and not equal expressions shall have same type");
1214 if(rel_expr.id() == ID_ieee_float_notequal)
1223 if(rel_expr.id() == ID_ieee_float_notequal)
1229 else if(expr.
id()==ID_le ||
1236 else if(expr.
id()==ID_plus)
1240 else if(expr.
id()==ID_floatbv_plus)
1244 else if(expr.
id()==ID_minus)
1248 else if(expr.
id()==ID_floatbv_minus)
1252 else if(expr.
id()==ID_div)
1256 else if(expr.
id()==ID_floatbv_div)
1260 else if(expr.
id()==ID_mod)
1264 else if(expr.
id()==ID_mult)
1268 else if(expr.
id()==ID_floatbv_mult)
1272 else if(expr.
id()==ID_address_of)
1278 else if(expr.
id()==ID_array_of)
1283 array_of_expr.
type().
id() == ID_array,
1284 "array of expression shall have array type");
1286 defined_expressionst::const_iterator it =
1291 else if(expr.
id()==ID_index)
1295 else if(expr.
id()==ID_ashr ||
1296 expr.
id()==ID_lshr ||
1302 if(type.
id()==ID_unsignedbv ||
1303 type.
id()==ID_signedbv ||
1306 if(shift_expr.
id() == ID_ashr)
1308 else if(shift_expr.
id() == ID_lshr)
1310 else if(shift_expr.
id() == ID_shl)
1340 if(width_op0==width_op1)
1342 else if(width_op0>width_op1)
1344 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1350 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1357 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1364 "unsupported type for " + shift_expr.
id_string() +
": " +
1367 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1373 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1378 if(shift_expr.
id() == ID_rol)
1379 out <<
"((_ rotate_left";
1380 else if(shift_expr.
id() == ID_ror)
1381 out <<
"((_ rotate_right";
1387 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.
distance());
1389 if(distance_int_op.has_value())
1391 out << distance_int_op.value();
1395 "distance type for " + shift_expr.
id_string() +
"must be constant");
1404 "unsupported type for " + shift_expr.
id_string() +
": " +
1407 else if(expr.
id()==ID_with)
1411 else if(expr.
id()==ID_update)
1415 else if(expr.
id()==ID_member)
1419 else if(expr.
id()==ID_pointer_offset)
1424 op.type().id() == ID_pointer,
1425 "operand of pointer offset expression shall be of pointer type");
1427 std::size_t offset_bits =
1432 if(offset_bits>result_width)
1433 offset_bits=result_width;
1436 if(result_width>offset_bits)
1437 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1439 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1443 if(result_width>offset_bits)
1446 else if(expr.
id()==ID_pointer_object)
1451 op.type().id() == ID_pointer,
1452 "pointer object expressions should be of pointer type");
1458 out <<
"((_ zero_extend " << ext <<
") ";
1460 out <<
"((_ extract "
1461 << pointer_width-1 <<
" "
1469 else if(expr.
id() == ID_is_dynamic_object)
1473 else if(expr.
id() == ID_is_invalid_pointer)
1477 out <<
"(= ((_ extract "
1478 << pointer_width-1 <<
" "
1484 else if(expr.
id()==ID_string_constant)
1490 else if(expr.
id()==ID_extractbit)
1499 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1505 out <<
"(= ((_ extract 0 0) ";
1514 else if(expr.
id()==ID_extractbits)
1528 std::swap(op1_i, op2_i);
1532 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1539 out <<
"(= ((_ extract 0 0) ";
1548 SMT2_TODO(
"smt2: extractbits with non-constant index");
1551 else if(expr.
id()==ID_replication)
1555 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1557 out <<
"((_ repeat " << times <<
") ";
1561 else if(expr.
id()==ID_byte_extract_little_endian ||
1562 expr.
id()==ID_byte_extract_big_endian)
1565 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1567 else if(expr.
id()==ID_byte_update_little_endian ||
1568 expr.
id()==ID_byte_update_big_endian)
1571 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1573 else if(expr.
id()==ID_width)
1581 out <<
"(_ bv" << op_width/8
1582 <<
" " << result_width <<
")";
1584 else if(expr.
id()==ID_abs)
1590 if(type.
id()==ID_signedbv)
1594 out <<
"(ite (bvslt ";
1596 out <<
" (_ bv0 " << result_width <<
")) ";
1603 else if(type.
id()==ID_fixedbv)
1607 out <<
"(ite (bvslt ";
1609 out <<
" (_ bv0 " << result_width <<
")) ";
1616 else if(type.
id()==ID_floatbv)
1630 else if(expr.
id()==ID_isnan)
1636 if(op_type.
id()==ID_fixedbv)
1638 else if(op_type.
id()==ID_floatbv)
1642 out <<
"(fp.isNaN ";
1652 else if(expr.
id()==ID_isfinite)
1658 if(op_type.
id()==ID_fixedbv)
1660 else if(op_type.
id()==ID_floatbv)
1666 out <<
"(not (fp.isNaN ";
1670 out <<
"(not (fp.isInf ";
1682 else if(expr.
id()==ID_isinf)
1688 if(op_type.
id()==ID_fixedbv)
1690 else if(op_type.
id()==ID_floatbv)
1694 out <<
"(fp.isInfinite ";
1704 else if(expr.
id()==ID_isnormal)
1710 if(op_type.
id()==ID_fixedbv)
1712 else if(op_type.
id()==ID_floatbv)
1716 out <<
"(fp.isNormal ";
1726 else if(expr.
id()==ID_overflow_plus ||
1727 expr.
id()==ID_overflow_minus)
1733 expr.
type().
id() == ID_bool,
1734 "overflow plus and overflow minus expressions shall be of Boolean type");
1736 bool subtract=expr.
id()==ID_overflow_minus;
1737 const typet &op_type = op0.type();
1740 if(op_type.
id()==ID_signedbv)
1743 out <<
"(let ((?sum (";
1744 out << (subtract?
"bvsub":
"bvadd");
1745 out <<
" ((_ sign_extend 1) ";
1748 out <<
" ((_ sign_extend 1) ";
1752 "((_ extract " << width <<
" " << width <<
") ?sum) "
1753 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1756 else if(op_type.
id()==ID_unsignedbv ||
1757 op_type.
id()==ID_pointer)
1761 out <<
"((_ extract " << width <<
" " << width <<
") ";
1762 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1763 out <<
" ((_ zero_extend 1) ";
1766 out <<
" ((_ zero_extend 1) ";
1774 "overflow check should not be performed on unsupported type",
1777 else if(expr.
id()==ID_overflow_mult)
1783 expr.
type().
id() == ID_bool,
1784 "overflow mult expression shall be of Boolean type");
1789 const typet &op_type = op0.type();
1792 if(op_type.
id()==ID_signedbv)
1794 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1796 out <<
") ((_ sign_extend " << width <<
") ";
1799 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
1801 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" "
1802 << width*2 <<
")))))";
1804 else if(op_type.
id()==ID_unsignedbv)
1806 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1808 out <<
") ((_ zero_extend " << width <<
") ";
1810 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1815 "overflow check should not be performed on unsupported type",
1818 else if(expr.
id()==ID_array)
1824 else if(expr.
id()==ID_literal)
1828 else if(expr.
id()==ID_forall ||
1829 expr.
id()==ID_exists)
1835 throw "MathSAT does not support quantifiers";
1837 if(quantifier_expr.
id() == ID_forall)
1839 else if(quantifier_expr.
id() == ID_exists)
1854 else if(expr.
id()==ID_vector)
1859 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1862 size == vector_expr.
operands().size(),
1863 "size indicated by type shall be equal to the number of operands");
1867 const std::string &smt_typename =
datatype_map.at(vector_type);
1869 out <<
"(mk-" << smt_typename;
1883 else if(expr.
id()==ID_object_size)
1887 else if(expr.
id()==ID_let)
1890 const auto &variables = let_expr.
variables();
1891 const auto &values = let_expr.
values();
1896 for(
auto &binding :
make_range(variables).zip(values))
1915 else if(expr.
id()==ID_constraint_select_one)
1918 "smt2_convt::convert_expr: '" + expr.
id_string() +
1919 "' is not yet supported");
1921 else if(expr.
id() == ID_bswap)
1927 "operand of byte swap expression shall have same type as the expression");
1930 out <<
"(let ((bswap_op ";
1935 bswap_expr.
type().
id() == ID_signedbv ||
1936 bswap_expr.
type().
id() == ID_unsignedbv)
1938 const std::size_t width =
1945 width % bits_per_byte == 0,
1946 "bit width indicated by type of bswap expression should be a multiple "
1947 "of the number of bits per byte");
1949 const std::size_t bytes = width / bits_per_byte;
1958 for(std::size_t
byte = 0;
byte < bytes;
byte++)
1962 out <<
"(bswap_byte_" <<
byte <<
' ';
1963 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
1964 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
1973 for(std::size_t
byte = 0;
byte < bytes;
byte++)
1974 out <<
" bswap_byte_" <<
byte;
1985 else if(expr.
id() == ID_popcount)
1993 "smt2_convt::convert_expr should not be applied to unsupported type",
2002 if(dest_type.
id()==ID_c_enum_tag)
2006 if(src_type.
id()==ID_c_enum_tag)
2009 if(dest_type.
id()==ID_bool)
2012 if(src_type.
id()==ID_signedbv ||
2013 src_type.
id()==ID_unsignedbv ||
2014 src_type.
id()==ID_c_bool ||
2015 src_type.
id()==ID_fixedbv ||
2016 src_type.
id()==ID_pointer ||
2017 src_type.
id()==ID_integer)
2025 else if(src_type.
id()==ID_floatbv)
2029 out <<
"(not (fp.isZero ";
2041 else if(dest_type.
id()==ID_c_bool)
2050 out <<
" (_ bv1 " << to_width <<
")";
2051 out <<
" (_ bv0 " << to_width <<
")";
2054 else if(dest_type.
id()==ID_signedbv ||
2055 dest_type.
id()==ID_unsignedbv ||
2056 dest_type.
id()==ID_c_enum ||
2057 dest_type.
id()==ID_bv)
2061 if(src_type.
id()==ID_signedbv ||
2062 src_type.
id()==ID_unsignedbv ||
2063 src_type.
id()==ID_c_bool ||
2064 src_type.
id()==ID_c_enum ||
2065 src_type.
id()==ID_bv)
2069 if(from_width==to_width)
2071 else if(from_width<to_width)
2073 if(src_type.
id()==ID_signedbv)
2074 out <<
"((_ sign_extend ";
2076 out <<
"((_ zero_extend ";
2078 out << (to_width-from_width)
2085 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2090 else if(src_type.
id()==ID_fixedbv)
2094 std::size_t from_width=fixedbv_type.
get_width();
2101 out <<
"(let ((?tcop ";
2107 if(to_width>from_integer_bits)
2109 out <<
"((_ sign_extend "
2110 << (to_width-from_integer_bits) <<
") ";
2111 out <<
"((_ extract " << (from_width-1) <<
" "
2112 << from_fraction_bits <<
") ";
2118 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2119 <<
" " << from_fraction_bits <<
") ";
2124 out <<
" (ite (and ";
2127 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2128 "(_ bv0 " << from_fraction_bits <<
")))";
2131 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2136 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2140 else if(src_type.
id()==ID_floatbv)
2142 if(dest_type.
id()==ID_bv)
2159 else if(dest_type.
id()==ID_signedbv)
2163 "typecast unexpected "+src_type.
id_string()+
" -> "+
2166 else if(dest_type.
id()==ID_unsignedbv)
2170 "typecast unexpected "+src_type.
id_string()+
" -> "+
2174 else if(src_type.
id()==ID_bool)
2179 if(dest_type.
id()==ID_fixedbv)
2182 out <<
" (concat (_ bv1 "
2185 "(_ bv0 " << spec.
width <<
")";
2189 out <<
" (_ bv1 " << to_width <<
")";
2190 out <<
" (_ bv0 " << to_width <<
")";
2195 else if(src_type.
id()==ID_pointer)
2199 if(from_width<to_width)
2201 out <<
"((_ sign_extend ";
2202 out << (to_width-from_width)
2209 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2214 else if(src_type.
id()==ID_integer)
2220 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2223 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2226 src_type.
id() == ID_struct ||
2227 src_type.
id() == ID_struct_tag)
2233 "bit vector with of source and destination type shall be equal");
2240 "bit vector with of source and destination type shall be equal");
2245 src_type.
id() == ID_union ||
2246 src_type.
id() == ID_union_tag)
2250 "bit vector with of source and destination type shall be equal");
2253 else if(src_type.
id()==ID_c_bit_field)
2257 if(from_width==to_width)
2268 std::ostringstream e_str;
2269 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2270 <<
" src == " <<
format(src);
2274 else if(dest_type.
id()==ID_fixedbv)
2280 if(src_type.
id()==ID_unsignedbv ||
2281 src_type.
id()==ID_signedbv ||
2282 src_type.
id()==ID_c_enum)
2289 if(from_width==to_integer_bits)
2291 else if(from_width>to_integer_bits)
2294 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2302 from_width < to_integer_bits,
2303 "from_width should be smaller than to_integer_bits as other case "
2304 "have been handled above");
2305 if(dest_type.
id()==ID_unsignedbv)
2307 out <<
"(_ zero_extend "
2308 << (to_integer_bits-from_width) <<
") ";
2314 out <<
"((_ sign_extend "
2315 << (to_integer_bits-from_width) <<
") ";
2321 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2324 else if(src_type.
id()==ID_bool)
2326 out <<
"(concat (concat"
2327 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2333 else if(src_type.
id()==ID_fixedbv)
2338 std::size_t from_width=from_fixedbv_type.
get_width();
2340 out <<
"(let ((?tcop ";
2346 if(to_integer_bits<=from_integer_bits)
2348 out <<
"((_ extract "
2349 << (from_fraction_bits+to_integer_bits-1) <<
" "
2350 << from_fraction_bits
2356 to_integer_bits > from_integer_bits,
2357 "to_integer_bits should be greater than from_integer_bits as the"
2358 "other case has been handled above");
2359 out <<
"((_ sign_extend "
2360 << (to_integer_bits-from_integer_bits)
2362 << (from_width-1) <<
" "
2363 << from_fraction_bits
2369 if(to_fraction_bits<=from_fraction_bits)
2371 out <<
"((_ extract "
2372 << (from_fraction_bits-1) <<
" "
2373 << (from_fraction_bits-to_fraction_bits)
2379 to_fraction_bits > from_fraction_bits,
2380 "to_fraction_bits should be greater than from_fraction_bits as the"
2381 "other case has been handled above");
2382 out <<
"(concat ((_ extract "
2383 << (from_fraction_bits-1) <<
" 0) ";
2386 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2395 else if(dest_type.
id()==ID_pointer)
2399 if(src_type.
id()==ID_pointer)
2405 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2406 src_type.
id() == ID_bv)
2412 if(from_width==to_width)
2414 else if(from_width<to_width)
2416 out <<
"((_ sign_extend "
2417 << (to_width-from_width)
2424 out <<
"((_ extract " << to_width <<
" 0) ";
2432 else if(dest_type.
id()==ID_range)
2436 else if(dest_type.
id()==ID_floatbv)
2445 if(src_type.
id()==ID_bool)
2460 a.
build(significand, exponent);
2468 a.
build(significand, exponent);
2474 else if(src_type.
id()==ID_c_bool)
2480 else if(src_type.
id() == ID_bv)
2489 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2490 << dest_floatbv_type.get_f() + 1 <<
") ";
2500 else if(dest_type.
id()==ID_integer)
2502 if(src_type.
id()==ID_bool)
2511 else if(dest_type.
id()==ID_c_bit_field)
2516 if(from_width==to_width)
2537 if(dest_type.
id()==ID_floatbv)
2539 if(src_type.
id()==ID_floatbv)
2566 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2567 << dst.
get_f() + 1 <<
") ";
2576 else if(src_type.
id()==ID_unsignedbv)
2597 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
2598 << dst.
get_f() + 1 <<
") ";
2607 else if(src_type.
id()==ID_signedbv)
2615 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2616 << dst.
get_f() + 1 <<
") ";
2625 else if(src_type.
id()==ID_c_enum_tag)
2641 else if(dest_type.
id()==ID_signedbv)
2646 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2655 else if(dest_type.
id()==ID_unsignedbv)
2660 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2684 components.size() == expr.
operands().size(),
2685 "number of struct components as indicated by the struct type shall be equal"
2686 "to the number of operands of the struct expression");
2688 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2692 const std::string &smt_typename =
datatype_map.at(struct_type);
2695 out <<
"(mk-" << smt_typename;
2698 for(struct_typet::componentst::const_iterator
2699 it=components.begin();
2700 it!=components.end();
2711 if(components.size()==1)
2716 for(std::size_t i=components.size(); i>1; i--)
2723 if(op.
type().
id() == ID_array)
2733 for(std::size_t i=1; i<components.size(); i++)
2743 const auto &size_expr = array_type.
size();
2749 out <<
"(let ((?far ";
2757 out <<
"(select ?far ";
2778 total_width != 0,
"failed to get union width for union");
2782 member_width != 0,
"failed to get union member width for union");
2784 if(total_width==member_width)
2792 total_width > member_width,
2793 "total_width should be greater than member_width as member_width can be"
2794 "at most as large as total_width and the other case has been handled "
2798 << (total_width-member_width) <<
") ";
2808 if(expr_type.
id()==ID_unsignedbv ||
2809 expr_type.
id()==ID_signedbv ||
2810 expr_type.
id()==ID_bv ||
2811 expr_type.
id()==ID_c_enum ||
2812 expr_type.
id()==ID_c_enum_tag ||
2813 expr_type.
id()==ID_c_bool ||
2814 expr_type.
id()==ID_c_bit_field)
2820 out <<
"(_ bv" << value
2821 <<
" " << width <<
")";
2823 else if(expr_type.
id()==ID_fixedbv)
2829 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2831 else if(expr_type.
id()==ID_floatbv)
2844 size_t e=floatbv_type.
get_e();
2845 size_t f=floatbv_type.
get_f()+1;
2851 out <<
"((_ to_fp " << e <<
" " << f <<
")"
2857 out <<
"(_ NaN " << e <<
" " << f <<
")";
2862 out <<
"(_ -oo " << e <<
" " << f <<
")";
2864 out <<
"(_ +oo " << e <<
" " << f <<
")";
2874 <<
"#b" << binaryString.substr(0, 1) <<
" "
2875 <<
"#b" << binaryString.substr(1, e) <<
" "
2876 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
2884 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
2887 else if(expr_type.
id()==ID_pointer)
2899 else if(expr_type.
id()==ID_bool)
2908 else if(expr_type.
id()==ID_array)
2914 else if(expr_type.
id()==ID_rational)
2917 size_t pos=value.find(
"/");
2919 if(
pos==std::string::npos)
2920 out << value <<
".0";
2923 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
2924 << value.substr(
pos+1) <<
".0)";
2927 else if(expr_type.
id()==ID_integer)
2937 if(expr.
type().
id()==ID_unsignedbv ||
2938 expr.
type().
id()==ID_signedbv)
2940 if(expr.
type().
id()==ID_unsignedbv)
2956 std::vector<std::size_t> dynamic_objects;
2959 if(dynamic_objects.empty())
2965 out <<
"(let ((?obj ((_ extract "
2966 << pointer_width-1 <<
" "
2971 if(dynamic_objects.size()==1)
2973 out <<
"(= (_ bv" << dynamic_objects.front()
2980 for(
const auto &
object : dynamic_objects)
2981 out <<
" (= (_ bv" <<
object
2995 if(op_type.
id()==ID_unsignedbv ||
2996 op_type.
id()==ID_pointer ||
2997 op_type.
id()==ID_bv)
3000 if(expr.
id()==ID_le)
3002 else if(expr.
id()==ID_lt)
3004 else if(expr.
id()==ID_ge)
3006 else if(expr.
id()==ID_gt)
3015 else if(op_type.
id()==ID_signedbv ||
3016 op_type.
id()==ID_fixedbv)
3019 if(expr.
id()==ID_le)
3021 else if(expr.
id()==ID_lt)
3023 else if(expr.
id()==ID_ge)
3025 else if(expr.
id()==ID_gt)
3034 else if(op_type.
id()==ID_floatbv)
3039 if(expr.
id()==ID_le)
3041 else if(expr.
id()==ID_lt)
3043 else if(expr.
id()==ID_ge)
3045 else if(expr.
id()==ID_gt)
3057 else if(op_type.
id()==ID_rational ||
3058 op_type.
id()==ID_integer)
3077 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3078 expr.
type().
id() == ID_real)
3083 for(
const auto &op : expr.
operands())
3092 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3093 expr.
type().
id() == ID_fixedbv)
3110 else if(expr.
type().
id() == ID_floatbv)
3117 else if(expr.
type().
id() == ID_pointer)
3123 if(p.
type().
id() != ID_pointer)
3127 p.
type().
id() == ID_pointer,
3128 "one of the operands should have pointer type");
3131 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3137 if(*element_size >= 2)
3154 else if(expr.
type().
id() == ID_vector)
3158 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3164 const std::string &smt_typename =
datatype_map.at(vector_type);
3166 out <<
"(mk-" << smt_typename;
3175 summands.reserve(expr.
operands().size());
3176 for(
const auto &op : expr.
operands())
3209 if(expr.
id()==ID_constant)
3213 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3216 out <<
"roundNearestTiesToEven";
3218 out <<
"roundTowardNegative";
3220 out <<
"roundTowardPositive";
3222 out <<
"roundTowardZero";
3226 "Rounding mode should have value 0, 1, 2, or 3",
3234 out <<
"(ite (= (_ bv0 " << width <<
") ";
3236 out <<
") roundNearestTiesToEven ";
3238 out <<
"(ite (= (_ bv1 " << width <<
") ";
3240 out <<
") roundTowardNegative ";
3242 out <<
"(ite (= (_ bv2 " << width <<
") ";
3244 out <<
") roundTowardPositive ";
3247 out <<
"roundTowardZero";
3258 type.
id() == ID_floatbv ||
3259 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv) ||
3260 (type.
id() == ID_vector && type.
subtype().
id() == ID_floatbv));
3264 if(type.
id()==ID_floatbv)
3274 else if(type.
id()==ID_complex)
3278 else if(type.
id()==ID_vector)
3285 "type should not be one of the unsupported types",
3294 if(expr.
type().
id()==ID_integer)
3302 else if(expr.
type().
id()==ID_unsignedbv ||
3303 expr.
type().
id()==ID_signedbv ||
3304 expr.
type().
id()==ID_fixedbv)
3306 if(expr.
op0().
type().
id()==ID_pointer &&
3311 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3313 if(*element_size >= 2)
3318 "bitvector width of operand shall be equal to the bitvector width of "
3327 if(*element_size >= 2)
3340 else if(expr.
type().
id()==ID_floatbv)
3347 else if(expr.
type().
id()==ID_pointer)
3351 else if(expr.
type().
id()==ID_vector)
3355 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3361 const std::string &smt_typename =
datatype_map.at(vector_type);
3363 out <<
"(mk-" << smt_typename;
3392 expr.
type().
id() == ID_floatbv,
3393 "type of ieee floating point expression shall be floatbv");
3411 if(expr.
type().
id()==ID_unsignedbv ||
3412 expr.
type().
id()==ID_signedbv)
3414 if(expr.
type().
id()==ID_unsignedbv)
3424 else if(expr.
type().
id()==ID_fixedbv)
3429 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3434 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3436 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3442 else if(expr.
type().
id()==ID_floatbv)
3456 expr.
type().
id() == ID_floatbv,
3457 "type of ieee floating point expression shall be floatbv");
3488 "expression should have been converted to a variant with two operands");
3490 if(expr.
type().
id()==ID_unsignedbv ||
3491 expr.
type().
id()==ID_signedbv)
3502 else if(expr.
type().
id()==ID_floatbv)
3509 else if(expr.
type().
id()==ID_fixedbv)
3514 out <<
"((_ extract "
3515 << spec.
width+fraction_bits-1 <<
" "
3516 << fraction_bits <<
") ";
3520 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3524 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3530 else if(expr.
type().
id()==ID_rational ||
3531 expr.
type().
id()==ID_integer ||
3532 expr.
type().
id()==ID_real)
3551 expr.
type().
id() == ID_floatbv,
3552 "type of ieee floating point expression shall be floatbv");
3574 std::size_t s=expr.
operands().size();
3589 "with expression should have been converted to a version with three "
3594 if(expr_type.
id()==ID_array)
3618 out <<
"(let ((distance? ";
3619 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3623 if(array_width>index_width)
3625 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3631 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3641 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
3643 out <<
"distance?)) ";
3647 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3649 out <<
") distance?)))";
3652 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
3659 const irep_idt &component_name=index.
get(ID_component_name);
3663 "struct should have accessed component");
3667 const std::string &smt_typename =
datatype_map.at(expr_type);
3669 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3683 out <<
"(let ((?withop ";
3687 if(m.
width==struct_width)
3697 <<
"((_ extract " << (struct_width-1) <<
" "
3698 << m.
width <<
") ?withop) ";
3707 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
3712 out <<
"(concat (concat "
3713 <<
"((_ extract " << (struct_width-1) <<
" "
3716 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3723 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
3731 total_width != 0,
"failed to get union width for with");
3735 member_width != 0,
"failed to get union member width for with");
3737 if(total_width==member_width)
3744 total_width > member_width,
3745 "total width should be greater than member_width as member_width is at "
3746 "most as large as total_width and the other case has been handled "
3749 out <<
"((_ extract "
3751 <<
" " << member_width <<
") ";
3758 else if(expr_type.
id()==ID_bv ||
3759 expr_type.
id()==ID_unsignedbv ||
3760 expr_type.
id()==ID_signedbv)
3766 total_width != 0,
"failed to get total width");
3773 value_width != 0,
"failed to get value width");
3785 out <<
" (bvnot (bvshl";
3788 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3789 out <<
" (repeat[" << value_width <<
"] bv1[1])";
3811 "with expects struct, union, or array type, but got "+
3819 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
3826 if(array_op_type.
id()==ID_array)
3862 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
3866 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3870 if(array_width>index_width)
3872 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3878 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3888 else if(array_op_type.
id()==ID_vector)
3894 const std::string &smt_typename =
datatype_map.at(vector_type);
3898 const auto index_int = numeric_cast<mp_integer>(expr.
index());
3899 if(!index_int.has_value())
3901 SMT2_TODO(
"non-constant index on vectors");
3905 out <<
"(" << smt_typename <<
"." << *index_int <<
" ";
3917 false,
"index with unsupported array type: " + array_op_type.
id_string());
3924 const typet &struct_op_type = struct_op.
type();
3927 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
3932 struct_type.
has_component(name),
"struct should have accessed component");
3936 const std::string &smt_typename =
datatype_map.at(struct_type);
3938 out <<
"(" << smt_typename <<
"."
3951 member_offset.has_value(),
"failed to get struct member offset");
3960 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
3964 width != 0,
"failed to get union member width");
3968 out <<
"((_ extract "
3978 "convert_member on an unexpected type "+struct_op_type.
id_string());
3985 if(type.
id()==ID_bool)
3991 else if(type.
id()==ID_vector)
3995 const std::string &smt_typename =
datatype_map.at(type);
4000 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4002 out <<
"(let ((?vflop ";
4010 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
4018 else if(type.
id()==ID_array)
4022 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4026 const std::string &smt_typename =
datatype_map.at(type);
4031 out <<
"(let ((?sflop ";
4039 for(std::size_t i=components.size(); i>1; i--)
4041 out <<
"(concat (" << smt_typename <<
"."
4042 << components[i-1].get_name() <<
" ?sflop)";
4047 out <<
"(" << smt_typename <<
"."
4048 << components[0].get_name() <<
" ?sflop)";
4050 for(std::size_t i=1; i<components.size(); i++)
4058 else if(type.
id()==ID_floatbv)
4062 "floatbv expressions should be flattened when using FPA theory");
4075 if(type.
id()==ID_bool)
4082 else if(type.
id()==ID_vector)
4086 const std::string &smt_typename =
datatype_map.at(type);
4093 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4096 out <<
"(let ((?ufop" << nesting <<
" ";
4101 out <<
"(mk-" << smt_typename;
4103 std::size_t offset=0;
4105 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4109 out <<
"((_ extract " << offset+subtype_width-1 <<
" "
4110 << offset <<
") ?ufop" << nesting <<
")";
4122 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4128 out <<
"(let ((?ufop" << nesting <<
" ";
4133 const std::string &smt_typename =
datatype_map.at(type);
4135 out <<
"(mk-" << smt_typename;
4142 std::size_t offset=0;
4145 for(struct_typet::componentst::const_iterator
4146 it=components.begin();
4147 it!=components.end();
4154 out <<
"((_ extract " << offset+member_width-1 <<
" "
4155 << offset <<
") ?ufop" << nesting <<
")";
4157 offset+=member_width;
4178 if(expr.
id()==ID_and && value)
4185 if(expr.
id()==ID_or && !value)
4192 if(expr.
id()==ID_not)
4202 if(expr.
id() == ID_equal && value)
4206 if(equal_expr.
lhs().
id()==ID_symbol)
4216 id.type=equal_expr.
lhs().
type();
4223 out <<
"; set_to true (equal)\n";
4224 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4243 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4268 exprt lowered_expr = expr;
4275 it->id() == ID_byte_extract_little_endian ||
4276 it->id() == ID_byte_extract_big_endian)
4281 it->id() == ID_byte_update_little_endian ||
4282 it->id() == ID_byte_update_big_endian)
4288 return lowered_expr;
4305 "lower_byte_operators should remove all byte operators");
4310 return lowered_expr;
4318 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4323 const auto identifier = q_expr.symbol().get_identifier();
4325 id.type = q_expr.symbol().type();
4335 if(expr.
id()==ID_symbol ||
4336 expr.
id()==ID_nondet_symbol)
4339 if(expr.
type().
id()==ID_code)
4344 if(expr.
id()==ID_symbol)
4347 identifier=
"nondet_"+
4352 if(
id.type.is_nil())
4354 id.type=expr.
type();
4359 out <<
"; find_symbols\n";
4360 out <<
"(declare-fun |"
4367 else if(expr.
id()==ID_array_of)
4373 out <<
"; the following is a substitute for lambda i. x" <<
"\n";
4374 out <<
"(declare-fun " <<
id <<
" () ";
4380 out <<
"(assert (forall ((i ";
4382 out <<
")) (= (select " <<
id <<
" i) ";
4384 out <<
")))" <<
"\n";
4390 else if(expr.
id()==ID_array)
4397 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4398 out <<
"(declare-fun " <<
id <<
" () ";
4402 for(std::size_t i=0; i<expr.
operands().size(); i++)
4404 out <<
"(assert (= (select " <<
id <<
" ";
4408 out <<
"))" <<
"\n";
4414 else if(expr.
id()==ID_string_constant)
4424 out <<
"; the following is a substitute for a string" <<
"\n";
4425 out <<
"(declare-fun " <<
id <<
" () ";
4429 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4431 out <<
"(assert (= (select " << id;
4435 out <<
"))" <<
"\n";
4441 else if(expr.
id() == ID_object_size)
4445 if(op.
type().
id()==ID_pointer)
4451 out <<
"(declare-fun " <<
id <<
" () ";
4462 (expr.
id() == ID_floatbv_plus ||
4463 expr.
id() == ID_floatbv_minus ||
4464 expr.
id() == ID_floatbv_mult ||
4465 expr.
id() == ID_floatbv_div ||
4466 expr.
id() == ID_floatbv_typecast ||
4467 expr.
id() == ID_ieee_float_equal ||
4468 expr.
id() == ID_ieee_float_notequal ||
4469 ((expr.
id() == ID_lt ||
4470 expr.
id() == ID_gt ||
4471 expr.
id() == ID_le ||
4472 expr.
id() == ID_ge ||
4473 expr.
id() == ID_isnan ||
4474 expr.
id() == ID_isnormal ||
4475 expr.
id() == ID_isfinite ||
4476 expr.
id() == ID_isinf ||
4477 expr.
id() == ID_sign ||
4478 expr.
id() == ID_unary_minus ||
4479 expr.
id() == ID_typecast ||
4480 expr.
id() == ID_abs) &&
4487 if(
bvfp_set.insert(
function).second)
4489 out <<
"; this is a model for " << expr.
id() <<
" : "
4492 <<
"(define-fun " <<
function <<
" (";
4494 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4498 out <<
"(op" << i <<
' ';
4508 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4535 if(expr.
id()==ID_with)
4537 else if(expr.
id()==ID_member)
4546 if(type.
id()==ID_array)
4559 out <<
"(_ BitVec 1)";
4565 else if(type.
id()==ID_bool)
4569 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4579 width != 0,
"failed to get width of struct");
4581 out <<
"(_ BitVec " << width <<
")";
4584 else if(type.
id()==ID_vector)
4594 width != 0,
"failed to get width of vector");
4596 out <<
"(_ BitVec " << width <<
")";
4599 else if(type.
id()==ID_code)
4606 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
4611 out <<
"(_ BitVec " << width <<
")";
4613 else if(type.
id()==ID_pointer)
4618 else if(type.
id()==ID_bv ||
4619 type.
id()==ID_fixedbv ||
4620 type.
id()==ID_unsignedbv ||
4621 type.
id()==ID_signedbv ||
4622 type.
id()==ID_c_bool)
4627 else if(type.
id()==ID_c_enum)
4633 else if(type.
id()==ID_c_enum_tag)
4637 else if(type.
id()==ID_floatbv)
4642 out <<
"(_ FloatingPoint "
4643 << floatbv_type.
get_e() <<
" "
4644 << floatbv_type.
get_f() + 1 <<
")";
4649 else if(type.
id()==ID_rational ||
4652 else if(type.
id()==ID_integer)
4654 else if(type.
id()==ID_complex)
4664 width != 0,
"failed to get width of complex");
4666 out <<
"(_ BitVec " << width <<
")";
4669 else if(type.
id()==ID_c_bit_field)
4681 std::set<irep_idt> recstack;
4687 std::set<irep_idt> &recstack)
4689 if(type.
id()==ID_array)
4695 else if(type.
id()==ID_complex)
4702 const std::string smt_typename =
4706 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4707 <<
"(mk-" << smt_typename;
4709 out <<
" (" << smt_typename <<
".imag ";
4713 out <<
" (" << smt_typename <<
".real ";
4720 else if(type.
id()==ID_vector)
4729 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4731 const std::string smt_typename =
4735 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4736 <<
"(mk-" << smt_typename;
4740 out <<
" (" << smt_typename <<
"." << i <<
" ";
4748 else if(type.
id() == ID_struct)
4751 bool need_decl=
false;
4755 const std::string smt_typename =
4770 const std::string &smt_typename =
datatype_map.at(type);
4781 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4782 <<
"(mk-" << smt_typename <<
" ";
4786 out <<
"(" << smt_typename <<
"." <<
component.get_name()
4792 out <<
"))))" <<
"\n";
4809 for(struct_union_typet::componentst::const_iterator
4810 it=components.begin();
4811 it!=components.end();
4815 out <<
"(define-fun update-" << smt_typename <<
"."
4817 <<
"((s " << smt_typename <<
") "
4820 out <<
")) " << smt_typename <<
" "
4821 <<
"(mk-" << smt_typename
4824 for(struct_union_typet::componentst::const_iterator
4825 it2=components.begin();
4826 it2!=components.end();
4833 out <<
"(" << smt_typename <<
"."
4834 << it2->get_name() <<
" s) ";
4838 out <<
"))" <<
"\n";
4844 else if(type.
id() == ID_union)
4852 else if(type.
id()==ID_code)
4856 for(
const auto ¶m : parameters)
4861 else if(type.
id()==ID_pointer)
4865 else if(type.
id() == ID_struct_tag)
4868 const irep_idt &
id = struct_tag.get_identifier();
4870 if(recstack.find(
id) == recstack.end())
4872 recstack.insert(
id);
4876 else if(type.
id() == ID_union_tag)
4879 const irep_idt &
id = union_tag.get_identifier();
4881 if(recstack.find(
id) == recstack.end())
4883 recstack.insert(
id);
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
bitvector_typet index_type()
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
Array constructor from single element.
const array_typet & type() const
const exprt & size() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
Bit-wise negation of bit-vectors.
std::size_t get_width() const
const membert & get_member(const struct_typet &type, const irep_idt &member) const
The byte swap expression.
std::size_t get_bits_per_byte() const
std::vector< parametert > parameterst
const parameterst & parameters() const
struct configt::bv_encodingt bv_encoding
A constant literal expression.
const irep_idt & get_value() const
void set_value(const irep_idt &value)
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
depth_iteratort depth_end()
depth_iteratort depth_begin()
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
The Boolean constant false.
std::size_t get_fraction_bits() const
Fixed-width bit-vector with signed fixed-point interpretation.
std::size_t get_fraction_bits() const
std::size_t get_integer_bits() const
Semantic type conversion from/to floating-point formats.
Fixed-width bit-vector with IEEE floating-point interpretation.
std::size_t get_f() const
std::size_t get_e() const
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
std::size_t width() const
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt NaN(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void build(const mp_integer &exp, const mp_integer &frac)
The trinary if-then-else operator.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const std::string & id_string() const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
exprt & where()
convenience accessor for binding().where()
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
literalt get_literal() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_identifier() const
The plus expression Associativity is not specified.
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t get_invalid_object() const
numberingt< exprt, irep_hash > objects
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A base class for quantifier expressions.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
const irep_idt & get_identifier() const
void convert_relation(const binary_relation_exprt &)
void convert_type(const typet &)
void unflatten(wheret, const typet &, unsigned nesting=0)
bool use_array_theory(const exprt &)
void find_symbols(const exprt &expr)
std::size_t number_of_solver_calls
void convert_typecast(const typecast_exprt &expr)
tvt l_get(literalt l) const
void convert_update(const exprt &expr)
std::set< irep_idt > bvfp_set
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
void push() override
Unimplemented.
void convert_is_dynamic_object(const unary_exprt &)
void convert_literal(const literalt)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
boolbv_widtht boolbv_width
void convert_constant(const constant_exprt &expr)
std::string floatbv_suffix(const exprt &) const
void flatten2bv(const exprt &)
void convert_div(const div_exprt &expr)
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
std::string type2id(const typet &) const
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
struct_exprt parse_struct(const irept &s, const struct_typet &type)
void convert_mult(const mult_exprt &expr)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
void define_object_size(const irep_idt &id, const exprt &expr)
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
datatype_mapt datatype_map
void convert_mod(const mod_exprt &expr)
std::string convert_identifier(const irep_idt &identifier)
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
void convert_member(const member_exprt &expr)
void convert_index(const index_exprt &expr)
pointer_logict pointer_logic
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...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
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'.
defined_expressionst object_sizes
exprt parse_rec(const irept &s, const typet &type)
void write_footer(std::ostream &)
void convert_union(const union_exprt &expr)
exprt parse_union(const irept &s, const union_typet &type)
exprt parse_array(const irept &s, const array_typet &type)
std::vector< bool > boolean_assignment
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
void convert_with(const with_exprt &expr)
std::vector< exprt > assumptions
void convert_plus(const plus_exprt &expr)
defined_expressionst defined_expressions
void pop() override
Currently, only implements a single stack element (no nested contexts)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
identifier_mapt identifier_map
void convert_minus(const minus_exprt &expr)
void convert_expr(const exprt &)
constant_exprt parse_literal(const irept &, const typet &type)
std::size_t no_boolean_variables
smt2_identifierst smt2_identifiers
void convert_floatbv(const exprt &expr)
resultt dec_solve() override
Run the decision procedure to solve the problem.
literalt convert(const exprt &expr)
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const irep_idt & get_name() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
const componentst & components() const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
Generic base class for unary expressions.
The unary minus expression.
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
const constant_exprt & size() const
Operator to update elements in structs and arrays.
#define forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Deprecated expression utility functions.
exprt float_bv(const exprt &src)
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const std::string & id2string(const irep_idt &d)
static std::string binary(const constant_exprt &src)
bool is_true(const literalt &l)
literalt const_literal(bool value)
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
const std::string integer2binary(const mp_integer &n, std::size_t width)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
exprt object_size(const exprt &pointer)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define UNEXPECTEDCASE(S)
int solver(std::istream &in)
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...
bool has_byte_operator(const exprt &src)
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.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#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...
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
std::size_t unsafe_string2size_t(const std::string &str, int base)
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.