Go to the documentation of this file.
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 <<
" () ";
4379 #if 0 // not really working in any solver yet!
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);
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'.
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 extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
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.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
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.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Vector constructor from list of elements.
bool is_true() const
Return whether the expression is a constant representing true.
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
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
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 floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
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...
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
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 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.
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 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.
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 isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
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.
API to expression classes for Pointers.
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 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 shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
numberingt< exprt, irep_hash > objects
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
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Bit-wise negation of bit-vectors.
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 and rotate 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 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.
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)
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
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)
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
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
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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 isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
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
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
API to expression classes for bitvectors.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
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