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)
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 <<
" ";
329 if(expr.
id()==ID_symbol)
336 return it->second.value;
339 else if(expr.
id()==ID_nondet_symbol)
346 return it->second.value;
348 else if(expr.
id() == ID_literal)
356 else if(expr.
id() == ID_not)
361 else if(op.is_false())
366 (!expr.
has_operands() && (expr.
id() == ID_struct || expr.
id() == ID_array)))
378 op = std::move(eval_op);
413 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
418 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
429 else if(src.
get_sub().size()==2 &&
434 else if(src.
get_sub().size()==3 &&
437 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
441 else if(src.
get_sub().size()==4 &&
444 if(type.
id()==ID_floatbv)
459 s1_int << (floatbv_type.
get_e() + floatbv_type.
get_f()),
465 else if(src.
get_sub().size()==4 &&
473 else if(src.
get_sub().size()==4 &&
481 else if(src.
get_sub().size()==4 &&
490 if(type.
id()==ID_signedbv ||
491 type.
id()==ID_unsignedbv ||
492 type.
id()==ID_c_enum ||
493 type.
id()==ID_c_bool)
497 else if(type.
id()==ID_c_enum_tag)
503 result.
type() = type;
506 else if(type.
id()==ID_fixedbv ||
507 type.
id()==ID_floatbv)
512 else if(type.
id()==ID_integer ||
519 "smt2_convt::parse_literal should not be of unsupported type " +
527 std::unordered_map<int64_t, exprt> operands_map;
531 auto maybe_default_op = operands_map.find(-1);
533 if(maybe_default_op == operands_map.end())
536 default_op = maybe_default_op->second;
539 if(maybe_size.has_value())
541 while(i < maybe_size.value())
543 auto found_op = operands_map.find(i);
544 if(found_op != operands_map.end())
545 operands.emplace_back(found_op->second);
547 operands.emplace_back(default_op);
555 auto found_op = operands_map.find(i);
556 while(found_op != operands_map.end())
558 operands.emplace_back(found_op->second);
560 found_op = operands_map.find(i);
562 operands.emplace_back(default_op);
568 std::unordered_map<int64_t, exprt> *operands_map,
581 bool failure =
to_integer(index_constant, tempint);
584 long index = tempint.to_long();
586 operands_map->emplace(index, value);
588 else if(src.
get_sub().size()==2 &&
589 src.
get_sub()[0].get_sub().size()==3 &&
590 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
591 src.
get_sub()[0].get_sub()[1].id()==
"const")
595 operands_map->emplace(-1, default_value);
628 if(components.empty())
636 for(std::size_t i=0; i<components.size(); i++)
646 src.
get_sub().size() > j,
"insufficient number of component values");
663 std::size_t offset=0;
665 for(std::size_t i=0; i<components.size(); i++)
670 std::size_t component_width=
boolbv_width(components[i].type());
673 offset + component_width <= total_width,
674 "struct component bits shall be within struct bit vector");
676 std::string component_binary=
678 total_width-offset-component_width, component_width);
683 offset+=component_width;
697 for(
const auto &binding : src.
get_sub()[1].get_sub())
699 const irep_idt &name = binding.get_sub()[0].id();
710 return parse_rec(bindings_it->second, type);
714 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
715 type.
id() == ID_integer || type.
id() == ID_rational ||
716 type.
id() == ID_real || type.
id() == ID_c_enum ||
717 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
718 type.
id() == ID_floatbv || type.
id() == ID_c_bool)
722 else if(type.
id()==ID_bool)
724 if(src.
id()==ID_1 || src.
id()==ID_true)
726 else if(src.
id()==ID_0 || src.
id()==ID_false)
729 else if(type.
id()==ID_pointer)
744 else if(type.
id()==ID_struct)
748 else if(type.
id() == ID_struct_tag)
753 struct_expr.type() = type;
754 return std::move(struct_expr);
756 else if(type.
id()==ID_union)
760 else if(type.
id() == ID_union_tag)
764 union_expr.type() = type;
767 else if(type.
id()==ID_array)
781 expr.
id() == ID_string_constant || expr.
id() == ID_label)
784 const std::size_t max_objects = std::size_t(1) << object_bits;
787 if(object_id >= max_objects)
790 "too many addressed objects: maximum number of objects is set to 2^n=" +
791 std::to_string(max_objects) +
792 " (with n=" + std::to_string(object_bits) +
"); " +
793 "use the `--object-bits n` option to increase the maximum number"};
796 out <<
"(concat (_ bv" << object_id <<
" " << object_bits <<
")"
797 <<
" (_ bv0 " <<
boolbv_width(result_type) - object_bits <<
"))";
799 else if(expr.
id()==ID_index)
808 if(array.
type().
id()==ID_pointer)
810 else if(array.
type().
id()==ID_array)
830 else if(expr.
id()==ID_member)
835 const typet &struct_op_type = struct_op.
type();
838 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
839 "member expression operand shall have struct type");
856 else if(expr.
id()==ID_if)
871 "operand of address of expression should not be of kind " +
879 if(node.
id() == ID_exists || node.
id() == ID_forall)
895 else if(expr.
id()==ID_literal)
907 out <<
"; convert\n";
908 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
918 out <<
"(declare-fun ";
920 out <<
" () Bool)\n";
921 out <<
"(assert (= ";
933 out <<
"(define-fun " << identifier <<
" () Bool ";
961 const auto identifier =
992 if(identifier.empty())
995 if(isdigit(identifier[0]))
1017 std::string result =
"|";
1019 for(
auto ch : identifier)
1027 result+=std::to_string(ch);
1044 if(type.
id()==ID_floatbv)
1047 return "f"+std::to_string(spec.
width())+
"_"+std::to_string(spec.
f);
1049 else if(type.
id() == ID_bv)
1053 else if(type.
id()==ID_unsignedbv)
1057 else if(type.
id()==ID_c_bool)
1061 else if(type.
id()==ID_signedbv)
1065 else if(type.
id()==ID_bool)
1069 else if(type.
id()==ID_c_enum_tag)
1073 else if(type.
id() == ID_pointer)
1077 else if(type.
id() == ID_struct_tag)
1084 else if(type.
id() == ID_union_tag)
1088 else if(type.
id() == ID_array)
1109 if(expr.
id()==ID_symbol)
1116 if(expr.
id()==ID_smt2_symbol)
1124 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
1130 for(
const auto &op : expr.
operands())
1158 converter_result->second(expr);
1163 if(expr.
id()==ID_symbol)
1169 else if(expr.
id()==ID_nondet_symbol)
1172 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1175 else if(expr.
id()==ID_smt2_symbol)
1181 else if(expr.
id()==ID_typecast)
1185 else if(expr.
id()==ID_floatbv_typecast)
1189 else if(expr.
id()==ID_struct)
1193 else if(expr.
id()==ID_union)
1201 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
1205 "concatenation over a single operand should have matching types",
1210 else if(expr.
id()==ID_concatenation ||
1211 expr.
id()==ID_bitand ||
1212 expr.
id()==ID_bitor ||
1213 expr.
id()==ID_bitxor ||
1214 expr.
id()==ID_bitnand ||
1215 expr.
id()==ID_bitnor)
1219 "given expression should have at least two operands",
1224 if(expr.
id()==ID_concatenation)
1226 else if(expr.
id()==ID_bitand)
1228 else if(expr.
id()==ID_bitor)
1230 else if(expr.
id()==ID_bitxor)
1232 else if(expr.
id()==ID_bitnand)
1234 else if(expr.
id()==ID_bitnor)
1237 for(
const auto &op : expr.
operands())
1245 else if(expr.
id()==ID_bitnot)
1253 else if(expr.
id()==ID_unary_minus)
1258 unary_minus_expr.
type().
id() == ID_rational ||
1259 unary_minus_expr.
type().
id() == ID_integer ||
1260 unary_minus_expr.
type().
id() == ID_real)
1266 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1285 else if(expr.
id()==ID_unary_plus)
1290 else if(expr.
id()==ID_sign)
1296 if(op_type.
id()==ID_floatbv)
1300 out <<
"(fp.isNegative ";
1307 else if(op_type.
id()==ID_signedbv)
1313 out <<
" (_ bv0 " << op_width <<
"))";
1318 "sign should not be applied to unsupported type",
1321 else if(expr.
id()==ID_if)
1333 else if(expr.
id()==ID_and ||
1339 "logical and, or, and xor expressions should have Boolean type");
1342 "logical and, or, and xor expressions should have at least two operands");
1344 out <<
"(" << expr.
id();
1345 for(
const auto &op : expr.
operands())
1352 else if(expr.
id()==ID_implies)
1357 implies_expr.
is_boolean(),
"implies expression should have Boolean type");
1365 else if(expr.
id()==ID_not)
1370 not_expr.
is_boolean(),
"not expression should have Boolean type");
1376 else if(expr.
id() == ID_equal)
1382 "operands of equal expression shall have same type");
1397 else if(expr.
id() == ID_notequal)
1403 "operands of not equal expression shall have same type");
1411 else if(expr.
id()==ID_ieee_float_equal ||
1412 expr.
id()==ID_ieee_float_notequal)
1419 rel_expr.lhs().type() == rel_expr.rhs().type(),
1420 "operands of float equal and not equal expressions shall have same type");
1425 if(rel_expr.id() == ID_ieee_float_notequal)
1434 if(rel_expr.id() == ID_ieee_float_notequal)
1440 else if(expr.
id()==ID_le ||
1447 else if(expr.
id()==ID_plus)
1451 else if(expr.
id()==ID_floatbv_plus)
1455 else if(expr.
id()==ID_minus)
1459 else if(expr.
id()==ID_floatbv_minus)
1463 else if(expr.
id()==ID_div)
1467 else if(expr.
id()==ID_floatbv_div)
1471 else if(expr.
id()==ID_mod)
1475 else if(expr.
id() == ID_euclidean_mod)
1479 else if(expr.
id()==ID_mult)
1483 else if(expr.
id()==ID_floatbv_mult)
1487 else if(expr.
id() == ID_floatbv_rem)
1491 else if(expr.
id()==ID_address_of)
1497 else if(expr.
id() == ID_array_of)
1502 array_of_expr.type().id() == ID_array,
1503 "array of expression shall have array type");
1507 out <<
"((as const ";
1515 defined_expressionst::const_iterator it =
1521 else if(expr.
id() == ID_array_comprehension)
1526 array_comprehension.type().id() == ID_array,
1527 "array_comprehension expression shall have array type");
1531 out <<
"(lambda ((";
1534 convert_type(array_comprehension.type().size().type());
1546 else if(expr.
id()==ID_index)
1550 else if(expr.
id()==ID_ashr ||
1551 expr.
id()==ID_lshr ||
1557 if(type.
id()==ID_unsignedbv ||
1558 type.
id()==ID_signedbv ||
1561 if(shift_expr.
id() == ID_ashr)
1563 else if(shift_expr.
id() == ID_lshr)
1565 else if(shift_expr.
id() == ID_shl)
1595 if(width_op0==width_op1)
1597 else if(width_op0>width_op1)
1599 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1605 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1612 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1619 "unsupported type for " + shift_expr.
id_string() +
": " +
1622 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1628 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1633 if(shift_expr.
id() == ID_rol)
1634 out <<
"((_ rotate_left";
1635 else if(shift_expr.
id() == ID_ror)
1636 out <<
"((_ rotate_right";
1644 if(distance_int_op.has_value())
1646 out << distance_int_op.value();
1650 "distance type for " + shift_expr.
id_string() +
"must be constant");
1659 "unsupported type for " + shift_expr.
id_string() +
": " +
1662 else if(expr.
id() == ID_named_term)
1666 convert(named_term_expr.value());
1670 else if(expr.
id()==ID_with)
1674 else if(expr.
id()==ID_update)
1678 else if(expr.
id() == ID_object_address)
1680 out <<
"(object-address ";
1685 else if(expr.
id() == ID_element_address)
1691 auto element_size_expr_opt =
1701 *element_size_expr_opt, element_address_expr.index().type()));
1704 else if(expr.
id() == ID_field_address)
1713 else if(expr.
id()==ID_member)
1717 else if(expr.
id()==ID_pointer_offset)
1722 op.type().id() == ID_pointer,
1723 "operand of pointer offset expression shall be of pointer type");
1725 std::size_t offset_bits =
1730 if(offset_bits>result_width)
1731 offset_bits=result_width;
1734 if(result_width>offset_bits)
1735 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1737 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1741 if(result_width>offset_bits)
1744 else if(expr.
id()==ID_pointer_object)
1749 op.type().id() == ID_pointer,
1750 "pointer object expressions should be of pointer type");
1756 out <<
"((_ zero_extend " << ext <<
") ";
1758 out <<
"((_ extract "
1759 << pointer_width-1 <<
" "
1767 else if(expr.
id() == ID_is_dynamic_object)
1771 else if(expr.
id() == ID_is_invalid_pointer)
1775 out <<
"(= ((_ extract "
1776 << pointer_width-1 <<
" "
1782 else if(expr.
id()==ID_string_constant)
1788 else if(expr.
id()==ID_extractbit)
1797 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1803 out <<
"(= ((_ extract 0 0) ";
1812 else if(expr.
id()==ID_extractbits)
1826 std::swap(op1_i, op2_i);
1830 out <<
"((_ extract " << op1_i <<
" " << op2_i <<
") ";
1837 out <<
"(= ((_ extract 0 0) ";
1846 SMT2_TODO(
"smt2: extractbits with non-constant index");
1849 else if(expr.
id()==ID_replication)
1855 out <<
"((_ repeat " << times <<
") ";
1859 else if(expr.
id()==ID_byte_extract_little_endian ||
1860 expr.
id()==ID_byte_extract_big_endian)
1863 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1865 else if(expr.
id()==ID_byte_update_little_endian ||
1866 expr.
id()==ID_byte_update_big_endian)
1869 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1871 else if(expr.
id()==ID_abs)
1877 if(type.
id()==ID_signedbv)
1881 out <<
"(ite (bvslt ";
1883 out <<
" (_ bv0 " << result_width <<
")) ";
1890 else if(type.
id()==ID_fixedbv)
1894 out <<
"(ite (bvslt ";
1896 out <<
" (_ bv0 " << result_width <<
")) ";
1903 else if(type.
id()==ID_floatbv)
1917 else if(expr.
id()==ID_isnan)
1923 if(op_type.
id()==ID_fixedbv)
1925 else if(op_type.
id()==ID_floatbv)
1929 out <<
"(fp.isNaN ";
1939 else if(expr.
id()==ID_isfinite)
1945 if(op_type.
id()==ID_fixedbv)
1947 else if(op_type.
id()==ID_floatbv)
1953 out <<
"(not (fp.isNaN ";
1957 out <<
"(not (fp.isInfinite ";
1969 else if(expr.
id()==ID_isinf)
1975 if(op_type.
id()==ID_fixedbv)
1977 else if(op_type.
id()==ID_floatbv)
1981 out <<
"(fp.isInfinite ";
1991 else if(expr.
id()==ID_isnormal)
1997 if(op_type.
id()==ID_fixedbv)
1999 else if(op_type.
id()==ID_floatbv)
2003 out <<
"(fp.isNormal ";
2016 expr.
id() == ID_overflow_result_plus ||
2017 expr.
id() == ID_overflow_result_minus)
2026 "overflow plus and overflow minus expressions shall be of Boolean type");
2029 expr.
id() == ID_overflow_result_minus;
2030 const typet &op_type = op0.type();
2033 if(op_type.
id()==ID_signedbv)
2036 out <<
"(let ((?sum (";
2037 out << (subtract?
"bvsub":
"bvadd");
2038 out <<
" ((_ sign_extend 1) ";
2041 out <<
" ((_ sign_extend 1) ";
2051 out <<
"(mk-" << smt_typename;
2056 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2061 "((_ extract " << width <<
" " << width <<
") ?sum) "
2062 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
2072 else if(op_type.
id()==ID_unsignedbv ||
2073 op_type.
id()==ID_pointer)
2076 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2077 out <<
" ((_ zero_extend 1) ";
2080 out <<
" ((_ zero_extend 1) ";
2092 out <<
"(mk-" << smt_typename;
2093 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2097 out <<
"((_ extract " << width <<
" " << width <<
") ?sum)";
2108 "overflow check should not be performed on unsupported type",
2113 expr.
id() == ID_overflow_result_mult)
2122 "overflow mult expression shall be of Boolean type");
2127 const typet &op_type = op0.type();
2130 if(op_type.
id()==ID_signedbv)
2132 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
2134 out <<
") ((_ sign_extend " << width <<
") ";
2144 out <<
"(mk-" << smt_typename;
2149 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2153 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
2155 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width - 1) <<
" "
2156 << width * 2 <<
"))))";
2165 else if(op_type.
id()==ID_unsignedbv)
2167 out <<
"(let ((prod (bvmul ((_ zero_extend " << width <<
") ";
2169 out <<
") ((_ zero_extend " << width <<
") ";
2179 out <<
"(mk-" << smt_typename;
2184 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2188 out <<
"(bvuge prod (_ bv" <<
power(2, width) <<
" " << width * 2 <<
"))";
2200 "overflow check should not be performed on unsupported type",
2203 else if(expr.
id() == ID_saturating_plus || expr.
id() == ID_saturating_minus)
2205 const bool subtract = expr.
id() == ID_saturating_minus;
2206 const auto &op_type = expr.
type();
2210 if(op_type.id() == ID_signedbv)
2215 out <<
"(let ((?sum (";
2216 out << (subtract ?
"bvsub" :
"bvadd");
2217 out <<
" ((_ sign_extend 1) ";
2220 out <<
" ((_ sign_extend 1) ";
2227 << width <<
" " << width
2230 << (width - 1) <<
" " << (width - 1) <<
") ?sum)";
2234 out <<
"((_ extract " << width - 1 <<
" 0) ?sum) ";
2237 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2244 else if(op_type.id() == ID_unsignedbv)
2249 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2250 out <<
" ((_ zero_extend 1) ";
2253 out <<
" ((_ zero_extend 1) ";
2258 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2261 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2275 "saturating_plus/minus on unsupported type",
2276 op_type.id_string());
2278 else if(expr.
id()==ID_array)
2284 else if(expr.
id()==ID_literal)
2288 else if(expr.
id()==ID_forall ||
2289 expr.
id()==ID_exists)
2295 throw "MathSAT does not support quantifiers";
2297 if(quantifier_expr.
id() == ID_forall)
2299 else if(quantifier_expr.
id() == ID_exists)
2304 for(
const auto &bound : quantifier_expr.
variables())
2327 else if(expr.
id()==ID_let)
2330 const auto &variables = let_expr.
variables();
2331 const auto &values = let_expr.
values();
2336 for(
auto &binding :
make_range(variables).zip(values))
2355 else if(expr.
id()==ID_constraint_select_one)
2358 "smt2_convt::convert_expr: '" + expr.
id_string() +
2359 "' is not yet supported");
2361 else if(expr.
id() == ID_bswap)
2367 "operand of byte swap expression shall have same type as the expression");
2370 out <<
"(let ((bswap_op ";
2375 bswap_expr.
type().
id() == ID_signedbv ||
2376 bswap_expr.
type().
id() == ID_unsignedbv)
2378 const std::size_t width =
2385 width % bits_per_byte == 0,
2386 "bit width indicated by type of bswap expression should be a multiple "
2387 "of the number of bits per byte");
2389 const std::size_t bytes = width / bits_per_byte;
2398 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2402 out <<
"(bswap_byte_" <<
byte <<
' ';
2403 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2404 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2413 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2414 out <<
" bswap_byte_" <<
byte;
2425 else if(expr.
id() == ID_popcount)
2429 else if(expr.
id() == ID_count_leading_zeros)
2433 else if(expr.
id() == ID_count_trailing_zeros)
2437 else if(expr.
id() == ID_find_first_set)
2441 else if(expr.
id() == ID_bitreverse)
2445 else if(expr.
id() == ID_function_application)
2449 if(function_application_expr.arguments().empty())
2457 for(
auto &op : function_application_expr.arguments())
2468 "smt2_convt::convert_expr should not be applied to unsupported type",
2477 if(dest_type.
id()==ID_c_enum_tag)
2481 if(src_type.
id()==ID_c_enum_tag)
2484 if(dest_type.
id()==ID_bool)
2487 if(src_type.
id()==ID_signedbv ||
2488 src_type.
id()==ID_unsignedbv ||
2489 src_type.
id()==ID_c_bool ||
2490 src_type.
id()==ID_fixedbv ||
2491 src_type.
id()==ID_pointer ||
2492 src_type.
id()==ID_integer)
2500 else if(src_type.
id()==ID_floatbv)
2504 out <<
"(not (fp.isZero ";
2516 else if(dest_type.
id()==ID_c_bool)
2525 out <<
" (_ bv1 " << to_width <<
")";
2526 out <<
" (_ bv0 " << to_width <<
")";
2529 else if(dest_type.
id()==ID_signedbv ||
2530 dest_type.
id()==ID_unsignedbv ||
2531 dest_type.
id()==ID_c_enum ||
2532 dest_type.
id()==ID_bv)
2536 if(src_type.
id()==ID_signedbv ||
2537 src_type.
id()==ID_unsignedbv ||
2538 src_type.
id()==ID_c_bool ||
2539 src_type.
id()==ID_c_enum ||
2540 src_type.
id()==ID_bv)
2544 if(from_width==to_width)
2546 else if(from_width<to_width)
2548 if(src_type.
id()==ID_signedbv)
2549 out <<
"((_ sign_extend ";
2551 out <<
"((_ zero_extend ";
2553 out << (to_width-from_width)
2560 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2565 else if(src_type.
id()==ID_fixedbv)
2569 std::size_t from_width=fixedbv_type.
get_width();
2576 out <<
"(let ((?tcop ";
2582 if(to_width>from_integer_bits)
2584 out <<
"((_ sign_extend "
2585 << (to_width-from_integer_bits) <<
") ";
2586 out <<
"((_ extract " << (from_width-1) <<
" "
2587 << from_fraction_bits <<
") ";
2593 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2594 <<
" " << from_fraction_bits <<
") ";
2599 out <<
" (ite (and ";
2602 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2603 "(_ bv0 " << from_fraction_bits <<
")))";
2606 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2611 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2615 else if(src_type.
id()==ID_floatbv)
2617 if(dest_type.
id()==ID_bv)
2623 defined_expressionst::const_iterator it =
2634 else if(dest_type.
id()==ID_signedbv)
2638 "typecast unexpected "+src_type.
id_string()+
" -> "+
2641 else if(dest_type.
id()==ID_unsignedbv)
2645 "typecast unexpected "+src_type.
id_string()+
" -> "+
2649 else if(src_type.
id()==ID_bool)
2654 if(dest_type.
id()==ID_fixedbv)
2657 out <<
" (concat (_ bv1 "
2660 "(_ bv0 " << spec.
width <<
")";
2664 out <<
" (_ bv1 " << to_width <<
")";
2665 out <<
" (_ bv0 " << to_width <<
")";
2670 else if(src_type.
id()==ID_pointer)
2674 if(from_width<to_width)
2676 out <<
"((_ sign_extend ";
2677 out << (to_width-from_width)
2684 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2689 else if(src_type.
id()==ID_integer)
2695 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2698 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2701 src_type.
id() == ID_struct ||
2702 src_type.
id() == ID_struct_tag)
2708 "bit vector with of source and destination type shall be equal");
2715 "bit vector with of source and destination type shall be equal");
2720 src_type.
id() == ID_union ||
2721 src_type.
id() == ID_union_tag)
2725 "bit vector with of source and destination type shall be equal");
2728 else if(src_type.
id()==ID_c_bit_field)
2732 if(from_width==to_width)
2743 std::ostringstream e_str;
2744 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2745 <<
" src == " <<
format(src);
2749 else if(dest_type.
id()==ID_fixedbv)
2755 if(src_type.
id()==ID_unsignedbv ||
2756 src_type.
id()==ID_signedbv ||
2757 src_type.
id()==ID_c_enum)
2764 if(from_width==to_integer_bits)
2766 else if(from_width>to_integer_bits)
2769 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2777 from_width < to_integer_bits,
2778 "from_width should be smaller than to_integer_bits as other case "
2779 "have been handled above");
2780 if(dest_type.
id()==ID_unsignedbv)
2782 out <<
"(_ zero_extend "
2783 << (to_integer_bits-from_width) <<
") ";
2789 out <<
"((_ sign_extend "
2790 << (to_integer_bits-from_width) <<
") ";
2796 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2799 else if(src_type.
id()==ID_bool)
2801 out <<
"(concat (concat"
2802 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2808 else if(src_type.
id()==ID_fixedbv)
2813 std::size_t from_width=from_fixedbv_type.
get_width();
2815 out <<
"(let ((?tcop ";
2821 if(to_integer_bits<=from_integer_bits)
2823 out <<
"((_ extract "
2824 << (from_fraction_bits+to_integer_bits-1) <<
" "
2825 << from_fraction_bits
2831 to_integer_bits > from_integer_bits,
2832 "to_integer_bits should be greater than from_integer_bits as the"
2833 "other case has been handled above");
2834 out <<
"((_ sign_extend "
2835 << (to_integer_bits-from_integer_bits)
2837 << (from_width-1) <<
" "
2838 << from_fraction_bits
2844 if(to_fraction_bits<=from_fraction_bits)
2846 out <<
"((_ extract "
2847 << (from_fraction_bits-1) <<
" "
2848 << (from_fraction_bits-to_fraction_bits)
2854 to_fraction_bits > from_fraction_bits,
2855 "to_fraction_bits should be greater than from_fraction_bits as the"
2856 "other case has been handled above");
2857 out <<
"(concat ((_ extract "
2858 << (from_fraction_bits-1) <<
" 0) ";
2861 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2870 else if(dest_type.
id()==ID_pointer)
2874 if(src_type.
id()==ID_pointer)
2880 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2881 src_type.
id() == ID_bv)
2887 if(from_width==to_width)
2889 else if(from_width<to_width)
2891 out <<
"((_ sign_extend "
2892 << (to_width-from_width)
2899 out <<
"((_ extract " << to_width <<
" 0) ";
2907 else if(dest_type.
id()==ID_range)
2911 else if(dest_type.
id()==ID_floatbv)
2920 if(src_type.
id()==ID_bool)
2935 a.
build(significand, exponent);
2943 a.
build(significand, exponent);
2949 else if(src_type.
id()==ID_c_bool)
2955 else if(src_type.
id() == ID_bv)
2964 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2965 << dest_floatbv_type.get_f() + 1 <<
") ";
2975 else if(dest_type.
id()==ID_integer)
2977 if(src_type.
id()==ID_bool)
2986 else if(dest_type.
id()==ID_c_bit_field)
2991 if(from_width==to_width)
3012 if(dest_type.
id()==ID_floatbv)
3014 if(src_type.
id()==ID_floatbv)
3041 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3042 << dst.
get_f() + 1 <<
") ";
3051 else if(src_type.
id()==ID_unsignedbv)
3072 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
3073 << dst.
get_f() + 1 <<
") ";
3082 else if(src_type.
id()==ID_signedbv)
3090 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3091 << dst.
get_f() + 1 <<
") ";
3100 else if(src_type.
id()==ID_c_enum_tag)
3114 else if(dest_type.
id()==ID_signedbv)
3119 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
3128 else if(dest_type.
id()==ID_unsignedbv)
3133 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
3157 components.size() == expr.
operands().size(),
3158 "number of struct components as indicated by the struct type shall be equal"
3159 "to the number of operands of the struct expression");
3161 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
3165 const std::string &smt_typename =
datatype_map.at(struct_type);
3168 out <<
"(mk-" << smt_typename;
3171 for(struct_typet::componentst::const_iterator
3172 it=components.begin();
3173 it!=components.end();
3186 auto convert_operand = [
this](
const exprt &op) {
3190 else if(op.type().id() == ID_bool)
3197 std::size_t n_concat = 0;
3198 for(std::size_t i = components.size(); i > 1; i--)
3208 convert_operand(expr.
operands()[i - 1]);
3214 convert_operand(expr.
op0());
3216 out << std::string(n_concat,
')');
3224 const auto &size_expr = array_type.
size();
3230 out <<
"(let ((?far ";
3238 out <<
"(select ?far ";
3261 if(total_width==member_width)
3269 total_width > member_width,
3270 "total_width should be greater than member_width as member_width can be"
3271 "at most as large as total_width and the other case has been handled "
3275 << (total_width-member_width) <<
") ";
3285 if(expr_type.
id()==ID_unsignedbv ||
3286 expr_type.
id()==ID_signedbv ||
3287 expr_type.
id()==ID_bv ||
3288 expr_type.
id()==ID_c_enum ||
3289 expr_type.
id()==ID_c_enum_tag ||
3290 expr_type.
id()==ID_c_bool ||
3291 expr_type.
id()==ID_c_bit_field)
3297 out <<
"(_ bv" << value
3298 <<
" " << width <<
")";
3300 else if(expr_type.
id()==ID_fixedbv)
3306 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
3308 else if(expr_type.
id()==ID_floatbv)
3321 size_t e=floatbv_type.
get_e();
3322 size_t f=floatbv_type.
get_f()+1;
3328 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3334 out <<
"(_ NaN " << e <<
" " << f <<
")";
3339 out <<
"(_ -oo " << e <<
" " << f <<
")";
3341 out <<
"(_ +oo " << e <<
" " << f <<
")";
3351 <<
"#b" << binaryString.substr(0, 1) <<
" "
3352 <<
"#b" << binaryString.substr(1, e) <<
" "
3353 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
3361 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3364 else if(expr_type.
id()==ID_pointer)
3378 out <<
"(_ bv" << value <<
" " << width <<
")";
3381 else if(expr_type.
id()==ID_bool)
3390 else if(expr_type.
id()==ID_array)
3396 else if(expr_type.
id()==ID_rational)
3399 const bool negative =
has_prefix(value,
"-");
3404 size_t pos=value.find(
"/");
3406 if(
pos==std::string::npos)
3407 out << value <<
".0";
3410 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3411 << value.substr(
pos+1) <<
".0)";
3417 else if(expr_type.
id()==ID_integer)
3423 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3433 if(expr.
type().
id() == ID_integer)
3443 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3448 if(expr.
type().
id()==ID_unsignedbv ||
3449 expr.
type().
id()==ID_signedbv)
3451 if(expr.
type().
id()==ID_unsignedbv)
3467 std::vector<mp_integer> dynamic_objects;
3470 if(dynamic_objects.empty())
3476 out <<
"(let ((?obj ((_ extract "
3477 << pointer_width-1 <<
" "
3482 if(dynamic_objects.size()==1)
3484 out <<
"(= (_ bv" << dynamic_objects.front()
3491 for(
const auto &
object : dynamic_objects)
3492 out <<
" (= (_ bv" <<
object
3506 if(op_type.
id()==ID_unsignedbv ||
3507 op_type.
id()==ID_bv)
3510 if(expr.
id()==ID_le)
3512 else if(expr.
id()==ID_lt)
3514 else if(expr.
id()==ID_ge)
3516 else if(expr.
id()==ID_gt)
3525 else if(op_type.
id()==ID_signedbv ||
3526 op_type.
id()==ID_fixedbv)
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_floatbv)
3549 if(expr.
id()==ID_le)
3551 else if(expr.
id()==ID_lt)
3553 else if(expr.
id()==ID_ge)
3555 else if(expr.
id()==ID_gt)
3567 else if(op_type.
id()==ID_rational ||
3568 op_type.
id()==ID_integer)
3579 else if(op_type.
id() == ID_pointer)
3587 if(expr.
id() == ID_le)
3589 else if(expr.
id() == ID_lt)
3591 else if(expr.
id() == ID_ge)
3593 else if(expr.
id() == ID_gt)
3612 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3613 expr.
type().
id() == ID_real)
3618 for(
const auto &op : expr.
operands())
3627 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3628 expr.
type().
id() == ID_fixedbv)
3645 else if(expr.
type().
id() == ID_floatbv)
3652 else if(expr.
type().
id() == ID_pointer)
3658 if(p.
type().
id() != ID_pointer)
3662 p.
type().
id() == ID_pointer,
3663 "one of the operands should have pointer type");
3667 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
3670 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3674 out <<
"(let ((?pointerop ";
3680 const std::size_t offset_bits =
3684 out <<
"((_ extract " << pointer_width - 1 <<
' ' << offset_bits
3685 <<
") ?pointerop) ";
3686 out <<
"(bvadd ((_ extract " << offset_bits - 1 <<
" 0) ?pointerop) ";
3688 if(element_size >= 2)
3690 out <<
"(bvmul ((_ extract " << offset_bits - 1 <<
" 0) ";
3692 out <<
") (_ bv" << element_size <<
" " << offset_bits <<
"))";
3696 out <<
"((_ extract " << offset_bits - 1 <<
" 0) ";
3735 out <<
"roundNearestTiesToEven";
3737 out <<
"roundTowardNegative";
3739 out <<
"roundTowardPositive";
3741 out <<
"roundTowardZero";
3745 "Rounding mode should have value 0, 1, 2, or 3",
3753 out <<
"(ite (= (_ bv0 " << width <<
") ";
3755 out <<
") roundNearestTiesToEven ";
3757 out <<
"(ite (= (_ bv1 " << width <<
") ";
3759 out <<
") roundTowardNegative ";
3761 out <<
"(ite (= (_ bv2 " << width <<
") ";
3763 out <<
") roundTowardPositive ";
3766 out <<
"roundTowardZero";
3777 type.
id() == ID_floatbv ||
3778 (type.
id() == ID_complex &&
3783 if(type.
id()==ID_floatbv)
3793 else if(type.
id()==ID_complex)
3800 "type should not be one of the unsupported types",
3809 if(expr.
type().
id()==ID_integer)
3817 else if(expr.
type().
id()==ID_unsignedbv ||
3818 expr.
type().
id()==ID_signedbv ||
3819 expr.
type().
id()==ID_fixedbv)
3821 if(expr.
op0().
type().
id()==ID_pointer &&
3827 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
3829 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3832 if(element_size >= 2)
3837 "bitvector width of operand shall be equal to the bitvector width of "
3846 if(element_size >= 2)
3859 else if(expr.
type().
id()==ID_floatbv)
3866 else if(expr.
type().
id()==ID_pointer)
3870 (expr.
op1().
type().
id() == ID_unsignedbv ||
3889 expr.
type().
id() == ID_floatbv,
3890 "type of ieee floating point expression shall be floatbv");
3908 if(expr.
type().
id()==ID_unsignedbv ||
3909 expr.
type().
id()==ID_signedbv)
3911 if(expr.
type().
id()==ID_unsignedbv)
3921 else if(expr.
type().
id()==ID_fixedbv)
3926 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3931 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3933 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3939 else if(expr.
type().
id()==ID_floatbv)
3953 expr.
type().
id() == ID_floatbv,
3954 "type of ieee floating point expression shall be floatbv");
3985 "expression should have been converted to a variant with two operands");
3987 if(expr.
type().
id()==ID_unsignedbv ||
3988 expr.
type().
id()==ID_signedbv)
3999 else if(expr.
type().
id()==ID_floatbv)
4006 else if(expr.
type().
id()==ID_fixedbv)
4011 out <<
"((_ extract "
4012 << spec.
width+fraction_bits-1 <<
" "
4013 << fraction_bits <<
") ";
4017 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4021 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4027 else if(expr.
type().
id()==ID_rational ||
4028 expr.
type().
id()==ID_integer ||
4029 expr.
type().
id()==ID_real)
4033 for(
const auto &op : expr.
operands())
4048 expr.
type().
id() == ID_floatbv,
4049 "type of ieee floating point expression shall be floatbv");
4068 expr.
type().
id() == ID_floatbv,
4069 "type of ieee floating point expression shall be floatbv");
4083 "smt2_convt::convert_floatbv_rem to be implemented when not using "
4094 std::size_t s=expr.
operands().size();
4109 "with expression should have been converted to a version with three "
4114 if(expr_type.
id()==ID_array)
4138 out <<
"(let ((distance? ";
4139 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4143 if(array_width>index_width)
4145 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4151 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4161 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
4163 out <<
"distance?)) ";
4167 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
4169 out <<
") distance?)))";
4172 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
4179 const irep_idt &component_name=index.
get(ID_component_name);
4183 "struct should have accessed component");
4187 const std::string &smt_typename =
datatype_map.at(expr_type);
4189 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
4203 out <<
"(let ((?withop ";
4207 if(m.
width==struct_width)
4217 <<
"((_ extract " << (struct_width-1) <<
" "
4218 << m.
width <<
") ?withop) ";
4227 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
4232 out <<
"(concat (concat "
4233 <<
"((_ extract " << (struct_width-1) <<
" "
4236 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
4243 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
4253 if(total_width==member_width)
4260 total_width > member_width,
4261 "total width should be greater than member_width as member_width is at "
4262 "most as large as total_width and the other case has been handled "
4265 out <<
"((_ extract "
4267 <<
" " << member_width <<
") ";
4274 else if(expr_type.
id()==ID_bv ||
4275 expr_type.
id()==ID_unsignedbv ||
4276 expr_type.
id()==ID_signedbv)
4296 out <<
" (bvnot (bvshl";
4299 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
4300 out <<
" (repeat[" << value_width <<
"] bv1[1])";
4322 "with expects struct, union, or array type, but got "+
4330 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4337 if(array_op_type.
id()==ID_array)
4372 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
4376 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4380 if(array_width>index_width)
4382 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4388 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4400 false,
"index with unsupported array type: " + array_op_type.
id_string());
4407 const typet &struct_op_type = struct_op.
type();
4410 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
4415 struct_type.
has_component(name),
"struct should have accessed component");
4419 const std::string &smt_typename =
datatype_map.at(struct_type);
4421 out <<
"(" << smt_typename <<
"."
4432 if(expr.
type().
id() == ID_bool)
4438 if(expr.
type().
id() == ID_bool)
4443 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4447 width != 0,
"failed to get union member width");
4451 out <<
"((_ extract "
4461 "convert_member on an unexpected type "+struct_op_type.
id_string());
4468 if(type.
id()==ID_bool)
4474 else if(type.
id()==ID_array)
4485 std::size_t n_concat = 0;
4499 out << std::string(n_concat,
')');
4504 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4515 std::size_t n_concat = 0;
4516 for(std::size_t i=components.size(); i>1; i--)
4536 out << std::string(n_concat,
')');
4541 else if(type.
id()==ID_floatbv)
4545 "floatbv expressions should be flattened when using FPA theory");
4558 if(type.
id()==ID_bool)
4565 else if(type.
id() == ID_array)
4572 out <<
"(let ((?ufop" << nesting <<
" ";
4583 "cannot unflatten arrays of non-constant size");
4590 out <<
"((as const ";
4595 out <<
"((_ extract " << subtype_width - 1 <<
" "
4596 <<
"0) ?ufop" << nesting <<
")";
4600 std::size_t offset = subtype_width;
4601 for(
mp_integer i = 1; i < size; ++i, offset += subtype_width)
4606 out <<
"((_ extract " << offset + subtype_width - 1 <<
" " << offset
4607 <<
") ?ufop" << nesting <<
")";
4620 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4626 out <<
"(let ((?ufop" << nesting <<
" ";
4631 const std::string &smt_typename =
datatype_map.at(type);
4633 out <<
"(mk-" << smt_typename;
4640 std::size_t offset=0;
4643 for(struct_typet::componentst::const_iterator
4644 it=components.begin();
4645 it!=components.end();
4655 out <<
"((_ extract " << offset+member_width-1 <<
" "
4656 << offset <<
") ?ufop" << nesting <<
")";
4658 offset+=member_width;
4679 if(expr.
id()==ID_and && value)
4681 for(
const auto &op : expr.
operands())
4686 if(expr.
id()==ID_or && !value)
4688 for(
const auto &op : expr.
operands())
4693 if(expr.
id()==ID_not)
4703 if(expr.
id() == ID_equal && value)
4712 if(equal_expr.
lhs().
id()==ID_symbol)
4719 equal_expr.
lhs() != equal_expr.
rhs())
4724 id.type=equal_expr.
lhs().
type();
4731 out <<
"; set_to true (equal)\n";
4733 if(equal_expr.
lhs().
type().
id() == ID_mathematical_function)
4737 out <<
"(declare-fun " << smt2_identifier;
4739 auto &mathematical_function_type =
4745 for(
auto &t : mathematical_function_type.domain())
4759 out <<
"(assert (= " << smt2_identifier <<
' ';
4761 out <<
')' <<
')' <<
'\n';
4765 out <<
"(define-fun " << smt2_identifier;
4768 equal_expr.
lhs().
type().
id() != ID_array ||
4776 out <<
"(_ BitVec " << width <<
")";
4795 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4806 out << found_literal->second;
4829 exprt lowered_expr = expr;
4836 it->id() == ID_byte_extract_little_endian ||
4837 it->id() == ID_byte_extract_big_endian)
4842 it->id() == ID_byte_update_little_endian ||
4843 it->id() == ID_byte_update_big_endian)
4849 return lowered_expr;
4866 "lower_byte_operators should remove all byte operators");
4873 auto prophecy_r_or_w_ok =
4877 it.mutate() = lowered;
4878 it.next_sibling_or_parent();
4881 auto prophecy_pointer_in_range =
4885 it.mutate() = lowered;
4886 it.next_sibling_or_parent();
4895 return lowered_expr;
4906 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4911 for(
const auto &symbol : q_expr.variables())
4913 const auto identifier = symbol.get_identifier();
4915 id.type = symbol.type();
4923 for(
const auto &op : expr.
operands())
4926 if(expr.
id()==ID_symbol ||
4927 expr.
id()==ID_nondet_symbol)
4930 if(expr.
type().
id()==ID_code)
4935 if(expr.
id()==ID_symbol)
4938 identifier=
"nondet_"+
4943 if(
id.type.is_nil())
4945 id.type=expr.
type();
4950 out <<
"; find_symbols\n";
4951 out <<
"(declare-fun " << smt2_identifier;
4953 if(expr.
type().
id() == ID_mathematical_function)
4955 auto &mathematical_function_type =
4960 for(
auto &type : mathematical_function_type.domain())
4981 else if(expr.
id() == ID_array_of)
4988 const auto &array_type = array_of.type();
4992 out <<
"; the following is a substitute for lambda i. x\n";
4993 out <<
"(declare-fun " <<
id <<
" () ";
5000 out <<
"(assert (forall ((i ";
5002 out <<
")) (= (select " <<
id <<
" i) ";
5020 else if(expr.
id() == ID_array_comprehension)
5027 const auto &array_type = array_comprehension.type();
5028 const auto &array_size = array_type.size();
5032 out <<
"(declare-fun " <<
id <<
" () ";
5036 out <<
"; the following is a substitute for lambda i . x(i)\n";
5037 out <<
"; universally quantified initialization of the array\n";
5038 out <<
"(assert (forall ((";
5042 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
5049 out <<
")) (= (select " <<
id <<
" ";
5068 else if(expr.
id()==ID_array)
5075 out <<
"; the following is a substitute for an array constructor" <<
"\n";
5076 out <<
"(declare-fun " <<
id <<
" () ";
5082 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5084 out <<
"(assert (= (select " <<
id <<
" ";
5105 else if(expr.
id()==ID_string_constant)
5115 out <<
"; the following is a substitute for a string" <<
"\n";
5116 out <<
"(declare-fun " <<
id <<
" () ";
5120 for(std::size_t i=0; i<tmp.
operands().size(); i++)
5122 out <<
"(assert (= (select " <<
id <<
' ';
5126 out <<
"))" <<
"\n";
5139 out <<
"(declare-fun " <<
id <<
" () ";
5150 (expr.
id() == ID_floatbv_plus ||
5151 expr.
id() == ID_floatbv_minus ||
5152 expr.
id() == ID_floatbv_mult ||
5153 expr.
id() == ID_floatbv_div ||
5154 expr.
id() == ID_floatbv_typecast ||
5155 expr.
id() == ID_ieee_float_equal ||
5156 expr.
id() == ID_ieee_float_notequal ||
5157 ((expr.
id() == ID_lt ||
5158 expr.
id() == ID_gt ||
5159 expr.
id() == ID_le ||
5160 expr.
id() == ID_ge ||
5161 expr.
id() == ID_isnan ||
5162 expr.
id() == ID_isnormal ||
5163 expr.
id() == ID_isfinite ||
5164 expr.
id() == ID_isinf ||
5165 expr.
id() == ID_sign ||
5166 expr.
id() == ID_unary_minus ||
5167 expr.
id() == ID_typecast ||
5168 expr.
id() == ID_abs) &&
5175 if(
bvfp_set.insert(function).second)
5177 out <<
"; this is a model for " << expr.
id() <<
" : "
5180 <<
"(define-fun " << function <<
" (";
5182 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5186 out <<
"(op" << i <<
' ';
5196 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
5212 expr.
type().
id() == ID_bv)
5222 out <<
"(declare-fun " <<
id <<
" () ";
5228 out <<
"(assert (= ";
5229 out <<
"((_ to_fp " << floatbv_type.get_e() <<
" "
5230 << floatbv_type.get_f() + 1 <<
") " <<
id <<
')';
5238 else if(expr.
id() == ID_initial_state)
5240 irep_idt function =
"initial-state";
5244 out <<
"(declare-fun " << function <<
" (";
5251 else if(expr.
id() == ID_evaluate)
5257 out <<
"(declare-fun " << function <<
" (";
5267 expr.
id() == ID_state_is_cstring ||
5268 expr.
id() == ID_state_is_dynamic_object ||
5269 expr.
id() == ID_state_live_object || expr.
id() == ID_state_writeable_object)
5272 expr.
id() == ID_state_is_cstring ?
"state-is-cstring"
5273 : expr.
id() == ID_state_is_dynamic_object ?
"state-is-dynamic-object"
5274 : expr.
id() == ID_state_live_object ?
"state-live-object"
5275 :
"state-writeable-object";
5279 out <<
"(declare-fun " << function <<
" (";
5289 expr.
id() == ID_state_r_ok || expr.
id() == ID_state_w_ok ||
5290 expr.
id() == ID_state_rw_ok)
5292 irep_idt function = expr.
id() == ID_state_r_ok ?
"state-r-ok"
5293 : expr.
id() == ID_state_w_ok ?
"state-w-ok"
5298 out <<
"(declare-fun " << function <<
" (";
5309 else if(expr.
id() == ID_update_state)
5316 out <<
"(declare-fun " << function <<
" (";
5327 else if(expr.
id() == ID_enter_scope_state)
5334 out <<
"(declare-fun " << function <<
" (";
5345 else if(expr.
id() == ID_exit_scope_state)
5352 out <<
"(declare-fun " << function <<
" (";
5361 else if(expr.
id() == ID_allocate)
5367 out <<
"(declare-fun " << function <<
" (";
5376 else if(expr.
id() == ID_reallocate)
5382 out <<
"(declare-fun " << function <<
" (";
5393 else if(expr.
id() == ID_deallocate_state)
5399 out <<
"(declare-fun " << function <<
" (";
5408 else if(expr.
id() == ID_object_address)
5410 irep_idt function =
"object-address";
5414 out <<
"(declare-fun " << function <<
" (String) ";
5419 else if(expr.
id() == ID_field_address)
5425 out <<
"(declare-fun " << function <<
" (";
5434 else if(expr.
id() == ID_element_address)
5440 out <<
"(declare-fun " << function <<
" (";
5459 if(expr.
id() == ID_with)
5467 if(type.
id()==ID_array)
5481 out <<
"(_ BitVec 1)";
5487 else if(type.
id()==ID_bool)
5491 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
5501 out <<
"(_ BitVec " << width <<
")";
5504 else if(type.
id()==ID_code)
5511 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
5516 "failed to get width of union");
5518 out <<
"(_ BitVec " << width <<
")";
5520 else if(type.
id()==ID_pointer)
5525 else if(type.
id()==ID_bv ||
5526 type.
id()==ID_fixedbv ||
5527 type.
id()==ID_unsignedbv ||
5528 type.
id()==ID_signedbv ||
5529 type.
id()==ID_c_bool)
5534 else if(type.
id()==ID_c_enum)
5541 else if(type.
id()==ID_c_enum_tag)
5545 else if(type.
id()==ID_floatbv)
5550 out <<
"(_ FloatingPoint "
5551 << floatbv_type.
get_e() <<
" "
5552 << floatbv_type.
get_f() + 1 <<
")";
5557 else if(type.
id()==ID_rational ||
5560 else if(type.
id()==ID_integer)
5562 else if(type.
id()==ID_complex)
5572 out <<
"(_ BitVec " << width <<
")";
5575 else if(type.
id()==ID_c_bit_field)
5579 else if(type.
id() == ID_state)
5591 std::set<irep_idt> recstack;
5597 std::set<irep_idt> &recstack)
5599 if(type.
id()==ID_array)
5605 else if(type.
id()==ID_complex)
5612 const std::string smt_typename =
5616 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5617 <<
"(((mk-" << smt_typename;
5619 out <<
" (" << smt_typename <<
".imag ";
5623 out <<
" (" << smt_typename <<
".real ";
5630 else if(type.
id() == ID_struct)
5633 bool need_decl=
false;
5637 const std::string smt_typename =
5652 const std::string &smt_typename =
datatype_map.at(type);
5663 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5664 <<
"(((mk-" << smt_typename <<
" ";
5671 out <<
"(" << smt_typename <<
"." <<
component.get_name()
5677 out <<
"))))" <<
"\n";
5694 for(struct_union_typet::componentst::const_iterator
5695 it=components.begin();
5696 it!=components.end();
5703 out <<
"(define-fun update-" << smt_typename <<
"."
5705 <<
"((s " << smt_typename <<
") "
5708 out <<
")) " << smt_typename <<
" "
5709 <<
"(mk-" << smt_typename
5712 for(struct_union_typet::componentst::const_iterator
5713 it2=components.begin();
5714 it2!=components.end();
5721 out <<
"(" << smt_typename <<
"."
5722 << it2->get_name() <<
" s) ";
5726 out <<
"))" <<
"\n";
5732 else if(type.
id() == ID_union)
5740 else if(type.
id()==ID_code)
5744 for(
const auto ¶m : parameters)
5749 else if(type.
id()==ID_pointer)
5753 else if(type.
id() == ID_struct_tag)
5756 const irep_idt &
id = struct_tag.get_identifier();
5758 if(recstack.find(
id) == recstack.end())
5761 recstack.insert(
id);
5766 else if(type.
id() == ID_union_tag)
5769 const irep_idt &
id = union_tag.get_identifier();
5771 if(recstack.find(
id) == recstack.end())
5773 recstack.insert(
id);
5777 else if(type.
id() == ID_state)
5782 out <<
"(declare-sort state 0)\n";
5785 else if(type.
id() == ID_mathematical_function)
5787 const auto &mathematical_function_type =
5789 for(
auto &d_type : mathematical_function_type.domain())
API to expression classes for bitvectors.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_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.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
bool can_cast_expr< minus_overflow_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.
bool can_cast_expr< overflow_result_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
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.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
bitvector_typet index_type()
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
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 exprt & size() const
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Bit-wise negation of bit-vectors.
std::size_t get_width() const
const membert & get_member(const struct_typet &type, const irep_idt &member) const
The byte swap expression.
std::size_t get_bits_per_byte() const
std::vector< parametert > parameterst
const parameterst & parameters() const
struct configt::bv_encodingt bv_encoding
A constant literal expression.
const irep_idt & get_value() const
void set_value(const irep_idt &value)
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Base class for all expressions.
std::vector< exprt > operandst
bool 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.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
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 irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
exprt & where()
convenience accessor for binding().where()
literalt get_literal() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_identifier() const
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
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)
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< exprt > assumptions
void convert_plus(const plus_exprt &expr)
defined_expressionst defined_expressions
void pop() override
Currently, only implements a single stack element (no nested contexts)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
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)
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
std::size_t no_boolean_variables
smt2_identifierst smt2_identifiers
void convert_floatbv(const exprt &expr)
resultt dec_solve() override
Run the decision procedure to solve the problem.
literalt convert(const exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const irep_idt & get_name() const
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
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.
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)
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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 ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
static std::string binary(const constant_exprt &src)
bool is_true(const literalt &l)
literalt const_literal(bool value)
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_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 element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt simplify_expr(exprt src, const namespacet &ns)
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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
#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 struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
std::size_t unsafe_string2size_t(const std::string &str, int base)
const string_constantt & to_string_constant(const exprt &expr)