49#define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
52#define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
56 const std::string &_benchmark,
57 const std::string &_notes,
58 const std::string &_logic,
61 : use_FPA_theory(false),
62 use_array_of_bool(false),
64 use_check_sat_assuming(false),
66 use_lambda_for_array(false),
70 benchmark(_benchmark),
76 no_boolean_variables(0)
149 "variable number shall be within bounds");
155 out <<
"; SMT 2" <<
"\n";
163 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
172 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
174 out <<
"(set-option :produce-models true)" <<
"\n";
180 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
193 out <<
"(check-sat-assuming (";
203 out <<
"; assumptions\n";
214 out <<
"(check-sat)\n";
222 out <<
"(get-value (|" <<
id <<
"|))"
230 out <<
"; end of SMT2 file"
242 std::size_t number = 0;
243 std::size_t h=pointer_width-1;
248 const typet &type = o.type();
251 numeric_cast<mp_integer>(size_expr.value_or(
nil_exprt()));
254 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
255 !size_expr.has_value() || !
object_size.has_value())
261 out <<
"(assert (=> (= "
262 <<
"((_ extract " << h <<
" " << l <<
") ";
265 <<
"(= |" <<
id <<
"| (_ bv" << *
object_size <<
" " << size_width
281 if(expr.
id()==ID_symbol)
288 return it->second.value;
291 else if(expr.
id()==ID_nondet_symbol)
298 return it->second.value;
300 else if(expr.
id()==ID_member)
308 else if(expr.
id() == ID_literal)
316 else if(expr.
id() == ID_not)
321 else if(op.is_false())
326 else if(
const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
328 exprt array_copy = *array;
329 for(
auto &element : array_copy.
operands())
331 element =
get(element);
366 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
371 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
382 else if(src.
get_sub().size()==2 &&
387 else if(src.
get_sub().size()==3 &&
390 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
394 else if(src.
get_sub().size()==4 &&
397 if(type.
id()==ID_floatbv)
406 const auto s1_int = numeric_cast_v<mp_integer>(
s1);
407 const auto s2_int = numeric_cast_v<mp_integer>(
s2);
408 const auto s3_int = numeric_cast_v<mp_integer>(s3);
412 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
418 else if(src.
get_sub().size()==4 &&
426 else if(src.
get_sub().size()==4 &&
434 else if(src.
get_sub().size()==4 &&
443 if(type.
id()==ID_signedbv ||
444 type.
id()==ID_unsignedbv ||
445 type.
id()==ID_c_enum ||
446 type.
id()==ID_c_bool)
450 else if(type.
id()==ID_c_enum_tag)
456 result.
type() = type;
459 else if(type.
id()==ID_fixedbv ||
460 type.
id()==ID_floatbv)
465 else if(type.
id()==ID_integer ||
473 "smt2_convt::parse_literal should not be of unsupported type " +
481 std::unordered_map<int64_t, exprt> operands_map;
485 auto maybe_default_op = operands_map.find(-1);
487 if(maybe_default_op == operands_map.end())
490 default_op = maybe_default_op->second;
492 auto maybe_size = numeric_cast<std::int64_t>(type.
size());
493 if(maybe_size.has_value())
495 while(i < maybe_size.value())
497 auto found_op = operands_map.find(i);
498 if(found_op != operands_map.end())
499 operands.emplace_back(found_op->second);
501 operands.emplace_back(default_op);
509 auto found_op = operands_map.find(i);
510 while(found_op != operands_map.end())
512 operands.emplace_back(found_op->second);
514 found_op = operands_map.find(i);
516 operands.emplace_back(default_op);
522 std::unordered_map<int64_t, exprt> *operands_map,
535 bool failure =
to_integer(index_constant, tempint);
538 long index = tempint.to_long();
540 operands_map->emplace(index, value);
542 else if(src.
get_sub().size() == 3 && src.
get_sub()[0].id() ==
"let")
547 operands_map, src.
get_sub()[1].get_sub()[0].get_sub()[1], type);
550 else if(src.
get_sub().size()==2 &&
551 src.
get_sub()[0].get_sub().size()==3 &&
552 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
553 src.
get_sub()[0].get_sub()[1].id()==
"const")
557 operands_map->emplace(-1, default_value);
584 if(components.empty())
592 if(src.
get_sub().size()!=components.size()+1)
595 for(std::size_t i=0; i<components.size(); i++)
612 std::size_t offset=0;
614 for(std::size_t i=0; i<components.size(); i++)
616 std::size_t component_width=
boolbv_width(components[i].type());
619 offset + component_width <= total_width,
620 "struct component bits shall be within struct bit vector");
622 std::string component_binary=
624 total_width-offset-component_width, component_width);
629 offset+=component_width;
639 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
640 type.
id() == ID_integer || type.
id() == ID_rational ||
641 type.
id() == ID_real || type.
id() == ID_c_enum ||
642 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
643 type.
id() == ID_floatbv)
647 else if(type.
id()==ID_bool)
649 if(src.
id()==ID_1 || src.
id()==ID_true)
651 else if(src.
id()==ID_0 || src.
id()==ID_false)
654 else if(type.
id()==ID_pointer)
660 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
665 ptr.
object = numeric_cast_v<std::size_t>(v / pow);
669 else if(type.
id()==ID_struct)
673 else if(type.
id() == ID_struct_tag)
678 struct_expr.type() = type;
679 return std::move(struct_expr);
681 else if(type.
id()==ID_union)
685 else if(type.
id() == ID_union_tag)
689 union_expr.type() = type;
692 else if(type.
id()==ID_array)
704 if(expr.
id()==ID_symbol ||
705 expr.
id()==ID_constant ||
706 expr.
id()==ID_string_constant ||
716 else if(expr.
id()==ID_index)
725 if(array.
type().
id()==ID_pointer)
727 else if(array.
type().
id()==ID_array)
747 else if(expr.
id()==ID_member)
752 const typet &struct_op_type = struct_op.
type();
755 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
756 "member expression operand shall have struct type");
773 else if(expr.
id()==ID_if)
788 "operand of address of expression should not be of kind " +
802 else if(expr.
id()==ID_literal)
814 out <<
"; convert\n";
815 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
823 out <<
"(define-fun ";
835 if(expr.
type().
id() != ID_bool)
886 for(std::size_t i=0; i<identifier.
size(); i++)
888 char ch=identifier[i];
911 if(type.
id()==ID_floatbv)
916 else if(type.
id()==ID_unsignedbv)
920 else if(type.
id()==ID_c_bool)
924 else if(type.
id()==ID_signedbv)
928 else if(type.
id()==ID_bool)
932 else if(type.
id()==ID_c_enum_tag)
936 else if(type.
id() == ID_pointer)
957 if(expr.
id()==ID_symbol)
964 if(expr.
id()==ID_smt2_symbol)
972 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
974 out <<
"(|float_bv." << expr.
id()
990 if(expr.
id()==ID_symbol)
996 else if(expr.
id()==ID_nondet_symbol)
999 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1002 else if(expr.
id()==ID_smt2_symbol)
1008 else if(expr.
id()==ID_typecast)
1012 else if(expr.
id()==ID_floatbv_typecast)
1016 else if(expr.
id()==ID_struct)
1020 else if(expr.
id()==ID_union)
1024 else if(expr.
id()==ID_constant)
1028 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
1032 "concatenation over a single operand should have matching types",
1037 else if(expr.
id()==ID_concatenation ||
1038 expr.
id()==ID_bitand ||
1039 expr.
id()==ID_bitor ||
1040 expr.
id()==ID_bitxor ||
1041 expr.
id()==ID_bitnand ||
1042 expr.
id()==ID_bitnor)
1046 "given expression should have at least two operands",
1051 if(expr.
id()==ID_concatenation)
1053 else if(expr.
id()==ID_bitand)
1055 else if(expr.
id()==ID_bitor)
1057 else if(expr.
id()==ID_bitxor)
1059 else if(expr.
id()==ID_bitnand)
1061 else if(expr.
id()==ID_bitnor)
1072 else if(expr.
id()==ID_bitnot)
1076 if(bitnot_expr.
type().
id() == ID_vector)
1085 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1087 out <<
"(let ((?vectorop ";
1091 out <<
"(mk-" << smt_typename;
1098 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
1114 else if(expr.
id()==ID_unary_minus)
1119 unary_minus_expr.
type().
id() == ID_rational ||
1120 unary_minus_expr.
type().
id() == ID_integer ||
1121 unary_minus_expr.
type().
id() == ID_real)
1127 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1139 else if(unary_minus_expr.
type().
id() == ID_vector)
1143 const std::string &smt_typename =
1150 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1152 out <<
"(let ((?vectorop ";
1156 out <<
"(mk-" << smt_typename;
1163 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1179 else if(expr.
id()==ID_unary_plus)
1184 else if(expr.
id()==ID_sign)
1190 if(op_type.
id()==ID_floatbv)
1194 out <<
"(fp.isNegative ";
1201 else if(op_type.
id()==ID_signedbv)
1207 out <<
" (_ bv0 " << op_width <<
"))";
1212 "sign should not be applied to unsupported type",
1215 else if(expr.
id()==ID_if)
1227 else if(expr.
id()==ID_and ||
1232 expr.
type().
id() == ID_bool,
1233 "logical and, or, and xor expressions should have Boolean type");
1236 "logical and, or, and xor expressions should have at least two operands");
1238 out <<
"(" << expr.
id();
1246 else if(expr.
id()==ID_implies)
1251 implies_expr.
type().
id() == ID_bool,
1252 "implies expression should have Boolean type");
1260 else if(expr.
id()==ID_not)
1265 not_expr.
type().
id() == ID_bool,
1266 "not expression should have Boolean type");
1272 else if(expr.
id() == ID_equal)
1278 "operands of equal expression shall have same type");
1286 else if(expr.
id() == ID_notequal)
1292 "operands of not equal expression shall have same type");
1300 else if(expr.
id()==ID_ieee_float_equal ||
1301 expr.
id()==ID_ieee_float_notequal)
1308 rel_expr.lhs().type() == rel_expr.rhs().type(),
1309 "operands of float equal and not equal expressions shall have same type");
1314 if(rel_expr.id() == ID_ieee_float_notequal)
1323 if(rel_expr.id() == ID_ieee_float_notequal)
1329 else if(expr.
id()==ID_le ||
1336 else if(expr.
id()==ID_plus)
1340 else if(expr.
id()==ID_floatbv_plus)
1344 else if(expr.
id()==ID_minus)
1348 else if(expr.
id()==ID_floatbv_minus)
1352 else if(expr.
id()==ID_div)
1356 else if(expr.
id()==ID_floatbv_div)
1360 else if(expr.
id()==ID_mod)
1364 else if(expr.
id() == ID_euclidean_mod)
1368 else if(expr.
id()==ID_mult)
1372 else if(expr.
id()==ID_floatbv_mult)
1376 else if(expr.
id() == ID_floatbv_rem)
1380 else if(expr.
id()==ID_address_of)
1386 else if(expr.
id() == ID_array_of)
1391 array_of_expr.type().id() == ID_array,
1392 "array of expression shall have array type");
1396 out <<
"((as const ";
1404 defined_expressionst::const_iterator it =
1410 else if(expr.
id() == ID_array_comprehension)
1415 array_comprehension.type().id() == ID_array,
1416 "array_comprehension expression shall have array type");
1420 out <<
"(lambda ((";
1423 convert_type(array_comprehension.type().size().type());
1435 else if(expr.
id()==ID_index)
1439 else if(expr.
id()==ID_ashr ||
1440 expr.
id()==ID_lshr ||
1446 if(type.
id()==ID_unsignedbv ||
1447 type.
id()==ID_signedbv ||
1450 if(shift_expr.
id() == ID_ashr)
1452 else if(shift_expr.
id() == ID_lshr)
1454 else if(shift_expr.
id() == ID_shl)
1484 if(width_op0==width_op1)
1486 else if(width_op0>width_op1)
1488 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1494 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1501 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1508 "unsupported type for " + shift_expr.
id_string() +
": " +
1511 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1517 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1522 if(shift_expr.
id() == ID_rol)
1523 out <<
"((_ rotate_left";
1524 else if(shift_expr.
id() == ID_ror)
1525 out <<
"((_ rotate_right";
1531 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.
distance());
1533 if(distance_int_op.has_value())
1535 out << distance_int_op.value();
1539 "distance type for " + shift_expr.
id_string() +
"must be constant");
1548 "unsupported type for " + shift_expr.
id_string() +
": " +
1551 else if(expr.
id()==ID_with)
1555 else if(expr.
id()==ID_update)
1559 else if(expr.
id()==ID_member)
1563 else if(expr.
id()==ID_pointer_offset)
1568 op.type().id() == ID_pointer,
1569 "operand of pointer offset expression shall be of pointer type");
1571 std::size_t offset_bits =
1576 if(offset_bits>result_width)
1577 offset_bits=result_width;
1580 if(result_width>offset_bits)
1581 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1583 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1587 if(result_width>offset_bits)
1590 else if(expr.
id()==ID_pointer_object)
1595 op.type().id() == ID_pointer,
1596 "pointer object expressions should be of pointer type");
1602 out <<
"((_ zero_extend " << ext <<
") ";
1604 out <<
"((_ extract "
1605 << pointer_width-1 <<
" "
1613 else if(expr.
id() == ID_is_dynamic_object)
1617 else if(expr.
id() == ID_is_invalid_pointer)
1621 out <<
"(= ((_ extract "
1622 << pointer_width-1 <<
" "
1628 else if(expr.
id()==ID_string_constant)
1634 else if(expr.
id()==ID_extractbit)
1643 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1649 out <<
"(= ((_ extract 0 0) ";
1658 else if(expr.
id()==ID_extractbits)
1672 std::swap(op1_i, op2_i);
1676 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1683 out <<
"(= ((_ extract 0 0) ";
1692 SMT2_TODO(
"smt2: extractbits with non-constant index");
1695 else if(expr.
id()==ID_replication)
1699 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1701 out <<
"((_ repeat " << times <<
") ";
1705 else if(expr.
id()==ID_byte_extract_little_endian ||
1706 expr.
id()==ID_byte_extract_big_endian)
1709 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1711 else if(expr.
id()==ID_byte_update_little_endian ||
1712 expr.
id()==ID_byte_update_big_endian)
1715 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1717 else if(expr.
id()==ID_abs)
1723 if(type.
id()==ID_signedbv)
1727 out <<
"(ite (bvslt ";
1729 out <<
" (_ bv0 " << result_width <<
")) ";
1736 else if(type.
id()==ID_fixedbv)
1740 out <<
"(ite (bvslt ";
1742 out <<
" (_ bv0 " << result_width <<
")) ";
1749 else if(type.
id()==ID_floatbv)
1763 else if(expr.
id()==ID_isnan)
1769 if(op_type.
id()==ID_fixedbv)
1771 else if(op_type.
id()==ID_floatbv)
1775 out <<
"(fp.isNaN ";
1785 else if(expr.
id()==ID_isfinite)
1791 if(op_type.
id()==ID_fixedbv)
1793 else if(op_type.
id()==ID_floatbv)
1799 out <<
"(not (fp.isNaN ";
1803 out <<
"(not (fp.isInf ";
1815 else if(expr.
id()==ID_isinf)
1821 if(op_type.
id()==ID_fixedbv)
1823 else if(op_type.
id()==ID_floatbv)
1827 out <<
"(fp.isInfinite ";
1837 else if(expr.
id()==ID_isnormal)
1843 if(op_type.
id()==ID_fixedbv)
1845 else if(op_type.
id()==ID_floatbv)
1849 out <<
"(fp.isNormal ";
1859 else if(expr.
id()==ID_overflow_plus ||
1860 expr.
id()==ID_overflow_minus)
1866 expr.
type().
id() == ID_bool,
1867 "overflow plus and overflow minus expressions shall be of Boolean type");
1869 bool subtract=expr.
id()==ID_overflow_minus;
1870 const typet &op_type = op0.type();
1873 if(op_type.
id()==ID_signedbv)
1876 out <<
"(let ((?sum (";
1877 out << (subtract?
"bvsub":
"bvadd");
1878 out <<
" ((_ sign_extend 1) ";
1881 out <<
" ((_ sign_extend 1) ";
1885 "((_ extract " << width <<
" " << width <<
") ?sum) "
1886 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1889 else if(op_type.
id()==ID_unsignedbv ||
1890 op_type.
id()==ID_pointer)
1894 out <<
"((_ extract " << width <<
" " << width <<
") ";
1895 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1896 out <<
" ((_ zero_extend 1) ";
1899 out <<
" ((_ zero_extend 1) ";
1907 "overflow check should not be performed on unsupported type",
1910 else if(expr.
id()==ID_overflow_mult)
1916 expr.
type().
id() == ID_bool,
1917 "overflow mult expression shall be of Boolean type");
1922 const typet &op_type = op0.type();
1925 if(op_type.
id()==ID_signedbv)
1927 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1929 out <<
") ((_ sign_extend " << width <<
") ";
1932 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
1934 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" "
1935 << width*2 <<
")))))";
1937 else if(op_type.
id()==ID_unsignedbv)
1939 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1941 out <<
") ((_ zero_extend " << width <<
") ";
1943 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1948 "overflow check should not be performed on unsupported type",
1951 else if(expr.
id()==ID_array)
1957 else if(expr.
id()==ID_literal)
1961 else if(expr.
id()==ID_forall ||
1962 expr.
id()==ID_exists)
1968 throw "MathSAT does not support quantifiers";
1970 if(quantifier_expr.
id() == ID_forall)
1972 else if(quantifier_expr.
id() == ID_exists)
1976 for(
const auto &bound : quantifier_expr.
variables())
1990 else if(expr.
id()==ID_vector)
1995 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1998 size == vector_expr.
operands().size(),
1999 "size indicated by type shall be equal to the number of operands");
2003 const std::string &smt_typename =
datatype_map.at(vector_type);
2005 out <<
"(mk-" << smt_typename;
2019 else if(expr.
id()==ID_object_size)
2023 else if(expr.
id()==ID_let)
2026 const auto &variables = let_expr.
variables();
2027 const auto &values = let_expr.
values();
2032 for(
auto &binding :
make_range(variables).zip(values))
2051 else if(expr.
id()==ID_constraint_select_one)
2054 "smt2_convt::convert_expr: '" + expr.
id_string() +
2055 "' is not yet supported");
2057 else if(expr.
id() == ID_bswap)
2063 "operand of byte swap expression shall have same type as the expression");
2066 out <<
"(let ((bswap_op ";
2071 bswap_expr.
type().
id() == ID_signedbv ||
2072 bswap_expr.
type().
id() == ID_unsignedbv)
2074 const std::size_t width =
2081 width % bits_per_byte == 0,
2082 "bit width indicated by type of bswap expression should be a multiple "
2083 "of the number of bits per byte");
2085 const std::size_t bytes = width / bits_per_byte;
2094 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2098 out <<
"(bswap_byte_" <<
byte <<
' ';
2099 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2100 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2109 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2110 out <<
" bswap_byte_" <<
byte;
2121 else if(expr.
id() == ID_popcount)
2125 else if(expr.
id() == ID_count_leading_zeros)
2129 else if(expr.
id() == ID_count_trailing_zeros)
2133 else if(expr.
id() == ID_empty_union)
2137 else if(expr.
id() == ID_bitreverse)
2144 "smt2_convt::convert_expr should not be applied to unsupported type",
2153 if(dest_type.
id()==ID_c_enum_tag)
2157 if(src_type.
id()==ID_c_enum_tag)
2160 if(dest_type.
id()==ID_bool)
2163 if(src_type.
id()==ID_signedbv ||
2164 src_type.
id()==ID_unsignedbv ||
2165 src_type.
id()==ID_c_bool ||
2166 src_type.
id()==ID_fixedbv ||
2167 src_type.
id()==ID_pointer ||
2168 src_type.
id()==ID_integer)
2176 else if(src_type.
id()==ID_floatbv)
2180 out <<
"(not (fp.isZero ";
2192 else if(dest_type.
id()==ID_c_bool)
2201 out <<
" (_ bv1 " << to_width <<
")";
2202 out <<
" (_ bv0 " << to_width <<
")";
2205 else if(dest_type.
id()==ID_signedbv ||
2206 dest_type.
id()==ID_unsignedbv ||
2207 dest_type.
id()==ID_c_enum ||
2208 dest_type.
id()==ID_bv)
2212 if(src_type.
id()==ID_signedbv ||
2213 src_type.
id()==ID_unsignedbv ||
2214 src_type.
id()==ID_c_bool ||
2215 src_type.
id()==ID_c_enum ||
2216 src_type.
id()==ID_bv)
2220 if(from_width==to_width)
2222 else if(from_width<to_width)
2224 if(src_type.
id()==ID_signedbv)
2225 out <<
"((_ sign_extend ";
2227 out <<
"((_ zero_extend ";
2229 out << (to_width-from_width)
2236 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2241 else if(src_type.
id()==ID_fixedbv)
2245 std::size_t from_width=fixedbv_type.
get_width();
2252 out <<
"(let ((?tcop ";
2258 if(to_width>from_integer_bits)
2260 out <<
"((_ sign_extend "
2261 << (to_width-from_integer_bits) <<
") ";
2262 out <<
"((_ extract " << (from_width-1) <<
" "
2263 << from_fraction_bits <<
") ";
2269 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2270 <<
" " << from_fraction_bits <<
") ";
2275 out <<
" (ite (and ";
2278 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2279 "(_ bv0 " << from_fraction_bits <<
")))";
2282 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2287 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2291 else if(src_type.
id()==ID_floatbv)
2293 if(dest_type.
id()==ID_bv)
2310 else if(dest_type.
id()==ID_signedbv)
2314 "typecast unexpected "+src_type.
id_string()+
" -> "+
2317 else if(dest_type.
id()==ID_unsignedbv)
2321 "typecast unexpected "+src_type.
id_string()+
" -> "+
2325 else if(src_type.
id()==ID_bool)
2330 if(dest_type.
id()==ID_fixedbv)
2333 out <<
" (concat (_ bv1 "
2336 "(_ bv0 " << spec.
width <<
")";
2340 out <<
" (_ bv1 " << to_width <<
")";
2341 out <<
" (_ bv0 " << to_width <<
")";
2346 else if(src_type.
id()==ID_pointer)
2350 if(from_width<to_width)
2352 out <<
"((_ sign_extend ";
2353 out << (to_width-from_width)
2360 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2365 else if(src_type.
id()==ID_integer)
2371 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2374 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2377 src_type.
id() == ID_struct ||
2378 src_type.
id() == ID_struct_tag)
2384 "bit vector with of source and destination type shall be equal");
2391 "bit vector with of source and destination type shall be equal");
2396 src_type.
id() == ID_union ||
2397 src_type.
id() == ID_union_tag)
2401 "bit vector with of source and destination type shall be equal");
2404 else if(src_type.
id()==ID_c_bit_field)
2408 if(from_width==to_width)
2419 std::ostringstream e_str;
2420 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2421 <<
" src == " <<
format(src);
2425 else if(dest_type.
id()==ID_fixedbv)
2431 if(src_type.
id()==ID_unsignedbv ||
2432 src_type.
id()==ID_signedbv ||
2433 src_type.
id()==ID_c_enum)
2440 if(from_width==to_integer_bits)
2442 else if(from_width>to_integer_bits)
2445 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2453 from_width < to_integer_bits,
2454 "from_width should be smaller than to_integer_bits as other case "
2455 "have been handled above");
2456 if(dest_type.
id()==ID_unsignedbv)
2458 out <<
"(_ zero_extend "
2459 << (to_integer_bits-from_width) <<
") ";
2465 out <<
"((_ sign_extend "
2466 << (to_integer_bits-from_width) <<
") ";
2472 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2475 else if(src_type.
id()==ID_bool)
2477 out <<
"(concat (concat"
2478 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2484 else if(src_type.
id()==ID_fixedbv)
2489 std::size_t from_width=from_fixedbv_type.
get_width();
2491 out <<
"(let ((?tcop ";
2497 if(to_integer_bits<=from_integer_bits)
2499 out <<
"((_ extract "
2500 << (from_fraction_bits+to_integer_bits-1) <<
" "
2501 << from_fraction_bits
2507 to_integer_bits > from_integer_bits,
2508 "to_integer_bits should be greater than from_integer_bits as the"
2509 "other case has been handled above");
2510 out <<
"((_ sign_extend "
2511 << (to_integer_bits-from_integer_bits)
2513 << (from_width-1) <<
" "
2514 << from_fraction_bits
2520 if(to_fraction_bits<=from_fraction_bits)
2522 out <<
"((_ extract "
2523 << (from_fraction_bits-1) <<
" "
2524 << (from_fraction_bits-to_fraction_bits)
2530 to_fraction_bits > from_fraction_bits,
2531 "to_fraction_bits should be greater than from_fraction_bits as the"
2532 "other case has been handled above");
2533 out <<
"(concat ((_ extract "
2534 << (from_fraction_bits-1) <<
" 0) ";
2537 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2546 else if(dest_type.
id()==ID_pointer)
2550 if(src_type.
id()==ID_pointer)
2556 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2557 src_type.
id() == ID_bv)
2563 if(from_width==to_width)
2565 else if(from_width<to_width)
2567 out <<
"((_ sign_extend "
2568 << (to_width-from_width)
2575 out <<
"((_ extract " << to_width <<
" 0) ";
2583 else if(dest_type.
id()==ID_range)
2587 else if(dest_type.
id()==ID_floatbv)
2596 if(src_type.
id()==ID_bool)
2611 a.
build(significand, exponent);
2619 a.
build(significand, exponent);
2625 else if(src_type.
id()==ID_c_bool)
2631 else if(src_type.
id() == ID_bv)
2640 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2641 << dest_floatbv_type.get_f() + 1 <<
") ";
2651 else if(dest_type.
id()==ID_integer)
2653 if(src_type.
id()==ID_bool)
2662 else if(dest_type.
id()==ID_c_bit_field)
2667 if(from_width==to_width)
2688 if(dest_type.
id()==ID_floatbv)
2690 if(src_type.
id()==ID_floatbv)
2717 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2718 << dst.
get_f() + 1 <<
") ";
2727 else if(src_type.
id()==ID_unsignedbv)
2748 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
2749 << dst.
get_f() + 1 <<
") ";
2758 else if(src_type.
id()==ID_signedbv)
2766 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2767 << dst.
get_f() + 1 <<
") ";
2776 else if(src_type.
id()==ID_c_enum_tag)
2790 else if(dest_type.
id()==ID_signedbv)
2795 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2804 else if(dest_type.
id()==ID_unsignedbv)
2809 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2833 components.size() == expr.
operands().size(),
2834 "number of struct components as indicated by the struct type shall be equal"
2835 "to the number of operands of the struct expression");
2837 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2841 const std::string &smt_typename =
datatype_map.at(struct_type);
2844 out <<
"(mk-" << smt_typename;
2847 for(struct_typet::componentst::const_iterator
2848 it=components.begin();
2849 it!=components.end();
2860 if(components.size()==1)
2865 for(std::size_t i=components.size(); i>1; i--)
2872 if(op.
type().
id() == ID_array)
2882 for(std::size_t i=1; i<components.size(); i++)
2892 const auto &size_expr = array_type.
size();
2898 out <<
"(let ((?far ";
2906 out <<
"(select ?far ";
2927 total_width != 0,
"failed to get union width for union");
2931 member_width != 0,
"failed to get union member width for union");
2933 if(total_width==member_width)
2941 total_width > member_width,
2942 "total_width should be greater than member_width as member_width can be"
2943 "at most as large as total_width and the other case has been handled "
2947 << (total_width-member_width) <<
") ";
2957 if(expr_type.
id()==ID_unsignedbv ||
2958 expr_type.
id()==ID_signedbv ||
2959 expr_type.
id()==ID_bv ||
2960 expr_type.
id()==ID_c_enum ||
2961 expr_type.
id()==ID_c_enum_tag ||
2962 expr_type.
id()==ID_c_bool ||
2963 expr_type.
id()==ID_c_bit_field)
2969 out <<
"(_ bv" << value
2970 <<
" " << width <<
")";
2972 else if(expr_type.
id()==ID_fixedbv)
2978 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2980 else if(expr_type.
id()==ID_floatbv)
2993 size_t e=floatbv_type.
get_e();
2994 size_t f=floatbv_type.
get_f()+1;
3000 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3006 out <<
"(_ NaN " << e <<
" " << f <<
")";
3011 out <<
"(_ -oo " << e <<
" " << f <<
")";
3013 out <<
"(_ +oo " << e <<
" " << f <<
")";
3023 <<
"#b" << binaryString.substr(0, 1) <<
" "
3024 <<
"#b" << binaryString.substr(1, e) <<
" "
3025 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
3033 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3036 else if(expr_type.
id()==ID_pointer)
3048 else if(expr_type.
id()==ID_bool)
3057 else if(expr_type.
id()==ID_array)
3063 else if(expr_type.
id()==ID_rational)
3066 const bool negative =
has_prefix(value,
"-");
3071 size_t pos=value.find(
"/");
3073 if(
pos==std::string::npos)
3074 out << value <<
".0";
3077 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3078 << value.substr(
pos+1) <<
".0)";
3084 else if(expr_type.
id()==ID_integer)
3090 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3100 if(expr.
type().
id() == ID_integer)
3110 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3115 if(expr.
type().
id()==ID_unsignedbv ||
3116 expr.
type().
id()==ID_signedbv)
3118 if(expr.
type().
id()==ID_unsignedbv)
3134 std::vector<std::size_t> dynamic_objects;
3137 if(dynamic_objects.empty())
3143 out <<
"(let ((?obj ((_ extract "
3144 << pointer_width-1 <<
" "
3149 if(dynamic_objects.size()==1)
3151 out <<
"(= (_ bv" << dynamic_objects.front()
3158 for(
const auto &
object : dynamic_objects)
3159 out <<
" (= (_ bv" <<
object
3173 if(op_type.
id()==ID_unsignedbv ||
3174 op_type.
id()==ID_bv)
3177 if(expr.
id()==ID_le)
3179 else if(expr.
id()==ID_lt)
3181 else if(expr.
id()==ID_ge)
3183 else if(expr.
id()==ID_gt)
3192 else if(op_type.
id()==ID_signedbv ||
3193 op_type.
id()==ID_fixedbv)
3196 if(expr.
id()==ID_le)
3198 else if(expr.
id()==ID_lt)
3200 else if(expr.
id()==ID_ge)
3202 else if(expr.
id()==ID_gt)
3211 else if(op_type.
id()==ID_floatbv)
3216 if(expr.
id()==ID_le)
3218 else if(expr.
id()==ID_lt)
3220 else if(expr.
id()==ID_ge)
3222 else if(expr.
id()==ID_gt)
3234 else if(op_type.
id()==ID_rational ||
3235 op_type.
id()==ID_integer)
3246 else if(op_type.
id() == ID_pointer)
3254 if(expr.
id() == ID_le)
3256 else if(expr.
id() == ID_lt)
3258 else if(expr.
id() == ID_ge)
3260 else if(expr.
id() == ID_gt)
3279 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3280 expr.
type().
id() == ID_real)
3285 for(
const auto &op : expr.
operands())
3294 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3295 expr.
type().
id() == ID_fixedbv)
3312 else if(expr.
type().
id() == ID_floatbv)
3319 else if(expr.
type().
id() == ID_pointer)
3325 if(p.
type().
id() != ID_pointer)
3329 p.
type().
id() == ID_pointer,
3330 "one of the operands should have pointer type");
3344 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3345 element_size = *element_size_opt;
3352 if(element_size >= 2)
3369 else if(expr.
type().
id() == ID_vector)
3373 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3379 const std::string &smt_typename =
datatype_map.at(vector_type);
3381 out <<
"(mk-" << smt_typename;
3390 summands.reserve(expr.
operands().size());
3391 for(
const auto &op : expr.
operands())
3425 if(expr.
id()==ID_constant)
3429 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3432 out <<
"roundNearestTiesToEven";
3434 out <<
"roundTowardNegative";
3436 out <<
"roundTowardPositive";
3438 out <<
"roundTowardZero";
3442 "Rounding mode should have value 0, 1, 2, or 3",
3450 out <<
"(ite (= (_ bv0 " << width <<
") ";
3452 out <<
") roundNearestTiesToEven ";
3454 out <<
"(ite (= (_ bv1 " << width <<
") ";
3456 out <<
") roundTowardNegative ";
3458 out <<
"(ite (= (_ bv2 " << width <<
") ";
3460 out <<
") roundTowardPositive ";
3463 out <<
"roundTowardZero";
3474 type.
id() == ID_floatbv ||
3475 (type.
id() == ID_complex &&
3477 (type.
id() == ID_vector &&
3482 if(type.
id()==ID_floatbv)
3492 else if(type.
id()==ID_complex)
3496 else if(type.
id()==ID_vector)
3503 "type should not be one of the unsupported types",
3512 if(expr.
type().
id()==ID_integer)
3520 else if(expr.
type().
id()==ID_unsignedbv ||
3521 expr.
type().
id()==ID_signedbv ||
3522 expr.
type().
id()==ID_fixedbv)
3524 if(expr.
op0().
type().
id()==ID_pointer &&
3530 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3532 if(*element_size >= 2)
3537 "bitvector width of operand shall be equal to the bitvector width of "
3546 if(*element_size >= 2)
3559 else if(expr.
type().
id()==ID_floatbv)
3566 else if(expr.
type().
id()==ID_pointer)
3570 else if(expr.
type().
id()==ID_vector)
3574 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3580 const std::string &smt_typename =
datatype_map.at(vector_type);
3582 out <<
"(mk-" << smt_typename;
3610 expr.
type().
id() == ID_floatbv,
3611 "type of ieee floating point expression shall be floatbv");
3629 if(expr.
type().
id()==ID_unsignedbv ||
3630 expr.
type().
id()==ID_signedbv)
3632 if(expr.
type().
id()==ID_unsignedbv)
3642 else if(expr.
type().
id()==ID_fixedbv)
3647 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3652 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3654 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3660 else if(expr.
type().
id()==ID_floatbv)
3674 expr.
type().
id() == ID_floatbv,
3675 "type of ieee floating point expression shall be floatbv");
3706 "expression should have been converted to a variant with two operands");
3708 if(expr.
type().
id()==ID_unsignedbv ||
3709 expr.
type().
id()==ID_signedbv)
3720 else if(expr.
type().
id()==ID_floatbv)
3727 else if(expr.
type().
id()==ID_fixedbv)
3732 out <<
"((_ extract "
3733 << spec.
width+fraction_bits-1 <<
" "
3734 << fraction_bits <<
") ";
3738 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3742 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3748 else if(expr.
type().
id()==ID_rational ||
3749 expr.
type().
id()==ID_integer ||
3750 expr.
type().
id()==ID_real)
3769 expr.
type().
id() == ID_floatbv,
3770 "type of ieee floating point expression shall be floatbv");
3789 expr.
type().
id() == ID_floatbv,
3790 "type of ieee floating point expression shall be floatbv");
3804 "smt2_convt::convert_floatbv_rem to be implemented when not using "
3815 std::size_t s=expr.
operands().size();
3830 "with expression should have been converted to a version with three "
3835 if(expr_type.
id()==ID_array)
3859 out <<
"(let ((distance? ";
3860 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3864 if(array_width>index_width)
3866 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3872 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3882 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
3884 out <<
"distance?)) ";
3888 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3890 out <<
") distance?)))";
3893 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
3900 const irep_idt &component_name=index.
get(ID_component_name);
3904 "struct should have accessed component");
3908 const std::string &smt_typename =
datatype_map.at(expr_type);
3910 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3924 out <<
"(let ((?withop ";
3928 if(m.
width==struct_width)
3938 <<
"((_ extract " << (struct_width-1) <<
" "
3939 << m.
width <<
") ?withop) ";
3948 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
3953 out <<
"(concat (concat "
3954 <<
"((_ extract " << (struct_width-1) <<
" "
3957 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3964 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
3972 total_width != 0,
"failed to get union width for with");
3976 member_width != 0,
"failed to get union member width for with");
3978 if(total_width==member_width)
3985 total_width > member_width,
3986 "total width should be greater than member_width as member_width is at "
3987 "most as large as total_width and the other case has been handled "
3990 out <<
"((_ extract "
3992 <<
" " << member_width <<
") ";
3999 else if(expr_type.
id()==ID_bv ||
4000 expr_type.
id()==ID_unsignedbv ||
4001 expr_type.
id()==ID_signedbv)
4007 total_width != 0,
"failed to get total width");
4014 value_width != 0,
"failed to get value width");
4026 out <<
" (bvnot (bvshl";
4029 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
4030 out <<
" (repeat[" << value_width <<
"] bv1[1])";
4052 "with expects struct, union, or array type, but got "+
4060 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4067 if(array_op_type.
id()==ID_array)
4103 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
4107 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4111 if(array_width>index_width)
4113 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4119 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4129 else if(array_op_type.
id()==ID_vector)
4135 const std::string &smt_typename =
datatype_map.at(vector_type);
4139 const auto index_int = numeric_cast<mp_integer>(expr.
index());
4140 if(!index_int.has_value())
4142 SMT2_TODO(
"non-constant index on vectors");
4146 out <<
"(" << smt_typename <<
"." << *index_int <<
" ";
4158 false,
"index with unsupported array type: " + array_op_type.
id_string());
4165 const typet &struct_op_type = struct_op.
type();
4168 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
4173 struct_type.
has_component(name),
"struct should have accessed component");
4177 const std::string &smt_typename =
datatype_map.at(struct_type);
4179 out <<
"(" << smt_typename <<
"."
4192 member_offset.has_value(),
"failed to get struct member offset");
4201 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4205 width != 0,
"failed to get union member width");
4209 out <<
"((_ extract "
4219 "convert_member on an unexpected type "+struct_op_type.
id_string());
4226 if(type.
id()==ID_bool)
4232 else if(type.
id()==ID_vector)
4236 const std::string &smt_typename =
datatype_map.at(type);
4241 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4243 out <<
"(let ((?vflop ";
4251 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
4259 else if(type.
id()==ID_array)
4263 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4267 const std::string &smt_typename =
datatype_map.at(type);
4272 out <<
"(let ((?sflop ";
4280 for(std::size_t i=components.size(); i>1; i--)
4282 out <<
"(concat (" << smt_typename <<
"."
4283 << components[i-1].get_name() <<
" ?sflop)";
4288 out <<
"(" << smt_typename <<
"."
4289 << components[0].get_name() <<
" ?sflop)";
4291 for(std::size_t i=1; i<components.size(); i++)
4299 else if(type.
id()==ID_floatbv)
4303 "floatbv expressions should be flattened when using FPA theory");
4316 if(type.
id()==ID_bool)
4323 else if(type.
id()==ID_vector)
4327 const std::string &smt_typename =
datatype_map.at(type);
4334 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4337 out <<
"(let ((?ufop" << nesting <<
" ";
4342 out <<
"(mk-" << smt_typename;
4344 std::size_t offset=0;
4346 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4350 out <<
"((_ extract " << offset+subtype_width-1 <<
" "
4351 << offset <<
") ?ufop" << nesting <<
")";
4363 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4369 out <<
"(let ((?ufop" << nesting <<
" ";
4374 const std::string &smt_typename =
datatype_map.at(type);
4376 out <<
"(mk-" << smt_typename;
4383 std::size_t offset=0;
4386 for(struct_typet::componentst::const_iterator
4387 it=components.begin();
4388 it!=components.end();
4395 out <<
"((_ extract " << offset+member_width-1 <<
" "
4396 << offset <<
") ?ufop" << nesting <<
")";
4398 offset+=member_width;
4419 if(expr.
id()==ID_and && value)
4426 if(expr.
id()==ID_or && !value)
4433 if(expr.
id()==ID_not)
4443 if(expr.
id() == ID_equal && value)
4447 equal_expr.
lhs().
type().
id() == ID_empty ||
4448 equal_expr.
rhs().
id() == ID_empty_union)
4454 if(equal_expr.
lhs().
id()==ID_symbol)
4464 id.type=equal_expr.
lhs().
type();
4471 out <<
"; set_to true (equal)\n";
4472 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4491 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4502 out << found_literal->second;
4525 exprt lowered_expr = expr;
4532 it->id() == ID_byte_extract_little_endian ||
4533 it->id() == ID_byte_extract_big_endian)
4538 it->id() == ID_byte_update_little_endian ||
4539 it->id() == ID_byte_update_big_endian)
4545 return lowered_expr;
4562 "lower_byte_operators should remove all byte operators");
4567 return lowered_expr;
4575 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4580 for(
const auto &symbol : q_expr.variables())
4582 const auto identifier = symbol.get_identifier();
4584 id.type = symbol.type();
4595 if(expr.
id()==ID_symbol ||
4596 expr.
id()==ID_nondet_symbol)
4599 if(expr.
type().
id()==ID_code)
4604 if(expr.
id()==ID_symbol)
4607 identifier=
"nondet_"+
4612 if(
id.type.is_nil())
4614 id.type=expr.
type();
4619 out <<
"; find_symbols\n";
4620 out <<
"(declare-fun |"
4627 else if(expr.
id() == ID_array_of)
4634 const auto &array_type = array_of.type();
4638 out <<
"; the following is a substitute for lambda i. x\n";
4639 out <<
"(declare-fun " <<
id <<
" () ";
4644 out <<
"(assert (forall ((i ";
4646 out <<
")) (= (select " <<
id <<
" i) ";
4663 else if(expr.
id() == ID_array_comprehension)
4670 const auto &array_type = array_comprehension.type();
4671 const auto &array_size = array_type.size();
4675 out <<
"(declare-fun " <<
id <<
" () ";
4679 out <<
"; the following is a substitute for lambda i . x(i)\n";
4680 out <<
"; universally quantified initialization of the array\n";
4681 out <<
"(assert (forall ((";
4685 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
4692 out <<
")) (= (select " <<
id <<
" ";
4711 else if(expr.
id()==ID_array)
4718 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4719 out <<
"(declare-fun " <<
id <<
" () ";
4723 for(std::size_t i=0; i<expr.
operands().size(); i++)
4725 out <<
"(assert (= (select " <<
id <<
" ";
4738 out <<
"))" <<
"\n";
4744 else if(expr.
id()==ID_string_constant)
4754 out <<
"; the following is a substitute for a string" <<
"\n";
4755 out <<
"(declare-fun " <<
id <<
" () ";
4759 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4761 out <<
"(assert (= (select " << id;
4765 out <<
"))" <<
"\n";
4771 else if(expr.
id() == ID_object_size)
4775 if(op.
type().
id()==ID_pointer)
4781 out <<
"(declare-fun |" <<
id <<
"| () ";
4792 (expr.
id() == ID_floatbv_plus ||
4793 expr.
id() == ID_floatbv_minus ||
4794 expr.
id() == ID_floatbv_mult ||
4795 expr.
id() == ID_floatbv_div ||
4796 expr.
id() == ID_floatbv_typecast ||
4797 expr.
id() == ID_ieee_float_equal ||
4798 expr.
id() == ID_ieee_float_notequal ||
4799 ((expr.
id() == ID_lt ||
4800 expr.
id() == ID_gt ||
4801 expr.
id() == ID_le ||
4802 expr.
id() == ID_ge ||
4803 expr.
id() == ID_isnan ||
4804 expr.
id() == ID_isnormal ||
4805 expr.
id() == ID_isfinite ||
4806 expr.
id() == ID_isinf ||
4807 expr.
id() == ID_sign ||
4808 expr.
id() == ID_unary_minus ||
4809 expr.
id() == ID_typecast ||
4810 expr.
id() == ID_abs) &&
4817 if(
bvfp_set.insert(function).second)
4819 out <<
"; this is a model for " << expr.
id() <<
" : "
4822 <<
"(define-fun " << function <<
" (";
4824 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4828 out <<
"(op" << i <<
' ';
4838 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4865 if(expr.
id()==ID_with)
4867 else if(expr.
id()==ID_member)
4876 if(type.
id()==ID_array)
4889 out <<
"(_ BitVec 1)";
4895 else if(type.
id()==ID_bool)
4899 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4909 width != 0,
"failed to get width of struct");
4911 out <<
"(_ BitVec " << width <<
")";
4914 else if(type.
id()==ID_vector)
4924 width != 0,
"failed to get width of vector");
4926 out <<
"(_ BitVec " << width <<
")";
4929 else if(type.
id()==ID_code)
4936 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
4941 "failed to get width of union");
4943 out <<
"(_ BitVec " << width <<
")";
4945 else if(type.
id()==ID_pointer)
4950 else if(type.
id()==ID_bv ||
4951 type.
id()==ID_fixedbv ||
4952 type.
id()==ID_unsignedbv ||
4953 type.
id()==ID_signedbv ||
4954 type.
id()==ID_c_bool)
4959 else if(type.
id()==ID_c_enum)
4966 else if(type.
id()==ID_c_enum_tag)
4970 else if(type.
id()==ID_floatbv)
4975 out <<
"(_ FloatingPoint "
4976 << floatbv_type.
get_e() <<
" "
4977 << floatbv_type.
get_f() + 1 <<
")";
4982 else if(type.
id()==ID_rational ||
4985 else if(type.
id()==ID_integer)
4987 else if(type.
id()==ID_complex)
4997 width != 0,
"failed to get width of complex");
4999 out <<
"(_ BitVec " << width <<
")";
5002 else if(type.
id()==ID_c_bit_field)
5014 std::set<irep_idt> recstack;
5020 std::set<irep_idt> &recstack)
5022 if(type.
id()==ID_array)
5028 else if(type.
id()==ID_complex)
5035 const std::string smt_typename =
5039 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5040 <<
"(mk-" << smt_typename;
5042 out <<
" (" << smt_typename <<
".imag ";
5046 out <<
" (" << smt_typename <<
".real ";
5053 else if(type.
id()==ID_vector)
5062 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
5064 const std::string smt_typename =
5068 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5069 <<
"(mk-" << smt_typename;
5073 out <<
" (" << smt_typename <<
"." << i <<
" ";
5081 else if(type.
id() == ID_struct)
5084 bool need_decl=
false;
5088 const std::string smt_typename =
5103 const std::string &smt_typename =
datatype_map.at(type);
5114 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5115 <<
"(mk-" << smt_typename <<
" ";
5119 out <<
"(" << smt_typename <<
"." <<
component.get_name()
5125 out <<
"))))" <<
"\n";
5142 for(struct_union_typet::componentst::const_iterator
5143 it=components.begin();
5144 it!=components.end();
5148 out <<
"(define-fun update-" << smt_typename <<
"."
5150 <<
"((s " << smt_typename <<
") "
5153 out <<
")) " << smt_typename <<
" "
5154 <<
"(mk-" << smt_typename
5157 for(struct_union_typet::componentst::const_iterator
5158 it2=components.begin();
5159 it2!=components.end();
5166 out <<
"(" << smt_typename <<
"."
5167 << it2->get_name() <<
" s) ";
5171 out <<
"))" <<
"\n";
5177 else if(type.
id() == ID_union)
5185 else if(type.
id()==ID_code)
5189 for(
const auto ¶m : parameters)
5194 else if(type.
id()==ID_pointer)
5198 else if(type.
id() == ID_struct_tag)
5201 const irep_idt &
id = struct_tag.get_identifier();
5203 if(recstack.find(
id) == recstack.end())
5206 recstack.insert(
id);
5211 else if(type.
id() == ID_union_tag)
5214 const irep_idt &
id = union_tag.get_identifier();
5216 if(recstack.find(
id) == recstack.end())
5218 recstack.insert(
id);
void base_type(typet &type, const namespacet &ns)
API to expression classes for bitvectors.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
bitvector_typet index_type()
pointer_typet pointer_type(const typet &subtype)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
Array constructor from list of elements.
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Bit-wise negation of bit-vectors.
std::size_t get_width() const
const membert & get_member(const struct_typet &type, const irep_idt &member) const
The byte swap expression.
std::size_t get_bits_per_byte() const
std::vector< parametert > parameterst
const parameterst & parameters() const
struct configt::bv_encodingt bv_encoding
A constant literal expression.
const irep_idt & get_value() const
void set_value(const irep_idt &value)
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
depth_iteratort depth_end()
depth_iteratort depth_begin()
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The Boolean constant false.
std::size_t get_fraction_bits() const
Fixed-width bit-vector with signed fixed-point interpretation.
std::size_t get_fraction_bits() const
std::size_t get_integer_bits() const
Semantic type conversion from/to floating-point formats.
Fixed-width bit-vector with IEEE floating-point interpretation.
std::size_t get_f() const
std::size_t get_e() const
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
std::size_t width() const
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt NaN(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void build(const mp_integer &exp, const mp_integer &frac)
The trinary if-then-else operator.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
exprt & where()
convenience accessor for binding().where()
literalt get_literal() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_identifier() const
The plus expression Associativity is not specified.
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t get_invalid_object() const
numberingt< exprt, irep_hash > objects
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
A base class for quantifier expressions.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
const irep_idt & get_identifier() const
void convert_relation(const binary_relation_exprt &)
bool use_lambda_for_array
void convert_type(const typet &)
void unflatten(wheret, const typet &, unsigned nesting=0)
bool use_array_theory(const exprt &)
void find_symbols(const exprt &expr)
std::size_t number_of_solver_calls
void convert_typecast(const typecast_exprt &expr)
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
tvt l_get(literalt l) const
void convert_floatbv_rem(const binary_exprt &expr)
void convert_update(const exprt &expr)
std::set< irep_idt > bvfp_set
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
void push() override
Unimplemented.
void convert_is_dynamic_object(const unary_exprt &)
void convert_literal(const literalt)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
boolbv_widtht boolbv_width
void convert_constant(const constant_exprt &expr)
std::string floatbv_suffix(const exprt &) const
void flatten2bv(const exprt &)
void convert_div(const div_exprt &expr)
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
std::string type2id(const typet &) const
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
struct_exprt parse_struct(const irept &s, const struct_typet &type)
void convert_mult(const mult_exprt &expr)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
void define_object_size(const irep_idt &id, const exprt &expr)
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
bool use_check_sat_assuming
datatype_mapt datatype_map
void convert_mod(const mod_exprt &expr)
static std::string convert_identifier(const irep_idt &identifier)
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
std::unordered_map< irep_idt, bool > set_values
The values which boolean identifiers have been smt2_convt::set_to or in other words those which are a...
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
void convert_member(const member_exprt &expr)
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
void convert_index(const index_exprt &expr)
pointer_logict pointer_logic
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
void walk_array_tree(std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)
This function walks the SMT output and populates a map with index/value pairs for the array.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
defined_expressionst object_sizes
exprt parse_rec(const irept &s, const typet &type)
void convert_union(const union_exprt &expr)
exprt parse_union(const irept &s, const union_typet &type)
exprt parse_array(const irept &s, const array_typet &type)
This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array ...
std::vector< bool > boolean_assignment
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
void convert_with(const with_exprt &expr)
std::vector< exprt > assumptions
void convert_plus(const plus_exprt &expr)
defined_expressionst defined_expressions
void pop() override
Currently, only implements a single stack element (no nested contexts)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
identifier_mapt identifier_map
void convert_minus(const minus_exprt &expr)
void convert_expr(const exprt &)
constant_exprt parse_literal(const irept &, const typet &type)
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
std::size_t no_boolean_variables
smt2_identifierst smt2_identifiers
void convert_floatbv(const exprt &expr)
resultt dec_solve() override
Run the decision procedure to solve the problem.
literalt convert(const exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const irep_idt & get_name() const
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
Generic base class for unary expressions.
The unary minus expression.
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Deprecated expression utility functions.
exprt float_bv(const exprt &src)
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
static std::string binary(const constant_exprt &src)
bool is_true(const literalt &l)
literalt const_literal(bool value)
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
const std::string integer2binary(const mp_integer &n, std::size_t width)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNEXPECTEDCASE(S)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
int solver(std::istream &in)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bool has_byte_operator(const exprt &src)
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::size_t unsafe_string2size_t(const std::string &str, int base)
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.