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 <<
" ";
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)
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;
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)
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=" +
799 std::to_string(max_objects) +
800 " (with n=" + std::to_string(object_bits) +
"); " +
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");
850 struct_op_type.
id() == ID_struct_tag
867 else if(expr.
id()==ID_if)
882 "operand of address of expression should not be of kind " +
890 if(node.
id() == ID_exists || node.
id() == ID_forall)
906 else if(expr.
id()==ID_literal)
918 out <<
"; convert\n";
919 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
929 out <<
"(declare-fun ";
931 out <<
" () Bool)\n";
932 out <<
"(assert (= ";
944 out <<
"(define-fun " << identifier <<
" () Bool ";
972 const auto identifier =
994 for(
auto &assumption : _assumptions)
1005 if(identifier.empty())
1008 if(isdigit(identifier[0]))
1030 std::string result =
"|";
1032 for(
auto ch : identifier)
1040 result+=std::to_string(ch);
1057 if(type.
id()==ID_floatbv)
1060 return "f"+std::to_string(spec.
width())+
"_"+std::to_string(spec.
f);
1062 else if(type.
id() == ID_bv)
1066 else if(type.
id()==ID_unsignedbv)
1070 else if(type.
id()==ID_c_bool)
1074 else if(type.
id()==ID_signedbv)
1078 else if(type.
id()==ID_bool)
1082 else if(type.
id()==ID_c_enum_tag)
1086 else if(type.
id() == ID_pointer)
1090 else if(type.
id() == ID_struct_tag)
1097 else if(type.
id() == ID_union_tag)
1101 else if(type.
id() == ID_array)
1122 if(expr.
id()==ID_symbol)
1129 if(expr.
id()==ID_smt2_symbol)
1137 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
1143 for(
const auto &op : expr.
operands())
1171 converter_result->second(expr);
1176 if(expr.
id()==ID_symbol)
1182 else if(expr.
id()==ID_nondet_symbol)
1185 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1188 else if(expr.
id()==ID_smt2_symbol)
1194 else if(expr.
id()==ID_typecast)
1198 else if(expr.
id()==ID_floatbv_typecast)
1202 else if(expr.
id()==ID_struct)
1206 else if(expr.
id()==ID_union)
1214 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
1218 "concatenation over a single operand should have matching types",
1223 else if(expr.
id()==ID_concatenation ||
1224 expr.
id()==ID_bitand ||
1225 expr.
id()==ID_bitor ||
1226 expr.
id()==ID_bitxor ||
1227 expr.
id()==ID_bitnand ||
1228 expr.
id()==ID_bitnor)
1232 "given expression should have at least two operands",
1237 if(expr.
id()==ID_concatenation)
1239 else if(expr.
id()==ID_bitand)
1241 else if(expr.
id()==ID_bitor)
1243 else if(expr.
id()==ID_bitxor)
1245 else if(expr.
id()==ID_bitnand)
1247 else if(expr.
id()==ID_bitnor)
1250 for(
const auto &op : expr.
operands())
1258 else if(expr.
id()==ID_bitnot)
1266 else if(expr.
id()==ID_unary_minus)
1271 unary_minus_expr.
type().
id() == ID_rational ||
1272 unary_minus_expr.
type().
id() == ID_integer ||
1273 unary_minus_expr.
type().
id() == ID_real)
1279 else if(unary_minus_expr.
type().
id() == ID_floatbv)
1298 else if(expr.
id()==ID_unary_plus)
1303 else if(expr.
id()==ID_sign)
1309 if(op_type.
id()==ID_floatbv)
1313 out <<
"(fp.isNegative ";
1320 else if(op_type.
id()==ID_signedbv)
1326 out <<
" (_ bv0 " << op_width <<
"))";
1331 "sign should not be applied to unsupported type",
1334 else if(expr.
id()==ID_if)
1346 else if(expr.
id()==ID_and ||
1352 "logical and, or, and xor expressions should have Boolean type");
1355 "logical and, or, and xor expressions should have at least two operands");
1357 out <<
"(" << expr.
id();
1358 for(
const auto &op : expr.
operands())
1365 else if(expr.
id()==ID_implies)
1370 implies_expr.
is_boolean(),
"implies expression should have Boolean type");
1378 else if(expr.
id()==ID_not)
1383 not_expr.
is_boolean(),
"not expression should have Boolean type");
1389 else if(expr.
id() == ID_equal)
1395 "operands of equal expression shall have same type");
1410 else if(expr.
id() == ID_notequal)
1416 "operands of not equal expression shall have same type");
1424 else if(expr.
id()==ID_ieee_float_equal ||
1425 expr.
id()==ID_ieee_float_notequal)
1432 rel_expr.lhs().type() == rel_expr.rhs().type(),
1433 "operands of float equal and not equal expressions shall have same type");
1438 if(rel_expr.id() == ID_ieee_float_notequal)
1447 if(rel_expr.id() == ID_ieee_float_notequal)
1453 else if(expr.
id()==ID_le ||
1460 else if(expr.
id()==ID_plus)
1464 else if(expr.
id()==ID_floatbv_plus)
1468 else if(expr.
id()==ID_minus)
1472 else if(expr.
id()==ID_floatbv_minus)
1476 else if(expr.
id()==ID_div)
1480 else if(expr.
id()==ID_floatbv_div)
1484 else if(expr.
id()==ID_mod)
1488 else if(expr.
id() == ID_euclidean_mod)
1492 else if(expr.
id()==ID_mult)
1496 else if(expr.
id()==ID_floatbv_mult)
1500 else if(expr.
id() == ID_floatbv_rem)
1504 else if(expr.
id()==ID_address_of)
1510 else if(expr.
id() == ID_array_of)
1515 array_of_expr.type().id() == ID_array,
1516 "array of expression shall have array type");
1520 out <<
"((as const ";
1528 defined_expressionst::const_iterator it =
1534 else if(expr.
id() == ID_array_comprehension)
1539 array_comprehension.type().id() == ID_array,
1540 "array_comprehension expression shall have array type");
1544 out <<
"(lambda ((";
1547 convert_type(array_comprehension.type().size().type());
1559 else if(expr.
id()==ID_index)
1563 else if(expr.
id()==ID_ashr ||
1564 expr.
id()==ID_lshr ||
1570 if(type.
id()==ID_unsignedbv ||
1571 type.
id()==ID_signedbv ||
1574 if(shift_expr.
id() == ID_ashr)
1576 else if(shift_expr.
id() == ID_lshr)
1578 else if(shift_expr.
id() == ID_shl)
1608 if(width_op0==width_op1)
1610 else if(width_op0>width_op1)
1612 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1618 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1625 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1632 "unsupported type for " + shift_expr.
id_string() +
": " +
1635 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1641 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1646 if(shift_expr.
id() == ID_rol)
1647 out <<
"((_ rotate_left";
1648 else if(shift_expr.
id() == ID_ror)
1649 out <<
"((_ rotate_right";
1657 if(distance_int_op.has_value())
1659 out << distance_int_op.value();
1663 "distance type for " + shift_expr.
id_string() +
"must be constant");
1672 "unsupported type for " + shift_expr.
id_string() +
": " +
1675 else if(expr.
id() == ID_named_term)
1679 convert(named_term_expr.value());
1683 else if(expr.
id()==ID_with)
1687 else if(expr.
id()==ID_update)
1691 else if(expr.
id() == ID_update_bit)
1695 else if(expr.
id() == ID_update_bits)
1699 else if(expr.
id() == ID_object_address)
1701 out <<
"(object-address ";
1706 else if(expr.
id() == ID_element_address)
1712 auto element_size_expr_opt =
1722 *element_size_expr_opt, element_address_expr.index().type()));
1725 else if(expr.
id() == ID_field_address)
1734 else if(expr.
id()==ID_member)
1738 else if(expr.
id()==ID_pointer_offset)
1743 op.type().id() == ID_pointer,
1744 "operand of pointer offset expression shall be of pointer type");
1746 std::size_t offset_bits =
1751 if(offset_bits>result_width)
1752 offset_bits=result_width;
1755 if(result_width>offset_bits)
1756 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1758 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1762 if(result_width>offset_bits)
1765 else if(expr.
id()==ID_pointer_object)
1770 op.type().id() == ID_pointer,
1771 "pointer object expressions should be of pointer type");
1777 out <<
"((_ zero_extend " << ext <<
") ";
1779 out <<
"((_ extract "
1780 << pointer_width-1 <<
" "
1788 else if(expr.
id() == ID_is_dynamic_object)
1792 else if(expr.
id() == ID_is_invalid_pointer)
1796 out <<
"(= ((_ extract "
1797 << pointer_width-1 <<
" "
1803 else if(expr.
id()==ID_string_constant)
1809 else if(expr.
id()==ID_extractbit)
1818 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1824 out <<
"(= ((_ extract 0 0) ";
1834 else if(expr.
id()==ID_extractbits)
1844 out <<
"((_ extract " << (width + index_i - 1) <<
" " << index_i <<
") ";
1851 out <<
"(= ((_ extract 0 0) ";
1860 SMT2_TODO(
"smt2: extractbits with non-constant index");
1863 else if(expr.
id()==ID_replication)
1869 out <<
"((_ repeat " << times <<
") ";
1873 else if(expr.
id()==ID_byte_extract_little_endian ||
1874 expr.
id()==ID_byte_extract_big_endian)
1877 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1879 else if(expr.
id()==ID_byte_update_little_endian ||
1880 expr.
id()==ID_byte_update_big_endian)
1883 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1885 else if(expr.
id()==ID_abs)
1891 if(type.
id()==ID_signedbv)
1895 out <<
"(ite (bvslt ";
1897 out <<
" (_ bv0 " << result_width <<
")) ";
1904 else if(type.
id()==ID_fixedbv)
1908 out <<
"(ite (bvslt ";
1910 out <<
" (_ bv0 " << result_width <<
")) ";
1917 else if(type.
id()==ID_floatbv)
1931 else if(expr.
id()==ID_isnan)
1937 if(op_type.
id()==ID_fixedbv)
1939 else if(op_type.
id()==ID_floatbv)
1943 out <<
"(fp.isNaN ";
1953 else if(expr.
id()==ID_isfinite)
1959 if(op_type.
id()==ID_fixedbv)
1961 else if(op_type.
id()==ID_floatbv)
1967 out <<
"(not (fp.isNaN ";
1971 out <<
"(not (fp.isInfinite ";
1983 else if(expr.
id()==ID_isinf)
1989 if(op_type.
id()==ID_fixedbv)
1991 else if(op_type.
id()==ID_floatbv)
1995 out <<
"(fp.isInfinite ";
2005 else if(expr.
id()==ID_isnormal)
2011 if(op_type.
id()==ID_fixedbv)
2013 else if(op_type.
id()==ID_floatbv)
2017 out <<
"(fp.isNormal ";
2030 expr.
id() == ID_overflow_result_plus ||
2031 expr.
id() == ID_overflow_result_minus)
2040 "overflow plus and overflow minus expressions shall be of Boolean type");
2043 expr.
id() == ID_overflow_result_minus;
2044 const typet &op_type = op0.type();
2047 if(op_type.
id()==ID_signedbv)
2050 out <<
"(let ((?sum (";
2051 out << (subtract?
"bvsub":
"bvadd");
2052 out <<
" ((_ sign_extend 1) ";
2055 out <<
" ((_ sign_extend 1) ";
2065 out <<
"(mk-" << smt_typename;
2070 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2075 "((_ extract " << width <<
" " << width <<
") ?sum) "
2076 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
2086 else if(op_type.
id()==ID_unsignedbv ||
2087 op_type.
id()==ID_pointer)
2090 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2091 out <<
" ((_ zero_extend 1) ";
2094 out <<
" ((_ zero_extend 1) ";
2106 out <<
"(mk-" << smt_typename;
2107 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2111 out <<
"((_ extract " << width <<
" " << width <<
") ?sum)";
2122 "overflow check should not be performed on unsupported type",
2127 expr.
id() == ID_overflow_result_mult)
2136 "overflow mult expression shall be of Boolean type");
2141 const typet &op_type = op0.type();
2144 if(op_type.
id()==ID_signedbv)
2146 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
2148 out <<
") ((_ sign_extend " << width <<
") ";
2158 out <<
"(mk-" << smt_typename;
2163 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2167 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
2169 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width - 1) <<
" "
2170 << width * 2 <<
"))))";
2179 else if(op_type.
id()==ID_unsignedbv)
2181 out <<
"(let ((prod (bvmul ((_ zero_extend " << width <<
") ";
2183 out <<
") ((_ zero_extend " << width <<
") ";
2193 out <<
"(mk-" << smt_typename;
2198 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2202 out <<
"(bvuge prod (_ bv" <<
power(2, width) <<
" " << width * 2 <<
"))";
2214 "overflow check should not be performed on unsupported type",
2217 else if(expr.
id() == ID_saturating_plus || expr.
id() == ID_saturating_minus)
2219 const bool subtract = expr.
id() == ID_saturating_minus;
2220 const auto &op_type = expr.
type();
2224 if(op_type.id() == ID_signedbv)
2229 out <<
"(let ((?sum (";
2230 out << (subtract ?
"bvsub" :
"bvadd");
2231 out <<
" ((_ sign_extend 1) ";
2234 out <<
" ((_ sign_extend 1) ";
2241 << width <<
" " << width
2244 << (width - 1) <<
" " << (width - 1) <<
") ?sum)";
2248 out <<
"((_ extract " << width - 1 <<
" 0) ?sum) ";
2251 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2258 else if(op_type.id() == ID_unsignedbv)
2263 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2264 out <<
" ((_ zero_extend 1) ";
2267 out <<
" ((_ zero_extend 1) ";
2272 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2275 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2289 "saturating_plus/minus on unsupported type",
2290 op_type.id_string());
2292 else if(expr.
id()==ID_array)
2298 else if(expr.
id()==ID_literal)
2302 else if(expr.
id()==ID_forall ||
2303 expr.
id()==ID_exists)
2309 throw "MathSAT does not support quantifiers";
2311 if(quantifier_expr.
id() == ID_forall)
2313 else if(quantifier_expr.
id() == ID_exists)
2318 for(
const auto &bound : quantifier_expr.
variables())
2341 else if(expr.
id()==ID_let)
2344 const auto &variables = let_expr.
variables();
2345 const auto &values = let_expr.
values();
2350 for(
auto &binding :
make_range(variables).zip(values))
2369 else if(expr.
id()==ID_constraint_select_one)
2372 "smt2_convt::convert_expr: '" + expr.
id_string() +
2373 "' is not yet supported");
2375 else if(expr.
id() == ID_bswap)
2381 "operand of byte swap expression shall have same type as the expression");
2384 out <<
"(let ((bswap_op ";
2389 bswap_expr.
type().
id() == ID_signedbv ||
2390 bswap_expr.
type().
id() == ID_unsignedbv)
2392 const std::size_t width =
2399 width % bits_per_byte == 0,
2400 "bit width indicated by type of bswap expression should be a multiple "
2401 "of the number of bits per byte");
2403 const std::size_t bytes = width / bits_per_byte;
2412 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2416 out <<
"(bswap_byte_" <<
byte <<
' ';
2417 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2418 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2427 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2428 out <<
" bswap_byte_" <<
byte;
2439 else if(expr.
id() == ID_popcount)
2443 else if(expr.
id() == ID_count_leading_zeros)
2447 else if(expr.
id() == ID_count_trailing_zeros)
2451 else if(expr.
id() == ID_find_first_set)
2455 else if(expr.
id() == ID_bitreverse)
2459 else if(expr.
id() == ID_function_application)
2463 if(function_application_expr.arguments().empty())
2471 for(
auto &op : function_application_expr.arguments())
2482 "smt2_convt::convert_expr should not be applied to unsupported type",
2491 if(dest_type.
id()==ID_c_enum_tag)
2495 if(src_type.
id()==ID_c_enum_tag)
2498 if(dest_type.
id()==ID_bool)
2501 if(src_type.
id()==ID_signedbv ||
2502 src_type.
id()==ID_unsignedbv ||
2503 src_type.
id()==ID_c_bool ||
2504 src_type.
id()==ID_fixedbv ||
2505 src_type.
id()==ID_pointer ||
2506 src_type.
id()==ID_integer)
2514 else if(src_type.
id()==ID_floatbv)
2518 out <<
"(not (fp.isZero ";
2530 else if(dest_type.
id()==ID_c_bool)
2539 out <<
" (_ bv1 " << to_width <<
")";
2540 out <<
" (_ bv0 " << to_width <<
")";
2543 else if(dest_type.
id()==ID_signedbv ||
2544 dest_type.
id()==ID_unsignedbv ||
2545 dest_type.
id()==ID_c_enum ||
2546 dest_type.
id()==ID_bv)
2550 if(src_type.
id()==ID_signedbv ||
2551 src_type.
id()==ID_unsignedbv ||
2552 src_type.
id()==ID_c_bool ||
2553 src_type.
id()==ID_c_enum ||
2554 src_type.
id()==ID_bv)
2558 if(from_width==to_width)
2560 else if(from_width<to_width)
2562 if(src_type.
id()==ID_signedbv)
2563 out <<
"((_ sign_extend ";
2565 out <<
"((_ zero_extend ";
2567 out << (to_width-from_width)
2574 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2579 else if(src_type.
id()==ID_fixedbv)
2583 std::size_t from_width=fixedbv_type.
get_width();
2590 out <<
"(let ((?tcop ";
2596 if(to_width>from_integer_bits)
2598 out <<
"((_ sign_extend "
2599 << (to_width-from_integer_bits) <<
") ";
2600 out <<
"((_ extract " << (from_width-1) <<
" "
2601 << from_fraction_bits <<
") ";
2607 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2608 <<
" " << from_fraction_bits <<
") ";
2613 out <<
" (ite (and ";
2616 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2617 "(_ bv0 " << from_fraction_bits <<
")))";
2620 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2625 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2629 else if(src_type.
id()==ID_floatbv)
2631 if(dest_type.
id()==ID_bv)
2637 defined_expressionst::const_iterator it =
2648 else if(dest_type.
id()==ID_signedbv)
2652 "typecast unexpected "+src_type.
id_string()+
" -> "+
2655 else if(dest_type.
id()==ID_unsignedbv)
2659 "typecast unexpected "+src_type.
id_string()+
" -> "+
2663 else if(src_type.
id()==ID_bool)
2668 if(dest_type.
id()==ID_fixedbv)
2671 out <<
" (concat (_ bv1 "
2674 "(_ bv0 " << spec.
width <<
")";
2678 out <<
" (_ bv1 " << to_width <<
")";
2679 out <<
" (_ bv0 " << to_width <<
")";
2684 else if(src_type.
id()==ID_pointer)
2688 if(from_width<to_width)
2690 out <<
"((_ sign_extend ";
2691 out << (to_width-from_width)
2698 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2703 else if(src_type.
id()==ID_integer)
2709 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2712 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2715 src_type.
id() == ID_struct ||
2716 src_type.
id() == ID_struct_tag)
2722 "bit vector with of source and destination type shall be equal");
2729 "bit vector with of source and destination type shall be equal");
2734 src_type.
id() == ID_union ||
2735 src_type.
id() == ID_union_tag)
2739 "bit vector with of source and destination type shall be equal");
2742 else if(src_type.
id()==ID_c_bit_field)
2746 if(from_width==to_width)
2757 std::ostringstream e_str;
2758 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2759 <<
" src == " <<
format(src);
2763 else if(dest_type.
id()==ID_fixedbv)
2769 if(src_type.
id()==ID_unsignedbv ||
2770 src_type.
id()==ID_signedbv ||
2771 src_type.
id()==ID_c_enum)
2778 if(from_width==to_integer_bits)
2780 else if(from_width>to_integer_bits)
2783 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2791 from_width < to_integer_bits,
2792 "from_width should be smaller than to_integer_bits as other case "
2793 "have been handled above");
2794 if(dest_type.
id()==ID_unsignedbv)
2796 out <<
"(_ zero_extend "
2797 << (to_integer_bits-from_width) <<
") ";
2803 out <<
"((_ sign_extend "
2804 << (to_integer_bits-from_width) <<
") ";
2810 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2813 else if(src_type.
id()==ID_bool)
2815 out <<
"(concat (concat"
2816 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2822 else if(src_type.
id()==ID_fixedbv)
2827 std::size_t from_width=from_fixedbv_type.
get_width();
2829 out <<
"(let ((?tcop ";
2835 if(to_integer_bits<=from_integer_bits)
2837 out <<
"((_ extract "
2838 << (from_fraction_bits+to_integer_bits-1) <<
" "
2839 << from_fraction_bits
2845 to_integer_bits > from_integer_bits,
2846 "to_integer_bits should be greater than from_integer_bits as the"
2847 "other case has been handled above");
2848 out <<
"((_ sign_extend "
2849 << (to_integer_bits-from_integer_bits)
2851 << (from_width-1) <<
" "
2852 << from_fraction_bits
2858 if(to_fraction_bits<=from_fraction_bits)
2860 out <<
"((_ extract "
2861 << (from_fraction_bits-1) <<
" "
2862 << (from_fraction_bits-to_fraction_bits)
2868 to_fraction_bits > from_fraction_bits,
2869 "to_fraction_bits should be greater than from_fraction_bits as the"
2870 "other case has been handled above");
2871 out <<
"(concat ((_ extract "
2872 << (from_fraction_bits-1) <<
" 0) ";
2875 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
2884 else if(dest_type.
id()==ID_pointer)
2888 if(src_type.
id()==ID_pointer)
2894 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
2895 src_type.
id() == ID_bv)
2901 if(from_width==to_width)
2903 else if(from_width<to_width)
2905 out <<
"((_ sign_extend "
2906 << (to_width-from_width)
2913 out <<
"((_ extract " << to_width <<
" 0) ";
2921 else if(dest_type.
id()==ID_range)
2925 else if(dest_type.
id()==ID_floatbv)
2934 if(src_type.
id()==ID_bool)
2949 a.
build(significand, exponent);
2957 a.
build(significand, exponent);
2963 else if(src_type.
id()==ID_c_bool)
2969 else if(src_type.
id() == ID_bv)
2978 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
2979 << dest_floatbv_type.get_f() + 1 <<
") ";
2989 else if(dest_type.
id()==ID_integer)
2991 if(src_type.
id()==ID_bool)
3000 else if(dest_type.
id()==ID_c_bit_field)
3005 if(from_width==to_width)
3026 if(dest_type.
id()==ID_floatbv)
3028 if(src_type.
id()==ID_floatbv)
3055 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3056 << dst.
get_f() + 1 <<
") ";
3065 else if(src_type.
id()==ID_unsignedbv)
3086 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
3087 << dst.
get_f() + 1 <<
") ";
3096 else if(src_type.
id()==ID_signedbv)
3104 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3105 << dst.
get_f() + 1 <<
") ";
3114 else if(src_type.
id()==ID_c_enum_tag)
3128 else if(dest_type.
id()==ID_signedbv)
3133 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
3142 else if(dest_type.
id()==ID_unsignedbv)
3147 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
3166 expr.
type().
id() == ID_struct_tag
3174 components.size() == expr.
operands().size(),
3175 "number of struct components as indicated by the struct type shall be equal"
3176 "to the number of operands of the struct expression");
3178 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
3182 const std::string &smt_typename =
datatype_map.at(struct_type);
3185 out <<
"(mk-" << smt_typename;
3188 for(struct_typet::componentst::const_iterator
3189 it=components.begin();
3190 it!=components.end();
3203 auto convert_operand = [
this](
const exprt &op) {
3207 else if(op.type().id() == ID_bool)
3214 std::size_t n_concat = 0;
3215 for(std::size_t i = components.size(); i > 1; i--)
3225 convert_operand(expr.
operands()[i - 1]);
3231 convert_operand(expr.
op0());
3233 out << std::string(n_concat,
')');
3241 const auto &size_expr = array_type.
size();
3247 out <<
"(let ((?far ";
3255 out <<
"(select ?far ";
3277 if(total_width==member_width)
3285 total_width > member_width,
3286 "total_width should be greater than member_width as member_width can be"
3287 "at most as large as total_width and the other case has been handled "
3291 << (total_width-member_width) <<
") ";
3301 if(expr_type.
id()==ID_unsignedbv ||
3302 expr_type.
id()==ID_signedbv ||
3303 expr_type.
id()==ID_bv ||
3304 expr_type.
id()==ID_c_enum ||
3305 expr_type.
id()==ID_c_enum_tag ||
3306 expr_type.
id()==ID_c_bool ||
3307 expr_type.
id()==ID_c_bit_field)
3313 out <<
"(_ bv" << value
3314 <<
" " << width <<
")";
3316 else if(expr_type.
id()==ID_fixedbv)
3322 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
3324 else if(expr_type.
id()==ID_floatbv)
3337 size_t e=floatbv_type.
get_e();
3338 size_t f=floatbv_type.
get_f()+1;
3344 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3350 out <<
"(_ NaN " << e <<
" " << f <<
")";
3355 out <<
"(_ -oo " << e <<
" " << f <<
")";
3357 out <<
"(_ +oo " << e <<
" " << f <<
")";
3367 <<
"#b" << binaryString.substr(0, 1) <<
" "
3368 <<
"#b" << binaryString.substr(1, e) <<
" "
3369 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
3377 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3380 else if(expr_type.
id()==ID_pointer)
3394 out <<
"(_ bv" << value <<
" " << width <<
")";
3397 else if(expr_type.
id()==ID_bool)
3406 else if(expr_type.
id()==ID_array)
3412 else if(expr_type.
id()==ID_rational)
3415 const bool negative =
has_prefix(value,
"-");
3420 size_t pos=value.find(
"/");
3422 if(
pos==std::string::npos)
3423 out << value <<
".0";
3426 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3427 << value.substr(
pos+1) <<
".0)";
3433 else if(expr_type.
id()==ID_integer)
3439 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3449 if(expr.
type().
id() == ID_integer)
3459 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3464 if(expr.
type().
id()==ID_unsignedbv ||
3465 expr.
type().
id()==ID_signedbv)
3467 if(expr.
type().
id()==ID_unsignedbv)
3483 std::vector<mp_integer> dynamic_objects;
3486 if(dynamic_objects.empty())
3492 out <<
"(let ((?obj ((_ extract "
3493 << pointer_width-1 <<
" "
3498 if(dynamic_objects.size()==1)
3500 out <<
"(= (_ bv" << dynamic_objects.front()
3507 for(
const auto &
object : dynamic_objects)
3508 out <<
" (= (_ bv" <<
object
3522 if(op_type.
id()==ID_unsignedbv ||
3523 op_type.
id()==ID_bv)
3526 if(expr.
id()==ID_le)
3528 else if(expr.
id()==ID_lt)
3530 else if(expr.
id()==ID_ge)
3532 else if(expr.
id()==ID_gt)
3541 else if(op_type.
id()==ID_signedbv ||
3542 op_type.
id()==ID_fixedbv)
3545 if(expr.
id()==ID_le)
3547 else if(expr.
id()==ID_lt)
3549 else if(expr.
id()==ID_ge)
3551 else if(expr.
id()==ID_gt)
3560 else if(op_type.
id()==ID_floatbv)
3565 if(expr.
id()==ID_le)
3567 else if(expr.
id()==ID_lt)
3569 else if(expr.
id()==ID_ge)
3571 else if(expr.
id()==ID_gt)
3583 else if(op_type.
id()==ID_rational ||
3584 op_type.
id()==ID_integer)
3595 else if(op_type.
id() == ID_pointer)
3603 if(expr.
id() == ID_le)
3605 else if(expr.
id() == ID_lt)
3607 else if(expr.
id() == ID_ge)
3609 else if(expr.
id() == ID_gt)
3628 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3629 expr.
type().
id() == ID_real)
3634 for(
const auto &op : expr.
operands())
3643 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3644 expr.
type().
id() == ID_fixedbv)
3661 else if(expr.
type().
id() == ID_floatbv)
3668 else if(expr.
type().
id() == ID_pointer)
3674 if(p.
type().
id() != ID_pointer)
3678 p.
type().
id() == ID_pointer,
3679 "one of the operands should have pointer type");
3683 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
3686 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3690 out <<
"(let ((?pointerop ";
3696 const std::size_t offset_bits =
3700 out <<
"((_ extract " << pointer_width - 1 <<
' ' << offset_bits
3701 <<
") ?pointerop) ";
3702 out <<
"(bvadd ((_ extract " << offset_bits - 1 <<
" 0) ?pointerop) ";
3704 if(element_size >= 2)
3706 out <<
"(bvmul ((_ extract " << offset_bits - 1 <<
" 0) ";
3708 out <<
") (_ bv" << element_size <<
" " << offset_bits <<
"))";
3712 out <<
"((_ extract " << offset_bits - 1 <<
" 0) ";
3751 out <<
"roundNearestTiesToEven";
3753 out <<
"roundTowardNegative";
3755 out <<
"roundTowardPositive";
3757 out <<
"roundTowardZero";
3761 "Rounding mode should have value 0, 1, 2, or 3",
3769 out <<
"(ite (= (_ bv0 " << width <<
") ";
3771 out <<
") roundNearestTiesToEven ";
3773 out <<
"(ite (= (_ bv1 " << width <<
") ";
3775 out <<
") roundTowardNegative ";
3777 out <<
"(ite (= (_ bv2 " << width <<
") ";
3779 out <<
") roundTowardPositive ";
3782 out <<
"roundTowardZero";
3793 type.
id() == ID_floatbv ||
3794 (type.
id() == ID_complex &&
3799 if(type.
id()==ID_floatbv)
3809 else if(type.
id()==ID_complex)
3816 "type should not be one of the unsupported types",
3825 if(expr.
type().
id()==ID_integer)
3833 else if(expr.
type().
id()==ID_unsignedbv ||
3834 expr.
type().
id()==ID_signedbv ||
3835 expr.
type().
id()==ID_fixedbv)
3837 if(expr.
op0().
type().
id()==ID_pointer &&
3843 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
3845 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3848 if(element_size >= 2)
3853 "bitvector width of operand shall be equal to the bitvector width of "
3862 if(element_size >= 2)
3875 else if(expr.
type().
id()==ID_floatbv)
3882 else if(expr.
type().
id()==ID_pointer)
3886 (expr.
op1().
type().
id() == ID_unsignedbv ||
3905 expr.
type().
id() == ID_floatbv,
3906 "type of ieee floating point expression shall be floatbv");
3924 if(expr.
type().
id()==ID_unsignedbv ||
3925 expr.
type().
id()==ID_signedbv)
3927 if(expr.
type().
id()==ID_unsignedbv)
3937 else if(expr.
type().
id()==ID_fixedbv)
3942 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3947 out <<
" (_ bv0 " << fraction_bits <<
")) ";
3949 out <<
"((_ sign_extend " << fraction_bits <<
") ";
3955 else if(expr.
type().
id()==ID_floatbv)
3969 expr.
type().
id() == ID_floatbv,
3970 "type of ieee floating point expression shall be floatbv");
4001 "expression should have been converted to a variant with two operands");
4003 if(expr.
type().
id()==ID_unsignedbv ||
4004 expr.
type().
id()==ID_signedbv)
4015 else if(expr.
type().
id()==ID_floatbv)
4022 else if(expr.
type().
id()==ID_fixedbv)
4027 out <<
"((_ extract "
4028 << spec.
width+fraction_bits-1 <<
" "
4029 << fraction_bits <<
") ";
4033 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4037 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4043 else if(expr.
type().
id()==ID_rational ||
4044 expr.
type().
id()==ID_integer ||
4045 expr.
type().
id()==ID_real)
4049 for(
const auto &op : expr.
operands())
4064 expr.
type().
id() == ID_floatbv,
4065 "type of ieee floating point expression shall be floatbv");
4084 expr.
type().
id() == ID_floatbv,
4085 "type of ieee floating point expression shall be floatbv");
4099 "smt2_convt::convert_floatbv_rem to be implemented when not using "
4110 std::size_t s=expr.
operands().size();
4125 "with expression should have been converted to a version with three "
4130 if(expr_type.
id()==ID_array)
4154 out <<
"(let ((distance? ";
4155 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4159 if(array_width>index_width)
4161 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4167 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4177 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
4179 out <<
"distance?)) ";
4183 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
4185 out <<
") distance?)))";
4188 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
4191 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)
4270 if(total_width==member_width)
4277 total_width > member_width,
4278 "total width should be greater than member_width as member_width is at "
4279 "most as large as total_width and the other case has been handled "
4282 out <<
"((_ extract "
4284 <<
" " << member_width <<
") ";
4291 else if(expr_type.
id()==ID_bv ||
4292 expr_type.
id()==ID_unsignedbv ||
4293 expr_type.
id()==ID_signedbv)
4308 "with expects struct, union, or array type, but got "+
4316 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4333 if(array_op_type.
id()==ID_array)
4368 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
4372 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4376 if(array_width>index_width)
4378 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4384 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4396 false,
"index with unsupported array type: " + array_op_type.
id_string());
4403 const typet &struct_op_type = struct_op.
type();
4406 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
4409 struct_op_type.
id() == ID_struct_tag
4414 struct_type.
has_component(name),
"struct should have accessed component");
4418 const std::string &smt_typename =
datatype_map.at(struct_type);
4420 out <<
"(" << smt_typename <<
"."
4431 if(expr.
type().
id() == ID_bool)
4437 if(expr.
type().
id() == ID_bool)
4442 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4446 width != 0,
"failed to get union member width");
4452 out <<
"((_ extract " << (width - 1) <<
" 0) ";
4460 out <<
"((_ extract " << (width - 1) <<
" 0) ";
4467 "convert_member on an unexpected type "+struct_op_type.
id_string());
4474 if(type.
id()==ID_bool)
4480 else if(type.
id()==ID_array)
4491 std::size_t n_concat = 0;
4505 out << std::string(n_concat,
')');
4510 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4523 std::size_t n_concat = 0;
4524 for(std::size_t i=components.size(); i>1; i--)
4544 out << std::string(n_concat,
')');
4549 else if(type.
id()==ID_floatbv)
4553 "floatbv expressions should be flattened when using FPA theory");
4566 if(type.
id()==ID_bool)
4573 else if(type.
id() == ID_array)
4578 out <<
"(let ((?ufop" << nesting <<
" ";
4589 "cannot unflatten arrays of non-constant size");
4596 out <<
"((as const ";
4601 out <<
"((_ extract " << subtype_width - 1 <<
" "
4602 <<
"0) ?ufop" << nesting <<
")";
4606 std::size_t offset = subtype_width;
4607 for(
mp_integer i = 1; i < size; ++i, offset += subtype_width)
4612 out <<
"((_ extract " << offset + subtype_width - 1 <<
" " << offset
4613 <<
") ?ufop" << nesting <<
")";
4621 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4627 out <<
"(let ((?ufop" << nesting <<
" ";
4632 const std::string &smt_typename =
datatype_map.at(type);
4634 out <<
"(mk-" << smt_typename;
4643 std::size_t offset=0;
4646 for(struct_typet::componentst::const_iterator
4647 it=components.begin();
4648 it!=components.end();
4658 out <<
"((_ extract " << offset+member_width-1 <<
" "
4659 << offset <<
") ?ufop" << nesting <<
")";
4661 offset+=member_width;
4682 if(expr.
id()==ID_and && value)
4684 for(
const auto &op : expr.
operands())
4689 if(expr.
id()==ID_or && !value)
4691 for(
const auto &op : expr.
operands())
4696 if(expr.
id()==ID_not)
4706 if(expr.
id() == ID_equal && value)
4715 if(equal_expr.
lhs().
id()==ID_symbol)
4722 equal_expr.
lhs() != equal_expr.
rhs())
4734 out <<
"; set_to true (equal)\n";
4736 if(equal_expr.
lhs().
type().
id() == ID_mathematical_function)
4740 out <<
"(declare-fun " << smt2_identifier;
4742 auto &mathematical_function_type =
4748 for(
auto &t : mathematical_function_type.domain())
4762 out <<
"(assert (= " << smt2_identifier <<
' ';
4764 out <<
')' <<
')' <<
'\n';
4768 out <<
"(define-fun " << smt2_identifier;
4773 equal_expr.
lhs().
type().
id() != ID_array ||
4801 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4812 out << found_literal->second;
4835 exprt lowered_expr = expr;
4842 it->id() == ID_byte_extract_little_endian ||
4843 it->id() == ID_byte_extract_big_endian)
4848 it->id() == ID_byte_update_little_endian ||
4849 it->id() == ID_byte_update_big_endian)
4855 return lowered_expr;
4872 "lower_byte_operators should remove all byte operators");
4879 auto prophecy_r_or_w_ok =
4883 it.mutate() = lowered;
4884 it.next_sibling_or_parent();
4887 auto prophecy_pointer_in_range =
4891 it.mutate() = lowered;
4892 it.next_sibling_or_parent();
4901 return lowered_expr;
4912 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
4914 std::unordered_map<irep_idt, std::optional<identifiert>> shadowed_syms;
4919 for(
const auto &symbol : q_expr.variables())
4921 const auto identifier = symbol.get_identifier();
4924 shadowed_syms.insert(
4926 id_entry.second ? std::nullopt
4927 : std::optional{id_entry.first->second}});
4930 for(
const auto &[
id, shadowed_val] : shadowed_syms)
4933 if(!shadowed_val.has_value())
4936 previous_entry->second = std::move(*shadowed_val);
4942 for(
const auto &op : expr.
operands())
4945 if(expr.
id()==ID_symbol ||
4946 expr.
id()==ID_nondet_symbol)
4949 if(expr.
type().
id()==ID_code)
4954 if(expr.
id()==ID_symbol)
4957 identifier=
"nondet_"+
4968 out <<
"; find_symbols\n";
4969 out <<
"(declare-fun " << smt2_identifier;
4971 if(expr.
type().
id() == ID_mathematical_function)
4973 auto &mathematical_function_type =
4978 for(
auto &type : mathematical_function_type.domain())
4999 else if(expr.
id() == ID_array_of)
5006 const auto &array_type = array_of.type();
5010 out <<
"; the following is a substitute for lambda i. x\n";
5011 out <<
"(declare-fun " <<
id <<
" () ";
5018 out <<
"(assert (forall ((i ";
5020 out <<
")) (= (select " <<
id <<
" i) ";
5038 else if(expr.
id() == ID_array_comprehension)
5045 const auto &array_type = array_comprehension.type();
5046 const auto &array_size = array_type.size();
5050 out <<
"(declare-fun " <<
id <<
" () ";
5054 out <<
"; the following is a substitute for lambda i . x(i)\n";
5055 out <<
"; universally quantified initialization of the array\n";
5056 out <<
"(assert (forall ((";
5060 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
5067 out <<
")) (= (select " <<
id <<
" ";
5086 else if(expr.
id()==ID_array)
5093 out <<
"; the following is a substitute for an array constructor" <<
"\n";
5094 out <<
"(declare-fun " <<
id <<
" () ";
5100 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5102 out <<
"(assert (= (select " <<
id <<
" ";
5123 else if(expr.
id()==ID_string_constant)
5133 out <<
"; the following is a substitute for a string" <<
"\n";
5134 out <<
"(declare-fun " <<
id <<
" () ";
5138 for(std::size_t i=0; i<tmp.
operands().size(); i++)
5140 out <<
"(assert (= (select " <<
id <<
' ';
5144 out <<
"))" <<
"\n";
5157 out <<
"(declare-fun " <<
id <<
" () ";
5168 (expr.
id() == ID_floatbv_plus ||
5169 expr.
id() == ID_floatbv_minus ||
5170 expr.
id() == ID_floatbv_mult ||
5171 expr.
id() == ID_floatbv_div ||
5172 expr.
id() == ID_floatbv_typecast ||
5173 expr.
id() == ID_ieee_float_equal ||
5174 expr.
id() == ID_ieee_float_notequal ||
5175 ((expr.
id() == ID_lt ||
5176 expr.
id() == ID_gt ||
5177 expr.
id() == ID_le ||
5178 expr.
id() == ID_ge ||
5179 expr.
id() == ID_isnan ||
5180 expr.
id() == ID_isnormal ||
5181 expr.
id() == ID_isfinite ||
5182 expr.
id() == ID_isinf ||
5183 expr.
id() == ID_sign ||
5184 expr.
id() == ID_unary_minus ||
5185 expr.
id() == ID_typecast ||
5186 expr.
id() == ID_abs) &&
5193 if(
bvfp_set.insert(function).second)
5195 out <<
"; this is a model for " << expr.
id() <<
" : "
5198 <<
"(define-fun " << function <<
" (";
5200 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5204 out <<
"(op" << i <<
' ';
5214 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
5230 expr.
type().
id() == ID_bv)
5240 out <<
"(declare-fun " <<
id <<
" () ";
5246 out <<
"(assert (= ";
5247 out <<
"((_ to_fp " << floatbv_type.get_e() <<
" "
5248 << floatbv_type.get_f() + 1 <<
") " <<
id <<
')';
5256 else if(expr.
id() == ID_initial_state)
5258 irep_idt function =
"initial-state";
5262 out <<
"(declare-fun " << function <<
" (";
5269 else if(expr.
id() == ID_evaluate)
5275 out <<
"(declare-fun " << function <<
" (";
5285 expr.
id() == ID_state_is_cstring ||
5286 expr.
id() == ID_state_is_dynamic_object ||
5287 expr.
id() == ID_state_live_object || expr.
id() == ID_state_writeable_object)
5290 expr.
id() == ID_state_is_cstring ?
"state-is-cstring"
5291 : expr.
id() == ID_state_is_dynamic_object ?
"state-is-dynamic-object"
5292 : expr.
id() == ID_state_live_object ?
"state-live-object"
5293 :
"state-writeable-object";
5297 out <<
"(declare-fun " << function <<
" (";
5307 expr.
id() == ID_state_r_ok || expr.
id() == ID_state_w_ok ||
5308 expr.
id() == ID_state_rw_ok)
5310 irep_idt function = expr.
id() == ID_state_r_ok ?
"state-r-ok"
5311 : expr.
id() == ID_state_w_ok ?
"state-w-ok"
5316 out <<
"(declare-fun " << function <<
" (";
5327 else if(expr.
id() == ID_update_state)
5334 out <<
"(declare-fun " << function <<
" (";
5345 else if(expr.
id() == ID_enter_scope_state)
5352 out <<
"(declare-fun " << function <<
" (";
5363 else if(expr.
id() == ID_exit_scope_state)
5370 out <<
"(declare-fun " << function <<
" (";
5379 else if(expr.
id() == ID_allocate)
5385 out <<
"(declare-fun " << function <<
" (";
5394 else if(expr.
id() == ID_reallocate)
5400 out <<
"(declare-fun " << function <<
" (";
5411 else if(expr.
id() == ID_deallocate_state)
5417 out <<
"(declare-fun " << function <<
" (";
5426 else if(expr.
id() == ID_object_address)
5428 irep_idt function =
"object-address";
5432 out <<
"(declare-fun " << function <<
" (String) ";
5437 else if(expr.
id() == ID_field_address)
5443 out <<
"(declare-fun " << function <<
" (";
5452 else if(expr.
id() == ID_element_address)
5458 out <<
"(declare-fun " << function <<
" (";
5477 if(expr.
id() == ID_with)
5485 if(type.
id()==ID_array)
5499 out <<
"(_ BitVec 1)";
5505 else if(type.
id()==ID_bool)
5509 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
5519 out <<
"(_ BitVec " << width <<
")";
5522 else if(type.
id()==ID_code)
5529 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
5536 union_type.
components().empty() || width != 0,
5537 "failed to get width of union");
5539 out <<
"(_ BitVec " << width <<
")";
5541 else if(type.
id()==ID_pointer)
5546 else if(type.
id()==ID_bv ||
5547 type.
id()==ID_fixedbv ||
5548 type.
id()==ID_unsignedbv ||
5549 type.
id()==ID_signedbv ||
5550 type.
id()==ID_c_bool)
5555 else if(type.
id()==ID_c_enum)
5562 else if(type.
id()==ID_c_enum_tag)
5566 else if(type.
id()==ID_floatbv)
5571 out <<
"(_ FloatingPoint "
5572 << floatbv_type.
get_e() <<
" "
5573 << floatbv_type.
get_f() + 1 <<
")";
5578 else if(type.
id()==ID_rational ||
5581 else if(type.
id()==ID_integer)
5583 else if(type.
id()==ID_complex)
5593 out <<
"(_ BitVec " << width <<
")";
5596 else if(type.
id()==ID_c_bit_field)
5600 else if(type.
id() == ID_state)
5612 std::set<irep_idt> recstack;
5618 std::set<irep_idt> &recstack)
5620 if(type.
id()==ID_array)
5626 else if(type.
id()==ID_complex)
5633 const std::string smt_typename =
5637 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5638 <<
"(((mk-" << smt_typename;
5640 out <<
" (" << smt_typename <<
".imag ";
5644 out <<
" (" << smt_typename <<
".real ";
5651 else if(type.
id() == ID_struct)
5654 bool need_decl=
false;
5658 const std::string smt_typename =
5673 const std::string &smt_typename =
datatype_map.at(type);
5684 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5685 <<
"(((mk-" << smt_typename <<
" ";
5692 out <<
"(" << smt_typename <<
"." <<
component.get_name()
5698 out <<
"))))" <<
"\n";
5715 for(struct_union_typet::componentst::const_iterator
5716 it=components.begin();
5717 it!=components.end();
5724 out <<
"(define-fun update-" << smt_typename <<
"."
5726 <<
"((s " << smt_typename <<
") "
5729 out <<
")) " << smt_typename <<
" "
5730 <<
"(mk-" << smt_typename
5733 for(struct_union_typet::componentst::const_iterator
5734 it2=components.begin();
5735 it2!=components.end();
5742 out <<
"(" << smt_typename <<
"."
5743 << it2->get_name() <<
" s) ";
5747 out <<
"))" <<
"\n";
5753 else if(type.
id() == ID_union)
5761 else if(type.
id()==ID_code)
5765 for(
const auto ¶m : parameters)
5770 else if(type.
id()==ID_pointer)
5774 else if(type.
id() == ID_struct_tag)
5777 const irep_idt &
id = struct_tag.get_identifier();
5779 if(recstack.find(
id) == recstack.end())
5782 recstack.insert(
id);
5787 else if(type.
id() == ID_union_tag)
5790 const irep_idt &
id = union_tag.get_identifier();
5792 if(recstack.find(
id) == recstack.end())
5794 recstack.insert(
id);
5798 else if(type.
id() == ID_state)
5803 out <<
"(declare-sort state 0)\n";
5806 else if(type.
id() == ID_mathematical_function)
5808 const auto &mathematical_function_type =
5810 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 update_bits_exprt & to_update_bits_expr(const exprt &expr)
Cast an exprt to an update_bits_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 update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
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)
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
const parameterst & parameters() const
std::vector< parametert > parameterst
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 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)
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)
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
std::vector< componentt > componentst
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 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)
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.
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.
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)
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)