51#define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
54#define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
58 const std::string &_benchmark,
59 const std::string &_notes,
60 const std::string &_logic,
63 : use_FPA_theory(false),
64 use_array_of_bool(false),
66 use_check_sat_assuming(false),
68 use_lambda_for_array(false),
72 benchmark(_benchmark),
78 no_boolean_variables(0)
151 "variable number shall be within bounds");
157 out <<
"; SMT 2" <<
"\n";
165 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
174 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
176 out <<
"(set-option :produce-models true)" <<
"\n";
182 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
195 out <<
"(check-sat-assuming (";
205 out <<
"; assumptions\n";
216 out <<
"(check-sat)\n";
224 out <<
"(get-value (|" <<
id <<
"|))"
232 out <<
"; end of SMT2 file"
244 std::size_t number = 0;
245 std::size_t h=pointer_width-1;
250 const typet &type = o.type();
253 numeric_cast<mp_integer>(size_expr.value_or(
nil_exprt()));
256 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
257 !size_expr.has_value() || !
object_size.has_value())
263 out <<
"(assert (=> (= "
264 <<
"((_ extract " << h <<
" " << l <<
") ";
267 <<
"(= |" <<
id <<
"| (_ bv" << *
object_size <<
" " << size_width
283 if(expr.
id()==ID_symbol)
290 return it->second.value;
293 else if(expr.
id()==ID_nondet_symbol)
300 return it->second.value;
302 else if(expr.
id()==ID_member)
310 else if(expr.
id() == ID_literal)
318 else if(expr.
id() == ID_not)
323 else if(op.is_false())
328 else if(
const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
330 exprt array_copy = *array;
331 for(
auto &element : array_copy.
operands())
333 element =
get(element);
368 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
373 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
384 else if(src.
get_sub().size()==2 &&
389 else if(src.
get_sub().size()==3 &&
392 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
396 else if(src.
get_sub().size()==4 &&
399 if(type.
id()==ID_floatbv)
408 const auto s1_int = numeric_cast_v<mp_integer>(
s1);
409 const auto s2_int = numeric_cast_v<mp_integer>(
s2);
410 const auto s3_int = numeric_cast_v<mp_integer>(s3);
414 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
420 else if(src.
get_sub().size()==4 &&
428 else if(src.
get_sub().size()==4 &&
436 else if(src.
get_sub().size()==4 &&
445 if(type.
id()==ID_signedbv ||
446 type.
id()==ID_unsignedbv ||
447 type.
id()==ID_c_enum ||
448 type.
id()==ID_c_bool)
452 else if(type.
id()==ID_c_enum_tag)
458 result.
type() = type;
461 else if(type.
id()==ID_fixedbv ||
462 type.
id()==ID_floatbv)
467 else if(type.
id()==ID_integer ||
475 "smt2_convt::parse_literal should not be of unsupported type " +
483 std::unordered_map<int64_t, exprt> operands_map;
487 auto maybe_default_op = operands_map.find(-1);
489 if(maybe_default_op == operands_map.end())
492 default_op = maybe_default_op->second;
494 auto maybe_size = numeric_cast<std::int64_t>(type.
size());
495 if(maybe_size.has_value())
497 while(i < maybe_size.value())
499 auto found_op = operands_map.find(i);
500 if(found_op != operands_map.end())
501 operands.emplace_back(found_op->second);
503 operands.emplace_back(default_op);
511 auto found_op = operands_map.find(i);
512 while(found_op != operands_map.end())
514 operands.emplace_back(found_op->second);
516 found_op = operands_map.find(i);
518 operands.emplace_back(default_op);
524 std::unordered_map<int64_t, exprt> *operands_map,
537 bool failure =
to_integer(index_constant, tempint);
540 long index = tempint.to_long();
542 operands_map->emplace(index, value);
544 else if(src.
get_sub().size() == 3 && src.
get_sub()[0].id() ==
"let")
549 operands_map, src.
get_sub()[1].get_sub()[0].get_sub()[1], type);
552 else if(src.
get_sub().size()==2 &&
553 src.
get_sub()[0].get_sub().size()==3 &&
554 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
555 src.
get_sub()[0].get_sub()[1].id()==
"const")
559 operands_map->emplace(-1, default_value);
586 if(components.empty())
594 if(src.
get_sub().size()!=components.size()+1)
597 for(std::size_t i=0; i<components.size(); i++)
614 std::size_t offset=0;
616 for(std::size_t i=0; i<components.size(); i++)
618 std::size_t component_width=
boolbv_width(components[i].type());
621 offset + component_width <= total_width,
622 "struct component bits shall be within struct bit vector");
624 std::string component_binary=
626 total_width-offset-component_width, component_width);
631 offset+=component_width;
641 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
642 type.
id() == ID_integer || type.
id() == ID_rational ||
643 type.
id() == ID_real || type.
id() == ID_c_enum ||
644 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
645 type.
id() == ID_floatbv)
649 else if(type.
id()==ID_bool)
651 if(src.
id()==ID_1 || src.
id()==ID_true)
653 else if(src.
id()==ID_0 || src.
id()==ID_false)
656 else if(type.
id()==ID_pointer)
662 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
667 ptr.
object = numeric_cast_v<std::size_t>(v / pow);
671 else if(type.
id()==ID_struct)
675 else if(type.
id() == ID_struct_tag)
680 struct_expr.type() = type;
681 return std::move(struct_expr);
683 else if(type.
id()==ID_union)
687 else if(type.
id() == ID_union_tag)
691 union_expr.type() = type;
694 else if(type.
id()==ID_array)
706 if(expr.
id()==ID_symbol ||
707 expr.
id()==ID_constant ||
708 expr.
id()==ID_string_constant ||
718 else if(expr.
id()==ID_index)
727 if(array.
type().
id()==ID_pointer)
729 else if(array.
type().
id()==ID_array)
749 else if(expr.
id()==ID_member)
754 const typet &struct_op_type = struct_op.
type();
757 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
758 "member expression operand shall have struct type");
775 else if(expr.
id()==ID_if)
790 "operand of address of expression should not be of kind " +
804 else if(expr.
id()==ID_literal)
816 out <<
"; convert\n";
817 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
824 std::string{
"|B"} + std::to_string(l.
var_no()) +
"|";
825 out <<
"(define-fun ";
837 if(expr.
type().
id() != ID_bool)
888 for(std::size_t i=0; i<identifier.
size(); i++)
890 char ch=identifier[i];
898 result+=std::to_string(ch);
913 if(type.
id()==ID_floatbv)
916 return "f"+std::to_string(spec.
width())+
"_"+std::to_string(spec.
f);
918 else if(type.
id()==ID_unsignedbv)
922 else if(type.
id()==ID_c_bool)
926 else if(type.
id()==ID_signedbv)
930 else if(type.
id()==ID_bool)
934 else if(type.
id()==ID_c_enum_tag)
938 else if(type.
id() == ID_pointer)
959 if(expr.
id()==ID_symbol)
966 if(expr.
id()==ID_smt2_symbol)
974 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
976 out <<
"(|float_bv." << expr.
id()
992 if(expr.
id()==ID_symbol)
998 else if(expr.
id()==ID_nondet_symbol)
1001 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1004 else if(expr.
id()==ID_smt2_symbol)
1010 else if(expr.
id()==ID_typecast)
1014 else if(expr.
id()==ID_floatbv_typecast)
1018 else if(expr.
id()==ID_struct)
1022 else if(expr.
id()==ID_union)
1026 else if(expr.
id()==ID_constant)
1030 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
1034 "concatenation over a single operand should have matching types",
1039 else if(expr.
id()==ID_concatenation ||
1040 expr.
id()==ID_bitand ||
1041 expr.
id()==ID_bitor ||
1042 expr.
id()==ID_bitxor ||
1043 expr.
id()==ID_bitnand ||
1044 expr.
id()==ID_bitnor)
1048 "given expression should have at least two operands",
1053 if(expr.
id()==ID_concatenation)
1055 else if(expr.
id()==ID_bitand)
1057 else if(expr.
id()==ID_bitor)
1059 else if(expr.
id()==ID_bitxor)
1061 else if(expr.
id()==ID_bitnand)
1063 else if(expr.
id()==ID_bitnor)
1074 else if(expr.
id()==ID_bitnot)
1078 if(bitnot_expr.
type().
id() == ID_vector)
1087 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1089 out <<
"(let ((?vectorop ";
1093 out <<
"(mk-" << smt_typename;
1100 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
1116 else if(expr.
id()==ID_unary_minus)
1121 unary_minus_expr.
type().
id() == ID_rational ||
1122 unary_minus_expr.
type().
id() == ID_integer ||
1123 unary_minus_expr.
type().
id() == ID_real)
1129 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1141 else if(unary_minus_expr.
type().
id() == ID_vector)
1145 const std::string &smt_typename =
1152 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1154 out <<
"(let ((?vectorop ";
1158 out <<
"(mk-" << smt_typename;
1165 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1181 else if(expr.
id()==ID_unary_plus)
1186 else if(expr.
id()==ID_sign)
1192 if(op_type.
id()==ID_floatbv)
1196 out <<
"(fp.isNegative ";
1203 else if(op_type.
id()==ID_signedbv)
1209 out <<
" (_ bv0 " << op_width <<
"))";
1214 "sign should not be applied to unsupported type",
1217 else if(expr.
id()==ID_if)
1229 else if(expr.
id()==ID_and ||
1234 expr.
type().
id() == ID_bool,
1235 "logical and, or, and xor expressions should have Boolean type");
1238 "logical and, or, and xor expressions should have at least two operands");
1240 out <<
"(" << expr.
id();
1248 else if(expr.
id()==ID_implies)
1253 implies_expr.
type().
id() == ID_bool,
1254 "implies expression should have Boolean type");
1262 else if(expr.
id()==ID_not)
1267 not_expr.
type().
id() == ID_bool,
1268 "not expression should have Boolean type");
1274 else if(expr.
id() == ID_equal)
1280 "operands of equal expression shall have same type");
1288 else if(expr.
id() == ID_notequal)
1294 "operands of not equal expression shall have same type");
1302 else if(expr.
id()==ID_ieee_float_equal ||
1303 expr.
id()==ID_ieee_float_notequal)
1310 rel_expr.lhs().type() == rel_expr.rhs().type(),
1311 "operands of float equal and not equal expressions shall have same type");
1316 if(rel_expr.id() == ID_ieee_float_notequal)
1325 if(rel_expr.id() == ID_ieee_float_notequal)
1331 else if(expr.
id()==ID_le ||
1338 else if(expr.
id()==ID_plus)
1342 else if(expr.
id()==ID_floatbv_plus)
1346 else if(expr.
id()==ID_minus)
1350 else if(expr.
id()==ID_floatbv_minus)
1354 else if(expr.
id()==ID_div)
1358 else if(expr.
id()==ID_floatbv_div)
1362 else if(expr.
id()==ID_mod)
1366 else if(expr.
id() == ID_euclidean_mod)
1370 else if(expr.
id()==ID_mult)
1374 else if(expr.
id()==ID_floatbv_mult)
1378 else if(expr.
id() == ID_floatbv_rem)
1382 else if(expr.
id()==ID_address_of)
1388 else if(expr.
id() == ID_array_of)
1393 array_of_expr.type().id() == ID_array,
1394 "array of expression shall have array type");
1398 out <<
"((as const ";
1406 defined_expressionst::const_iterator it =
1412 else if(expr.
id() == ID_array_comprehension)
1417 array_comprehension.type().id() == ID_array,
1418 "array_comprehension expression shall have array type");
1422 out <<
"(lambda ((";
1425 convert_type(array_comprehension.type().size().type());
1437 else if(expr.
id()==ID_index)
1441 else if(expr.
id()==ID_ashr ||
1442 expr.
id()==ID_lshr ||
1448 if(type.
id()==ID_unsignedbv ||
1449 type.
id()==ID_signedbv ||
1452 if(shift_expr.
id() == ID_ashr)
1454 else if(shift_expr.
id() == ID_lshr)
1456 else if(shift_expr.
id() == ID_shl)
1486 if(width_op0==width_op1)
1488 else if(width_op0>width_op1)
1490 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1496 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1503 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1510 "unsupported type for " + shift_expr.
id_string() +
": " +
1513 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1519 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1524 if(shift_expr.
id() == ID_rol)
1525 out <<
"((_ rotate_left";
1526 else if(shift_expr.
id() == ID_ror)
1527 out <<
"((_ rotate_right";
1533 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.
distance());
1535 if(distance_int_op.has_value())
1537 out << distance_int_op.value();
1541 "distance type for " + shift_expr.
id_string() +
"must be constant");
1550 "unsupported type for " + shift_expr.
id_string() +
": " +
1553 else if(expr.
id()==ID_with)
1557 else if(expr.
id()==ID_update)
1561 else if(expr.
id()==ID_member)
1565 else if(expr.
id()==ID_pointer_offset)
1570 op.type().id() == ID_pointer,
1571 "operand of pointer offset expression shall be of pointer type");
1573 std::size_t offset_bits =
1578 if(offset_bits>result_width)
1579 offset_bits=result_width;
1582 if(result_width>offset_bits)
1583 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1585 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1589 if(result_width>offset_bits)
1592 else if(expr.
id()==ID_pointer_object)
1597 op.type().id() == ID_pointer,
1598 "pointer object expressions should be of pointer type");
1604 out <<
"((_ zero_extend " << ext <<
") ";
1606 out <<
"((_ extract "
1607 << pointer_width-1 <<
" "
1615 else if(expr.
id() == ID_is_dynamic_object)
1619 else if(expr.
id() == ID_is_invalid_pointer)
1623 out <<
"(= ((_ extract "
1624 << pointer_width-1 <<
" "
1630 else if(expr.
id()==ID_string_constant)
1636 else if(expr.
id()==ID_extractbit)
1645 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1651 out <<
"(= ((_ extract 0 0) ";
1660 else if(expr.
id()==ID_extractbits)
1674 std::swap(op1_i, op2_i);
1678 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1685 out <<
"(= ((_ extract 0 0) ";
1694 SMT2_TODO(
"smt2: extractbits with non-constant index");
1697 else if(expr.
id()==ID_replication)
1701 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1703 out <<
"((_ repeat " << times <<
") ";
1707 else if(expr.
id()==ID_byte_extract_little_endian ||
1708 expr.
id()==ID_byte_extract_big_endian)
1711 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1713 else if(expr.
id()==ID_byte_update_little_endian ||
1714 expr.
id()==ID_byte_update_big_endian)
1717 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1719 else if(expr.
id()==ID_abs)
1725 if(type.
id()==ID_signedbv)
1729 out <<
"(ite (bvslt ";
1731 out <<
" (_ bv0 " << result_width <<
")) ";
1738 else if(type.
id()==ID_fixedbv)
1742 out <<
"(ite (bvslt ";
1744 out <<
" (_ bv0 " << result_width <<
")) ";
1751 else if(type.
id()==ID_floatbv)
1765 else if(expr.
id()==ID_isnan)
1771 if(op_type.
id()==ID_fixedbv)
1773 else if(op_type.
id()==ID_floatbv)
1777 out <<
"(fp.isNaN ";
1787 else if(expr.
id()==ID_isfinite)
1793 if(op_type.
id()==ID_fixedbv)
1795 else if(op_type.
id()==ID_floatbv)
1801 out <<
"(not (fp.isNaN ";
1805 out <<
"(not (fp.isInf ";
1817 else if(expr.
id()==ID_isinf)
1823 if(op_type.
id()==ID_fixedbv)
1825 else if(op_type.
id()==ID_floatbv)
1829 out <<
"(fp.isInfinite ";
1839 else if(expr.
id()==ID_isnormal)
1845 if(op_type.
id()==ID_fixedbv)
1847 else if(op_type.
id()==ID_floatbv)
1851 out <<
"(fp.isNormal ";
1861 else if(expr.
id()==ID_overflow_plus ||
1862 expr.
id()==ID_overflow_minus)
1868 expr.
type().
id() == ID_bool,
1869 "overflow plus and overflow minus expressions shall be of Boolean type");
1871 bool subtract=expr.
id()==ID_overflow_minus;
1872 const typet &op_type = op0.type();
1875 if(op_type.
id()==ID_signedbv)
1878 out <<
"(let ((?sum (";
1879 out << (subtract?
"bvsub":
"bvadd");
1880 out <<
" ((_ sign_extend 1) ";
1883 out <<
" ((_ sign_extend 1) ";
1887 "((_ extract " << width <<
" " << width <<
") ?sum) "
1888 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1891 else if(op_type.
id()==ID_unsignedbv ||
1892 op_type.
id()==ID_pointer)
1896 out <<
"((_ extract " << width <<
" " << width <<
") ";
1897 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1898 out <<
" ((_ zero_extend 1) ";
1901 out <<
" ((_ zero_extend 1) ";
1909 "overflow check should not be performed on unsupported type",
1912 else if(expr.
id()==ID_overflow_mult)
1918 expr.
type().
id() == ID_bool,
1919 "overflow mult expression shall be of Boolean type");
1924 const typet &op_type = op0.type();
1927 if(op_type.
id()==ID_signedbv)
1929 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1931 out <<
") ((_ sign_extend " << width <<
") ";
1934 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
1936 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" "
1937 << width*2 <<
")))))";
1939 else if(op_type.
id()==ID_unsignedbv)
1941 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1943 out <<
") ((_ zero_extend " << width <<
") ";
1945 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1950 "overflow check should not be performed on unsupported type",
1953 else if(expr.
id()==ID_array)
1959 else if(expr.
id()==ID_literal)
1963 else if(expr.
id()==ID_forall ||
1964 expr.
id()==ID_exists)
1970 throw "MathSAT does not support quantifiers";
1972 if(quantifier_expr.
id() == ID_forall)
1974 else if(quantifier_expr.
id() == ID_exists)
1978 for(
const auto &bound : quantifier_expr.
variables())
1992 else if(expr.
id()==ID_vector)
1997 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
2000 size == vector_expr.
operands().size(),
2001 "size indicated by type shall be equal to the number of operands");
2005 const std::string &smt_typename =
datatype_map.at(vector_type);
2007 out <<
"(mk-" << smt_typename;
2021 else if(expr.
id()==ID_object_size)
2025 else if(expr.
id()==ID_let)
2028 const auto &variables = let_expr.
variables();
2029 const auto &values = let_expr.
values();
2034 for(
auto &binding :
make_range(variables).zip(values))
2053 else if(expr.
id()==ID_constraint_select_one)
2056 "smt2_convt::convert_expr: '" + expr.
id_string() +
2057 "' is not yet supported");
2059 else if(expr.
id() == ID_bswap)
2065 "operand of byte swap expression shall have same type as the expression");
2068 out <<
"(let ((bswap_op ";
2073 bswap_expr.
type().
id() == ID_signedbv ||
2074 bswap_expr.
type().
id() == ID_unsignedbv)
2076 const std::size_t width =
2083 width % bits_per_byte == 0,
2084 "bit width indicated by type of bswap expression should be a multiple "
2085 "of the number of bits per byte");
2087 const std::size_t bytes = width / bits_per_byte;
2096 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2100 out <<
"(bswap_byte_" <<
byte <<
' ';
2101 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2102 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2111 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2112 out <<
" bswap_byte_" <<
byte;
2123 else if(expr.
id() == ID_popcount)
2127 else if(expr.
id() == ID_count_leading_zeros)
2131 else if(expr.
id() == ID_count_trailing_zeros)
2135 else if(expr.
id() == ID_empty_union)
2139 else if(expr.
id() == ID_bitreverse)
2146 "smt2_convt::convert_expr should not be applied to unsupported type",
2155 if(dest_type.
id()==ID_c_enum_tag)
2159 if(src_type.
id()==ID_c_enum_tag)
2162 if(dest_type.
id()==ID_bool)
2165 if(src_type.
id()==ID_signedbv ||
2166 src_type.
id()==ID_unsignedbv ||
2167 src_type.
id()==ID_c_bool ||
2168 src_type.
id()==ID_fixedbv ||
2169 src_type.
id()==ID_pointer ||
2170 src_type.
id()==ID_integer)
2178 else if(src_type.
id()==ID_floatbv)
2182 out <<
"(not (fp.isZero ";
2194 else if(dest_type.
id()==ID_c_bool)
2203 out <<
" (_ bv1 " << to_width <<
")";
2204 out <<
" (_ bv0 " << to_width <<
")";
2207 else if(dest_type.
id()==ID_signedbv ||
2208 dest_type.
id()==ID_unsignedbv ||
2209 dest_type.
id()==ID_c_enum ||
2210 dest_type.
id()==ID_bv)
2214 if(src_type.
id()==ID_signedbv ||
2215 src_type.
id()==ID_unsignedbv ||
2216 src_type.
id()==ID_c_bool ||
2217 src_type.
id()==ID_c_enum ||
2218 src_type.
id()==ID_bv)
2222 if(from_width==to_width)
2224 else if(from_width<to_width)
2226 if(src_type.
id()==ID_signedbv)
2227 out <<
"((_ sign_extend ";
2229 out <<
"((_ zero_extend ";
2231 out << (to_width-from_width)
2238 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2243 else if(src_type.
id()==ID_fixedbv)
2247 std::size_t from_width=fixedbv_type.
get_width();
2254 out <<
"(let ((?tcop ";
2260 if(to_width>from_integer_bits)
2262 out <<
"((_ sign_extend "
2263 << (to_width-from_integer_bits) <<
") ";
2264 out <<
"((_ extract " << (from_width-1) <<
" "
2265 << from_fraction_bits <<
") ";
2271 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2272 <<
" " << from_fraction_bits <<
") ";
2277 out <<
" (ite (and ";
2280 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2281 "(_ bv0 " << from_fraction_bits <<
")))";
2284 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2289 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2293 else if(src_type.
id()==ID_floatbv)
2295 if(dest_type.
id()==ID_bv)
2312 else if(dest_type.
id()==ID_signedbv)
2316 "typecast unexpected "+src_type.
id_string()+
" -> "+
2319 else if(dest_type.
id()==ID_unsignedbv)
2323 "typecast unexpected "+src_type.
id_string()+
" -> "+
2327 else if(src_type.
id()==ID_bool)
2332 if(dest_type.
id()==ID_fixedbv)
2335 out <<
" (concat (_ bv1 "
2338 "(_ bv0 " << spec.
width <<
")";
2342 out <<
" (_ bv1 " << to_width <<
")";
2343 out <<
" (_ bv0 " << to_width <<
")";
2348 else if(src_type.
id()==ID_pointer)
2352 if(from_width<to_width)
2354 out <<
"((_ sign_extend ";
2355 out << (to_width-from_width)
2362 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2367 else if(src_type.
id()==ID_integer)
2373 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2376 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2379 src_type.
id() == ID_struct ||
2380 src_type.
id() == ID_struct_tag)
2386 "bit vector with of source and destination type shall be equal");
2393 "bit vector with of source and destination type shall be equal");
2398 src_type.
id() == ID_union ||
2399 src_type.
id() == ID_union_tag)
2403 "bit vector with of source and destination type shall be equal");
2406 else if(src_type.
id()==ID_c_bit_field)
2410 if(from_width==to_width)
2421 std::ostringstream e_str;
2422 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2423 <<
" src == " <<
format(src);
2427 else if(dest_type.
id()==ID_fixedbv)
2433 if(src_type.
id()==ID_unsignedbv ||
2434 src_type.
id()==ID_signedbv ||
2435 src_type.
id()==ID_c_enum)
2442 if(from_width==to_integer_bits)
2444 else if(from_width>to_integer_bits)
2447 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2455 from_width < to_integer_bits,
2456 "from_width should be smaller than to_integer_bits as other case "
2457 "have been handled above");
2458 if(dest_type.
id()==ID_unsignedbv)
2460 out <<
"(_ zero_extend "
2461 << (to_integer_bits-from_width) <<
") ";
2467 out <<
"((_ sign_extend "
2468 << (to_integer_bits-from_width) <<
") ";
2474 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2477 else if(src_type.
id()==ID_bool)
2479 out <<
"(concat (concat"
2480 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2486 else if(src_type.
id()==ID_fixedbv)
2491 std::size_t from_width=from_fixedbv_type.
get_width();
2493 out <<
"(let ((?tcop ";
2499 if(to_integer_bits<=from_integer_bits)
2501 out <<
"((_ extract "
2502 << (from_fraction_bits+to_integer_bits-1) <<
" "
2503 << from_fraction_bits
2509 to_integer_bits > from_integer_bits,
2510 "to_integer_bits should be greater than from_integer_bits as the"
2511 "other case has been handled above");
2512 out <<
"((_ sign_extend "
2513 << (to_integer_bits-from_integer_bits)
2515 << (from_width-1) <<
" "
2516 << from_fraction_bits
2522 if(to_fraction_bits<=from_fraction_bits)
2524 out <<
"((_ extract "
2525 << (from_fraction_bits-1) <<
" "
2526 << (from_fraction_bits-to_fraction_bits)
2532 to_fraction_bits > from_fraction_bits,
2533 "to_fraction_bits should be greater than from_fraction_bits as the"
2534 "other case has been handled above");
2535 out <<
"(concat ((_ extract "
2536 << (from_fraction_bits-1) <<
" 0) ";
2539 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2548 else if(dest_type.
id()==ID_pointer)
2552 if(src_type.
id()==ID_pointer)
2558 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2559 src_type.
id() == ID_bv)
2565 if(from_width==to_width)
2567 else if(from_width<to_width)
2569 out <<
"((_ sign_extend "
2570 << (to_width-from_width)
2577 out <<
"((_ extract " << to_width <<
" 0) ";
2585 else if(dest_type.
id()==ID_range)
2589 else if(dest_type.
id()==ID_floatbv)
2598 if(src_type.
id()==ID_bool)
2613 a.
build(significand, exponent);
2621 a.
build(significand, exponent);
2627 else if(src_type.
id()==ID_c_bool)
2633 else if(src_type.
id() == ID_bv)
2642 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2643 << dest_floatbv_type.get_f() + 1 <<
") ";
2653 else if(dest_type.
id()==ID_integer)
2655 if(src_type.
id()==ID_bool)
2664 else if(dest_type.
id()==ID_c_bit_field)
2669 if(from_width==to_width)
2690 if(dest_type.
id()==ID_floatbv)
2692 if(src_type.
id()==ID_floatbv)
2719 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2720 << dst.
get_f() + 1 <<
") ";
2729 else if(src_type.
id()==ID_unsignedbv)
2750 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
2751 << dst.
get_f() + 1 <<
") ";
2760 else if(src_type.
id()==ID_signedbv)
2768 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2769 << dst.
get_f() + 1 <<
") ";
2778 else if(src_type.
id()==ID_c_enum_tag)
2792 else if(dest_type.
id()==ID_signedbv)
2797 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2806 else if(dest_type.
id()==ID_unsignedbv)
2811 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2835 components.size() == expr.
operands().size(),
2836 "number of struct components as indicated by the struct type shall be equal"
2837 "to the number of operands of the struct expression");
2839 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2843 const std::string &smt_typename =
datatype_map.at(struct_type);
2846 out <<
"(mk-" << smt_typename;
2849 for(struct_typet::componentst::const_iterator
2850 it=components.begin();
2851 it!=components.end();
2862 if(components.size()==1)
2867 for(std::size_t i=components.size(); i>1; i--)
2874 if(op.
type().
id() == ID_array)
2884 for(std::size_t i=1; i<components.size(); i++)
2894 const auto &size_expr = array_type.
size();
2900 out <<
"(let ((?far ";
2908 out <<
"(select ?far ";
2929 total_width != 0,
"failed to get union width for union");
2933 member_width != 0,
"failed to get union member width for union");
2935 if(total_width==member_width)
2943 total_width > member_width,
2944 "total_width should be greater than member_width as member_width can be"
2945 "at most as large as total_width and the other case has been handled "
2949 << (total_width-member_width) <<
") ";
2959 if(expr_type.
id()==ID_unsignedbv ||
2960 expr_type.
id()==ID_signedbv ||
2961 expr_type.
id()==ID_bv ||
2962 expr_type.
id()==ID_c_enum ||
2963 expr_type.
id()==ID_c_enum_tag ||
2964 expr_type.
id()==ID_c_bool ||
2965 expr_type.
id()==ID_c_bit_field)
2971 out <<
"(_ bv" << value
2972 <<
" " << width <<
")";
2974 else if(expr_type.
id()==ID_fixedbv)
2980 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2982 else if(expr_type.
id()==ID_floatbv)
2995 size_t e=floatbv_type.
get_e();
2996 size_t f=floatbv_type.
get_f()+1;
3002 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3008 out <<
"(_ NaN " << e <<
" " << f <<
")";
3013 out <<
"(_ -oo " << e <<
" " << f <<
")";
3015 out <<
"(_ +oo " << e <<
" " << f <<
")";
3025 <<
"#b" << binaryString.substr(0, 1) <<
" "
3026 <<
"#b" << binaryString.substr(1, e) <<
" "
3027 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
3035 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3038 else if(expr_type.
id()==ID_pointer)
3050 else if(expr_type.
id()==ID_bool)
3059 else if(expr_type.
id()==ID_array)
3065 else if(expr_type.
id()==ID_rational)
3068 const bool negative =
has_prefix(value,
"-");
3073 size_t pos=value.find(
"/");
3075 if(
pos==std::string::npos)
3076 out << value <<
".0";
3079 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3080 << value.substr(
pos+1) <<
".0)";
3086 else if(expr_type.
id()==ID_integer)
3092 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3102 if(expr.
type().
id() == ID_integer)
3112 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3117 if(expr.
type().
id()==ID_unsignedbv ||
3118 expr.
type().
id()==ID_signedbv)
3120 if(expr.
type().
id()==ID_unsignedbv)
3136 std::vector<std::size_t> dynamic_objects;
3139 if(dynamic_objects.empty())
3145 out <<
"(let ((?obj ((_ extract "
3146 << pointer_width-1 <<
" "
3151 if(dynamic_objects.size()==1)
3153 out <<
"(= (_ bv" << dynamic_objects.front()
3160 for(
const auto &
object : dynamic_objects)
3161 out <<
" (= (_ bv" <<
object
3175 if(op_type.
id()==ID_unsignedbv ||
3176 op_type.
id()==ID_bv)
3179 if(expr.
id()==ID_le)
3181 else if(expr.
id()==ID_lt)
3183 else if(expr.
id()==ID_ge)
3185 else if(expr.
id()==ID_gt)
3194 else if(op_type.
id()==ID_signedbv ||
3195 op_type.
id()==ID_fixedbv)
3198 if(expr.
id()==ID_le)
3200 else if(expr.
id()==ID_lt)
3202 else if(expr.
id()==ID_ge)
3204 else if(expr.
id()==ID_gt)
3213 else if(op_type.
id()==ID_floatbv)
3218 if(expr.
id()==ID_le)
3220 else if(expr.
id()==ID_lt)
3222 else if(expr.
id()==ID_ge)
3224 else if(expr.
id()==ID_gt)
3236 else if(op_type.
id()==ID_rational ||
3237 op_type.
id()==ID_integer)
3248 else if(op_type.
id() == ID_pointer)
3256 if(expr.
id() == ID_le)
3258 else if(expr.
id() == ID_lt)
3260 else if(expr.
id() == ID_ge)
3262 else if(expr.
id() == ID_gt)
3281 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3282 expr.
type().
id() == ID_real)
3287 for(
const auto &op : expr.
operands())
3296 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3297 expr.
type().
id() == ID_fixedbv)
3314 else if(expr.
type().
id() == ID_floatbv)
3321 else if(expr.
type().
id() == ID_pointer)
3327 if(p.
type().
id() != ID_pointer)
3331 p.
type().
id() == ID_pointer,
3332 "one of the operands should have pointer type");
3346 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3347 element_size = *element_size_opt;
3354 if(element_size >= 2)
3371 else if(expr.
type().
id() == ID_vector)
3375 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3381 const std::string &smt_typename =
datatype_map.at(vector_type);
3383 out <<
"(mk-" << smt_typename;
3392 summands.reserve(expr.
operands().size());
3393 for(
const auto &op : expr.
operands())
3427 if(expr.
id()==ID_constant)
3431 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3434 out <<
"roundNearestTiesToEven";
3436 out <<
"roundTowardNegative";
3438 out <<
"roundTowardPositive";
3440 out <<
"roundTowardZero";
3444 "Rounding mode should have value 0, 1, 2, or 3",
3452 out <<
"(ite (= (_ bv0 " << width <<
") ";
3454 out <<
") roundNearestTiesToEven ";
3456 out <<
"(ite (= (_ bv1 " << width <<
") ";
3458 out <<
") roundTowardNegative ";
3460 out <<
"(ite (= (_ bv2 " << width <<
") ";
3462 out <<
") roundTowardPositive ";
3465 out <<
"roundTowardZero";
3476 type.
id() == ID_floatbv ||
3477 (type.
id() == ID_complex &&
3479 (type.
id() == ID_vector &&
3484 if(type.
id()==ID_floatbv)
3494 else if(type.
id()==ID_complex)
3498 else if(type.
id()==ID_vector)
3505 "type should not be one of the unsupported types",
3514 if(expr.
type().
id()==ID_integer)
3522 else if(expr.
type().
id()==ID_unsignedbv ||
3523 expr.
type().
id()==ID_signedbv ||
3524 expr.
type().
id()==ID_fixedbv)
3526 if(expr.
op0().
type().
id()==ID_pointer &&
3532 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3534 if(*element_size >= 2)
3539 "bitvector width of operand shall be equal to the bitvector width of "
3548 if(*element_size >= 2)
3561 else if(expr.
type().
id()==ID_floatbv)
3568 else if(expr.
type().
id()==ID_pointer)
3572 else if(expr.
type().
id()==ID_vector)
3576 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3582 const std::string &smt_typename =
datatype_map.at(vector_type);
3584 out <<
"(mk-" << smt_typename;
3612 expr.
type().
id() == ID_floatbv,
3613 "type of ieee floating point expression shall be floatbv");
3631 if(expr.
type().
id()==ID_unsignedbv ||
3632 expr.
type().
id()==ID_signedbv)
3634 if(expr.
type().
id()==ID_unsignedbv)
3644 else if(expr.
type().
id()==ID_fixedbv)
3649 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3654 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3656 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3662 else if(expr.
type().
id()==ID_floatbv)
3676 expr.
type().
id() == ID_floatbv,
3677 "type of ieee floating point expression shall be floatbv");
3708 "expression should have been converted to a variant with two operands");
3710 if(expr.
type().
id()==ID_unsignedbv ||
3711 expr.
type().
id()==ID_signedbv)
3722 else if(expr.
type().
id()==ID_floatbv)
3729 else if(expr.
type().
id()==ID_fixedbv)
3734 out <<
"((_ extract "
3735 << spec.
width+fraction_bits-1 <<
" "
3736 << fraction_bits <<
") ";
3740 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3744 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3750 else if(expr.
type().
id()==ID_rational ||
3751 expr.
type().
id()==ID_integer ||
3752 expr.
type().
id()==ID_real)
3771 expr.
type().
id() == ID_floatbv,
3772 "type of ieee floating point expression shall be floatbv");
3791 expr.
type().
id() == ID_floatbv,
3792 "type of ieee floating point expression shall be floatbv");
3806 "smt2_convt::convert_floatbv_rem to be implemented when not using "
3817 std::size_t s=expr.
operands().size();
3832 "with expression should have been converted to a version with three "
3837 if(expr_type.
id()==ID_array)
3861 out <<
"(let ((distance? ";
3862 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3866 if(array_width>index_width)
3868 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3874 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3884 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
3886 out <<
"distance?)) ";
3890 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3892 out <<
") distance?)))";
3895 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
3902 const irep_idt &component_name=index.
get(ID_component_name);
3906 "struct should have accessed component");
3910 const std::string &smt_typename =
datatype_map.at(expr_type);
3912 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3926 out <<
"(let ((?withop ";
3930 if(m.
width==struct_width)
3940 <<
"((_ extract " << (struct_width-1) <<
" "
3941 << m.
width <<
") ?withop) ";
3950 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
3955 out <<
"(concat (concat "
3956 <<
"((_ extract " << (struct_width-1) <<
" "
3959 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3966 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
3974 total_width != 0,
"failed to get union width for with");
3978 member_width != 0,
"failed to get union member width for with");
3980 if(total_width==member_width)
3987 total_width > member_width,
3988 "total width should be greater than member_width as member_width is at "
3989 "most as large as total_width and the other case has been handled "
3992 out <<
"((_ extract "
3994 <<
" " << member_width <<
") ";
4001 else if(expr_type.
id()==ID_bv ||
4002 expr_type.
id()==ID_unsignedbv ||
4003 expr_type.
id()==ID_signedbv)
4009 total_width != 0,
"failed to get total width");
4016 value_width != 0,
"failed to get value width");
4028 out <<
" (bvnot (bvshl";
4031 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
4032 out <<
" (repeat[" << value_width <<
"] bv1[1])";
4054 "with expects struct, union, or array type, but got "+
4062 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4069 if(array_op_type.
id()==ID_array)
4105 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
4109 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4113 if(array_width>index_width)
4115 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4121 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4131 else if(array_op_type.
id()==ID_vector)
4137 const std::string &smt_typename =
datatype_map.at(vector_type);
4141 const auto index_int = numeric_cast<mp_integer>(expr.
index());
4142 if(!index_int.has_value())
4144 SMT2_TODO(
"non-constant index on vectors");
4148 out <<
"(" << smt_typename <<
"." << *index_int <<
" ";
4160 false,
"index with unsupported array type: " + array_op_type.
id_string());
4167 const typet &struct_op_type = struct_op.
type();
4170 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
4175 struct_type.
has_component(name),
"struct should have accessed component");
4179 const std::string &smt_typename =
datatype_map.at(struct_type);
4181 out <<
"(" << smt_typename <<
"."
4194 member_offset.has_value(),
"failed to get struct member offset");
4203 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4207 width != 0,
"failed to get union member width");
4211 out <<
"((_ extract "
4221 "convert_member on an unexpected type "+struct_op_type.
id_string());
4228 if(type.
id()==ID_bool)
4234 else if(type.
id()==ID_vector)
4238 const std::string &smt_typename =
datatype_map.at(type);
4243 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4245 out <<
"(let ((?vflop ";
4253 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
4261 else if(type.
id()==ID_array)
4265 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4269 const std::string &smt_typename =
datatype_map.at(type);
4274 out <<
"(let ((?sflop ";
4282 for(std::size_t i=components.size(); i>1; i--)
4284 out <<
"(concat (" << smt_typename <<
"."
4285 << components[i-1].get_name() <<
" ?sflop)";
4290 out <<
"(" << smt_typename <<
"."
4291 << components[0].get_name() <<
" ?sflop)";
4293 for(std::size_t i=1; i<components.size(); i++)
4301 else if(type.
id()==ID_floatbv)
4305 "floatbv expressions should be flattened when using FPA theory");
4318 if(type.
id()==ID_bool)
4325 else if(type.
id()==ID_vector)
4329 const std::string &smt_typename =
datatype_map.at(type);
4336 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4339 out <<
"(let ((?ufop" << nesting <<
" ";
4344 out <<
"(mk-" << smt_typename;
4346 std::size_t offset=0;
4348 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4352 out <<
"((_ extract " << offset+subtype_width-1 <<
" "
4353 << offset <<
") ?ufop" << nesting <<
")";
4365 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4371 out <<
"(let ((?ufop" << nesting <<
" ";
4376 const std::string &smt_typename =
datatype_map.at(type);
4378 out <<
"(mk-" << smt_typename;
4385 std::size_t offset=0;
4388 for(struct_typet::componentst::const_iterator
4389 it=components.begin();
4390 it!=components.end();
4397 out <<
"((_ extract " << offset+member_width-1 <<
" "
4398 << offset <<
") ?ufop" << nesting <<
")";
4400 offset+=member_width;
4421 if(expr.
id()==ID_and && value)
4428 if(expr.
id()==ID_or && !value)
4435 if(expr.
id()==ID_not)
4445 if(expr.
id() == ID_equal && value)
4449 equal_expr.
lhs().
type().
id() == ID_empty ||
4450 equal_expr.
rhs().
id() == ID_empty_union)
4456 if(equal_expr.
lhs().
id()==ID_symbol)
4466 id.type=equal_expr.
lhs().
type();
4473 out <<
"; set_to true (equal)\n";
4474 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4493 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4504 out << found_literal->second;
4527 exprt lowered_expr = expr;
4534 it->id() == ID_byte_extract_little_endian ||
4535 it->id() == ID_byte_extract_big_endian)
4540 it->id() == ID_byte_update_little_endian ||
4541 it->id() == ID_byte_update_big_endian)
4547 return lowered_expr;
4564 "lower_byte_operators should remove all byte operators");
4569 return lowered_expr;
4577 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4582 for(
const auto &symbol : q_expr.variables())
4584 const auto identifier = symbol.get_identifier();
4586 id.type = symbol.type();
4597 if(expr.
id()==ID_symbol ||
4598 expr.
id()==ID_nondet_symbol)
4601 if(expr.
type().
id()==ID_code)
4606 if(expr.
id()==ID_symbol)
4609 identifier=
"nondet_"+
4614 if(
id.type.is_nil())
4616 id.type=expr.
type();
4621 out <<
"; find_symbols\n";
4622 out <<
"(declare-fun |"
4629 else if(expr.
id() == ID_array_of)
4636 const auto &array_type = array_of.type();
4640 out <<
"; the following is a substitute for lambda i. x\n";
4641 out <<
"(declare-fun " <<
id <<
" () ";
4646 out <<
"(assert (forall ((i ";
4648 out <<
")) (= (select " <<
id <<
" i) ";
4665 else if(expr.
id() == ID_array_comprehension)
4672 const auto &array_type = array_comprehension.type();
4673 const auto &array_size = array_type.size();
4677 out <<
"(declare-fun " <<
id <<
" () ";
4681 out <<
"; the following is a substitute for lambda i . x(i)\n";
4682 out <<
"; universally quantified initialization of the array\n";
4683 out <<
"(assert (forall ((";
4687 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
4694 out <<
")) (= (select " <<
id <<
" ";
4713 else if(expr.
id()==ID_array)
4720 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4721 out <<
"(declare-fun " <<
id <<
" () ";
4725 for(std::size_t i=0; i<expr.
operands().size(); i++)
4727 out <<
"(assert (= (select " <<
id <<
" ";
4740 out <<
"))" <<
"\n";
4746 else if(expr.
id()==ID_string_constant)
4756 out <<
"; the following is a substitute for a string" <<
"\n";
4757 out <<
"(declare-fun " <<
id <<
" () ";
4761 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4763 out <<
"(assert (= (select " << id;
4767 out <<
"))" <<
"\n";
4773 else if(expr.
id() == ID_object_size)
4777 if(op.
type().
id()==ID_pointer)
4783 out <<
"(declare-fun |" <<
id <<
"| () ";
4794 (expr.
id() == ID_floatbv_plus ||
4795 expr.
id() == ID_floatbv_minus ||
4796 expr.
id() == ID_floatbv_mult ||
4797 expr.
id() == ID_floatbv_div ||
4798 expr.
id() == ID_floatbv_typecast ||
4799 expr.
id() == ID_ieee_float_equal ||
4800 expr.
id() == ID_ieee_float_notequal ||
4801 ((expr.
id() == ID_lt ||
4802 expr.
id() == ID_gt ||
4803 expr.
id() == ID_le ||
4804 expr.
id() == ID_ge ||
4805 expr.
id() == ID_isnan ||
4806 expr.
id() == ID_isnormal ||
4807 expr.
id() == ID_isfinite ||
4808 expr.
id() == ID_isinf ||
4809 expr.
id() == ID_sign ||
4810 expr.
id() == ID_unary_minus ||
4811 expr.
id() == ID_typecast ||
4812 expr.
id() == ID_abs) &&
4819 if(
bvfp_set.insert(function).second)
4821 out <<
"; this is a model for " << expr.
id() <<
" : "
4824 <<
"(define-fun " << function <<
" (";
4826 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4830 out <<
"(op" << i <<
' ';
4840 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4867 if(expr.
id()==ID_with)
4869 else if(expr.
id()==ID_member)
4878 if(type.
id()==ID_array)
4891 out <<
"(_ BitVec 1)";
4897 else if(type.
id()==ID_bool)
4901 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4911 width != 0,
"failed to get width of struct");
4913 out <<
"(_ BitVec " << width <<
")";
4916 else if(type.
id()==ID_vector)
4926 width != 0,
"failed to get width of vector");
4928 out <<
"(_ BitVec " << width <<
")";
4931 else if(type.
id()==ID_code)
4938 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
4943 "failed to get width of union");
4945 out <<
"(_ BitVec " << width <<
")";
4947 else if(type.
id()==ID_pointer)
4952 else if(type.
id()==ID_bv ||
4953 type.
id()==ID_fixedbv ||
4954 type.
id()==ID_unsignedbv ||
4955 type.
id()==ID_signedbv ||
4956 type.
id()==ID_c_bool)
4961 else if(type.
id()==ID_c_enum)
4968 else if(type.
id()==ID_c_enum_tag)
4972 else if(type.
id()==ID_floatbv)
4977 out <<
"(_ FloatingPoint "
4978 << floatbv_type.
get_e() <<
" "
4979 << floatbv_type.
get_f() + 1 <<
")";
4984 else if(type.
id()==ID_rational ||
4987 else if(type.
id()==ID_integer)
4989 else if(type.
id()==ID_complex)
4999 width != 0,
"failed to get width of complex");
5001 out <<
"(_ BitVec " << width <<
")";
5004 else if(type.
id()==ID_c_bit_field)
5016 std::set<irep_idt> recstack;
5022 std::set<irep_idt> &recstack)
5024 if(type.
id()==ID_array)
5030 else if(type.
id()==ID_complex)
5037 const std::string smt_typename =
5041 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5042 <<
"(mk-" << smt_typename;
5044 out <<
" (" << smt_typename <<
".imag ";
5048 out <<
" (" << smt_typename <<
".real ";
5055 else if(type.
id()==ID_vector)
5064 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
5066 const std::string smt_typename =
5070 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5071 <<
"(mk-" << smt_typename;
5075 out <<
" (" << smt_typename <<
"." << i <<
" ";
5083 else if(type.
id() == ID_struct)
5086 bool need_decl=
false;
5090 const std::string smt_typename =
5105 const std::string &smt_typename =
datatype_map.at(type);
5116 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5117 <<
"(mk-" << smt_typename <<
" ";
5121 out <<
"(" << smt_typename <<
"." <<
component.get_name()
5127 out <<
"))))" <<
"\n";
5144 for(struct_union_typet::componentst::const_iterator
5145 it=components.begin();
5146 it!=components.end();
5150 out <<
"(define-fun update-" << smt_typename <<
"."
5152 <<
"((s " << smt_typename <<
") "
5155 out <<
")) " << smt_typename <<
" "
5156 <<
"(mk-" << smt_typename
5159 for(struct_union_typet::componentst::const_iterator
5160 it2=components.begin();
5161 it2!=components.end();
5168 out <<
"(" << smt_typename <<
"."
5169 << it2->get_name() <<
" s) ";
5173 out <<
"))" <<
"\n";
5179 else if(type.
id() == ID_union)
5187 else if(type.
id()==ID_code)
5191 for(
const auto ¶m : parameters)
5196 else if(type.
id()==ID_pointer)
5200 else if(type.
id() == ID_struct_tag)
5203 const irep_idt &
id = struct_tag.get_identifier();
5205 if(recstack.find(
id) == recstack.end())
5208 recstack.insert(
id);
5213 else if(type.
id() == ID_union_tag)
5216 const irep_idt &
id = union_tag.get_identifier();
5218 if(recstack.find(
id) == recstack.end())
5220 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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#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)