48 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
51 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
55 const std::string &_benchmark,
56 const std::string &_notes,
57 const std::string &_logic,
60 : use_FPA_theory(false),
61 use_array_of_bool(false),
63 use_check_sat_assuming(false),
65 use_lambda_for_array(false),
69 benchmark(_benchmark),
75 no_boolean_variables(0)
147 "variable number shall be within bounds");
153 out <<
"; SMT 2" <<
"\n";
161 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
170 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
172 out <<
"(set-option :produce-models true)" <<
"\n";
178 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
191 out <<
"(check-sat-assuming (";
201 out <<
"; assumptions\n";
212 out <<
"(check-sat)\n";
220 out <<
"(get-value (|" <<
id <<
"|))"
228 out <<
"; end of SMT2 file"
240 std::size_t number = 0;
241 std::size_t h=pointer_width-1;
246 const typet &type = o.type();
249 numeric_cast<mp_integer>(size_expr.value_or(
nil_exprt()));
252 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
253 !size_expr.has_value() || !
object_size.has_value())
259 out <<
"(assert (=> (= "
260 <<
"((_ extract " << h <<
" " << l <<
") ";
263 <<
"(= |" <<
id <<
"| (_ bv" << *
object_size <<
" " << size_width
279 if(expr.
id()==ID_symbol)
286 return it->second.value;
289 else if(expr.
id()==ID_nondet_symbol)
296 return it->second.value;
298 else if(expr.
id()==ID_member)
306 else if(expr.
id() == ID_literal)
314 else if(expr.
id() == ID_not)
319 else if(op.is_false())
324 else if(
const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
326 exprt array_copy = *array;
327 for(
auto &element : array_copy.
operands())
329 element =
get(element);
364 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
369 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
380 else if(src.
get_sub().size()==2 &&
385 else if(src.
get_sub().size()==3 &&
388 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
392 else if(src.
get_sub().size()==4 &&
395 if(type.
id()==ID_floatbv)
404 const auto s1_int = numeric_cast_v<mp_integer>(
s1);
405 const auto s2_int = numeric_cast_v<mp_integer>(
s2);
406 const auto s3_int = numeric_cast_v<mp_integer>(s3);
410 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
416 else if(src.
get_sub().size()==4 &&
424 else if(src.
get_sub().size()==4 &&
432 else if(src.
get_sub().size()==4 &&
441 if(type.
id()==ID_signedbv ||
442 type.
id()==ID_unsignedbv ||
443 type.
id()==ID_c_enum ||
444 type.
id()==ID_c_bool)
448 else if(type.
id()==ID_c_enum_tag)
454 result.
type() = type;
457 else if(type.
id()==ID_fixedbv ||
458 type.
id()==ID_floatbv)
463 else if(type.
id()==ID_integer ||
471 "smt2_convt::parse_literal should not be of unsupported type " +
479 std::unordered_map<int64_t, exprt> operands_map;
483 auto maybe_default_op = operands_map.find(-1);
485 if(maybe_default_op == operands_map.end())
488 default_op = maybe_default_op->second;
490 auto maybe_size = numeric_cast<std::int64_t>(type.
size());
491 if(maybe_size.has_value())
493 while(i < maybe_size.value())
495 auto found_op = operands_map.find(i);
496 if(found_op != operands_map.end())
497 operands.emplace_back(found_op->second);
499 operands.emplace_back(default_op);
507 auto found_op = operands_map.find(i);
508 while(found_op != operands_map.end())
510 operands.emplace_back(found_op->second);
512 found_op = operands_map.find(i);
514 operands.emplace_back(default_op);
520 std::unordered_map<int64_t, exprt> *operands_map,
533 bool failure =
to_integer(index_constant, tempint);
536 long index = tempint.to_long();
538 operands_map->emplace(index, value);
540 else if(src.
get_sub().size() == 3 && src.
get_sub()[0].id() ==
"let")
545 operands_map, src.
get_sub()[1].get_sub()[0].get_sub()[1], type);
548 else if(src.
get_sub().size()==2 &&
549 src.
get_sub()[0].get_sub().size()==3 &&
550 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
551 src.
get_sub()[0].get_sub()[1].id()==
"const")
555 operands_map->emplace(-1, default_value);
582 if(components.empty())
590 if(src.
get_sub().size()!=components.size()+1)
593 for(std::size_t i=0; i<components.size(); i++)
610 std::size_t offset=0;
612 for(std::size_t i=0; i<components.size(); i++)
614 std::size_t component_width=
boolbv_width(components[i].type());
617 offset + component_width <= total_width,
618 "struct component bits shall be within struct bit vector");
620 std::string component_binary=
622 total_width-offset-component_width, component_width);
627 offset+=component_width;
637 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
638 type.
id() == ID_integer || type.
id() == ID_rational ||
639 type.
id() == ID_real || type.
id() == ID_c_enum ||
640 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
641 type.
id() == ID_floatbv)
645 else if(type.
id()==ID_bool)
647 if(src.
id()==ID_1 || src.
id()==ID_true)
649 else if(src.
id()==ID_0 || src.
id()==ID_false)
652 else if(type.
id()==ID_pointer)
658 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
663 ptr.
object = numeric_cast_v<std::size_t>(v / pow);
667 else if(type.
id()==ID_struct)
671 else if(type.
id() == ID_struct_tag)
676 struct_expr.type() = type;
677 return std::move(struct_expr);
679 else if(type.
id()==ID_union)
683 else if(type.
id() == ID_union_tag)
687 union_expr.type() = type;
690 else if(type.
id()==ID_array)
702 if(expr.
id()==ID_symbol ||
703 expr.
id()==ID_constant ||
704 expr.
id()==ID_string_constant ||
714 else if(expr.
id()==ID_index)
723 if(array.
type().
id()==ID_pointer)
725 else if(array.
type().
id()==ID_array)
745 else if(expr.
id()==ID_member)
750 const typet &struct_op_type = struct_op.
type();
753 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
754 "member expression operand shall have struct type");
771 else if(expr.
id()==ID_if)
786 "operand of address of expression should not be of kind " +
800 else if(expr.
id()==ID_literal)
812 out <<
"; convert\n";
813 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
821 out <<
"(define-fun ";
833 if(expr.
type().
id() != ID_bool)
884 for(std::size_t i=0; i<identifier.
size(); i++)
886 char ch=identifier[i];
909 if(type.
id()==ID_floatbv)
914 else if(type.
id()==ID_unsignedbv)
918 else if(type.
id()==ID_c_bool)
922 else if(type.
id()==ID_signedbv)
926 else if(type.
id()==ID_bool)
930 else if(type.
id()==ID_c_enum_tag)
934 else if(type.
id() == ID_pointer)
955 if(expr.
id()==ID_symbol)
962 if(expr.
id()==ID_smt2_symbol)
970 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
972 out <<
"(|float_bv." << expr.
id()
988 if(expr.
id()==ID_symbol)
994 else if(expr.
id()==ID_nondet_symbol)
997 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1000 else if(expr.
id()==ID_smt2_symbol)
1006 else if(expr.
id()==ID_typecast)
1010 else if(expr.
id()==ID_floatbv_typecast)
1014 else if(expr.
id()==ID_struct)
1018 else if(expr.
id()==ID_union)
1022 else if(expr.
id()==ID_constant)
1026 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
1030 "concatenation over a single operand should have matching types",
1035 else if(expr.
id()==ID_concatenation ||
1036 expr.
id()==ID_bitand ||
1037 expr.
id()==ID_bitor ||
1038 expr.
id()==ID_bitxor ||
1039 expr.
id()==ID_bitnand ||
1040 expr.
id()==ID_bitnor)
1044 "given expression should have at least two operands",
1049 if(expr.
id()==ID_concatenation)
1051 else if(expr.
id()==ID_bitand)
1053 else if(expr.
id()==ID_bitor)
1055 else if(expr.
id()==ID_bitxor)
1057 else if(expr.
id()==ID_bitnand)
1059 else if(expr.
id()==ID_bitnor)
1070 else if(expr.
id()==ID_bitnot)
1074 if(bitnot_expr.
type().
id() == ID_vector)
1083 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1085 out <<
"(let ((?vectorop ";
1089 out <<
"(mk-" << smt_typename;
1096 out <<
" (bvnot (" << smt_typename <<
"." << (size-i-1)
1112 else if(expr.
id()==ID_unary_minus)
1117 unary_minus_expr.
type().
id() == ID_rational ||
1118 unary_minus_expr.
type().
id() == ID_integer ||
1119 unary_minus_expr.
type().
id() == ID_real)
1125 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1137 else if(unary_minus_expr.
type().
id() == ID_vector)
1141 const std::string &smt_typename =
1148 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1150 out <<
"(let ((?vectorop ";
1154 out <<
"(mk-" << smt_typename;
1161 out <<
" (bvneg (" << smt_typename <<
"." << (size-i-1)
1177 else if(expr.
id()==ID_unary_plus)
1182 else if(expr.
id()==ID_sign)
1188 if(op_type.
id()==ID_floatbv)
1192 out <<
"(fp.isNegative ";
1199 else if(op_type.
id()==ID_signedbv)
1205 out <<
" (_ bv0 " << op_width <<
"))";
1210 "sign should not be applied to unsupported type",
1213 else if(expr.
id()==ID_if)
1225 else if(expr.
id()==ID_and ||
1230 expr.
type().
id() == ID_bool,
1231 "logical and, or, and xor expressions should have Boolean type");
1234 "logical and, or, and xor expressions should have at least two operands");
1236 out <<
"(" << expr.
id();
1244 else if(expr.
id()==ID_implies)
1249 implies_expr.
type().
id() == ID_bool,
1250 "implies expression should have Boolean type");
1258 else if(expr.
id()==ID_not)
1263 not_expr.
type().
id() == ID_bool,
1264 "not expression should have Boolean type");
1270 else if(expr.
id() == ID_equal)
1276 "operands of equal expression shall have same type");
1284 else if(expr.
id() == ID_notequal)
1290 "operands of not equal expression shall have same type");
1298 else if(expr.
id()==ID_ieee_float_equal ||
1299 expr.
id()==ID_ieee_float_notequal)
1306 rel_expr.lhs().type() == rel_expr.rhs().type(),
1307 "operands of float equal and not equal expressions shall have same type");
1312 if(rel_expr.id() == ID_ieee_float_notequal)
1321 if(rel_expr.id() == ID_ieee_float_notequal)
1327 else if(expr.
id()==ID_le ||
1334 else if(expr.
id()==ID_plus)
1338 else if(expr.
id()==ID_floatbv_plus)
1342 else if(expr.
id()==ID_minus)
1346 else if(expr.
id()==ID_floatbv_minus)
1350 else if(expr.
id()==ID_div)
1354 else if(expr.
id()==ID_floatbv_div)
1358 else if(expr.
id()==ID_mod)
1362 else if(expr.
id() == ID_euclidean_mod)
1366 else if(expr.
id()==ID_mult)
1370 else if(expr.
id()==ID_floatbv_mult)
1374 else if(expr.
id() == ID_floatbv_rem)
1378 else if(expr.
id()==ID_address_of)
1384 else if(expr.
id() == ID_array_of)
1389 array_of_expr.type().id() == ID_array,
1390 "array of expression shall have array type");
1394 out <<
"((as const ";
1402 defined_expressionst::const_iterator it =
1408 else if(expr.
id() == ID_array_comprehension)
1413 array_comprehension.type().id() == ID_array,
1414 "array_comprehension expression shall have array type");
1418 out <<
"(lambda ((";
1421 convert_type(array_comprehension.type().size().type());
1433 else if(expr.
id()==ID_index)
1437 else if(expr.
id()==ID_ashr ||
1438 expr.
id()==ID_lshr ||
1444 if(type.
id()==ID_unsignedbv ||
1445 type.
id()==ID_signedbv ||
1448 if(shift_expr.
id() == ID_ashr)
1450 else if(shift_expr.
id() == ID_lshr)
1452 else if(shift_expr.
id() == ID_shl)
1482 if(width_op0==width_op1)
1484 else if(width_op0>width_op1)
1486 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1492 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1499 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1506 "unsupported type for " + shift_expr.
id_string() +
": " +
1509 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1515 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1520 if(shift_expr.
id() == ID_rol)
1521 out <<
"((_ rotate_left";
1522 else if(shift_expr.
id() == ID_ror)
1523 out <<
"((_ rotate_right";
1529 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.
distance());
1531 if(distance_int_op.has_value())
1533 out << distance_int_op.value();
1537 "distance type for " + shift_expr.
id_string() +
"must be constant");
1546 "unsupported type for " + shift_expr.
id_string() +
": " +
1549 else if(expr.
id()==ID_with)
1553 else if(expr.
id()==ID_update)
1557 else if(expr.
id()==ID_member)
1561 else if(expr.
id()==ID_pointer_offset)
1566 op.type().id() == ID_pointer,
1567 "operand of pointer offset expression shall be of pointer type");
1569 std::size_t offset_bits =
1574 if(offset_bits>result_width)
1575 offset_bits=result_width;
1578 if(result_width>offset_bits)
1579 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1581 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1585 if(result_width>offset_bits)
1588 else if(expr.
id()==ID_pointer_object)
1593 op.type().id() == ID_pointer,
1594 "pointer object expressions should be of pointer type");
1600 out <<
"((_ zero_extend " << ext <<
") ";
1602 out <<
"((_ extract "
1603 << pointer_width-1 <<
" "
1611 else if(expr.
id() == ID_is_dynamic_object)
1615 else if(expr.
id() == ID_is_invalid_pointer)
1619 out <<
"(= ((_ extract "
1620 << pointer_width-1 <<
" "
1626 else if(expr.
id()==ID_string_constant)
1632 else if(expr.
id()==ID_extractbit)
1641 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1647 out <<
"(= ((_ extract 0 0) ";
1656 else if(expr.
id()==ID_extractbits)
1670 std::swap(op1_i, op2_i);
1674 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1681 out <<
"(= ((_ extract 0 0) ";
1690 SMT2_TODO(
"smt2: extractbits with non-constant index");
1693 else if(expr.
id()==ID_replication)
1697 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1699 out <<
"((_ repeat " << times <<
") ";
1703 else if(expr.
id()==ID_byte_extract_little_endian ||
1704 expr.
id()==ID_byte_extract_big_endian)
1707 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1709 else if(expr.
id()==ID_byte_update_little_endian ||
1710 expr.
id()==ID_byte_update_big_endian)
1713 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1715 else if(expr.
id()==ID_abs)
1721 if(type.
id()==ID_signedbv)
1725 out <<
"(ite (bvslt ";
1727 out <<
" (_ bv0 " << result_width <<
")) ";
1734 else if(type.
id()==ID_fixedbv)
1738 out <<
"(ite (bvslt ";
1740 out <<
" (_ bv0 " << result_width <<
")) ";
1747 else if(type.
id()==ID_floatbv)
1761 else if(expr.
id()==ID_isnan)
1767 if(op_type.
id()==ID_fixedbv)
1769 else if(op_type.
id()==ID_floatbv)
1773 out <<
"(fp.isNaN ";
1783 else if(expr.
id()==ID_isfinite)
1789 if(op_type.
id()==ID_fixedbv)
1791 else if(op_type.
id()==ID_floatbv)
1797 out <<
"(not (fp.isNaN ";
1801 out <<
"(not (fp.isInf ";
1813 else if(expr.
id()==ID_isinf)
1819 if(op_type.
id()==ID_fixedbv)
1821 else if(op_type.
id()==ID_floatbv)
1825 out <<
"(fp.isInfinite ";
1835 else if(expr.
id()==ID_isnormal)
1841 if(op_type.
id()==ID_fixedbv)
1843 else if(op_type.
id()==ID_floatbv)
1847 out <<
"(fp.isNormal ";
1857 else if(expr.
id()==ID_overflow_plus ||
1858 expr.
id()==ID_overflow_minus)
1864 expr.
type().
id() == ID_bool,
1865 "overflow plus and overflow minus expressions shall be of Boolean type");
1867 bool subtract=expr.
id()==ID_overflow_minus;
1868 const typet &op_type = op0.type();
1871 if(op_type.
id()==ID_signedbv)
1874 out <<
"(let ((?sum (";
1875 out << (subtract?
"bvsub":
"bvadd");
1876 out <<
" ((_ sign_extend 1) ";
1879 out <<
" ((_ sign_extend 1) ";
1883 "((_ extract " << width <<
" " << width <<
") ?sum) "
1884 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1887 else if(op_type.
id()==ID_unsignedbv ||
1888 op_type.
id()==ID_pointer)
1892 out <<
"((_ extract " << width <<
" " << width <<
") ";
1893 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1894 out <<
" ((_ zero_extend 1) ";
1897 out <<
" ((_ zero_extend 1) ";
1905 "overflow check should not be performed on unsupported type",
1908 else if(expr.
id()==ID_overflow_mult)
1914 expr.
type().
id() == ID_bool,
1915 "overflow mult expression shall be of Boolean type");
1920 const typet &op_type = op0.type();
1923 if(op_type.
id()==ID_signedbv)
1925 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1927 out <<
") ((_ sign_extend " << width <<
") ";
1930 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
1932 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" "
1933 << width*2 <<
")))))";
1935 else if(op_type.
id()==ID_unsignedbv)
1937 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1939 out <<
") ((_ zero_extend " << width <<
") ";
1941 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1946 "overflow check should not be performed on unsupported type",
1949 else if(expr.
id()==ID_array)
1955 else if(expr.
id()==ID_literal)
1959 else if(expr.
id()==ID_forall ||
1960 expr.
id()==ID_exists)
1966 throw "MathSAT does not support quantifiers";
1968 if(quantifier_expr.
id() == ID_forall)
1970 else if(quantifier_expr.
id() == ID_exists)
1985 else if(expr.
id()==ID_vector)
1990 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
1993 size == vector_expr.
operands().size(),
1994 "size indicated by type shall be equal to the number of operands");
1998 const std::string &smt_typename =
datatype_map.at(vector_type);
2000 out <<
"(mk-" << smt_typename;
2014 else if(expr.
id()==ID_object_size)
2018 else if(expr.
id()==ID_let)
2021 const auto &variables = let_expr.
variables();
2022 const auto &values = let_expr.
values();
2027 for(
auto &binding :
make_range(variables).zip(values))
2046 else if(expr.
id()==ID_constraint_select_one)
2049 "smt2_convt::convert_expr: '" + expr.
id_string() +
2050 "' is not yet supported");
2052 else if(expr.
id() == ID_bswap)
2058 "operand of byte swap expression shall have same type as the expression");
2061 out <<
"(let ((bswap_op ";
2066 bswap_expr.
type().
id() == ID_signedbv ||
2067 bswap_expr.
type().
id() == ID_unsignedbv)
2069 const std::size_t width =
2076 width % bits_per_byte == 0,
2077 "bit width indicated by type of bswap expression should be a multiple "
2078 "of the number of bits per byte");
2080 const std::size_t bytes = width / bits_per_byte;
2089 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2093 out <<
"(bswap_byte_" <<
byte <<
' ';
2094 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2095 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2104 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2105 out <<
" bswap_byte_" <<
byte;
2116 else if(expr.
id() == ID_popcount)
2120 else if(expr.
id() == ID_count_leading_zeros)
2124 else if(expr.
id() == ID_count_trailing_zeros)
2131 "smt2_convt::convert_expr should not be applied to unsupported type",
2140 if(dest_type.
id()==ID_c_enum_tag)
2144 if(src_type.
id()==ID_c_enum_tag)
2147 if(dest_type.
id()==ID_bool)
2150 if(src_type.
id()==ID_signedbv ||
2151 src_type.
id()==ID_unsignedbv ||
2152 src_type.
id()==ID_c_bool ||
2153 src_type.
id()==ID_fixedbv ||
2154 src_type.
id()==ID_pointer ||
2155 src_type.
id()==ID_integer)
2163 else if(src_type.
id()==ID_floatbv)
2167 out <<
"(not (fp.isZero ";
2179 else if(dest_type.
id()==ID_c_bool)
2188 out <<
" (_ bv1 " << to_width <<
")";
2189 out <<
" (_ bv0 " << to_width <<
")";
2192 else if(dest_type.
id()==ID_signedbv ||
2193 dest_type.
id()==ID_unsignedbv ||
2194 dest_type.
id()==ID_c_enum ||
2195 dest_type.
id()==ID_bv)
2199 if(src_type.
id()==ID_signedbv ||
2200 src_type.
id()==ID_unsignedbv ||
2201 src_type.
id()==ID_c_bool ||
2202 src_type.
id()==ID_c_enum ||
2203 src_type.
id()==ID_bv)
2207 if(from_width==to_width)
2209 else if(from_width<to_width)
2211 if(src_type.
id()==ID_signedbv)
2212 out <<
"((_ sign_extend ";
2214 out <<
"((_ zero_extend ";
2216 out << (to_width-from_width)
2223 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2228 else if(src_type.
id()==ID_fixedbv)
2232 std::size_t from_width=fixedbv_type.
get_width();
2239 out <<
"(let ((?tcop ";
2245 if(to_width>from_integer_bits)
2247 out <<
"((_ sign_extend "
2248 << (to_width-from_integer_bits) <<
") ";
2249 out <<
"((_ extract " << (from_width-1) <<
" "
2250 << from_fraction_bits <<
") ";
2256 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2257 <<
" " << from_fraction_bits <<
") ";
2262 out <<
" (ite (and ";
2265 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2266 "(_ bv0 " << from_fraction_bits <<
")))";
2269 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2274 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2278 else if(src_type.
id()==ID_floatbv)
2280 if(dest_type.
id()==ID_bv)
2297 else if(dest_type.
id()==ID_signedbv)
2301 "typecast unexpected "+src_type.
id_string()+
" -> "+
2304 else if(dest_type.
id()==ID_unsignedbv)
2308 "typecast unexpected "+src_type.
id_string()+
" -> "+
2312 else if(src_type.
id()==ID_bool)
2317 if(dest_type.
id()==ID_fixedbv)
2320 out <<
" (concat (_ bv1 "
2323 "(_ bv0 " << spec.
width <<
")";
2327 out <<
" (_ bv1 " << to_width <<
")";
2328 out <<
" (_ bv0 " << to_width <<
")";
2333 else if(src_type.
id()==ID_pointer)
2337 if(from_width<to_width)
2339 out <<
"((_ sign_extend ";
2340 out << (to_width-from_width)
2347 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2352 else if(src_type.
id()==ID_integer)
2358 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2361 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2364 src_type.
id() == ID_struct ||
2365 src_type.
id() == ID_struct_tag)
2371 "bit vector with of source and destination type shall be equal");
2378 "bit vector with of source and destination type shall be equal");
2383 src_type.
id() == ID_union ||
2384 src_type.
id() == ID_union_tag)
2388 "bit vector with of source and destination type shall be equal");
2391 else if(src_type.
id()==ID_c_bit_field)
2395 if(from_width==to_width)
2406 std::ostringstream e_str;
2407 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2408 <<
" src == " <<
format(src);
2412 else if(dest_type.
id()==ID_fixedbv)
2418 if(src_type.
id()==ID_unsignedbv ||
2419 src_type.
id()==ID_signedbv ||
2420 src_type.
id()==ID_c_enum)
2427 if(from_width==to_integer_bits)
2429 else if(from_width>to_integer_bits)
2432 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2440 from_width < to_integer_bits,
2441 "from_width should be smaller than to_integer_bits as other case "
2442 "have been handled above");
2443 if(dest_type.
id()==ID_unsignedbv)
2445 out <<
"(_ zero_extend "
2446 << (to_integer_bits-from_width) <<
") ";
2452 out <<
"((_ sign_extend "
2453 << (to_integer_bits-from_width) <<
") ";
2459 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2462 else if(src_type.
id()==ID_bool)
2464 out <<
"(concat (concat"
2465 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2471 else if(src_type.
id()==ID_fixedbv)
2476 std::size_t from_width=from_fixedbv_type.
get_width();
2478 out <<
"(let ((?tcop ";
2484 if(to_integer_bits<=from_integer_bits)
2486 out <<
"((_ extract "
2487 << (from_fraction_bits+to_integer_bits-1) <<
" "
2488 << from_fraction_bits
2494 to_integer_bits > from_integer_bits,
2495 "to_integer_bits should be greater than from_integer_bits as the"
2496 "other case has been handled above");
2497 out <<
"((_ sign_extend "
2498 << (to_integer_bits-from_integer_bits)
2500 << (from_width-1) <<
" "
2501 << from_fraction_bits
2507 if(to_fraction_bits<=from_fraction_bits)
2509 out <<
"((_ extract "
2510 << (from_fraction_bits-1) <<
" "
2511 << (from_fraction_bits-to_fraction_bits)
2517 to_fraction_bits > from_fraction_bits,
2518 "to_fraction_bits should be greater than from_fraction_bits as the"
2519 "other case has been handled above");
2520 out <<
"(concat ((_ extract "
2521 << (from_fraction_bits-1) <<
" 0) ";
2524 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2533 else if(dest_type.
id()==ID_pointer)
2537 if(src_type.
id()==ID_pointer)
2543 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2544 src_type.
id() == ID_bv)
2550 if(from_width==to_width)
2552 else if(from_width<to_width)
2554 out <<
"((_ sign_extend "
2555 << (to_width-from_width)
2562 out <<
"((_ extract " << to_width <<
" 0) ";
2570 else if(dest_type.
id()==ID_range)
2574 else if(dest_type.
id()==ID_floatbv)
2583 if(src_type.
id()==ID_bool)
2598 a.
build(significand, exponent);
2606 a.
build(significand, exponent);
2612 else if(src_type.
id()==ID_c_bool)
2618 else if(src_type.
id() == ID_bv)
2627 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2628 << dest_floatbv_type.get_f() + 1 <<
") ";
2638 else if(dest_type.
id()==ID_integer)
2640 if(src_type.
id()==ID_bool)
2649 else if(dest_type.
id()==ID_c_bit_field)
2654 if(from_width==to_width)
2675 if(dest_type.
id()==ID_floatbv)
2677 if(src_type.
id()==ID_floatbv)
2704 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2705 << dst.
get_f() + 1 <<
") ";
2714 else if(src_type.
id()==ID_unsignedbv)
2735 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
2736 << dst.
get_f() + 1 <<
") ";
2745 else if(src_type.
id()==ID_signedbv)
2753 out <<
"((_ to_fp " << dst.
get_e() <<
" "
2754 << dst.
get_f() + 1 <<
") ";
2763 else if(src_type.
id()==ID_c_enum_tag)
2779 else if(dest_type.
id()==ID_signedbv)
2784 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
2793 else if(dest_type.
id()==ID_unsignedbv)
2798 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
2822 components.size() == expr.
operands().size(),
2823 "number of struct components as indicated by the struct type shall be equal"
2824 "to the number of operands of the struct expression");
2826 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2830 const std::string &smt_typename =
datatype_map.at(struct_type);
2833 out <<
"(mk-" << smt_typename;
2836 for(struct_typet::componentst::const_iterator
2837 it=components.begin();
2838 it!=components.end();
2849 if(components.size()==1)
2854 for(std::size_t i=components.size(); i>1; i--)
2861 if(op.
type().
id() == ID_array)
2871 for(std::size_t i=1; i<components.size(); i++)
2881 const auto &size_expr = array_type.
size();
2887 out <<
"(let ((?far ";
2895 out <<
"(select ?far ";
2916 total_width != 0,
"failed to get union width for union");
2920 member_width != 0,
"failed to get union member width for union");
2922 if(total_width==member_width)
2930 total_width > member_width,
2931 "total_width should be greater than member_width as member_width can be"
2932 "at most as large as total_width and the other case has been handled "
2936 << (total_width-member_width) <<
") ";
2946 if(expr_type.
id()==ID_unsignedbv ||
2947 expr_type.
id()==ID_signedbv ||
2948 expr_type.
id()==ID_bv ||
2949 expr_type.
id()==ID_c_enum ||
2950 expr_type.
id()==ID_c_enum_tag ||
2951 expr_type.
id()==ID_c_bool ||
2952 expr_type.
id()==ID_c_bit_field)
2958 out <<
"(_ bv" << value
2959 <<
" " << width <<
")";
2961 else if(expr_type.
id()==ID_fixedbv)
2967 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
2969 else if(expr_type.
id()==ID_floatbv)
2982 size_t e=floatbv_type.
get_e();
2983 size_t f=floatbv_type.
get_f()+1;
2989 out <<
"((_ to_fp " << e <<
" " << f <<
")"
2995 out <<
"(_ NaN " << e <<
" " << f <<
")";
3000 out <<
"(_ -oo " << e <<
" " << f <<
")";
3002 out <<
"(_ +oo " << e <<
" " << f <<
")";
3012 <<
"#b" << binaryString.substr(0, 1) <<
" "
3013 <<
"#b" << binaryString.substr(1, e) <<
" "
3014 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
3022 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3025 else if(expr_type.
id()==ID_pointer)
3037 else if(expr_type.
id()==ID_bool)
3046 else if(expr_type.
id()==ID_array)
3052 else if(expr_type.
id()==ID_rational)
3055 const bool negative =
has_prefix(value,
"-");
3060 size_t pos=value.find(
"/");
3062 if(
pos==std::string::npos)
3063 out << value <<
".0";
3066 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3067 << value.substr(
pos+1) <<
".0)";
3073 else if(expr_type.
id()==ID_integer)
3079 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3089 if(expr.
type().
id() == ID_integer)
3099 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3104 if(expr.
type().
id()==ID_unsignedbv ||
3105 expr.
type().
id()==ID_signedbv)
3107 if(expr.
type().
id()==ID_unsignedbv)
3123 std::vector<std::size_t> dynamic_objects;
3126 if(dynamic_objects.empty())
3132 out <<
"(let ((?obj ((_ extract "
3133 << pointer_width-1 <<
" "
3138 if(dynamic_objects.size()==1)
3140 out <<
"(= (_ bv" << dynamic_objects.front()
3147 for(
const auto &
object : dynamic_objects)
3148 out <<
" (= (_ bv" <<
object
3162 if(op_type.
id()==ID_unsignedbv ||
3163 op_type.
id()==ID_pointer ||
3164 op_type.
id()==ID_bv)
3167 if(expr.
id()==ID_le)
3169 else if(expr.
id()==ID_lt)
3171 else if(expr.
id()==ID_ge)
3173 else if(expr.
id()==ID_gt)
3182 else if(op_type.
id()==ID_signedbv ||
3183 op_type.
id()==ID_fixedbv)
3186 if(expr.
id()==ID_le)
3188 else if(expr.
id()==ID_lt)
3190 else if(expr.
id()==ID_ge)
3192 else if(expr.
id()==ID_gt)
3201 else if(op_type.
id()==ID_floatbv)
3206 if(expr.
id()==ID_le)
3208 else if(expr.
id()==ID_lt)
3210 else if(expr.
id()==ID_ge)
3212 else if(expr.
id()==ID_gt)
3224 else if(op_type.
id()==ID_rational ||
3225 op_type.
id()==ID_integer)
3244 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3245 expr.
type().
id() == ID_real)
3250 for(
const auto &op : expr.
operands())
3259 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3260 expr.
type().
id() == ID_fixedbv)
3277 else if(expr.
type().
id() == ID_floatbv)
3284 else if(expr.
type().
id() == ID_pointer)
3290 if(p.
type().
id() != ID_pointer)
3294 p.
type().
id() == ID_pointer,
3295 "one of the operands should have pointer type");
3307 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3308 element_size = *element_size_opt;
3315 if(element_size >= 2)
3332 else if(expr.
type().
id() == ID_vector)
3336 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3342 const std::string &smt_typename =
datatype_map.at(vector_type);
3344 out <<
"(mk-" << smt_typename;
3353 summands.reserve(expr.
operands().size());
3354 for(
const auto &op : expr.
operands())
3386 if(expr.
id()==ID_constant)
3390 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3393 out <<
"roundNearestTiesToEven";
3395 out <<
"roundTowardNegative";
3397 out <<
"roundTowardPositive";
3399 out <<
"roundTowardZero";
3403 "Rounding mode should have value 0, 1, 2, or 3",
3411 out <<
"(ite (= (_ bv0 " << width <<
") ";
3413 out <<
") roundNearestTiesToEven ";
3415 out <<
"(ite (= (_ bv1 " << width <<
") ";
3417 out <<
") roundTowardNegative ";
3419 out <<
"(ite (= (_ bv2 " << width <<
") ";
3421 out <<
") roundTowardPositive ";
3424 out <<
"roundTowardZero";
3435 type.
id() == ID_floatbv ||
3436 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv) ||
3437 (type.
id() == ID_vector && type.
subtype().
id() == ID_floatbv));
3441 if(type.
id()==ID_floatbv)
3451 else if(type.
id()==ID_complex)
3455 else if(type.
id()==ID_vector)
3462 "type should not be one of the unsupported types",
3471 if(expr.
type().
id()==ID_integer)
3479 else if(expr.
type().
id()==ID_unsignedbv ||
3480 expr.
type().
id()==ID_signedbv ||
3481 expr.
type().
id()==ID_fixedbv)
3483 if(expr.
op0().
type().
id()==ID_pointer &&
3488 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3490 if(*element_size >= 2)
3495 "bitvector width of operand shall be equal to the bitvector width of "
3504 if(*element_size >= 2)
3517 else if(expr.
type().
id()==ID_floatbv)
3524 else if(expr.
type().
id()==ID_pointer)
3528 else if(expr.
type().
id()==ID_vector)
3532 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
3538 const std::string &smt_typename =
datatype_map.at(vector_type);
3540 out <<
"(mk-" << smt_typename;
3569 expr.
type().
id() == ID_floatbv,
3570 "type of ieee floating point expression shall be floatbv");
3588 if(expr.
type().
id()==ID_unsignedbv ||
3589 expr.
type().
id()==ID_signedbv)
3591 if(expr.
type().
id()==ID_unsignedbv)
3601 else if(expr.
type().
id()==ID_fixedbv)
3606 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3611 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3613 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3619 else if(expr.
type().
id()==ID_floatbv)
3633 expr.
type().
id() == ID_floatbv,
3634 "type of ieee floating point expression shall be floatbv");
3665 "expression should have been converted to a variant with two operands");
3667 if(expr.
type().
id()==ID_unsignedbv ||
3668 expr.
type().
id()==ID_signedbv)
3679 else if(expr.
type().
id()==ID_floatbv)
3686 else if(expr.
type().
id()==ID_fixedbv)
3691 out <<
"((_ extract "
3692 << spec.
width+fraction_bits-1 <<
" "
3693 << fraction_bits <<
") ";
3697 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3701 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3707 else if(expr.
type().
id()==ID_rational ||
3708 expr.
type().
id()==ID_integer ||
3709 expr.
type().
id()==ID_real)
3728 expr.
type().
id() == ID_floatbv,
3729 "type of ieee floating point expression shall be floatbv");
3748 expr.
type().
id() == ID_floatbv,
3749 "type of ieee floating point expression shall be floatbv");
3763 "smt2_convt::convert_floatbv_rem to be implemented when not using "
3774 std::size_t s=expr.
operands().size();
3789 "with expression should have been converted to a version with three "
3794 if(expr_type.
id()==ID_array)
3818 out <<
"(let ((distance? ";
3819 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
3823 if(array_width>index_width)
3825 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
3831 out <<
"((_ extract " << array_width-1 <<
" 0) ";
3841 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
3843 out <<
"distance?)) ";
3847 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
3849 out <<
") distance?)))";
3852 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
3859 const irep_idt &component_name=index.
get(ID_component_name);
3863 "struct should have accessed component");
3867 const std::string &smt_typename =
datatype_map.at(expr_type);
3869 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
3883 out <<
"(let ((?withop ";
3887 if(m.
width==struct_width)
3897 <<
"((_ extract " << (struct_width-1) <<
" "
3898 << m.
width <<
") ?withop) ";
3907 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
3912 out <<
"(concat (concat "
3913 <<
"((_ extract " << (struct_width-1) <<
" "
3916 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3923 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
3931 total_width != 0,
"failed to get union width for with");
3935 member_width != 0,
"failed to get union member width for with");
3937 if(total_width==member_width)
3944 total_width > member_width,
3945 "total width should be greater than member_width as member_width is at "
3946 "most as large as total_width and the other case has been handled "
3949 out <<
"((_ extract "
3951 <<
" " << member_width <<
") ";
3958 else if(expr_type.
id()==ID_bv ||
3959 expr_type.
id()==ID_unsignedbv ||
3960 expr_type.
id()==ID_signedbv)
3966 total_width != 0,
"failed to get total width");
3973 value_width != 0,
"failed to get value width");
3985 out <<
" (bvnot (bvshl";
3988 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
3989 out <<
" (repeat[" << value_width <<
"] bv1[1])";
4011 "with expects struct, union, or array type, but got "+
4019 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4026 if(array_op_type.
id()==ID_array)
4062 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
4066 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4070 if(array_width>index_width)
4072 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4078 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4088 else if(array_op_type.
id()==ID_vector)
4094 const std::string &smt_typename =
datatype_map.at(vector_type);
4098 const auto index_int = numeric_cast<mp_integer>(expr.
index());
4099 if(!index_int.has_value())
4101 SMT2_TODO(
"non-constant index on vectors");
4105 out <<
"(" << smt_typename <<
"." << *index_int <<
" ";
4117 false,
"index with unsupported array type: " + array_op_type.
id_string());
4124 const typet &struct_op_type = struct_op.
type();
4127 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
4132 struct_type.
has_component(name),
"struct should have accessed component");
4136 const std::string &smt_typename =
datatype_map.at(struct_type);
4138 out <<
"(" << smt_typename <<
"."
4151 member_offset.has_value(),
"failed to get struct member offset");
4160 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4164 width != 0,
"failed to get union member width");
4168 out <<
"((_ extract "
4178 "convert_member on an unexpected type "+struct_op_type.
id_string());
4185 if(type.
id()==ID_bool)
4191 else if(type.
id()==ID_vector)
4195 const std::string &smt_typename =
datatype_map.at(type);
4200 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4202 out <<
"(let ((?vflop ";
4210 out <<
" (" << smt_typename <<
"." << i <<
" ?vflop)";
4218 else if(type.
id()==ID_array)
4222 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4226 const std::string &smt_typename =
datatype_map.at(type);
4231 out <<
"(let ((?sflop ";
4239 for(std::size_t i=components.size(); i>1; i--)
4241 out <<
"(concat (" << smt_typename <<
"."
4242 << components[i-1].get_name() <<
" ?sflop)";
4247 out <<
"(" << smt_typename <<
"."
4248 << components[0].get_name() <<
" ?sflop)";
4250 for(std::size_t i=1; i<components.size(); i++)
4258 else if(type.
id()==ID_floatbv)
4262 "floatbv expressions should be flattened when using FPA theory");
4275 if(type.
id()==ID_bool)
4282 else if(type.
id()==ID_vector)
4286 const std::string &smt_typename =
datatype_map.at(type);
4293 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
4296 out <<
"(let ((?ufop" << nesting <<
" ";
4301 out <<
"(mk-" << smt_typename;
4303 std::size_t offset=0;
4305 for(
mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4309 out <<
"((_ extract " << offset+subtype_width-1 <<
" "
4310 << offset <<
") ?ufop" << nesting <<
")";
4322 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4328 out <<
"(let ((?ufop" << nesting <<
" ";
4333 const std::string &smt_typename =
datatype_map.at(type);
4335 out <<
"(mk-" << smt_typename;
4342 std::size_t offset=0;
4345 for(struct_typet::componentst::const_iterator
4346 it=components.begin();
4347 it!=components.end();
4354 out <<
"((_ extract " << offset+member_width-1 <<
" "
4355 << offset <<
") ?ufop" << nesting <<
")";
4357 offset+=member_width;
4378 if(expr.
id()==ID_and && value)
4385 if(expr.
id()==ID_or && !value)
4392 if(expr.
id()==ID_not)
4402 if(expr.
id() == ID_equal && value)
4405 if(equal_expr.
lhs().
type().
id() == ID_empty)
4411 if(equal_expr.
lhs().
id()==ID_symbol)
4421 id.type=equal_expr.
lhs().
type();
4428 out <<
"; set_to true (equal)\n";
4429 out <<
"(define-fun |" << smt2_identifier <<
"| () ";
4448 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4459 out << found_literal->second;
4482 exprt lowered_expr = expr;
4489 it->id() == ID_byte_extract_little_endian ||
4490 it->id() == ID_byte_extract_big_endian)
4495 it->id() == ID_byte_update_little_endian ||
4496 it->id() == ID_byte_update_big_endian)
4502 return lowered_expr;
4519 "lower_byte_operators should remove all byte operators");
4524 return lowered_expr;
4532 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4537 const auto identifier = q_expr.symbol().get_identifier();
4539 id.type = q_expr.symbol().type();
4549 if(expr.
id()==ID_symbol ||
4550 expr.
id()==ID_nondet_symbol)
4553 if(expr.
type().
id()==ID_code)
4558 if(expr.
id()==ID_symbol)
4561 identifier=
"nondet_"+
4566 if(
id.type.is_nil())
4568 id.type=expr.
type();
4573 out <<
"; find_symbols\n";
4574 out <<
"(declare-fun |"
4581 else if(expr.
id() == ID_array_of)
4588 const auto &array_type = array_of.type();
4592 out <<
"; the following is a substitute for lambda i. x\n";
4593 out <<
"(declare-fun " <<
id <<
" () ";
4598 out <<
"(assert (forall ((i ";
4600 out <<
")) (= (select " <<
id <<
" i) ";
4617 else if(expr.
id() == ID_array_comprehension)
4624 const auto &array_type = array_comprehension.type();
4625 const auto &array_size = array_type.size();
4629 out <<
"(declare-fun " <<
id <<
" () ";
4633 out <<
"; the following is a substitute for lambda i . x(i)\n";
4634 out <<
"; universally quantified initialization of the array\n";
4635 out <<
"(assert (forall ((";
4639 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
4646 out <<
")) (= (select " <<
id <<
" ";
4665 else if(expr.
id()==ID_array)
4672 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4673 out <<
"(declare-fun " <<
id <<
" () ";
4677 for(std::size_t i=0; i<expr.
operands().size(); i++)
4679 out <<
"(assert (= (select " <<
id <<
" ";
4692 out <<
"))" <<
"\n";
4698 else if(expr.
id()==ID_string_constant)
4708 out <<
"; the following is a substitute for a string" <<
"\n";
4709 out <<
"(declare-fun " <<
id <<
" () ";
4713 for(std::size_t i=0; i<tmp.
operands().size(); i++)
4715 out <<
"(assert (= (select " << id;
4719 out <<
"))" <<
"\n";
4725 else if(expr.
id() == ID_object_size)
4729 if(op.
type().
id()==ID_pointer)
4735 out <<
"(declare-fun |" <<
id <<
"| () ";
4746 (expr.
id() == ID_floatbv_plus ||
4747 expr.
id() == ID_floatbv_minus ||
4748 expr.
id() == ID_floatbv_mult ||
4749 expr.
id() == ID_floatbv_div ||
4750 expr.
id() == ID_floatbv_typecast ||
4751 expr.
id() == ID_ieee_float_equal ||
4752 expr.
id() == ID_ieee_float_notequal ||
4753 ((expr.
id() == ID_lt ||
4754 expr.
id() == ID_gt ||
4755 expr.
id() == ID_le ||
4756 expr.
id() == ID_ge ||
4757 expr.
id() == ID_isnan ||
4758 expr.
id() == ID_isnormal ||
4759 expr.
id() == ID_isfinite ||
4760 expr.
id() == ID_isinf ||
4761 expr.
id() == ID_sign ||
4762 expr.
id() == ID_unary_minus ||
4763 expr.
id() == ID_typecast ||
4764 expr.
id() == ID_abs) &&
4771 if(
bvfp_set.insert(
function).second)
4773 out <<
"; this is a model for " << expr.
id() <<
" : "
4776 <<
"(define-fun " <<
function <<
" (";
4778 for(std::size_t i = 0; i < expr.
operands().size(); i++)
4782 out <<
"(op" << i <<
' ';
4792 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
4819 if(expr.
id()==ID_with)
4821 else if(expr.
id()==ID_member)
4830 if(type.
id()==ID_array)
4843 out <<
"(_ BitVec 1)";
4849 else if(type.
id()==ID_bool)
4853 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4863 width != 0,
"failed to get width of struct");
4865 out <<
"(_ BitVec " << width <<
")";
4868 else if(type.
id()==ID_vector)
4878 width != 0,
"failed to get width of vector");
4880 out <<
"(_ BitVec " << width <<
")";
4883 else if(type.
id()==ID_code)
4890 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
4895 out <<
"(_ BitVec " << width <<
")";
4897 else if(type.
id()==ID_pointer)
4902 else if(type.
id()==ID_bv ||
4903 type.
id()==ID_fixedbv ||
4904 type.
id()==ID_unsignedbv ||
4905 type.
id()==ID_signedbv ||
4906 type.
id()==ID_c_bool)
4911 else if(type.
id()==ID_c_enum)
4917 else if(type.
id()==ID_c_enum_tag)
4921 else if(type.
id()==ID_floatbv)
4926 out <<
"(_ FloatingPoint "
4927 << floatbv_type.
get_e() <<
" "
4928 << floatbv_type.
get_f() + 1 <<
")";
4933 else if(type.
id()==ID_rational ||
4936 else if(type.
id()==ID_integer)
4938 else if(type.
id()==ID_complex)
4948 width != 0,
"failed to get width of complex");
4950 out <<
"(_ BitVec " << width <<
")";
4953 else if(type.
id()==ID_c_bit_field)
4965 std::set<irep_idt> recstack;
4971 std::set<irep_idt> &recstack)
4973 if(type.
id()==ID_array)
4979 else if(type.
id()==ID_complex)
4986 const std::string smt_typename =
4990 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
4991 <<
"(mk-" << smt_typename;
4993 out <<
" (" << smt_typename <<
".imag ";
4997 out <<
" (" << smt_typename <<
".real ";
5004 else if(type.
id()==ID_vector)
5013 mp_integer size = numeric_cast_v<mp_integer>(vector_type.
size());
5015 const std::string smt_typename =
5019 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5020 <<
"(mk-" << smt_typename;
5024 out <<
" (" << smt_typename <<
"." << i <<
" ";
5032 else if(type.
id() == ID_struct)
5035 bool need_decl=
false;
5039 const std::string smt_typename =
5054 const std::string &smt_typename =
datatype_map.at(type);
5065 out <<
"(declare-datatypes () ((" << smt_typename <<
" "
5066 <<
"(mk-" << smt_typename <<
" ";
5070 out <<
"(" << smt_typename <<
"." <<
component.get_name()
5076 out <<
"))))" <<
"\n";
5093 for(struct_union_typet::componentst::const_iterator
5094 it=components.begin();
5095 it!=components.end();
5099 out <<
"(define-fun update-" << smt_typename <<
"."
5101 <<
"((s " << smt_typename <<
") "
5104 out <<
")) " << smt_typename <<
" "
5105 <<
"(mk-" << smt_typename
5108 for(struct_union_typet::componentst::const_iterator
5109 it2=components.begin();
5110 it2!=components.end();
5117 out <<
"(" << smt_typename <<
"."
5118 << it2->get_name() <<
" s) ";
5122 out <<
"))" <<
"\n";
5128 else if(type.
id() == ID_union)
5136 else if(type.
id()==ID_code)
5140 for(
const auto ¶m : parameters)
5145 else if(type.
id()==ID_pointer)
5149 else if(type.
id() == ID_struct_tag)
5152 const irep_idt &
id = struct_tag.get_identifier();
5154 if(recstack.find(
id) == recstack.end())
5157 recstack.insert(
id);
5162 else if(type.
id() == ID_union_tag)
5165 const irep_idt &
id = union_tag.get_identifier();
5167 if(recstack.find(
id) == recstack.end())
5169 recstack.insert(
id);
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
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 union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Operator to return the address of an object.
Array constructor from list of elements.
const exprt & size() const
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.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
The Boolean constant false.
std::size_t get_fraction_bits() const
Fixed-width bit-vector with signed fixed-point interpretation.
std::size_t get_fraction_bits() const
std::size_t get_integer_bits() const
Semantic type conversion from/to floating-point formats.
Fixed-width bit-vector with IEEE floating-point interpretation.
std::size_t get_f() const
std::size_t get_e() const
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
std::size_t width() const
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt NaN(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void build(const mp_integer &exp, const mp_integer &frac)
The trinary if-then-else operator.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const std::string & id_string() const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
exprt & where()
convenience accessor for binding().where()
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
literalt get_literal() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
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 ...
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)
std::size_t no_boolean_variables
smt2_identifierst smt2_identifiers
void convert_floatbv(const exprt &expr)
resultt dec_solve() override
Run the decision procedure to solve the problem.
literalt convert(const exprt &expr)
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const irep_idt & get_name() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
const componentst & components() const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
Generic base class for unary expressions.
The unary minus expression.
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
const constant_exprt & size() const
Operator to update elements in structs and arrays.
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 isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const std::string & id2string(const irep_idt &d)
static std::string binary(const constant_exprt &src)
bool is_true(const literalt &l)
literalt const_literal(bool value)
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
const std::string integer2binary(const mp_integer &n, std::size_t width)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
exprt object_size(const exprt &pointer)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNEXPECTEDCASE(S)
int solver(std::istream &in)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bool has_byte_operator(const exprt &src)
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const 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 not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_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.