Go to the documentation of this file.
44 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
47 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
51 const std::string &_benchmark,
52 const std::string &_notes,
53 const std::string &_logic,
56 : use_FPA_theory(false),
57 use_array_of_bool(false),
59 use_check_sat_assuming(false),
61 use_lambda_for_array(false),
65 benchmark(_benchmark),
71 no_boolean_variables(0)
141 "variable number shall be within bounds");
147 out <<
"; SMT 2" <<
"\n";
155 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
164 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
166 out <<
"(set-option :produce-models true)" <<
"\n";
172 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
185 os <<
"(check-sat-assuming (";
195 os <<
"; assumptions\n";
206 os <<
"(check-sat)\n";
214 os <<
"(get-value (|" <<
id <<
"|))"
222 os <<
"; end of SMT2 file"
234 std::size_t number = 0;
235 std::size_t h=pointer_width-1;
240 const typet &type = o.type();
243 numeric_cast<mp_integer>(size_expr.value_or(
nil_exprt()));
246 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
247 !size_expr.has_value() || !
object_size.has_value())
253 out <<
"(assert (=> (= "
254 <<
"((_ extract " << h <<
" " << l <<
") ";
257 <<
"(= " <<
id <<
" (_ bv" << *
object_size <<
" " << size_width
273 if(expr.
id()==ID_symbol)
280 return it->second.value;
282 else if(expr.
id()==ID_nondet_symbol)
289 return it->second.value;
291 else if(expr.
id()==ID_member)
299 else if(expr.
id() == ID_literal)
307 else if(expr.
id() == ID_not)
312 else if(op.is_false())
348 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
353 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
364 else if(src.
get_sub().size()==2 &&
369 else if(src.
get_sub().size()==3 &&
372 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
376 else if(src.
get_sub().size()==4 &&
379 if(type.
id()==ID_floatbv)
388 const auto s1_int = numeric_cast_v<mp_integer>(
s1);
389 const auto s2_int = numeric_cast_v<mp_integer>(
s2);
390 const auto s3_int = numeric_cast_v<mp_integer>(s3);
394 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
400 else if(src.
get_sub().size()==4 &&
408 else if(src.
get_sub().size()==4 &&
416 else if(src.
get_sub().size()==4 &&
425 if(type.
id()==ID_signedbv ||
426 type.
id()==ID_unsignedbv ||
427 type.
id()==ID_c_enum ||
428 type.
id()==ID_c_bool)
432 else if(type.
id()==ID_c_enum_tag)
438 result.
type() = type;
441 else if(type.
id()==ID_fixedbv ||
442 type.
id()==ID_floatbv)
447 else if(type.
id()==ID_integer ||
455 "smt2_convt::parse_literal should not be of unsupported type " +
475 else if(src.
get_sub().size()==2 &&
476 src.
get_sub()[0].get_sub().size()==3 &&
477 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
478 src.
get_sub()[0].get_sub()[1].id()==
"const")
512 if(components.empty())
520 if(src.
get_sub().size()!=components.size()+1)
523 for(std::size_t i=0; i<components.size(); i++)
540 std::size_t offset=0;
542 for(std::size_t i=0; i<components.size(); i++)
544 std::size_t component_width=
boolbv_width(components[i].type());
547 offset + component_width <= total_width,
548 "struct component bits shall be within struct bit vector");
550 std::string component_binary=
552 total_width-offset-component_width, component_width);
557 offset+=component_width;
567 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
568 type.
id() == ID_integer || type.
id() == ID_rational ||
569 type.
id() == ID_real || type.
id() == ID_c_enum ||
570 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
571 type.
id() == ID_floatbv)
575 else if(type.
id()==ID_bool)
577 if(src.
id()==ID_1 || src.
id()==ID_true)
579 else if(src.
id()==ID_0 || src.
id()==ID_false)
582 else if(type.
id()==ID_pointer)
588 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
593 ptr.
object = numeric_cast_v<std::size_t>(v / pow);
597 else if(type.
id()==ID_struct)
601 else if(type.
id() == ID_struct_tag)
606 struct_expr.type() = type;
607 return std::move(struct_expr);
609 else if(type.
id()==ID_union)
613 else if(type.
id() == ID_union_tag)
617 union_expr.type() = type;
620 else if(type.
id()==ID_array)
632 if(expr.
id()==ID_symbol ||
633 expr.
id()==ID_constant ||
634 expr.
id()==ID_string_constant ||
644 else if(expr.
id()==ID_index)
653 if(array.
type().
id()==ID_pointer)
655 else if(array.
type().
id()==ID_array)
675 else if(expr.
id()==ID_member)
680 const typet &struct_op_type = struct_op.
type();
683 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
684 "member expression operand shall have struct type");
701 else if(expr.
id()==ID_if)
716 "operand of address of expression should not be of kind " +
730 else if(expr.
id()==ID_literal)
742 out <<
"; convert\n";
743 out <<
"(define-fun ";
755 if(expr.
type().
id() != ID_bool)
806 for(std::size_t i=0; i<identifier.
size(); i++)
808 char ch=identifier[i];
831 if(type.
id()==ID_floatbv)
836 else if(type.
id()==ID_unsignedbv)
840 else if(type.
id()==ID_c_bool)
844 else if(type.
id()==ID_signedbv)
848 else if(type.
id()==ID_bool)
852 else if(type.
id()==ID_c_enum_tag)
856 else if(type.
id() == ID_pointer)
877 if(expr.
id()==ID_symbol)
884 if(expr.
id()==ID_smt2_symbol)
892 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
894 out <<
"(|float_bv." << expr.
id()
910 if(expr.
id()==ID_symbol)
916 else if(expr.
id()==ID_nondet_symbol)
919 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
922 else if(expr.
id()==ID_smt2_symbol)
928 else if(expr.
id()==ID_typecast)
932 else if(expr.
id()==ID_floatbv_typecast)
936 else if(expr.
id()==ID_struct)
940 else if(expr.
id()==ID_union)
944 else if(expr.
id()==ID_constant)
948 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
952 "concatenation over a single operand should have matching types",
957 else if(expr.
id()==ID_concatenation ||
958 expr.
id()==ID_bitand ||
959 expr.
id()==ID_bitor ||
960 expr.
id()==ID_bitxor ||
961 expr.
id()==ID_bitnand ||
962 expr.
id()==ID_bitnor)
966 "given expression should have at least two operands",
971 if(expr.
id()==ID_concatenation)
973 else if(expr.
id()==ID_bitand)
975 else if(expr.
id()==ID_bitor)
977 else if(expr.
id()==ID_bitxor)
979 else if(expr.
id()==ID_bitnand)
981 else if(expr.
id()==ID_bitnor)
992 else if(expr.
id()==ID_bitnot)
996 if(bitnot_expr.
type().
id() == ID_vector)
1005 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1007 out <<
"(let ((?vectorop ";
1011 out <<
"(mk-" << smt_typename;
1018 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
1034 else if(expr.
id()==ID_unary_minus)
1039 unary_minus_expr.
type().
id() == ID_rational ||
1040 unary_minus_expr.
type().
id() == ID_integer ||
1041 unary_minus_expr.
type().
id() == ID_real)
1047 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1059 else if(unary_minus_expr.
type().
id() == ID_vector)
1063 const std::string &smt_typename =
1070 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1072 out <<
"(let ((?vectorop ";
1076 out <<
"(mk-" << smt_typename;
1083 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1099 else if(expr.
id()==ID_unary_plus)
1104 else if(expr.
id()==ID_sign)
1110 if(op_type.
id()==ID_floatbv)
1114 out <<
"(fp.isNegative ";
1121 else if(op_type.
id()==ID_signedbv)
1127 out <<
" (_ bv0 " << op_width <<
"))";
1132 "sign should not be applied to unsupported type",
1135 else if(expr.
id()==ID_if)
1147 else if(expr.
id()==ID_and ||
1152 expr.
type().
id() == ID_bool,
1153 "logical and, or, and xor expressions should have Boolean type");
1156 "logical and, or, and xor expressions should have at least two operands");
1158 out <<
"(" << expr.
id();
1166 else if(expr.
id()==ID_implies)
1171 implies_expr.
type().
id() == ID_bool,
1172 "implies expression should have Boolean type");
1180 else if(expr.
id()==ID_not)
1185 not_expr.
type().
id() == ID_bool,
1186 "not expression should have Boolean type");
1192 else if(expr.
id() == ID_equal)
1198 "operands of equal expression shall have same type");
1206 else if(expr.
id() == ID_notequal)
1212 "operands of not equal expression shall have same type");
1220 else if(expr.
id()==ID_ieee_float_equal ||
1221 expr.
id()==ID_ieee_float_notequal)
1228 rel_expr.lhs().type() == rel_expr.rhs().type(),
1229 "operands of float equal and not equal expressions shall have same type");
1234 if(rel_expr.id() == ID_ieee_float_notequal)
1243 if(rel_expr.id() == ID_ieee_float_notequal)
1249 else if(expr.
id()==ID_le ||
1256 else if(expr.
id()==ID_plus)
1260 else if(expr.
id()==ID_floatbv_plus)
1264 else if(expr.
id()==ID_minus)
1268 else if(expr.
id()==ID_floatbv_minus)
1272 else if(expr.
id()==ID_div)
1276 else if(expr.
id()==ID_floatbv_div)
1280 else if(expr.
id()==ID_mod)
1284 else if(expr.
id()==ID_mult)
1288 else if(expr.
id()==ID_floatbv_mult)
1292 else if(expr.
id()==ID_address_of)
1298 else if(expr.
id() == ID_array_of)
1303 array_of_expr.type().id() == ID_array,
1304 "array of expression shall have array type");
1308 out <<
"((as const ";
1316 defined_expressionst::const_iterator it =
1322 else if(expr.
id() == ID_array_comprehension)
1327 array_comprehension.type().id() == ID_array,
1328 "array_comprehension expression shall have array type");
1332 out <<
"(lambda ((";
1335 convert_type(array_comprehension.type().size().type());
1347 else if(expr.
id()==ID_index)
1351 else if(expr.
id()==ID_ashr ||
1352 expr.
id()==ID_lshr ||
1358 if(type.
id()==ID_unsignedbv ||
1359 type.
id()==ID_signedbv ||
1362 if(shift_expr.
id() == ID_ashr)
1364 else if(shift_expr.
id() == ID_lshr)
1366 else if(shift_expr.
id() == ID_shl)
1396 if(width_op0==width_op1)
1398 else if(width_op0>width_op1)
1400 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1406 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1413 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1420 "unsupported type for " + shift_expr.
id_string() +
": " +
1423 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1429 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1434 if(shift_expr.
id() == ID_rol)
1435 out <<
"((_ rotate_left";
1436 else if(shift_expr.
id() == ID_ror)
1437 out <<
"((_ rotate_right";
1443 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.
distance());
1445 if(distance_int_op.has_value())
1447 out << distance_int_op.value();
1451 "distance type for " + shift_expr.
id_string() +
"must be constant");
1460 "unsupported type for " + shift_expr.
id_string() +
": " +
1463 else if(expr.
id()==ID_with)
1467 else if(expr.
id()==ID_update)
1471 else if(expr.
id()==ID_member)
1475 else if(expr.
id()==ID_pointer_offset)
1480 op.type().id() == ID_pointer,
1481 "operand of pointer offset expression shall be of pointer type");
1483 std::size_t offset_bits =
1488 if(offset_bits>result_width)
1489 offset_bits=result_width;
1492 if(result_width>offset_bits)
1493 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1495 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1499 if(result_width>offset_bits)
1502 else if(expr.
id()==ID_pointer_object)
1507 op.type().id() == ID_pointer,
1508 "pointer object expressions should be of pointer type");
1514 out <<
"((_ zero_extend " << ext <<
") ";
1516 out <<
"((_ extract "
1517 << pointer_width-1 <<
" "
1525 else if(expr.
id() == ID_is_dynamic_object)
1529 else if(expr.
id() == ID_is_invalid_pointer)
1533 out <<
"(= ((_ extract "
1534 << pointer_width-1 <<
" "
1540 else if(expr.
id()==ID_string_constant)
1546 else if(expr.
id()==ID_extractbit)
1555 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1561 out <<
"(= ((_ extract 0 0) ";
1570 else if(expr.
id()==ID_extractbits)
1584 std::swap(op1_i, op2_i);
1588 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1595 out <<
"(= ((_ extract 0 0) ";
1604 SMT2_TODO(
"smt2: extractbits with non-constant index");
1607 else if(expr.
id()==ID_replication)
1611 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1613 out <<
"((_ repeat " << times <<
") ";
1617 else if(expr.
id()==ID_byte_extract_little_endian ||
1618 expr.
id()==ID_byte_extract_big_endian)
1621 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1623 else if(expr.
id()==ID_byte_update_little_endian ||
1624 expr.
id()==ID_byte_update_big_endian)
1627 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1629 else if(expr.
id()==ID_abs)
1635 if(type.
id()==ID_signedbv)
1639 out <<
"(ite (bvslt ";
1641 out <<
" (_ bv0 " << result_width <<
")) ";
1648 else if(type.
id()==ID_fixedbv)
1652 out <<
"(ite (bvslt ";
1654 out <<
" (_ bv0 " << result_width <<
")) ";
1661 else if(type.
id()==ID_floatbv)
1675 else if(expr.
id()==ID_isnan)
1681 if(op_type.
id()==ID_fixedbv)
1683 else if(op_type.
id()==ID_floatbv)
1687 out <<
"(fp.isNaN ";
1697 else if(expr.
id()==ID_isfinite)
1703 if(op_type.
id()==ID_fixedbv)
1705 else if(op_type.
id()==ID_floatbv)
1711 out <<
"(not (fp.isNaN ";
1715 out <<
"(not (fp.isInf ";
1727 else if(expr.
id()==ID_isinf)
1733 if(op_type.
id()==ID_fixedbv)
1735 else if(op_type.
id()==ID_floatbv)
1739 out <<
"(fp.isInfinite ";
1749 else if(expr.
id()==ID_isnormal)
1755 if(op_type.
id()==ID_fixedbv)
1757 else if(op_type.
id()==ID_floatbv)
1761 out <<
"(fp.isNormal ";
1771 else if(expr.
id()==ID_overflow_plus ||
1772 expr.
id()==ID_overflow_minus)
1778 expr.
type().
id() == ID_bool,
1779 "overflow plus and overflow minus expressions shall be of Boolean type");
1781 bool subtract=expr.
id()==ID_overflow_minus;
1782 const typet &op_type = op0.type();
1785 if(op_type.
id()==ID_signedbv)
1788 out <<
"(let ((?sum (";
1789 out << (subtract?
"bvsub":
"bvadd");
1790 out <<
" ((_ sign_extend 1) ";
1793 out <<
" ((_ sign_extend 1) ";
1797 "((_ extract " << width <<
" " << width <<
") ?sum) "
1798 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1801 else if(op_type.
id()==ID_unsignedbv ||
1802 op_type.
id()==ID_pointer)
1806 out <<
"((_ extract " << width <<
" " << width <<
") ";
1807 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1808 out <<
" ((_ zero_extend 1) ";
1811 out <<
" ((_ zero_extend 1) ";
1819 "overflow check should not be performed on unsupported type",
1822 else if(expr.
id()==ID_overflow_mult)
1828 expr.
type().
id() == ID_bool,
1829 "overflow mult expression shall be of Boolean type");
1834 const typet &op_type = op0.type();
1837 if(op_type.
id()==ID_signedbv)
1839 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1841 out <<
") ((_ sign_extend " << width <<
") ";
1844 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
1846 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" "
1847 << width*2 <<
")))))";
1849 else if(op_type.
id()==ID_unsignedbv)
1851 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1853 out <<
") ((_ zero_extend " << width <<
") ";
1855 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1860 "overflow check should not be performed on unsupported type",
1863 else if(expr.
id()==ID_array)
1869 else if(expr.
id()==ID_literal)
1873 else if(expr.
id()==ID_forall ||
1874 expr.
id()==ID_exists)
1880 throw "MathSAT does not support quantifiers";
1882 if(quantifier_expr.
id() == ID_forall)
1884 else if(quantifier_expr.
id() == ID_exists)
1899 else if(expr.
id()==ID_vector)
1904 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1907 size == vector_expr.
operands().size(),
1908 "size indicated by type shall be equal to the number of operands");
1912 const std::string &smt_typename =
datatype_map.at(vector_type);
1914 out <<
"(mk-" << smt_typename;
1928 else if(expr.
id()==ID_object_size)
1932 else if(expr.
id()==ID_let)
1935 const auto &variables = let_expr.
variables();
1936 const auto &values = let_expr.
values();
1941 for(
auto &binding :
make_range(variables).zip(values))
1960 else if(expr.
id()==ID_constraint_select_one)
1963 "smt2_convt::convert_expr: '" + expr.
id_string() +
1964 "' is not yet supported");
1966 else if(expr.
id() == ID_bswap)
1972 "operand of byte swap expression shall have same type as the expression");
1975 out <<
"(let ((bswap_op ";
1980 bswap_expr.
type().
id() == ID_signedbv ||
1981 bswap_expr.
type().
id() == ID_unsignedbv)
1983 const std::size_t width =
1990 width % bits_per_byte == 0,
1991 "bit width indicated by type of bswap expression should be a multiple "
1992 "of the number of bits per byte");
1994 const std::size_t bytes = width / bits_per_byte;
2003 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2007 out <<
"(bswap_byte_" <<
byte <<
' ';
2008 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2009 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2018 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2019 out <<
" bswap_byte_" <<
byte;
2030 else if(expr.
id() == ID_popcount)
2034 else if(expr.
id() == ID_count_leading_zeros)
2041 "smt2_convt::convert_expr should not be applied to unsupported type",
2050 if(dest_type.
id()==ID_c_enum_tag)
2054 if(src_type.
id()==ID_c_enum_tag)
2057 if(dest_type.
id()==ID_bool)
2060 if(src_type.
id()==ID_signedbv ||
2061 src_type.
id()==ID_unsignedbv ||
2062 src_type.
id()==ID_c_bool ||
2063 src_type.
id()==ID_fixedbv ||
2064 src_type.
id()==ID_pointer ||
2065 src_type.
id()==ID_integer)
2073 else if(src_type.
id()==ID_floatbv)
2077 out <<
"(not (fp.isZero ";
2089 else if(dest_type.
id()==ID_c_bool)
2098 out <<
" (_ bv1 " << to_width <<
")";
2099 out <<
" (_ bv0 " << to_width <<
")";
2102 else if(dest_type.
id()==ID_signedbv ||
2103 dest_type.
id()==ID_unsignedbv ||
2104 dest_type.
id()==ID_c_enum ||
2105 dest_type.
id()==ID_bv)
2109 if(src_type.
id()==ID_signedbv ||
2110 src_type.
id()==ID_unsignedbv ||
2111 src_type.
id()==ID_c_bool ||
2112 src_type.
id()==ID_c_enum ||
2113 src_type.
id()==ID_bv)
2117 if(from_width==to_width)
2119 else if(from_width<to_width)
2121 if(src_type.
id()==ID_signedbv)
2122 out <<
"((_ sign_extend ";
2124 out <<
"((_ zero_extend ";
2126 out << (to_width-from_width)
2133 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2138 else if(src_type.
id()==ID_fixedbv)
2142 std::size_t from_width=fixedbv_type.
get_width();
2149 out <<
"(let ((?tcop ";
2155 if(to_width>from_integer_bits)
2157 out <<
"((_ sign_extend "
2158 << (to_width-from_integer_bits) <<
") ";
2159 out <<
"((_ extract " << (from_width-1) <<
" "
2160 << from_fraction_bits <<
") ";
2166 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2167 <<
" " << from_fraction_bits <<
") ";
2172 out <<
" (ite (and ";
2175 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2176 "(_ bv0 " << from_fraction_bits <<
")))";
2179 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2184 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2188 else if(src_type.
id()==ID_floatbv)
2190 if(dest_type.
id()==ID_bv)
2207 else if(dest_type.
id()==ID_signedbv)
2211 "typecast unexpected "+src_type.
id_string()+
" -> "+
2214 else if(dest_type.
id()==ID_unsignedbv)
2218 "typecast unexpected "+src_type.
id_string()+
" -> "+
2222 else if(src_type.
id()==ID_bool)
2227 if(dest_type.
id()==ID_fixedbv)
2230 out <<
" (concat (_ bv1 "
2233 "(_ bv0 " << spec.
width <<
")";
2237 out <<
" (_ bv1 " << to_width <<
")";
2238 out <<
" (_ bv0 " << to_width <<
")";
2243 else if(src_type.
id()==ID_pointer)
2247 if(from_width<to_width)
2249 out <<
"((_ sign_extend ";
2250 out << (to_width-from_width)
2257 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2262 else if(src_type.
id()==ID_integer)
2268 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2271 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2274 src_type.
id() == ID_struct ||
2275 src_type.
id() == ID_struct_tag)
2281 "bit vector with of source and destination type shall be equal");
2288 "bit vector with of source and destination type shall be equal");
2293 src_type.
id() == ID_union ||
2294 src_type.
id() == ID_union_tag)
2298 "bit vector with of source and destination type shall be equal");
2301 else if(src_type.
id()==ID_c_bit_field)
2305 if(from_width==to_width)
2316 std::ostringstream e_str;
2317 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2318 <<
" src == " <<
format(src);
2322 else if(dest_type.
id()==ID_fixedbv)
2328 if(src_type.
id()==ID_unsignedbv ||
2329 src_type.
id()==ID_signedbv ||
2330 src_type.
id()==ID_c_enum)
2337 if(from_width==to_integer_bits)
2339 else if(from_width>to_integer_bits)
2342 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2350 from_width < to_integer_bits,
2351 "from_width should be smaller than to_integer_bits as other case "
2352 "have been handled above");
2353 if(dest_type.
id()==ID_unsignedbv)
2355 out <<
"(_ zero_extend "
2356 << (to_integer_bits-from_width) <<
") ";
2362 out <<
"((_ sign_extend "
2363 << (to_integer_bits-from_width) <<
") ";
2369 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2372 else if(src_type.
id()==ID_bool)
2374 out <<
"(concat (concat"
2375 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2381 else if(src_type.
id()==ID_fixedbv)
2386 std::size_t from_width=from_fixedbv_type.
get_width();
2388 out <<
"(let ((?tcop ";
2394 if(to_integer_bits<=from_integer_bits)
2396 out <<
"((_ extract "
2397 << (from_fraction_bits+to_integer_bits-1) <<
" "
2398 << from_fraction_bits
2404 to_integer_bits > from_integer_bits,
2405 "to_integer_bits should be greater than from_integer_bits as the"
2406 "other case has been handled above");
2407 out <<
"((_ sign_extend "
2408 << (to_integer_bits-from_integer_bits)
2410 << (from_width-1) <<
" "
2411 << from_fraction_bits
2417 if(to_fraction_bits<=from_fraction_bits)
2419 out <<
"((_ extract "
2420 << (from_fraction_bits-1) <<
" "
2421 << (from_fraction_bits-to_fraction_bits)
2427 to_fraction_bits > from_fraction_bits,
2428 "to_fraction_bits should be greater than from_fraction_bits as the"
2429 "other case has been handled above");
2430 out <<
"(concat ((_ extract "
2431 << (from_fraction_bits-1) <<
" 0) ";
2434 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2443 else if(dest_type.
id()==ID_pointer)
2447 if(src_type.
id()==ID_pointer)
2453 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2454 src_type.
id() == ID_bv)
2460 if(from_width==to_width)
2462 else if(from_width<to_width)
2464 out <<
"((_ sign_extend "
2465 << (to_width-from_width)
2472 out <<
"((_ extract " << to_width <<
" 0) ";
2480 else if(dest_type.
id()==ID_range)
2484 else if(dest_type.
id()==ID_floatbv)
2493 if(src_type.
id()==ID_bool)
2508 a.
build(significand, exponent);
2516 a.
build(significand, exponent);
2522 else if(src_type.
id()==ID_c_bool)
2528 else if(src_type.
id() == ID_bv)
2537 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2538 << dest_floatbv_type.get_f() + 1 <<
") ";
2548 else if(dest_type.
id()==ID_integer)
2550 if(src_type.
id()==ID_bool)
2559 else if(dest_type.
id()==ID_c_bit_field)
2564 if(from_width==to_width)
2585 if(dest_type.
id()==ID_floatbv)
2587 if(src_type.
id()==ID_floatbv)
2614 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2615 << dst.
get_f() + 1 <<
") ";
2624 else if(src_type.
id()==ID_unsignedbv)
2645 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
2646 << dst.
get_f() + 1 <<
") ";
2655 else if(src_type.
id()==ID_signedbv)
2663 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2664 << dst.
get_f() + 1 <<
") ";
2673 else if(src_type.
id()==ID_c_enum_tag)
2689 else if(dest_type.
id()==ID_signedbv)
2694 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2703 else if(dest_type.
id()==ID_unsignedbv)
2708 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2732 components.size() == expr.
operands().size(),
2733 "number of struct components as indicated by the struct type shall be equal"
2734 "to the number of operands of the struct expression");
2736 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2740 const std::string &smt_typename =
datatype_map.at(struct_type);
2743 out <<
"(mk-" << smt_typename;
2746 for(struct_typet::componentst::const_iterator
2747 it=components.begin();
2748 it!=components.end();
2759 if(components.size()==1)
2764 for(std::size_t i=components.size(); i>1; i--)
2771 if(op.
type().
id() == ID_array)
2781 for(std::size_t i=1; i<components.size(); i++)
2791 const auto &size_expr = array_type.
size();
2797 out <<
"(let ((?far ";
2805 out <<
"(select ?far ";
2826 total_width != 0,
"failed to get union width for union");
2830 member_width != 0,
"failed to get union member width for union");
2832 if(total_width==member_width)
2840 total_width > member_width,
2841 "total_width should be greater than member_width as member_width can be"
2842 "at most as large as total_width and the other case has been handled "
2846 << (total_width-member_width) <<
") ";
2856 if(expr_type.
id()==ID_unsignedbv ||
2857 expr_type.
id()==ID_signedbv ||
2858 expr_type.
id()==ID_bv ||
2859 expr_type.
id()==ID_c_enum ||
2860 expr_type.
id()==ID_c_enum_tag ||
2861 expr_type.
id()==ID_c_bool ||
2862 expr_type.
id()==ID_c_bit_field)
2868 out <<
"(_ bv" << value
2869 <<
" " << width <<
")";
2871 else if(expr_type.
id()==ID_fixedbv)
2877 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2879 else if(expr_type.
id()==ID_floatbv)
2892 size_t e=floatbv_type.
get_e();
2893 size_t f=floatbv_type.
get_f()+1;
2899 out <<
"((_ to_fp " << e <<
" " << f <<
")"
2905 out <<
"(_ NaN " << e <<
" " << f <<
")";
2910 out <<
"(_ -oo " << e <<
" " << f <<
")";
2912 out <<
"(_ +oo " << e <<
" " << f <<
")";
2922 <<
"#b" << binaryString.substr(0, 1) <<
" "
2923 <<
"#b" << binaryString.substr(1, e) <<
" "
2924 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
2932 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
2935 else if(expr_type.
id()==ID_pointer)
2947 else if(expr_type.
id()==ID_bool)
2956 else if(expr_type.
id()==ID_array)
2962 else if(expr_type.
id()==ID_rational)
2965 size_t pos=value.find(
"/");
2967 if(
pos==std::string::npos)
2968 out << value <<
".0";
2971 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
2972 << value.substr(
pos+1) <<
".0)";
2975 else if(expr_type.
id()==ID_integer)
2985 if(expr.
type().
id()==ID_unsignedbv ||
2986 expr.
type().
id()==ID_signedbv)
2988 if(expr.
type().
id()==ID_unsignedbv)
3004 std::vector<std::size_t> dynamic_objects;
3007 if(dynamic_objects.empty())
3013 out <<
"(let ((?obj ((_ extract "
3014 << pointer_width-1 <<
" "
3019 if(dynamic_objects.size()==1)
3021 out <<
"(= (_ bv" << dynamic_objects.front()
3028 for(
const auto &
object : dynamic_objects)
3029 out <<
" (= (_ bv" <<
object
3043 if(op_type.
id()==ID_unsignedbv ||
3044 op_type.
id()==ID_pointer ||
3045 op_type.
id()==ID_bv)
3048 if(expr.
id()==ID_le)
3050 else if(expr.
id()==ID_lt)
3052 else if(expr.
id()==ID_ge)
3054 else if(expr.
id()==ID_gt)
3063 else if(op_type.
id()==ID_signedbv ||
3064 op_type.
id()==ID_fixedbv)
3067 if(expr.
id()==ID_le)
3069 else if(expr.
id()==ID_lt)
3071 else if(expr.
id()==ID_ge)
3073 else if(expr.
id()==ID_gt)
3082 else if(op_type.
id()==ID_floatbv)
3087 if(expr.
id()==ID_le)
3089 else if(expr.
id()==ID_lt)
3091 else if(expr.
id()==ID_ge)
3093 else if(expr.
id()==ID_gt)
3105 else if(op_type.
id()==ID_rational ||
3106 op_type.
id()==ID_integer)
3125 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3126 expr.
type().
id() == ID_real)
3131 for(
const auto &op : expr.
operands())
3140 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3141 expr.
type().
id() == ID_fixedbv)
3158 else if(expr.
type().
id() == ID_floatbv)
3165 else if(expr.
type().
id() == ID_pointer)
3171 if(p.
type().
id() != ID_pointer)
3175 p.
type().
id() == ID_pointer,
3176 "one of the operands should have pointer type");
3188 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3189 element_size = *element_size_opt;
3196 if(element_size >= 2)
3213 else if(expr.
type().
id() == ID_vector)
3217 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3223 const std::string &smt_typename =
datatype_map.at(vector_type);
3225 out <<
"(mk-" << smt_typename;
3234 summands.reserve(expr.
operands().size());
3235 for(
const auto &op : expr.
operands())
3267 if(expr.
id()==ID_constant)
3271 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3274 out <<
"roundNearestTiesToEven";
3276 out <<
"roundTowardNegative";
3278 out <<
"roundTowardPositive";
3280 out <<
"roundTowardZero";
3284 "Rounding mode should have value 0, 1, 2, or 3",
3292 out <<
"(ite (= (_ bv0 " << width <<
") ";
3294 out <<
") roundNearestTiesToEven ";
3296 out <<
"(ite (= (_ bv1 " << width <<
") ";
3298 out <<
") roundTowardNegative ";
3300 out <<
"(ite (= (_ bv2 " << width <<
") ";
3302 out <<
") roundTowardPositive ";
3305 out <<
"roundTowardZero";
3316 type.
id() == ID_floatbv ||
3317 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv) ||
3318 (type.
id() == ID_vector && type.
subtype().
id() == ID_floatbv));
3322 if(type.
id()==ID_floatbv)
3332 else if(type.
id()==ID_complex)
3336 else if(type.
id()==ID_vector)
3343 "type should not be one of the unsupported types",
3352 if(expr.
type().
id()==ID_integer)
3360 else if(expr.
type().
id()==ID_unsignedbv ||
3361 expr.
type().
id()==ID_signedbv ||
3362 expr.
type().
id()==ID_fixedbv)
3364 if(expr.
op0().
type().
id()==ID_pointer &&
3369 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3371 if(*element_size >= 2)
3376 "bitvector width of operand shall be equal to the bitvector width of "
3385 if(*element_size >= 2)
3398 else if(expr.
type().
id()==ID_floatbv)
3405 else if(expr.
type().
id()==ID_pointer)
3409 else if(expr.
type().
id()==ID_vector)
3413 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3419 const std::string &smt_typename =
datatype_map.at(vector_type);
3421 out <<
"(mk-" << smt_typename;
3450 expr.
type().
id() == ID_floatbv,
3451 "type of ieee floating point expression shall be floatbv");
3469 if(expr.
type().
id()==ID_unsignedbv ||
3470 expr.
type().
id()==ID_signedbv)
3472 if(expr.
type().
id()==ID_unsignedbv)
3482 else if(expr.
type().
id()==ID_fixedbv)
3487 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3492 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3494 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3500 else if(expr.
type().
id()==ID_floatbv)
3514 expr.
type().
id() == ID_floatbv,
3515 "type of ieee floating point expression shall be floatbv");
3546 "expression should have been converted to a variant with two operands");
3548 if(expr.
type().
id()==ID_unsignedbv ||
3549 expr.
type().
id()==ID_signedbv)
3560 else if(expr.
type().
id()==ID_floatbv)
3567 else if(expr.
type().
id()==ID_fixedbv)
3572 out <<
"((_ extract "
3573 << spec.
width+fraction_bits-1 <<
" "
3574 << fraction_bits <<
") ";
3578 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3582 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3588 else if(expr.
type().
id()==ID_rational ||
3589 expr.
type().
id()==ID_integer ||
3590 expr.
type().
id()==ID_real)
3609 expr.
type().
id() == ID_floatbv,
3610 "type of ieee floating point expression shall be floatbv");
3632 std::size_t s=expr.
operands().size();
3647 "with expression should have been converted to a version with three "
3652 if(expr_type.
id()==ID_array)
3676 out <<
"(let ((distance? ";
3677 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3681 if(array_width>index_width)
3683 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3689 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3699 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
3701 out <<
"distance?)) ";
3705 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3707 out <<
") distance?)))";
3710 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
3717 const irep_idt &component_name=index.
get(ID_component_name);
3721 "struct should have accessed component");
3725 const std::string &smt_typename =
datatype_map.at(expr_type);
3727 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3741 out <<
"(let ((?withop ";
3745 if(m.
width==struct_width)
3755 <<
"((_ extract " << (struct_width-1) <<
" "
3756 << m.
width <<
") ?withop) ";
3765 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
3770 out <<
"(concat (concat "
3771 <<
"((_ extract " << (struct_width-1) <<
" "
3774 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3781 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
3789 total_width != 0,
"failed to get union width for with");
3793 member_width != 0,
"failed to get union member width for with");
3795 if(total_width==member_width)
3802 total_width > member_width,
3803 "total width should be greater than member_width as member_width is at "
3804 "most as large as total_width and the other case has been handled "
3807 out <<
"((_ extract "
3809 <<
" " << member_width <<
") ";
3816 else if(expr_type.
id()==ID_bv ||
3817 expr_type.
id()==ID_unsignedbv ||
3818 expr_type.
id()==ID_signedbv)
3824 total_width != 0,
"failed to get total width");
3831 value_width != 0,
"failed to get value width");
3843 out <<
" (bvnot (bvshl";
3846 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3847 out <<
" (repeat[" << value_width <<
"] bv1[1])";
3869 "with expects struct, union, or array type, but got "+
3877 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
3884 if(array_op_type.
id()==ID_array)
3920 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
3924 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3928 if(array_width>index_width)
3930 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3936 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3946 else if(array_op_type.
id()==ID_vector)
3952 const std::string &smt_typename =
datatype_map.at(vector_type);
3956 const auto index_int = numeric_cast<mp_integer>(expr.
index());
3957 if(!index_int.has_value())
3959 SMT2_TODO(
"non-constant index on vectors");
3963 out <<
"(" << smt_typename <<
"." << *index_int <<
" ";
3975 false,
"index with unsupported array type: " + array_op_type.
id_string());
3982 const typet &struct_op_type = struct_op.
type();
3985 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
3990 struct_type.
has_component(name),
"struct should have accessed component");
3994 const std::string &smt_typename =
datatype_map.at(struct_type);
3996 out <<
"(" << smt_typename <<
"."
4009 member_offset.has_value(),
"failed to get struct member offset");
4018 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4022 width != 0,
"failed to get union member width");
4026 out <<
"((_ extract "
4036 "convert_member on an unexpected type "+struct_op_type.
id_string());
4043 if(type.
id()==ID_bool)
4049 else if(type.
id()==ID_vector)
4053 const std::string &smt_typename =
datatype_map.at(type);
4058 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4060 out <<
"(let ((?vflop ";
4068 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
4076 else if(type.
id()==ID_array)
4080 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4084 const std::string &smt_typename =
datatype_map.at(type);
4089 out <<
"(let ((?sflop ";
4097 for(std::size_t i=components.size(); i>1; i--)
4099 out <<
"(concat (" << smt_typename <<
"."
4100 << components[i-1].get_name() <<
" ?sflop)";
4105 out <<
"(" << smt_typename <<
"."
4106 << components[0].get_name() <<
" ?sflop)";
4108 for(std::size_t i=1; i<components.size(); i++)
4116 else if(type.
id()==ID_floatbv)
4120 "floatbv expressions should be flattened when using FPA theory");
4133 if(type.
id()==ID_bool)
4140 else if(type.
id()==ID_vector)
4144 const std::string &smt_typename =
datatype_map.at(type);
4151 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4154 out <<
"(let ((?ufop" << nesting <<
" ";
4159 out <<
"(mk-" << smt_typename;
4161 std::size_t offset=0;
4163 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4167 out <<
"((_ extract " << offset+subtype_width-1 <<
" "
4168 << offset <<
") ?ufop" << nesting <<
")";
4180 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4186 out <<
"(let ((?ufop" << nesting <<
" ";
4191 const std::string &smt_typename =
datatype_map.at(type);
4193 out <<
"(mk-" << smt_typename;
4200 std::size_t offset=0;
4203 for(struct_typet::componentst::const_iterator
4204 it=components.begin();
4205 it!=components.end();
4212 out <<
"((_ extract " << offset+member_width-1 <<
" "
4213 << offset <<
") ?ufop" << nesting <<
")";
4215 offset+=member_width;
4236 if(expr.
id()==ID_and && value)
4243 if(expr.
id()==ID_or && !value)
4250 if(expr.
id()==ID_not)
4260 if(expr.
id() == ID_equal && value)
4263 if(equal_expr.
lhs().
type().
id() == ID_empty)
4269 if(equal_expr.
lhs().
id()==ID_symbol)
4279 id.type=equal_expr.
lhs().
type();
4286 out <<
"; set_to true (equal)\n";
4287 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4306 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4331 exprt lowered_expr = expr;
4338 it->id() == ID_byte_extract_little_endian ||
4339 it->id() == ID_byte_extract_big_endian)
4344 it->id() == ID_byte_update_little_endian ||
4345 it->id() == ID_byte_update_big_endian)
4351 return lowered_expr;
4368 "lower_byte_operators should remove all byte operators");
4373 return lowered_expr;
4381 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4386 const auto identifier = q_expr.symbol().get_identifier();
4388 id.type = q_expr.symbol().type();
4398 if(expr.
id()==ID_symbol ||
4399 expr.
id()==ID_nondet_symbol)
4402 if(expr.
type().
id()==ID_code)
4407 if(expr.
id()==ID_symbol)
4410 identifier=
"nondet_"+
4415 if(
id.type.is_nil())
4417 id.type=expr.
type();
4422 out <<
"; find_symbols\n";
4423 out <<
"(declare-fun |"
4430 else if(expr.
id() == ID_array_of)
4437 const auto &array_type = array_of.type();
4441 out <<
"; the following is a substitute for lambda i. x\n";
4442 out <<
"(declare-fun " <<
id <<
" () ";
4447 out <<
"(assert (forall ((i ";
4449 out <<
")) (= (select " <<
id <<
" i) ";
4466 else if(expr.
id() == ID_array_comprehension)
4473 const auto &array_type = array_comprehension.type();
4474 const auto &array_size = array_type.size();
4478 out <<
"(declare-fun " <<
id <<
" () ";
4482 out <<
"; the following is a substitute for lambda i . x(i)\n";
4483 out <<
"; universally quantified initialization of the array\n";
4484 out <<
"(assert (forall ((";
4488 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
4495 out <<
")) (= (select " <<
id <<
" ";
4514 else if(expr.
id()==ID_array)
4521 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4522 out <<
"(declare-fun " <<
id <<
" () ";
4526 for(std::size_t i=0; i<expr.
operands().size(); i++)
4528 out <<
"(assert (= (select " <<
id <<
" ";
4541 out <<
"))" <<
"\n";
4547 else if(expr.
id()==ID_string_constant)
4557 out <<
"; the following is a substitute for a string" <<
"\n";
4558 out <<
"(declare-fun " <<
id <<
" () ";
4562 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4564 out <<
"(assert (= (select " << id;
4568 out <<
"))" <<
"\n";
4574 else if(expr.
id() == ID_object_size)
4578 if(op.
type().
id()==ID_pointer)
4584 out <<
"(declare-fun " <<
id <<
" () ";
4595 (expr.
id() == ID_floatbv_plus ||
4596 expr.
id() == ID_floatbv_minus ||
4597 expr.
id() == ID_floatbv_mult ||
4598 expr.
id() == ID_floatbv_div ||
4599 expr.
id() == ID_floatbv_typecast ||
4600 expr.
id() == ID_ieee_float_equal ||
4601 expr.
id() == ID_ieee_float_notequal ||
4602 ((expr.
id() == ID_lt ||
4603 expr.
id() == ID_gt ||
4604 expr.
id() == ID_le ||
4605 expr.
id() == ID_ge ||
4606 expr.
id() == ID_isnan ||
4607 expr.
id() == ID_isnormal ||
4608 expr.
id() == ID_isfinite ||
4609 expr.
id() == ID_isinf ||
4610 expr.
id() == ID_sign ||
4611 expr.
id() == ID_unary_minus ||
4612 expr.
id() == ID_typecast ||
4613 expr.
id() == ID_abs) &&
4620 if(
bvfp_set.insert(
function).second)
4622 out <<
"; this is a model for " << expr.
id() <<
" : "
4625 <<
"(define-fun " <<
function <<
" (";
4627 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4631 out <<
"(op" << i <<
' ';
4641 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4668 if(expr.
id()==ID_with)
4670 else if(expr.
id()==ID_member)
4679 if(type.
id()==ID_array)
4692 out <<
"(_ BitVec 1)";
4698 else if(type.
id()==ID_bool)
4702 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4712 width != 0,
"failed to get width of struct");
4714 out <<
"(_ BitVec " << width <<
")";
4717 else if(type.
id()==ID_vector)
4727 width != 0,
"failed to get width of vector");
4729 out <<
"(_ BitVec " << width <<
")";
4732 else if(type.
id()==ID_code)
4739 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
4744 out <<
"(_ BitVec " << width <<
")";
4746 else if(type.
id()==ID_pointer)
4751 else if(type.
id()==ID_bv ||
4752 type.
id()==ID_fixedbv ||
4753 type.
id()==ID_unsignedbv ||
4754 type.
id()==ID_signedbv ||
4755 type.
id()==ID_c_bool)
4760 else if(type.
id()==ID_c_enum)
4766 else if(type.
id()==ID_c_enum_tag)
4770 else if(type.
id()==ID_floatbv)
4775 out <<
"(_ FloatingPoint "
4776 << floatbv_type.
get_e() <<
" "
4777 << floatbv_type.
get_f() + 1 <<
")";
4782 else if(type.
id()==ID_rational ||
4785 else if(type.
id()==ID_integer)
4787 else if(type.
id()==ID_complex)
4797 width != 0,
"failed to get width of complex");
4799 out <<
"(_ BitVec " << width <<
")";
4802 else if(type.
id()==ID_c_bit_field)
4814 std::set<irep_idt> recstack;
4820 std::set<irep_idt> &recstack)
4822 if(type.
id()==ID_array)
4828 else if(type.
id()==ID_complex)
4835 const std::string smt_typename =
4839 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4840 <<
"(mk-" << smt_typename;
4842 out <<
" (" << smt_typename <<
".imag ";
4846 out <<
" (" << smt_typename <<
".real ";
4853 else if(type.
id()==ID_vector)
4862 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4864 const std::string smt_typename =
4868 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4869 <<
"(mk-" << smt_typename;
4873 out <<
" (" << smt_typename <<
"." << i <<
" ";
4881 else if(type.
id() == ID_struct)
4884 bool need_decl=
false;
4888 const std::string smt_typename =
4903 const std::string &smt_typename =
datatype_map.at(type);
4914 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4915 <<
"(mk-" << smt_typename <<
" ";
4919 out <<
"(" << smt_typename <<
"." <<
component.get_name()
4925 out <<
"))))" <<
"\n";
4942 for(struct_union_typet::componentst::const_iterator
4943 it=components.begin();
4944 it!=components.end();
4948 out <<
"(define-fun update-" << smt_typename <<
"."
4950 <<
"((s " << smt_typename <<
") "
4953 out <<
")) " << smt_typename <<
" "
4954 <<
"(mk-" << smt_typename
4957 for(struct_union_typet::componentst::const_iterator
4958 it2=components.begin();
4959 it2!=components.end();
4966 out <<
"(" << smt_typename <<
"."
4967 << it2->get_name() <<
" s) ";
4971 out <<
"))" <<
"\n";
4977 else if(type.
id() == ID_union)
4985 else if(type.
id()==ID_code)
4989 for(
const auto ¶m : parameters)
4994 else if(type.
id()==ID_pointer)
4998 else if(type.
id() == ID_struct_tag)
5001 const irep_idt &
id = struct_tag.get_identifier();
5003 if(recstack.find(
id) == recstack.end())
5006 recstack.insert(
id);
5011 else if(type.
id() == ID_union_tag)
5014 const irep_idt &
id = union_tag.get_identifier();
5016 if(recstack.find(
id) == recstack.end())
5018 recstack.insert(
id);
Operator to update elements in structs and arrays.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define UNEXPECTEDCASE(S)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
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
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
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 floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
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 bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
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.
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.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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 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 fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
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)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
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
void convert_relation(const binary_relation_exprt &)
Semantic type conversion from/to floating-point formats.
identifier_mapt identifier_map
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#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 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)
bool use_check_sat_assuming
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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
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 use_lambda_for_array
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 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)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
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.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
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.
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
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 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
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
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.
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