51 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
54 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
58 const std::string &_benchmark,
59 const std::string &_notes,
60 const std::string &_logic,
63 : use_FPA_theory(false),
64 use_array_of_bool(false),
66 use_check_sat_assuming(false),
68 use_lambda_for_array(false),
72 benchmark(_benchmark),
78 no_boolean_variables(0)
169 "variable number shall be within bounds");
175 out <<
"; SMT 2" <<
"\n";
184 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
194 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
196 out <<
"(set-option :produce-models true)" <<
"\n";
202 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
215 out <<
"(check-sat-assuming (";
225 out <<
"; assumptions\n";
236 out <<
"(check-sat)\n";
244 out <<
"(get-value (" <<
id <<
"))"
252 out <<
"; end of SMT2 file"
259 if(type.
id() == ID_empty)
261 else if(type.
id() == ID_struct_tag)
263 else if(type.
id() == ID_union_tag)
265 else if(type.
id() == ID_struct || type.
id() == ID_union)
274 else if(
auto array_type = type_try_dynamic_cast<array_typet>(type))
290 std::size_t number = 0;
291 std::size_t h=pointer_width-1;
296 const typet &type = o.type();
300 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
301 !size_expr.has_value())
308 out <<
"(assert (=> (= "
309 <<
"((_ extract " << h <<
" " << l <<
") ";
312 <<
"(= " <<
id <<
" ";
337 if(expr.
id()==ID_symbol)
344 return it->second.value;
347 else if(expr.
id()==ID_nondet_symbol)
354 return it->second.value;
356 else if(expr.
id() == ID_literal)
364 else if(expr.
id() == ID_not)
369 else if(op.is_false())
374 (!expr.
has_operands() && (expr.
id() == ID_struct || expr.
id() == ID_array)))
386 op = std::move(eval_op);
421 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
426 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
437 else if(src.
get_sub().size()==2 &&
442 else if(src.
get_sub().size()==3 &&
445 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
449 else if(src.
get_sub().size()==4 &&
452 if(type.
id()==ID_floatbv)
461 const auto s1_int = numeric_cast_v<mp_integer>(
s1);
462 const auto s2_int = numeric_cast_v<mp_integer>(
s2);
463 const auto s3_int = numeric_cast_v<mp_integer>(s3);
467 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
473 else if(src.
get_sub().size()==4 &&
481 else if(src.
get_sub().size()==4 &&
489 else if(src.
get_sub().size()==4 &&
498 if(type.
id()==ID_signedbv ||
499 type.
id()==ID_unsignedbv ||
500 type.
id()==ID_c_enum ||
501 type.
id()==ID_c_bool)
505 else if(type.
id()==ID_c_enum_tag)
511 result.
type() = type;
514 else if(type.
id()==ID_fixedbv ||
515 type.
id()==ID_floatbv)
520 else if(type.
id()==ID_integer ||
527 "smt2_convt::parse_literal should not be of unsupported type " +
535 std::unordered_map<int64_t, exprt> operands_map;
539 auto maybe_default_op = operands_map.find(-1);
541 if(maybe_default_op == operands_map.end())
544 default_op = maybe_default_op->second;
546 auto maybe_size = numeric_cast<std::int64_t>(type.
size());
547 if(maybe_size.has_value())
549 while(i < maybe_size.value())
551 auto found_op = operands_map.find(i);
552 if(found_op != operands_map.end())
553 operands.emplace_back(found_op->second);
555 operands.emplace_back(default_op);
563 auto found_op = operands_map.find(i);
564 while(found_op != operands_map.end())
566 operands.emplace_back(found_op->second);
568 found_op = operands_map.find(i);
570 operands.emplace_back(default_op);
576 std::unordered_map<int64_t, exprt> *operands_map,
589 bool failure =
to_integer(index_constant, tempint);
592 long index = tempint.to_long();
594 operands_map->emplace(index, value);
596 else if(src.
get_sub().size()==2 &&
597 src.
get_sub()[0].get_sub().size()==3 &&
598 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
599 src.
get_sub()[0].get_sub()[1].id()==
"const")
603 operands_map->emplace(-1, default_value);
636 if(components.empty())
644 for(std::size_t i=0; i<components.size(); i++)
654 src.
get_sub().size() > j,
"insufficient number of component values");
671 std::size_t offset=0;
673 for(std::size_t i=0; i<components.size(); i++)
678 std::size_t component_width=
boolbv_width(components[i].type());
681 offset + component_width <= total_width,
682 "struct component bits shall be within struct bit vector");
684 std::string component_binary=
686 total_width-offset-component_width, component_width);
691 offset+=component_width;
705 for(
const auto &binding : src.
get_sub()[1].get_sub())
707 const irep_idt &name = binding.get_sub()[0].id();
718 return parse_rec(bindings_it->second, type);
722 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
723 type.
id() == ID_integer || type.
id() == ID_rational ||
724 type.
id() == ID_real || type.
id() == ID_c_enum ||
725 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
726 type.
id() == ID_floatbv || type.
id() == ID_c_bool)
730 else if(type.
id()==ID_bool)
732 if(src.
id()==ID_1 || src.
id()==ID_true)
734 else if(src.
id()==ID_0 || src.
id()==ID_false)
737 else if(type.
id()==ID_pointer)
743 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
752 else if(type.
id()==ID_struct)
756 else if(type.
id() == ID_struct_tag)
761 struct_expr.type() = type;
762 return std::move(struct_expr);
764 else if(type.
id()==ID_union)
768 else if(type.
id() == ID_union_tag)
772 union_expr.type() = type;
775 else if(type.
id()==ID_array)
789 expr.
id() == ID_string_constant || expr.
id() == ID_label)
792 const std::size_t max_objects = std::size_t(1) << object_bits;
795 if(object_id >= max_objects)
798 "too many addressed objects: maximum number of objects is set to 2^n=" +
801 "use the `--object-bits n` option to increase the maximum number"};
804 out <<
"(concat (_ bv" << object_id <<
" " << object_bits <<
")"
805 <<
" (_ bv0 " <<
boolbv_width(result_type) - object_bits <<
"))";
807 else if(expr.
id()==ID_index)
816 if(array.
type().
id()==ID_pointer)
818 else if(array.
type().
id()==ID_array)
838 else if(expr.
id()==ID_member)
843 const typet &struct_op_type = struct_op.
type();
846 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
847 "member expression operand shall have struct type");
864 else if(expr.
id()==ID_if)
879 "operand of address of expression should not be of kind " +
887 if(node.
id() == ID_exists || node.
id() == ID_forall)
903 else if(expr.
id()==ID_literal)
915 out <<
"; convert\n";
916 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
926 out <<
"(declare-fun ";
928 out <<
" () Bool)\n";
929 out <<
"(assert (= ";
941 out <<
"(define-fun " << identifier <<
" () Bool ";
969 const auto identifier =
991 for(
auto &assumption : _assumptions)
1002 if(identifier.empty())
1027 std::string result =
"|";
1029 for(
auto ch : identifier)
1054 if(type.
id()==ID_floatbv)
1059 else if(type.
id() == ID_bv)
1063 else if(type.
id()==ID_unsignedbv)
1067 else if(type.
id()==ID_c_bool)
1071 else if(type.
id()==ID_signedbv)
1075 else if(type.
id()==ID_bool)
1079 else if(type.
id()==ID_c_enum_tag)
1083 else if(type.
id() == ID_pointer)
1087 else if(type.
id() == ID_struct_tag)
1094 else if(type.
id() == ID_union_tag)
1098 else if(type.
id() == ID_array)
1119 if(expr.
id()==ID_symbol)
1126 if(expr.
id()==ID_smt2_symbol)
1134 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
1140 for(
const auto &op : expr.
operands())
1168 converter_result->second(expr);
1173 if(expr.
id()==ID_symbol)
1179 else if(expr.
id()==ID_nondet_symbol)
1182 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1185 else if(expr.
id()==ID_smt2_symbol)
1191 else if(expr.
id()==ID_typecast)
1195 else if(expr.
id()==ID_floatbv_typecast)
1199 else if(expr.
id()==ID_struct)
1203 else if(expr.
id()==ID_union)
1211 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
1215 "concatenation over a single operand should have matching types",
1220 else if(expr.
id()==ID_concatenation ||
1221 expr.
id()==ID_bitand ||
1222 expr.
id()==ID_bitor ||
1223 expr.
id()==ID_bitxor ||
1224 expr.
id()==ID_bitnand ||
1225 expr.
id()==ID_bitnor)
1229 "given expression should have at least two operands",
1234 if(expr.
id()==ID_concatenation)
1236 else if(expr.
id()==ID_bitand)
1238 else if(expr.
id()==ID_bitor)
1240 else if(expr.
id()==ID_bitxor)
1242 else if(expr.
id()==ID_bitnand)
1244 else if(expr.
id()==ID_bitnor)
1247 for(
const auto &op : expr.
operands())
1255 else if(expr.
id()==ID_bitnot)
1263 else if(expr.
id()==ID_unary_minus)
1268 unary_minus_expr.
type().
id() == ID_rational ||
1269 unary_minus_expr.
type().
id() == ID_integer ||
1270 unary_minus_expr.
type().
id() == ID_real)
1276 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1295 else if(expr.
id()==ID_unary_plus)
1300 else if(expr.
id()==ID_sign)
1306 if(op_type.
id()==ID_floatbv)
1310 out <<
"(fp.isNegative ";
1317 else if(op_type.
id()==ID_signedbv)
1323 out <<
" (_ bv0 " << op_width <<
"))";
1328 "sign should not be applied to unsupported type",
1331 else if(expr.
id()==ID_if)
1343 else if(expr.
id()==ID_and ||
1349 "logical and, or, and xor expressions should have Boolean type");
1352 "logical and, or, and xor expressions should have at least two operands");
1354 out <<
"(" << expr.
id();
1355 for(
const auto &op : expr.
operands())
1362 else if(expr.
id()==ID_implies)
1367 implies_expr.
is_boolean(),
"implies expression should have Boolean type");
1375 else if(expr.
id()==ID_not)
1380 not_expr.
is_boolean(),
"not expression should have Boolean type");
1386 else if(expr.
id() == ID_equal)
1392 "operands of equal expression shall have same type");
1407 else if(expr.
id() == ID_notequal)
1413 "operands of not equal expression shall have same type");
1421 else if(expr.
id()==ID_ieee_float_equal ||
1422 expr.
id()==ID_ieee_float_notequal)
1429 rel_expr.lhs().type() == rel_expr.rhs().type(),
1430 "operands of float equal and not equal expressions shall have same type");
1435 if(rel_expr.id() == ID_ieee_float_notequal)
1444 if(rel_expr.id() == ID_ieee_float_notequal)
1450 else if(expr.
id()==ID_le ||
1457 else if(expr.
id()==ID_plus)
1461 else if(expr.
id()==ID_floatbv_plus)
1465 else if(expr.
id()==ID_minus)
1469 else if(expr.
id()==ID_floatbv_minus)
1473 else if(expr.
id()==ID_div)
1477 else if(expr.
id()==ID_floatbv_div)
1481 else if(expr.
id()==ID_mod)
1485 else if(expr.
id() == ID_euclidean_mod)
1489 else if(expr.
id()==ID_mult)
1493 else if(expr.
id()==ID_floatbv_mult)
1497 else if(expr.
id() == ID_floatbv_rem)
1501 else if(expr.
id()==ID_address_of)
1507 else if(expr.
id() == ID_array_of)
1512 array_of_expr.type().id() == ID_array,
1513 "array of expression shall have array type");
1517 out <<
"((as const ";
1525 defined_expressionst::const_iterator it =
1531 else if(expr.
id() == ID_array_comprehension)
1536 array_comprehension.type().id() == ID_array,
1537 "array_comprehension expression shall have array type");
1541 out <<
"(lambda ((";
1544 convert_type(array_comprehension.type().size().type());
1556 else if(expr.
id()==ID_index)
1560 else if(expr.
id()==ID_ashr ||
1561 expr.
id()==ID_lshr ||
1567 if(type.
id()==ID_unsignedbv ||
1568 type.
id()==ID_signedbv ||
1571 if(shift_expr.
id() == ID_ashr)
1573 else if(shift_expr.
id() == ID_lshr)
1575 else if(shift_expr.
id() == ID_shl)
1605 if(width_op0==width_op1)
1607 else if(width_op0>width_op1)
1609 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1615 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1622 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1629 "unsupported type for " + shift_expr.
id_string() +
": " +
1632 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1638 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1643 if(shift_expr.
id() == ID_rol)
1644 out <<
"((_ rotate_left";
1645 else if(shift_expr.
id() == ID_ror)
1646 out <<
"((_ rotate_right";
1652 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.
distance());
1654 if(distance_int_op.has_value())
1656 out << distance_int_op.value();
1660 "distance type for " + shift_expr.
id_string() +
"must be constant");
1669 "unsupported type for " + shift_expr.
id_string() +
": " +
1672 else if(expr.
id() == ID_named_term)
1676 convert(named_term_expr.value());
1680 else if(expr.
id()==ID_with)
1684 else if(expr.
id()==ID_update)
1688 else if(expr.
id() == ID_update_bit)
1692 else if(expr.
id() == ID_update_bits)
1696 else if(expr.
id() == ID_object_address)
1698 out <<
"(object-address ";
1703 else if(expr.
id() == ID_element_address)
1709 auto element_size_expr_opt =
1719 *element_size_expr_opt, element_address_expr.index().type()));
1722 else if(expr.
id() == ID_field_address)
1731 else if(expr.
id()==ID_member)
1735 else if(expr.
id()==ID_pointer_offset)
1740 op.type().id() == ID_pointer,
1741 "operand of pointer offset expression shall be of pointer type");
1743 std::size_t offset_bits =
1748 if(offset_bits>result_width)
1749 offset_bits=result_width;
1752 if(result_width>offset_bits)
1753 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1755 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1759 if(result_width>offset_bits)
1762 else if(expr.
id()==ID_pointer_object)
1767 op.type().id() == ID_pointer,
1768 "pointer object expressions should be of pointer type");
1774 out <<
"((_ zero_extend " << ext <<
") ";
1776 out <<
"((_ extract "
1777 << pointer_width-1 <<
" "
1785 else if(expr.
id() == ID_is_dynamic_object)
1789 else if(expr.
id() == ID_is_invalid_pointer)
1793 out <<
"(= ((_ extract "
1794 << pointer_width-1 <<
" "
1800 else if(expr.
id()==ID_string_constant)
1806 else if(expr.
id()==ID_extractbit)
1815 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1821 out <<
"(= ((_ extract 0 0) ";
1831 else if(expr.
id()==ID_extractbits)
1845 std::swap(op1_i, op2_i);
1849 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1856 out <<
"(= ((_ extract 0 0) ";
1865 SMT2_TODO(
"smt2: extractbits with non-constant index");
1868 else if(expr.
id()==ID_replication)
1872 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.
times());
1874 out <<
"((_ repeat " << times <<
") ";
1878 else if(expr.
id()==ID_byte_extract_little_endian ||
1879 expr.
id()==ID_byte_extract_big_endian)
1882 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1884 else if(expr.
id()==ID_byte_update_little_endian ||
1885 expr.
id()==ID_byte_update_big_endian)
1888 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1890 else if(expr.
id()==ID_abs)
1896 if(type.
id()==ID_signedbv)
1900 out <<
"(ite (bvslt ";
1902 out <<
" (_ bv0 " << result_width <<
")) ";
1909 else if(type.
id()==ID_fixedbv)
1913 out <<
"(ite (bvslt ";
1915 out <<
" (_ bv0 " << result_width <<
")) ";
1922 else if(type.
id()==ID_floatbv)
1936 else if(expr.
id()==ID_isnan)
1942 if(op_type.
id()==ID_fixedbv)
1944 else if(op_type.
id()==ID_floatbv)
1948 out <<
"(fp.isNaN ";
1958 else if(expr.
id()==ID_isfinite)
1964 if(op_type.
id()==ID_fixedbv)
1966 else if(op_type.
id()==ID_floatbv)
1972 out <<
"(not (fp.isNaN ";
1976 out <<
"(not (fp.isInfinite ";
1988 else if(expr.
id()==ID_isinf)
1994 if(op_type.
id()==ID_fixedbv)
1996 else if(op_type.
id()==ID_floatbv)
2000 out <<
"(fp.isInfinite ";
2010 else if(expr.
id()==ID_isnormal)
2016 if(op_type.
id()==ID_fixedbv)
2018 else if(op_type.
id()==ID_floatbv)
2022 out <<
"(fp.isNormal ";
2035 expr.
id() == ID_overflow_result_plus ||
2036 expr.
id() == ID_overflow_result_minus)
2045 "overflow plus and overflow minus expressions shall be of Boolean type");
2048 expr.
id() == ID_overflow_result_minus;
2049 const typet &op_type = op0.type();
2052 if(op_type.
id()==ID_signedbv)
2055 out <<
"(let ((?sum (";
2056 out << (subtract?
"bvsub":
"bvadd");
2057 out <<
" ((_ sign_extend 1) ";
2060 out <<
" ((_ sign_extend 1) ";
2070 out <<
"(mk-" << smt_typename;
2075 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2080 "((_ extract " << width <<
" " << width <<
") ?sum) "
2081 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
2091 else if(op_type.
id()==ID_unsignedbv ||
2092 op_type.
id()==ID_pointer)
2095 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2096 out <<
" ((_ zero_extend 1) ";
2099 out <<
" ((_ zero_extend 1) ";
2111 out <<
"(mk-" << smt_typename;
2112 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2116 out <<
"((_ extract " << width <<
" " << width <<
") ?sum)";
2127 "overflow check should not be performed on unsupported type",
2132 expr.
id() == ID_overflow_result_mult)
2141 "overflow mult expression shall be of Boolean type");
2146 const typet &op_type = op0.type();
2149 if(op_type.
id()==ID_signedbv)
2151 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
2153 out <<
") ((_ sign_extend " << width <<
") ";
2163 out <<
"(mk-" << smt_typename;
2168 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2172 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
2174 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width - 1) <<
" "
2175 << width * 2 <<
"))))";
2184 else if(op_type.
id()==ID_unsignedbv)
2186 out <<
"(let ((prod (bvmul ((_ zero_extend " << width <<
") ";
2188 out <<
") ((_ zero_extend " << width <<
") ";
2198 out <<
"(mk-" << smt_typename;
2203 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2207 out <<
"(bvuge prod (_ bv" <<
power(2, width) <<
" " << width * 2 <<
"))";
2219 "overflow check should not be performed on unsupported type",
2222 else if(expr.
id() == ID_saturating_plus || expr.
id() == ID_saturating_minus)
2224 const bool subtract = expr.
id() == ID_saturating_minus;
2225 const auto &op_type = expr.
type();
2229 if(op_type.id() == ID_signedbv)
2234 out <<
"(let ((?sum (";
2235 out << (subtract ?
"bvsub" :
"bvadd");
2236 out <<
" ((_ sign_extend 1) ";
2239 out <<
" ((_ sign_extend 1) ";
2246 << width <<
" " << width
2249 << (width - 1) <<
" " << (width - 1) <<
") ?sum)";
2253 out <<
"((_ extract " << width - 1 <<
" 0) ?sum) ";
2256 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2263 else if(op_type.id() == ID_unsignedbv)
2268 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2269 out <<
" ((_ zero_extend 1) ";
2272 out <<
" ((_ zero_extend 1) ";
2277 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2280 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2294 "saturating_plus/minus on unsupported type",
2295 op_type.id_string());
2297 else if(expr.
id()==ID_array)
2303 else if(expr.
id()==ID_literal)
2307 else if(expr.
id()==ID_forall ||
2308 expr.
id()==ID_exists)
2314 throw "MathSAT does not support quantifiers";
2316 if(quantifier_expr.
id() == ID_forall)
2318 else if(quantifier_expr.
id() == ID_exists)
2323 for(
const auto &bound : quantifier_expr.
variables())
2342 const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
2346 else if(expr.
id()==ID_let)
2349 const auto &variables = let_expr.
variables();
2350 const auto &values = let_expr.
values();
2355 for(
auto &binding :
make_range(variables).zip(values))
2374 else if(expr.
id()==ID_constraint_select_one)
2377 "smt2_convt::convert_expr: '" + expr.
id_string() +
2378 "' is not yet supported");
2380 else if(expr.
id() == ID_bswap)
2386 "operand of byte swap expression shall have same type as the expression");
2389 out <<
"(let ((bswap_op ";
2394 bswap_expr.
type().
id() == ID_signedbv ||
2395 bswap_expr.
type().
id() == ID_unsignedbv)
2397 const std::size_t width =
2404 width % bits_per_byte == 0,
2405 "bit width indicated by type of bswap expression should be a multiple "
2406 "of the number of bits per byte");
2408 const std::size_t bytes = width / bits_per_byte;
2417 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2421 out <<
"(bswap_byte_" <<
byte <<
' ';
2422 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2423 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2432 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2433 out <<
" bswap_byte_" <<
byte;
2444 else if(expr.
id() == ID_popcount)
2448 else if(expr.
id() == ID_count_leading_zeros)
2452 else if(expr.
id() == ID_count_trailing_zeros)
2456 else if(expr.
id() == ID_find_first_set)
2460 else if(expr.
id() == ID_bitreverse)
2464 else if(expr.
id() == ID_function_application)
2468 if(function_application_expr.arguments().empty())
2476 for(
auto &op : function_application_expr.arguments())
2487 "smt2_convt::convert_expr should not be applied to unsupported type",
2496 if(dest_type.
id()==ID_c_enum_tag)
2500 if(src_type.
id()==ID_c_enum_tag)
2503 if(dest_type.
id()==ID_bool)
2506 if(src_type.
id()==ID_signedbv ||
2507 src_type.
id()==ID_unsignedbv ||
2508 src_type.
id()==ID_c_bool ||
2509 src_type.
id()==ID_fixedbv ||
2510 src_type.
id()==ID_pointer ||
2511 src_type.
id()==ID_integer)
2519 else if(src_type.
id()==ID_floatbv)
2523 out <<
"(not (fp.isZero ";
2535 else if(dest_type.
id()==ID_c_bool)
2544 out <<
" (_ bv1 " << to_width <<
")";
2545 out <<
" (_ bv0 " << to_width <<
")";
2548 else if(dest_type.
id()==ID_signedbv ||
2549 dest_type.
id()==ID_unsignedbv ||
2550 dest_type.
id()==ID_c_enum ||
2551 dest_type.
id()==ID_bv)
2555 if(src_type.
id()==ID_signedbv ||
2556 src_type.
id()==ID_unsignedbv ||
2557 src_type.
id()==ID_c_bool ||
2558 src_type.
id()==ID_c_enum ||
2559 src_type.
id()==ID_bv)
2563 if(from_width==to_width)
2565 else if(from_width<to_width)
2567 if(src_type.
id()==ID_signedbv)
2568 out <<
"((_ sign_extend ";
2570 out <<
"((_ zero_extend ";
2572 out << (to_width-from_width)
2579 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2584 else if(src_type.
id()==ID_fixedbv)
2588 std::size_t from_width=fixedbv_type.
get_width();
2595 out <<
"(let ((?tcop ";
2601 if(to_width>from_integer_bits)
2603 out <<
"((_ sign_extend "
2604 << (to_width-from_integer_bits) <<
") ";
2605 out <<
"((_ extract " << (from_width-1) <<
" "
2606 << from_fraction_bits <<
") ";
2612 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2613 <<
" " << from_fraction_bits <<
") ";
2618 out <<
" (ite (and ";
2621 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2622 "(_ bv0 " << from_fraction_bits <<
")))";
2625 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2630 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2634 else if(src_type.
id()==ID_floatbv)
2636 if(dest_type.
id()==ID_bv)
2642 defined_expressionst::const_iterator it =
2653 else if(dest_type.
id()==ID_signedbv)
2657 "typecast unexpected "+src_type.
id_string()+
" -> "+
2660 else if(dest_type.
id()==ID_unsignedbv)
2664 "typecast unexpected "+src_type.
id_string()+
" -> "+
2668 else if(src_type.
id()==ID_bool)
2673 if(dest_type.
id()==ID_fixedbv)
2676 out <<
" (concat (_ bv1 "
2679 "(_ bv0 " << spec.
width <<
")";
2683 out <<
" (_ bv1 " << to_width <<
")";
2684 out <<
" (_ bv0 " << to_width <<
")";
2689 else if(src_type.
id()==ID_pointer)
2693 if(from_width<to_width)
2695 out <<
"((_ sign_extend ";
2696 out << (to_width-from_width)
2703 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2708 else if(src_type.
id()==ID_integer)
2714 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2717 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2720 src_type.
id() == ID_struct ||
2721 src_type.
id() == ID_struct_tag)
2727 "bit vector with of source and destination type shall be equal");
2734 "bit vector with of source and destination type shall be equal");
2739 src_type.
id() == ID_union ||
2740 src_type.
id() == ID_union_tag)
2744 "bit vector with of source and destination type shall be equal");
2747 else if(src_type.
id()==ID_c_bit_field)
2751 if(from_width==to_width)
2762 std::ostringstream e_str;
2763 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2764 <<
" src == " <<
format(src);
2768 else if(dest_type.
id()==ID_fixedbv)
2774 if(src_type.
id()==ID_unsignedbv ||
2775 src_type.
id()==ID_signedbv ||
2776 src_type.
id()==ID_c_enum)
2783 if(from_width==to_integer_bits)
2785 else if(from_width>to_integer_bits)
2788 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2796 from_width < to_integer_bits,
2797 "from_width should be smaller than to_integer_bits as other case "
2798 "have been handled above");
2799 if(dest_type.
id()==ID_unsignedbv)
2801 out <<
"(_ zero_extend "
2802 << (to_integer_bits-from_width) <<
") ";
2808 out <<
"((_ sign_extend "
2809 << (to_integer_bits-from_width) <<
") ";
2815 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2818 else if(src_type.
id()==ID_bool)
2820 out <<
"(concat (concat"
2821 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2827 else if(src_type.
id()==ID_fixedbv)
2832 std::size_t from_width=from_fixedbv_type.
get_width();
2834 out <<
"(let ((?tcop ";
2840 if(to_integer_bits<=from_integer_bits)
2842 out <<
"((_ extract "
2843 << (from_fraction_bits+to_integer_bits-1) <<
" "
2844 << from_fraction_bits
2850 to_integer_bits > from_integer_bits,
2851 "to_integer_bits should be greater than from_integer_bits as the"
2852 "other case has been handled above");
2853 out <<
"((_ sign_extend "
2854 << (to_integer_bits-from_integer_bits)
2856 << (from_width-1) <<
" "
2857 << from_fraction_bits
2863 if(to_fraction_bits<=from_fraction_bits)
2865 out <<
"((_ extract "
2866 << (from_fraction_bits-1) <<
" "
2867 << (from_fraction_bits-to_fraction_bits)
2873 to_fraction_bits > from_fraction_bits,
2874 "to_fraction_bits should be greater than from_fraction_bits as the"
2875 "other case has been handled above");
2876 out <<
"(concat ((_ extract "
2877 << (from_fraction_bits-1) <<
" 0) ";
2880 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2889 else if(dest_type.
id()==ID_pointer)
2893 if(src_type.
id()==ID_pointer)
2899 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2900 src_type.
id() == ID_bv)
2906 if(from_width==to_width)
2908 else if(from_width<to_width)
2910 out <<
"((_ sign_extend "
2911 << (to_width-from_width)
2918 out <<
"((_ extract " << to_width <<
" 0) ";
2926 else if(dest_type.
id()==ID_range)
2930 else if(dest_type.
id()==ID_floatbv)
2939 if(src_type.
id()==ID_bool)
2954 a.
build(significand, exponent);
2962 a.
build(significand, exponent);
2968 else if(src_type.
id()==ID_c_bool)
2974 else if(src_type.
id() == ID_bv)
2983 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2984 << dest_floatbv_type.get_f() + 1 <<
") ";
2994 else if(dest_type.
id()==ID_integer)
2996 if(src_type.
id()==ID_bool)
3005 else if(dest_type.
id()==ID_c_bit_field)
3010 if(from_width==to_width)
3031 if(dest_type.
id()==ID_floatbv)
3033 if(src_type.
id()==ID_floatbv)
3060 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3061 << dst.
get_f() + 1 <<
") ";
3070 else if(src_type.
id()==ID_unsignedbv)
3091 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
3092 << dst.
get_f() + 1 <<
") ";
3101 else if(src_type.
id()==ID_signedbv)
3109 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3110 << dst.
get_f() + 1 <<
") ";
3119 else if(src_type.
id()==ID_c_enum_tag)
3133 else if(dest_type.
id()==ID_signedbv)
3138 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
3147 else if(dest_type.
id()==ID_unsignedbv)
3152 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
3176 components.size() == expr.
operands().size(),
3177 "number of struct components as indicated by the struct type shall be equal"
3178 "to the number of operands of the struct expression");
3180 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
3184 const std::string &smt_typename =
datatype_map.at(struct_type);
3187 out <<
"(mk-" << smt_typename;
3190 for(struct_typet::componentst::const_iterator
3191 it=components.begin();
3192 it!=components.end();
3205 auto convert_operand = [
this](
const exprt &op) {
3209 else if(op.type().id() == ID_bool)
3216 std::size_t n_concat = 0;
3217 for(std::size_t i = components.size(); i > 1; i--)
3227 convert_operand(expr.
operands()[i - 1]);
3233 convert_operand(expr.
op0());
3235 out << std::string(n_concat,
')');
3243 const auto &size_expr = array_type.
size();
3249 out <<
"(let ((?far ";
3257 out <<
"(select ?far ";
3280 if(total_width==member_width)
3288 total_width > member_width,
3289 "total_width should be greater than member_width as member_width can be"
3290 "at most as large as total_width and the other case has been handled "
3294 << (total_width-member_width) <<
") ";
3304 if(expr_type.
id()==ID_unsignedbv ||
3305 expr_type.
id()==ID_signedbv ||
3306 expr_type.
id()==ID_bv ||
3307 expr_type.
id()==ID_c_enum ||
3308 expr_type.
id()==ID_c_enum_tag ||
3309 expr_type.
id()==ID_c_bool ||
3310 expr_type.
id()==ID_c_bit_field)
3316 out <<
"(_ bv" << value
3317 <<
" " << width <<
")";
3319 else if(expr_type.
id()==ID_fixedbv)
3325 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
3327 else if(expr_type.
id()==ID_floatbv)
3340 size_t e=floatbv_type.
get_e();
3341 size_t f=floatbv_type.
get_f()+1;
3347 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3353 out <<
"(_ NaN " << e <<
" " << f <<
")";
3358 out <<
"(_ -oo " << e <<
" " << f <<
")";
3360 out <<
"(_ +oo " << e <<
" " << f <<
")";
3370 <<
"#b" << binaryString.substr(0, 1) <<
" "
3371 <<
"#b" << binaryString.substr(1, e) <<
" "
3372 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
3380 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3383 else if(expr_type.
id()==ID_pointer)
3397 out <<
"(_ bv" << value <<
" " << width <<
")";
3400 else if(expr_type.
id()==ID_bool)
3409 else if(expr_type.
id()==ID_array)
3415 else if(expr_type.
id()==ID_rational)
3418 const bool negative =
has_prefix(value,
"-");
3423 size_t pos=value.find(
"/");
3425 if(
pos==std::string::npos)
3426 out << value <<
".0";
3429 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3430 << value.substr(
pos+1) <<
".0)";
3436 else if(expr_type.
id()==ID_integer)
3442 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3452 if(expr.
type().
id() == ID_integer)
3462 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3467 if(expr.
type().
id()==ID_unsignedbv ||
3468 expr.
type().
id()==ID_signedbv)
3470 if(expr.
type().
id()==ID_unsignedbv)
3486 std::vector<mp_integer> dynamic_objects;
3489 if(dynamic_objects.empty())
3495 out <<
"(let ((?obj ((_ extract "
3496 << pointer_width-1 <<
" "
3501 if(dynamic_objects.size()==1)
3503 out <<
"(= (_ bv" << dynamic_objects.front()
3510 for(
const auto &
object : dynamic_objects)
3511 out <<
" (= (_ bv" <<
object
3525 if(op_type.
id()==ID_unsignedbv ||
3526 op_type.
id()==ID_bv)
3529 if(expr.
id()==ID_le)
3531 else if(expr.
id()==ID_lt)
3533 else if(expr.
id()==ID_ge)
3535 else if(expr.
id()==ID_gt)
3544 else if(op_type.
id()==ID_signedbv ||
3545 op_type.
id()==ID_fixedbv)
3548 if(expr.
id()==ID_le)
3550 else if(expr.
id()==ID_lt)
3552 else if(expr.
id()==ID_ge)
3554 else if(expr.
id()==ID_gt)
3563 else if(op_type.
id()==ID_floatbv)
3568 if(expr.
id()==ID_le)
3570 else if(expr.
id()==ID_lt)
3572 else if(expr.
id()==ID_ge)
3574 else if(expr.
id()==ID_gt)
3586 else if(op_type.
id()==ID_rational ||
3587 op_type.
id()==ID_integer)
3598 else if(op_type.
id() == ID_pointer)
3606 if(expr.
id() == ID_le)
3608 else if(expr.
id() == ID_lt)
3610 else if(expr.
id() == ID_ge)
3612 else if(expr.
id() == ID_gt)
3631 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3632 expr.
type().
id() == ID_real)
3637 for(
const auto &op : expr.
operands())
3646 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3647 expr.
type().
id() == ID_fixedbv)
3664 else if(expr.
type().
id() == ID_floatbv)
3671 else if(expr.
type().
id() == ID_pointer)
3677 if(p.
type().
id() != ID_pointer)
3681 p.
type().
id() == ID_pointer,
3682 "one of the operands should have pointer type");
3686 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
3689 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3693 out <<
"(let ((?pointerop ";
3699 const std::size_t offset_bits =
3703 out <<
"((_ extract " << pointer_width - 1 <<
' ' << offset_bits
3704 <<
") ?pointerop) ";
3705 out <<
"(bvadd ((_ extract " << offset_bits - 1 <<
" 0) ?pointerop) ";
3707 if(element_size >= 2)
3709 out <<
"(bvmul ((_ extract " << offset_bits - 1 <<
" 0) ";
3711 out <<
") (_ bv" << element_size <<
" " << offset_bits <<
"))";
3715 out <<
"((_ extract " << offset_bits - 1 <<
" 0) ";
3751 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3754 out <<
"roundNearestTiesToEven";
3756 out <<
"roundTowardNegative";
3758 out <<
"roundTowardPositive";
3760 out <<
"roundTowardZero";
3764 "Rounding mode should have value 0, 1, 2, or 3",
3772 out <<
"(ite (= (_ bv0 " << width <<
") ";
3774 out <<
") roundNearestTiesToEven ";
3776 out <<
"(ite (= (_ bv1 " << width <<
") ";
3778 out <<
") roundTowardNegative ";
3780 out <<
"(ite (= (_ bv2 " << width <<
") ";
3782 out <<
") roundTowardPositive ";
3785 out <<
"roundTowardZero";
3796 type.
id() == ID_floatbv ||
3797 (type.
id() == ID_complex &&
3802 if(type.
id()==ID_floatbv)
3812 else if(type.
id()==ID_complex)
3819 "type should not be one of the unsupported types",
3828 if(expr.
type().
id()==ID_integer)
3836 else if(expr.
type().
id()==ID_unsignedbv ||
3837 expr.
type().
id()==ID_signedbv ||
3838 expr.
type().
id()==ID_fixedbv)
3840 if(expr.
op0().
type().
id()==ID_pointer &&
3846 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
3848 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3851 if(element_size >= 2)
3856 "bitvector width of operand shall be equal to the bitvector width of "
3865 if(element_size >= 2)
3878 else if(expr.
type().
id()==ID_floatbv)
3885 else if(expr.
type().
id()==ID_pointer)
3889 (expr.
op1().
type().
id() == ID_unsignedbv ||
3908 expr.
type().
id() == ID_floatbv,
3909 "type of ieee floating point expression shall be floatbv");
3927 if(expr.
type().
id()==ID_unsignedbv ||
3928 expr.
type().
id()==ID_signedbv)
3930 if(expr.
type().
id()==ID_unsignedbv)
3940 else if(expr.
type().
id()==ID_fixedbv)
3945 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3950 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3952 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3958 else if(expr.
type().
id()==ID_floatbv)
3972 expr.
type().
id() == ID_floatbv,
3973 "type of ieee floating point expression shall be floatbv");
4004 "expression should have been converted to a variant with two operands");
4006 if(expr.
type().
id()==ID_unsignedbv ||
4007 expr.
type().
id()==ID_signedbv)
4018 else if(expr.
type().
id()==ID_floatbv)
4025 else if(expr.
type().
id()==ID_fixedbv)
4030 out <<
"((_ extract "
4031 << spec.
width+fraction_bits-1 <<
" "
4032 << fraction_bits <<
") ";
4036 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4040 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4046 else if(expr.
type().
id()==ID_rational ||
4047 expr.
type().
id()==ID_integer ||
4048 expr.
type().
id()==ID_real)
4052 for(
const auto &op : expr.
operands())
4067 expr.
type().
id() == ID_floatbv,
4068 "type of ieee floating point expression shall be floatbv");
4087 expr.
type().
id() == ID_floatbv,
4088 "type of ieee floating point expression shall be floatbv");
4102 "smt2_convt::convert_floatbv_rem to be implemented when not using "
4113 std::size_t s=expr.
operands().size();
4128 "with expression should have been converted to a version with three "
4133 if(expr_type.
id()==ID_array)
4157 out <<
"(let ((distance? ";
4158 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4162 if(array_width>index_width)
4164 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4170 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4180 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
4182 out <<
"distance?)) ";
4186 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
4188 out <<
") distance?)))";
4191 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
4198 const irep_idt &component_name=index.
get(ID_component_name);
4202 "struct should have accessed component");
4206 const std::string &smt_typename =
datatype_map.at(expr_type);
4208 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
4222 out <<
"(let ((?withop ";
4226 if(m.
width==struct_width)
4236 <<
"((_ extract " << (struct_width-1) <<
" "
4237 << m.
width <<
") ?withop) ";
4246 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
4251 out <<
"(concat (concat "
4252 <<
"((_ extract " << (struct_width-1) <<
" "
4255 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
4262 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
4272 if(total_width==member_width)
4279 total_width > member_width,
4280 "total width should be greater than member_width as member_width is at "
4281 "most as large as total_width and the other case has been handled "
4284 out <<
"((_ extract "
4286 <<
" " << member_width <<
") ";
4293 else if(expr_type.
id()==ID_bv ||
4294 expr_type.
id()==ID_unsignedbv ||
4295 expr_type.
id()==ID_signedbv)
4310 "with expects struct, union, or array type, but got "+
4318 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4335 if(array_op_type.
id()==ID_array)
4370 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
4374 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4378 if(array_width>index_width)
4380 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4386 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4398 false,
"index with unsupported array type: " + array_op_type.
id_string());
4405 const typet &struct_op_type = struct_op.
type();
4408 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
4413 struct_type.
has_component(name),
"struct should have accessed component");
4417 const std::string &smt_typename =
datatype_map.at(struct_type);
4419 out <<
"(" << smt_typename <<
"."
4430 if(expr.
type().
id() == ID_bool)
4436 if(expr.
type().
id() == ID_bool)
4441 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4445 width != 0,
"failed to get union member width");
4449 out <<
"((_ extract "
4459 "convert_member on an unexpected type "+struct_op_type.
id_string());
4466 if(type.
id()==ID_bool)
4472 else if(type.
id()==ID_array)
4483 std::size_t n_concat = 0;
4497 out << std::string(n_concat,
')');
4502 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4513 std::size_t n_concat = 0;
4514 for(std::size_t i=components.size(); i>1; i--)
4534 out << std::string(n_concat,
')');
4539 else if(type.
id()==ID_floatbv)
4543 "floatbv expressions should be flattened when using FPA theory");
4556 if(type.
id()==ID_bool)
4563 else if(type.
id() == ID_array)
4570 out <<
"(let ((?ufop" << nesting <<
" ";
4581 "cannot unflatten arrays of non-constant size");
4588 out <<
"((as const ";
4593 out <<
"((_ extract " << subtype_width - 1 <<
" "
4594 <<
"0) ?ufop" << nesting <<
")";
4598 std::size_t offset = subtype_width;
4599 for(
mp_integer i = 1; i < size; ++i, offset += subtype_width)
4604 out <<
"((_ extract " << offset + subtype_width - 1 <<
" " << offset
4605 <<
") ?ufop" << nesting <<
")";
4618 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4624 out <<
"(let ((?ufop" << nesting <<
" ";
4629 const std::string &smt_typename =
datatype_map.at(type);
4631 out <<
"(mk-" << smt_typename;
4638 std::size_t offset=0;
4641 for(struct_typet::componentst::const_iterator
4642 it=components.begin();
4643 it!=components.end();
4653 out <<
"((_ extract " << offset+member_width-1 <<
" "
4654 << offset <<
") ?ufop" << nesting <<
")";
4656 offset+=member_width;
4677 if(expr.
id()==ID_and && value)
4679 for(
const auto &op : expr.
operands())
4684 if(expr.
id()==ID_or && !value)
4686 for(
const auto &op : expr.
operands())
4691 if(expr.
id()==ID_not)
4701 if(expr.
id() == ID_equal && value)
4710 if(equal_expr.
lhs().
id()==ID_symbol)
4717 equal_expr.
lhs() != equal_expr.
rhs())
4722 id.type=equal_expr.
lhs().
type();
4729 out <<
"; set_to true (equal)\n";
4731 if(equal_expr.
lhs().
type().
id() == ID_mathematical_function)
4735 out <<
"(declare-fun " << smt2_identifier;
4737 auto &mathematical_function_type =
4743 for(
auto &t : mathematical_function_type.domain())
4757 out <<
"(assert (= " << smt2_identifier <<
' ';
4759 out <<
')' <<
')' <<
'\n';
4763 out <<
"(define-fun " << smt2_identifier;
4766 equal_expr.
lhs().
type().
id() != ID_array ||
4774 out <<
"(_ BitVec " << width <<
")";
4793 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4804 out << found_literal->second;
4827 exprt lowered_expr = expr;
4834 it->id() == ID_byte_extract_little_endian ||
4835 it->id() == ID_byte_extract_big_endian)
4840 it->id() == ID_byte_update_little_endian ||
4841 it->id() == ID_byte_update_big_endian)
4847 return lowered_expr;
4864 "lower_byte_operators should remove all byte operators");
4871 auto prophecy_r_or_w_ok =
4872 expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(*it))
4875 it.mutate() = lowered;
4876 it.next_sibling_or_parent();
4879 auto prophecy_pointer_in_range =
4880 expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(*it))
4883 it.mutate() = lowered;
4884 it.next_sibling_or_parent();
4893 return lowered_expr;
4904 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4909 for(
const auto &symbol : q_expr.variables())
4911 const auto identifier = symbol.get_identifier();
4913 id.type = symbol.type();
4921 for(
const auto &op : expr.
operands())
4924 if(expr.
id()==ID_symbol ||
4925 expr.
id()==ID_nondet_symbol)
4928 if(expr.
type().
id()==ID_code)
4933 if(expr.
id()==ID_symbol)
4936 identifier=
"nondet_"+
4941 if(
id.type.is_nil())
4943 id.type=expr.
type();
4948 out <<
"; find_symbols\n";
4949 out <<
"(declare-fun " << smt2_identifier;
4951 if(expr.
type().
id() == ID_mathematical_function)
4953 auto &mathematical_function_type =
4958 for(
auto &type : mathematical_function_type.domain())
4979 else if(expr.
id() == ID_array_of)
4986 const auto &array_type = array_of.type();
4990 out <<
"; the following is a substitute for lambda i. x\n";
4991 out <<
"(declare-fun " <<
id <<
" () ";
4998 out <<
"(assert (forall ((i ";
5000 out <<
")) (= (select " <<
id <<
" i) ";
5018 else if(expr.
id() == ID_array_comprehension)
5025 const auto &array_type = array_comprehension.type();
5026 const auto &array_size = array_type.size();
5030 out <<
"(declare-fun " <<
id <<
" () ";
5034 out <<
"; the following is a substitute for lambda i . x(i)\n";
5035 out <<
"; universally quantified initialization of the array\n";
5036 out <<
"(assert (forall ((";
5040 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
5047 out <<
")) (= (select " <<
id <<
" ";
5066 else if(expr.
id()==ID_array)
5073 out <<
"; the following is a substitute for an array constructor" <<
"\n";
5074 out <<
"(declare-fun " <<
id <<
" () ";
5080 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5082 out <<
"(assert (= (select " <<
id <<
" ";
5103 else if(expr.
id()==ID_string_constant)
5113 out <<
"; the following is a substitute for a string" <<
"\n";
5114 out <<
"(declare-fun " <<
id <<
" () ";
5118 for(std::size_t i=0; i<tmp.
operands().size(); i++)
5120 out <<
"(assert (= (select " <<
id <<
' ';
5124 out <<
"))" <<
"\n";
5131 const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
5137 out <<
"(declare-fun " <<
id <<
" () ";
5148 (expr.
id() == ID_floatbv_plus ||
5149 expr.
id() == ID_floatbv_minus ||
5150 expr.
id() == ID_floatbv_mult ||
5151 expr.
id() == ID_floatbv_div ||
5152 expr.
id() == ID_floatbv_typecast ||
5153 expr.
id() == ID_ieee_float_equal ||
5154 expr.
id() == ID_ieee_float_notequal ||
5155 ((expr.
id() == ID_lt ||
5156 expr.
id() == ID_gt ||
5157 expr.
id() == ID_le ||
5158 expr.
id() == ID_ge ||
5159 expr.
id() == ID_isnan ||
5160 expr.
id() == ID_isnormal ||
5161 expr.
id() == ID_isfinite ||
5162 expr.
id() == ID_isinf ||
5163 expr.
id() == ID_sign ||
5164 expr.
id() == ID_unary_minus ||
5165 expr.
id() == ID_typecast ||
5166 expr.
id() == ID_abs) &&
5173 if(
bvfp_set.insert(
function).second)
5175 out <<
"; this is a model for " << expr.
id() <<
" : "
5178 <<
"(define-fun " <<
function <<
" (";
5180 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5184 out <<
"(op" << i <<
' ';
5194 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
5210 expr.
type().
id() == ID_bv)
5220 out <<
"(declare-fun " <<
id <<
" () ";
5226 out <<
"(assert (= ";
5227 out <<
"((_ to_fp " << floatbv_type.get_e() <<
" "
5228 << floatbv_type.get_f() + 1 <<
") " <<
id <<
')';
5236 else if(expr.
id() == ID_initial_state)
5238 irep_idt function =
"initial-state";
5242 out <<
"(declare-fun " <<
function <<
" (";
5249 else if(expr.
id() == ID_evaluate)
5255 out <<
"(declare-fun " <<
function <<
" (";
5265 expr.
id() == ID_state_is_cstring ||
5266 expr.
id() == ID_state_is_dynamic_object ||
5267 expr.
id() == ID_state_live_object || expr.
id() == ID_state_writeable_object)
5270 expr.
id() == ID_state_is_cstring ?
"state-is-cstring"
5271 : expr.
id() == ID_state_is_dynamic_object ?
"state-is-dynamic-object"
5272 : expr.
id() == ID_state_live_object ?
"state-live-object"
5273 :
"state-writeable-object";
5277 out <<
"(declare-fun " <<
function <<
" (";
5287 expr.
id() == ID_state_r_ok || expr.
id() == ID_state_w_ok ||
5288 expr.
id() == ID_state_rw_ok)
5290 irep_idt function = expr.
id() == ID_state_r_ok ?
"state-r-ok"
5291 : expr.
id() == ID_state_w_ok ?
"state-w-ok"
5296 out <<
"(declare-fun " <<
function <<
" (";
5307 else if(expr.
id() == ID_update_state)
5314 out <<
"(declare-fun " <<
function <<
" (";
5325 else if(expr.
id() == ID_enter_scope_state)
5332 out <<
"(declare-fun " <<
function <<
" (";
5343 else if(expr.
id() == ID_exit_scope_state)
5350 out <<
"(declare-fun " <<
function <<
" (";
5359 else if(expr.
id() == ID_allocate)
5365 out <<
"(declare-fun " <<
function <<
" (";
5374 else if(expr.
id() == ID_reallocate)
5380 out <<
"(declare-fun " <<
function <<
" (";
5391 else if(expr.
id() == ID_deallocate_state)
5397 out <<
"(declare-fun " <<
function <<
" (";
5406 else if(expr.
id() == ID_object_address)
5408 irep_idt function =
"object-address";
5412 out <<
"(declare-fun " <<
function <<
" (String) ";
5417 else if(expr.
id() == ID_field_address)
5423 out <<
"(declare-fun " <<
function <<
" (";
5432 else if(expr.
id() == ID_element_address)
5438 out <<
"(declare-fun " <<
function <<
" (";
5457 if(expr.
id() == ID_with)
5465 if(type.
id()==ID_array)
5479 out <<
"(_ BitVec 1)";
5485 else if(type.
id()==ID_bool)
5489 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
5499 out <<
"(_ BitVec " << width <<
")";
5502 else if(type.
id()==ID_code)
5509 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
5514 "failed to get width of union");
5516 out <<
"(_ BitVec " << width <<
")";
5518 else if(type.
id()==ID_pointer)
5523 else if(type.
id()==ID_bv ||
5524 type.
id()==ID_fixedbv ||
5525 type.
id()==ID_unsignedbv ||
5526 type.
id()==ID_signedbv ||
5527 type.
id()==ID_c_bool)
5532 else if(type.
id()==ID_c_enum)
5539 else if(type.
id()==ID_c_enum_tag)
5543 else if(type.
id()==ID_floatbv)
5548 out <<
"(_ FloatingPoint "
5549 << floatbv_type.
get_e() <<
" "
5550 << floatbv_type.
get_f() + 1 <<
")";
5555 else if(type.
id()==ID_rational ||
5558 else if(type.
id()==ID_integer)
5560 else if(type.
id()==ID_complex)
5570 out <<
"(_ BitVec " << width <<
")";
5573 else if(type.
id()==ID_c_bit_field)
5577 else if(type.
id() == ID_state)
5589 std::set<irep_idt> recstack;
5595 std::set<irep_idt> &recstack)
5597 if(type.
id()==ID_array)
5603 else if(type.
id()==ID_complex)
5610 const std::string smt_typename =
5614 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5615 <<
"(((mk-" << smt_typename;
5617 out <<
" (" << smt_typename <<
".imag ";
5621 out <<
" (" << smt_typename <<
".real ";
5628 else if(type.
id() == ID_struct)
5631 bool need_decl=
false;
5635 const std::string smt_typename =
5650 const std::string &smt_typename =
datatype_map.at(type);
5661 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5662 <<
"(((mk-" << smt_typename <<
" ";
5669 out <<
"(" << smt_typename <<
"." <<
component.get_name()
5675 out <<
"))))" <<
"\n";
5692 for(struct_union_typet::componentst::const_iterator
5693 it=components.begin();
5694 it!=components.end();
5701 out <<
"(define-fun update-" << smt_typename <<
"."
5703 <<
"((s " << smt_typename <<
") "
5706 out <<
")) " << smt_typename <<
" "
5707 <<
"(mk-" << smt_typename
5710 for(struct_union_typet::componentst::const_iterator
5711 it2=components.begin();
5712 it2!=components.end();
5719 out <<
"(" << smt_typename <<
"."
5720 << it2->get_name() <<
" s) ";
5724 out <<
"))" <<
"\n";
5730 else if(type.
id() == ID_union)
5738 else if(type.
id()==ID_code)
5742 for(
const auto ¶m : parameters)
5747 else if(type.
id()==ID_pointer)
5751 else if(type.
id() == ID_struct_tag)
5754 const irep_idt &
id = struct_tag.get_identifier();
5756 if(recstack.find(
id) == recstack.end())
5759 recstack.insert(
id);
5764 else if(type.
id() == ID_union_tag)
5767 const irep_idt &
id = union_tag.get_identifier();
5769 if(recstack.find(
id) == recstack.end())
5771 recstack.insert(
id);
5775 else if(type.
id() == ID_state)
5780 out <<
"(declare-sort state 0)\n";
5783 else if(type.
id() == ID_mathematical_function)
5785 const auto &mathematical_function_type =
5787 for(
auto &d_type : mathematical_function_type.domain())
API to expression classes for bitvectors.
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
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.
bool can_cast_expr< overflow_result_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
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 update_bits_exprt & to_update_bits_expr(const exprt &expr)
Cast an exprt to an update_bits_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.
bool has_byte_operator(const exprt &src)
Return true iff src or one of its operands contain a byte extract or byte update expression.
Expression classes for byte-level operators.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
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)
pointer_typet pointer_type(const typet &subtype)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
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.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
Array constructor from list of elements.
typet index_type() const
The type of the index expressions into any instance of this type.
const typet & element_type() const
The type of the elements of the array.
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 has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
depth_iteratort depth_end()
bool is_boolean() const
Return whether the expression represents a Boolean.
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.
void visit_post(std::function< void(exprt &)>)
These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...
The Boolean constant false.
std::size_t get_fraction_bits() const
Fixed-width bit-vector with signed fixed-point interpretation.
std::size_t get_fraction_bits() const
std::size_t get_integer_bits() const
Semantic type conversion from/to floating-point formats.
Fixed-width bit-vector with IEEE floating-point interpretation.
std::size_t get_f() const
std::size_t get_e() const
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
std::size_t width() const
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt NaN(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void build(const mp_integer &exp, const mp_integer &frac)
The trinary if-then-else operator.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
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
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
const mp_integer & get_invalid_object() const
numberingt< exprt, irep_hash > objects
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
void get_dynamic_objects(std::vector< mp_integer > &objects) const
mp_integer add_object(const exprt &expr)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
A base class for quantifier expressions.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
const irep_idt & get_identifier() const
void convert_relation(const binary_relation_exprt &)
bool use_lambda_for_array
void convert_type(const typet &)
void unflatten(wheret, const typet &, unsigned nesting=0)
bool use_array_theory(const exprt &)
void find_symbols(const exprt &expr)
std::size_t number_of_solver_calls
void convert_typecast(const typecast_exprt &expr)
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
tvt l_get(literalt l) const
void convert_floatbv_rem(const binary_exprt &expr)
std::unordered_map< irep_idt, irept > current_bindings
resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
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)
void convert_string_literal(const std::string &)
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)
void convert_update_bit(const update_bit_exprt &)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_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
std::map< object_size_exprt, irep_idt > object_sizes
void define_object_size(const irep_idt &id, const object_size_exprt &expr)
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'.
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< literalt > 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 convert_update_bits(const update_bits_exprt &)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
void convert_update(const update_exprt &)
std::set< irep_idt > state_fkt_declared
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)
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.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
The unary minus expression.
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Replaces a sub-range of a bit-vector operand.
exprt lower() const
A lowering to masking, shifting, or.
Replaces a sub-range of a bit-vector operand.
exprt lower() const
A lowering to masking, shifting, or.
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
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
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
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.
double pow(double x, double y)
API to expression classes for 'mathematical' expressions.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
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)
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt simplify_expr(exprt src, const namespacet &ns)
static bool has_quantifier(const exprt &expr)
static bool is_zero_width(const typet &type, const namespacet &ns)
Returns true iff type has effective width of zero bits.
static bool is_smt2_simple_identifier(const std::string &identifier)
#define UNEXPECTEDCASE(S)
bool is_smt2_simple_symbol_character(char ch)
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
#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,...)
#define UNREACHABLE_BECAUSE(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 update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_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 named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_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 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 ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_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 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 complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_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.