Go to the documentation of this file.
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);
Operator to update elements in structs and arrays.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
void convert_typecast(const typecast_exprt &expr)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define UNEXPECTEDCASE(S)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
void get_dynamic_objects(std::vector< std::size_t > &objects) const
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
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.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
literalt get_literal() const
const typet & subtype() const
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
struct configt::bv_encodingt bv_encoding
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
depth_iteratort depth_begin()
exprt float_bv(const exprt &src)
void convert_type(const typet &)
const irep_idt & get_identifier() const
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
#define CHECK_RETURN(CONDITION)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
The type of an expression, extends irept.
std::vector< parametert > parameterst
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void pop() override
Currently, only implements a single stack element (no nested contexts)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
datatype_mapt datatype_map
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
exprt parse_array(const irept &s, const array_typet &type)
This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array ...
bool use_array_theory(const exprt &)
void convert_floatbv(const exprt &expr)
std::size_t get_f() const
literalt convert(const exprt &expr)
The trinary if-then-else operator.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
bool has_byte_operator(const exprt &src)
Fixed-width bit-vector with IEEE floating-point interpretation.
const mp_integer string2integer(const std::string &n, unsigned base)
std::size_t add_object(const exprt &expr)
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
std::size_t get_fraction_bits() const
void convert_update(const exprt &expr)
Union constructor from single element.
const string_constantt & to_string_constant(const exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
void convert_plus(const plus_exprt &expr)
The plus expression Associativity is not specified.
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
Base class for all expressions.
std::vector< componentt > componentst
Generic base class for unary expressions.
void convert_expr(const exprt &)
A base class for binary expressions.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
std::size_t get_bits_per_byte() const
void convert_constant(const constant_exprt &expr)
Sign of an expression Predicate is true if _op is negative, false otherwise.
void convert_literal(const literalt)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
A base class for quantifier expressions.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Vector constructor from list of elements.
bool is_true() const
Return whether the expression is a constant representing true.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
bitvector_typet index_type()
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
std::string type2id(const typet &) const
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Evaluates to true if the operand is finite.
void convert_is_dynamic_object(const unary_exprt &)
bool is_false() const
Return whether the expression is a constant representing false.
Fixed-width bit-vector with unsigned binary interpretation.
void convert_index(const index_exprt &expr)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Struct constructor from list of elements.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
typet & type()
Return the type of the expression.
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
std::size_t number_of_solver_calls
void convert_mult(const mult_exprt &expr)
Expression classes for byte-level operators.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
static std::string convert_identifier(const irep_idt &identifier)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
void push() override
Unimplemented.
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...
constant_exprt parse_literal(const irept &, const typet &type)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
bool has_prefix(const std::string &s, const std::string &prefix)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
std::size_t width() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
const std::string & id2string(const irep_idt &d)
const irep_idt & get_name() const
void convert_relation(const binary_relation_exprt &)
Semantic type conversion from/to floating-point formats.
identifier_mapt identifier_map
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#define forall_operands(it, expr)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
void convert_mod(const mod_exprt &expr)
const exprt & struct_op() const
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
const irep_idt & get_identifier() const
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
API to expression classes for Pointers.
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
bool use_check_sat_assuming
const std::string & id_string() const
literalt const_literal(bool value)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Binary multiplication Associativity is not specified.
std::size_t get_e() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
void convert_struct(const struct_exprt &expr)
pointer_typet pointer_type(const typet &subtype)
The unary minus expression.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool use_lambda_for_array
bool has_component(const irep_idt &component_name) const
exprt object_size(const exprt &pointer)
const irep_idt & id() const
void define_object_size(const irep_idt &id, const exprt &expr)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
defined_expressionst object_sizes
Ranges: pair of begin and end iterators, which can be initialized from containers,...
std::vector< exprt > operandst
std::set< irep_idt > bvfp_set
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
The Boolean constant false.
API to expression classes for floating-point arithmetic.
void convert_div(const div_exprt &expr)
const parameterst & parameters() const
const constant_exprt & size() const
void convert_minus(const minus_exprt &expr)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
numberingt< exprt, irep_hash > objects
resultt
Result of running the decision procedure.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
boolbv_widtht boolbv_width
Fixed-width bit-vector with signed fixed-point interpretation.
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
std::size_t get_width() const
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Bit-wise negation of bit-vectors.
bool is_zero() const
Return whether the expression is a constant representing 0.
void convert_with(const with_exprt &expr)
Extract member of struct or union.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Deprecated expression utility functions.
A base class for shift and rotate operators.
array_exprt to_array_expr() const
convert string into array constant
Structure type, corresponds to C style structs.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Forward depth-first search iterators These iterators' copy operations are expensive,...
std::size_t get_fraction_bits() const
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const irep_idt & get(const irep_namet &name) const
exprt parse_rec(const irept &s, const typet &type)
Evaluates to true if the operand is infinite.
resultt dec_solve() override
Run the decision procedure to solve the problem.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
std::string floatbv_suffix(const exprt &) const
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
int solver(std::istream &in)
std::vector< exprt > assumptions
std::size_t get_integer_bits() const
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates whose two operands have the same type.
void convert_floatbv_rem(const binary_exprt &expr)
struct_exprt parse_struct(const irept &s, const struct_typet &type)
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
std::size_t no_boolean_variables
void convert_union(const union_exprt &expr)
static std::string binary(const constant_exprt &src)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
std::size_t get_invalid_object() const
pointer_logict pointer_logic
std::size_t unsafe_string2size_t(const std::string &str, int base)
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
The byte swap expression.
irep_idt get_component_name() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
tvt l_get(literalt l) const
constant_exprt to_expr() const
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
void find_symbols(const exprt &expr)
const std::string integer2binary(const mp_integer &n, std::size_t width)
std::vector< bool > boolean_assignment
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
static ieee_floatt NaN(const ieee_float_spect &_spec)
The Boolean constant true.
A constant literal expression.
depth_iteratort depth_end()
bool is_true(const literalt &l)
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
exprt & where()
convenience accessor for binding().where()
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
void set_value(const irep_idt &value)
void unflatten(wheret, const typet &, unsigned nesting=0)
const irep_idt & get_value() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const membert & get_member(const struct_typet &type, const irep_idt &member) const
Array constructor from list of elements.
exprt parse_union(const irept &s, const union_typet &type)
ranget< iteratort > make_range(iteratort begin, iteratort end)
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
void flatten2bv(const exprt &)
Evaluates to true if the operand is a normal number.
smt2_identifierst smt2_identifiers
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
API to expression classes for bitvectors.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
Evaluates to true if the operand is NaN.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
API to expression classes for 'mathematical' expressions.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void build(const mp_integer &exp, const mp_integer &frac)
void convert_member(const member_exprt &expr)
defined_expressionst defined_expressions