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,
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;
292 std::size_t l=pointer_width-
config.bv_encoding.object_bits;
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 <<
") ";
311 out <<
") (_ bv" << number <<
" " <<
config.bv_encoding.object_bits <<
"))"
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 &&
482 else if(src.
get_sub().size()==4 &&
491 else if(src.
get_sub().size()==4 &&
500 if(type.
id()==ID_signedbv ||
501 type.
id()==ID_unsignedbv ||
502 type.
id()==ID_c_enum ||
503 type.
id()==ID_c_bool)
507 else if(type.
id()==ID_c_enum_tag)
513 result.
type() = type;
516 else if(type.
id()==ID_fixedbv ||
517 type.
id()==ID_floatbv)
522 else if(type.
id() == ID_integer)
526 else if(type.
id() == ID_range)
532 "smt2_convt::parse_literal should not be of unsupported type " +
540 std::unordered_map<int64_t, exprt> operands_map;
544 auto maybe_default_op = operands_map.find(-1);
546 if(maybe_default_op == operands_map.end())
549 default_op = maybe_default_op->second;
552 if(maybe_size.has_value())
554 while(i < maybe_size.value())
556 auto found_op = operands_map.find(i);
557 if(found_op != operands_map.end())
558 operands.emplace_back(found_op->second);
560 operands.emplace_back(default_op);
568 auto found_op = operands_map.find(i);
569 while(found_op != operands_map.end())
571 operands.emplace_back(found_op->second);
573 found_op = operands_map.find(i);
575 operands.emplace_back(default_op);
581 std::unordered_map<int64_t, exprt> *operands_map,
594 bool failure =
to_integer(index_constant, tempint);
597 long index = tempint.to_long();
599 operands_map->emplace(index, value);
601 else if(src.
get_sub().size()==2 &&
602 src.
get_sub()[0].get_sub().size()==3 &&
603 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
604 src.
get_sub()[0].get_sub()[1].id()==
"const")
608 operands_map->emplace(-1, default_value);
641 if(components.empty())
649 for(std::size_t i=0; i<components.size(); i++)
659 src.
get_sub().size() > j,
"insufficient number of component values");
676 std::size_t offset=0;
678 for(std::size_t i=0; i<components.size(); i++)
683 std::size_t component_width=
boolbv_width(components[i].type());
686 offset + component_width <= total_width,
687 "struct component bits shall be within struct bit vector");
689 std::string component_binary=
691 total_width-offset-component_width, component_width);
696 offset+=component_width;
710 for(
const auto &binding : src.
get_sub()[1].get_sub())
712 const irep_idt &name = binding.get_sub()[0].id();
723 return parse_rec(bindings_it->second, type);
727 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
728 type.
id() == ID_integer || type.
id() == ID_rational ||
729 type.
id() == ID_real || type.
id() == ID_c_enum ||
730 type.
id() == ID_c_enum_tag || type.
id() == ID_fixedbv ||
731 type.
id() == ID_floatbv || type.
id() == ID_c_bool || type.
id() == ID_range)
735 else if(type.
id()==ID_bool)
737 if(src.
id()==ID_1 || src.
id()==ID_true)
739 else if(src.
id()==ID_0 || src.
id()==ID_false)
742 else if(type.
id()==ID_pointer)
757 else if(type.
id()==ID_struct)
761 else if(type.
id() == ID_struct_tag)
766 struct_expr.type() = type;
767 return std::move(struct_expr);
769 else if(type.
id()==ID_union)
773 else if(type.
id() == ID_union_tag)
777 union_expr.type() = type;
780 else if(type.
id()==ID_array)
794 expr.
id() == ID_string_constant || expr.
id() == ID_label)
796 const std::size_t object_bits =
config.bv_encoding.object_bits;
797 const std::size_t max_objects = std::size_t(1) << object_bits;
800 if(object_id >= max_objects)
803 "too many addressed objects: maximum number of objects is set to 2^n=" +
804 std::to_string(max_objects) +
805 " (with n=" + std::to_string(object_bits) +
"); " +
806 "use the `--object-bits n` option to increase the maximum number"};
809 out <<
"(concat (_ bv" << object_id <<
" " << object_bits <<
")"
810 <<
" (_ bv0 " <<
boolbv_width(result_type) - object_bits <<
"))";
812 else if(expr.
id()==ID_index)
821 if(array.
type().
id()==ID_pointer)
823 else if(array.
type().
id()==ID_array)
843 else if(expr.
id()==ID_member)
848 const typet &struct_op_type = struct_op.
type();
851 struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag,
852 "member expression operand shall have struct type");
855 struct_op_type.
id() == ID_struct_tag
872 else if(expr.
id()==ID_if)
887 "operand of address of expression should not be of kind " +
895 if(node.
id() == ID_exists || node.
id() == ID_forall)
911 else if(expr.
id()==ID_literal)
923 out <<
"; convert\n";
924 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
934 out <<
"(declare-fun ";
936 out <<
" () Bool)\n";
937 out <<
"(assert (= ";
949 out <<
"(define-fun " << identifier <<
" () Bool ";
977 const auto identifier =
999 for(
auto &assumption : _assumptions)
1010 if(identifier.empty())
1013 if(isdigit(identifier[0]))
1035 std::string result =
"|";
1037 for(
auto ch : identifier)
1045 result+=std::to_string(ch);
1062 if(type.
id()==ID_floatbv)
1065 return "f"+std::to_string(spec.
width())+
"_"+std::to_string(spec.
f);
1067 else if(type.
id() == ID_bv)
1071 else if(type.
id()==ID_unsignedbv)
1075 else if(type.
id()==ID_c_bool)
1079 else if(type.
id()==ID_signedbv)
1083 else if(type.
id()==ID_bool)
1087 else if(type.
id()==ID_c_enum_tag)
1091 else if(type.
id() == ID_pointer)
1095 else if(type.
id() == ID_struct_tag)
1102 else if(type.
id() == ID_union_tag)
1106 else if(type.
id() == ID_array)
1127 if(expr.
id()==ID_symbol)
1134 if(expr.
id()==ID_smt2_symbol)
1142 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
1148 for(
const auto &op : expr.
operands())
1176 converter_result->second(expr);
1181 if(expr.
id()==ID_symbol)
1187 else if(expr.
id()==ID_nondet_symbol)
1190 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1193 else if(expr.
id()==ID_smt2_symbol)
1199 else if(expr.
id()==ID_typecast)
1203 else if(expr.
id()==ID_floatbv_typecast)
1207 else if(expr.
id() == ID_floatbv_round_to_integral)
1211 else if(expr.
id()==ID_struct)
1215 else if(expr.
id()==ID_union)
1223 else if(expr.
id() == ID_concatenation && expr.
operands().size() == 1)
1227 "concatenation over a single operand should have matching types",
1233 expr.
id() == ID_concatenation || expr.
id() == ID_bitand ||
1234 expr.
id() == ID_bitor || expr.
id() == ID_bitxor)
1238 "given expression should have at least two operands",
1243 if(expr.
id()==ID_concatenation)
1245 else if(expr.
id()==ID_bitand)
1247 else if(expr.
id()==ID_bitor)
1249 else if(expr.
id()==ID_bitxor)
1251 else if(expr.
id()==ID_bitnand)
1253 else if(expr.
id()==ID_bitnor)
1256 for(
const auto &op : expr.
operands())
1265 expr.
id() == ID_bitxnor || expr.
id() == ID_bitnand ||
1266 expr.
id() == ID_bitnor)
1275 if(binary_expr.id() == ID_bitxnor)
1277 else if(binary_expr.id() == ID_bitnand)
1279 else if(binary_expr.id() == ID_bitnor)
1287 else if(expr.
operands().size() == 1)
1293 else if(expr.
operands().size() >= 3)
1296 if(expr.
id() == ID_bitxnor)
1298 else if(expr.
id() == ID_bitnand)
1300 else if(expr.
id() == ID_bitnor)
1303 for(
const auto &op : expr.
operands())
1315 expr.
id_string() +
" should have at least one operand");
1318 else if(expr.
id()==ID_bitnot)
1326 else if(expr.
id()==ID_unary_minus)
1329 const auto &type = expr.
type();
1332 type.id() == ID_rational || type.id() == ID_integer ||
1333 type.id() == ID_real)
1339 else if(type.id() == ID_range)
1348 else if(type.id() == ID_floatbv)
1367 else if(expr.
id()==ID_unary_plus)
1372 else if(expr.
id()==ID_sign)
1378 if(op_type.
id()==ID_floatbv)
1382 out <<
"(fp.isNegative ";
1389 else if(op_type.
id()==ID_signedbv)
1395 out <<
" (_ bv0 " << op_width <<
"))";
1400 "sign should not be applied to unsupported type",
1403 else if(expr.
id()==ID_if)
1415 else if(expr.
id()==ID_and ||
1421 "logical and, or, and xor expressions should have Boolean type");
1424 "logical and, or, and xor expressions should have at least two operands");
1426 out <<
"(" << expr.
id();
1427 for(
const auto &op : expr.
operands())
1434 else if(expr.
id() == ID_nand || expr.
id() == ID_nor || expr.
id() == ID_xnor)
1438 "logical nand, nor, xnor expressions should have Boolean type");
1441 "logical nand, nor, xnor expressions should have at least one operand");
1449 if(expr.
id() == ID_nand)
1451 else if(expr.
id() == ID_nor)
1453 else if(expr.
id() == ID_xnor)
1457 for(
const auto &op : expr.
operands())
1466 else if(expr.
id()==ID_implies)
1471 implies_expr.
is_boolean(),
"implies expression should have Boolean type");
1479 else if(expr.
id()==ID_not)
1484 not_expr.
is_boolean(),
"not expression should have Boolean type");
1490 else if(expr.
id() == ID_equal)
1496 "operands of equal expression shall have same type");
1511 else if(expr.
id() == ID_notequal)
1517 "operands of not equal expression shall have same type");
1525 else if(expr.
id()==ID_ieee_float_equal ||
1526 expr.
id()==ID_ieee_float_notequal)
1533 rel_expr.lhs().type() == rel_expr.rhs().type(),
1534 "operands of float equal and not equal expressions shall have same type");
1539 if(rel_expr.id() == ID_ieee_float_notequal)
1548 if(rel_expr.id() == ID_ieee_float_notequal)
1554 else if(expr.
id()==ID_le ||
1561 else if(expr.
id()==ID_plus)
1565 else if(expr.
id()==ID_floatbv_plus)
1569 else if(expr.
id()==ID_minus)
1573 else if(expr.
id()==ID_floatbv_minus)
1577 else if(expr.
id()==ID_div)
1581 else if(expr.
id()==ID_floatbv_div)
1585 else if(expr.
id()==ID_mod)
1589 else if(expr.
id() == ID_euclidean_mod)
1593 else if(expr.
id()==ID_mult)
1597 else if(expr.
id()==ID_floatbv_mult)
1601 else if(expr.
id() == ID_floatbv_rem)
1605 else if(expr.
id()==ID_address_of)
1611 else if(expr.
id() == ID_array_of)
1616 array_of_expr.type().id() == ID_array,
1617 "array of expression shall have array type");
1621 out <<
"((as const ";
1629 defined_expressionst::const_iterator it =
1635 else if(expr.
id() == ID_array_comprehension)
1640 array_comprehension.type().id() == ID_array,
1641 "array_comprehension expression shall have array type");
1645 out <<
"(lambda ((";
1648 convert_type(array_comprehension.type().size().type());
1660 else if(expr.
id()==ID_index)
1664 else if(expr.
id()==ID_ashr ||
1665 expr.
id()==ID_lshr ||
1671 if(type.
id()==ID_unsignedbv ||
1672 type.
id()==ID_signedbv ||
1675 if(shift_expr.
id() == ID_ashr)
1677 else if(shift_expr.
id() == ID_lshr)
1679 else if(shift_expr.
id() == ID_shl)
1690 const auto &distance_type = shift_expr.
distance().
type();
1691 if(distance_type.id() == ID_integer || distance_type.id() == ID_natural)
1702 distance_type.id() == ID_signedbv ||
1703 distance_type.id() == ID_unsignedbv ||
1704 distance_type.id() == ID_c_enum || distance_type.id() == ID_c_bool)
1709 if(width_op0==width_op1)
1711 else if(width_op0>width_op1)
1713 out <<
"((_ zero_extend " << width_op0-width_op1 <<
") ";
1719 out <<
"((_ extract " << width_op0-1 <<
" 0) ";
1727 "unsupported distance type for " + shift_expr.
id_string() +
": " +
1728 distance_type.id_string());
1735 "unsupported type for " + shift_expr.
id_string() +
": " +
1738 else if(expr.
id() == ID_rol || expr.
id() == ID_ror)
1744 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1749 if(shift_expr.
id() == ID_rol)
1750 out <<
"((_ rotate_left";
1751 else if(shift_expr.
id() == ID_ror)
1752 out <<
"((_ rotate_right";
1760 if(distance_int_op.has_value())
1762 out << distance_int_op.value();
1766 "distance type for " + shift_expr.
id_string() +
"must be constant");
1775 "unsupported type for " + shift_expr.
id_string() +
": " +
1778 else if(expr.
id() == ID_named_term)
1782 convert(named_term_expr.value());
1786 else if(expr.
id()==ID_with)
1790 else if(expr.
id()==ID_update)
1794 else if(expr.
id() == ID_update_bit)
1798 else if(expr.
id() == ID_update_bits)
1802 else if(expr.
id() == ID_object_address)
1804 out <<
"(object-address ";
1809 else if(expr.
id() == ID_element_address)
1815 auto element_size_expr_opt =
1825 *element_size_expr_opt, element_address_expr.index().type()));
1828 else if(expr.
id() == ID_field_address)
1837 else if(expr.
id()==ID_member)
1841 else if(expr.
id()==ID_pointer_offset)
1846 op.type().id() == ID_pointer,
1847 "operand of pointer offset expression shall be of pointer type");
1849 std::size_t offset_bits =
1854 if(offset_bits>result_width)
1855 offset_bits=result_width;
1858 if(result_width>offset_bits)
1859 out <<
"((_ zero_extend " << result_width-offset_bits <<
") ";
1861 out <<
"((_ extract " << offset_bits-1 <<
" 0) ";
1865 if(result_width>offset_bits)
1868 else if(expr.
id()==ID_pointer_object)
1873 op.type().id() == ID_pointer,
1874 "pointer object expressions should be of pointer type");
1880 out <<
"((_ zero_extend " << ext <<
") ";
1882 out <<
"((_ extract "
1883 << pointer_width-1 <<
" "
1884 << pointer_width-
config.bv_encoding.object_bits <<
") ";
1891 else if(expr.
id() == ID_is_dynamic_object)
1895 else if(expr.
id() == ID_is_invalid_pointer)
1899 out <<
"(= ((_ extract "
1900 << pointer_width-1 <<
" "
1901 << pointer_width-
config.bv_encoding.object_bits <<
") ";
1904 <<
" " <<
config.bv_encoding.object_bits <<
"))";
1906 else if(expr.
id()==ID_string_constant)
1912 else if(expr.
id()==ID_extractbit)
1921 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
1927 out <<
"(= ((_ extract 0 0) ";
1937 else if(expr.
id() == ID_onehot)
1941 else if(expr.
id() == ID_onehot0)
1945 else if(expr.
id()==ID_extractbits)
1955 out <<
"((_ extract " << (width + index_i - 1) <<
" " << index_i <<
") ";
1962 out <<
"(= ((_ extract 0 0) ";
1971 SMT2_TODO(
"smt2: extractbits with non-constant index");
1974 else if(expr.
id()==ID_replication)
1980 out <<
"((_ repeat " << times <<
") ";
1984 else if(expr.
id()==ID_byte_extract_little_endian ||
1985 expr.
id()==ID_byte_extract_big_endian)
1988 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1990 else if(expr.
id()==ID_byte_update_little_endian ||
1991 expr.
id()==ID_byte_update_big_endian)
1994 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1996 else if(expr.
id()==ID_abs)
2002 if(type.
id()==ID_signedbv)
2006 out <<
"(ite (bvslt ";
2008 out <<
" (_ bv0 " << result_width <<
")) ";
2015 else if(type.
id()==ID_fixedbv)
2019 out <<
"(ite (bvslt ";
2021 out <<
" (_ bv0 " << result_width <<
")) ";
2028 else if(type.
id()==ID_floatbv)
2042 else if(expr.
id()==ID_isnan)
2048 if(op_type.
id()==ID_fixedbv)
2050 else if(op_type.
id()==ID_floatbv)
2054 out <<
"(fp.isNaN ";
2064 else if(expr.
id()==ID_isfinite)
2070 if(op_type.
id()==ID_fixedbv)
2072 else if(op_type.
id()==ID_floatbv)
2078 out <<
"(not (fp.isNaN ";
2082 out <<
"(not (fp.isInfinite ";
2094 else if(expr.
id()==ID_isinf)
2100 if(op_type.
id()==ID_fixedbv)
2102 else if(op_type.
id()==ID_floatbv)
2106 out <<
"(fp.isInfinite ";
2116 else if(expr.
id()==ID_isnormal)
2122 if(op_type.
id()==ID_fixedbv)
2124 else if(op_type.
id()==ID_floatbv)
2128 out <<
"(fp.isNormal ";
2141 expr.
id() == ID_overflow_result_plus ||
2142 expr.
id() == ID_overflow_result_minus)
2151 "overflow plus and overflow minus expressions shall be of Boolean type");
2154 expr.
id() == ID_overflow_result_minus;
2155 const typet &op_type = op0.type();
2158 if(op_type.
id()==ID_signedbv)
2161 out <<
"(let ((?sum (";
2162 out << (subtract?
"bvsub":
"bvadd");
2163 out <<
" ((_ sign_extend 1) ";
2166 out <<
" ((_ sign_extend 1) ";
2176 out <<
"(mk-" << smt_typename;
2181 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2186 "((_ extract " << width <<
" " << width <<
") ?sum) "
2187 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
2197 else if(op_type.
id()==ID_unsignedbv ||
2198 op_type.
id()==ID_pointer)
2201 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2202 out <<
" ((_ zero_extend 1) ";
2205 out <<
" ((_ zero_extend 1) ";
2217 out <<
"(mk-" << smt_typename;
2218 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2222 out <<
"((_ extract " << width <<
" " << width <<
") ?sum)";
2233 "overflow check should not be performed on unsupported type",
2238 expr.
id() == ID_overflow_result_mult)
2247 "overflow mult expression shall be of Boolean type");
2252 const typet &op_type = op0.type();
2255 if(op_type.
id()==ID_signedbv)
2257 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
2259 out <<
") ((_ sign_extend " << width <<
") ";
2269 out <<
"(mk-" << smt_typename;
2274 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2278 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
2280 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width - 1) <<
" "
2281 << width * 2 <<
"))))";
2290 else if(op_type.
id()==ID_unsignedbv)
2292 out <<
"(let ((prod (bvmul ((_ zero_extend " << width <<
") ";
2294 out <<
") ((_ zero_extend " << width <<
") ";
2304 out <<
"(mk-" << smt_typename;
2309 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2313 out <<
"(bvuge prod (_ bv" <<
power(2, width) <<
" " << width * 2 <<
"))";
2325 "overflow check should not be performed on unsupported type",
2328 else if(expr.
id() == ID_saturating_plus || expr.
id() == ID_saturating_minus)
2330 const bool subtract = expr.
id() == ID_saturating_minus;
2331 const auto &op_type = expr.
type();
2335 if(op_type.id() == ID_signedbv)
2340 out <<
"(let ((?sum (";
2341 out << (subtract ?
"bvsub" :
"bvadd");
2342 out <<
" ((_ sign_extend 1) ";
2345 out <<
" ((_ sign_extend 1) ";
2352 << width <<
" " << width
2355 << (width - 1) <<
" " << (width - 1) <<
") ?sum)";
2359 out <<
"((_ extract " << width - 1 <<
" 0) ?sum) ";
2362 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2369 else if(op_type.id() == ID_unsignedbv)
2374 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2375 out <<
" ((_ zero_extend 1) ";
2378 out <<
" ((_ zero_extend 1) ";
2383 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2386 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2400 "saturating_plus/minus on unsupported type",
2401 op_type.id_string());
2403 else if(expr.
id()==ID_array)
2409 else if(expr.
id()==ID_literal)
2413 else if(expr.
id()==ID_forall ||
2414 expr.
id()==ID_exists)
2420 throw "MathSAT does not support quantifiers";
2422 if(quantifier_expr.
id() == ID_forall)
2424 else if(quantifier_expr.
id() == ID_exists)
2429 for(
const auto &bound : quantifier_expr.
variables())
2452 else if(expr.
id()==ID_let)
2455 const auto &variables = let_expr.
variables();
2456 const auto &values = let_expr.
values();
2461 for(
auto &binding :
make_range(variables).zip(values))
2480 else if(expr.
id()==ID_constraint_select_one)
2483 "smt2_convt::convert_expr: '" + expr.
id_string() +
2484 "' is not yet supported");
2486 else if(expr.
id() == ID_bswap)
2492 "operand of byte swap expression shall have same type as the expression");
2495 out <<
"(let ((bswap_op ";
2500 bswap_expr.
type().
id() == ID_signedbv ||
2501 bswap_expr.
type().
id() == ID_unsignedbv)
2503 const std::size_t width =
2510 width % bits_per_byte == 0,
2511 "bit width indicated by type of bswap expression should be a multiple "
2512 "of the number of bits per byte");
2514 const std::size_t bytes = width / bits_per_byte;
2523 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2527 out <<
"(bswap_byte_" <<
byte <<
' ';
2528 out <<
"((_ extract " << (
byte * bits_per_byte + (bits_per_byte - 1))
2529 <<
" " << (
byte * bits_per_byte) <<
") bswap_op)";
2538 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2539 out <<
" bswap_byte_" <<
byte;
2550 else if(expr.
id() == ID_popcount)
2554 else if(expr.
id() == ID_count_leading_zeros)
2558 else if(expr.
id() == ID_count_trailing_zeros)
2562 else if(expr.
id() == ID_find_first_set)
2566 else if(expr.
id() == ID_bitreverse)
2570 else if(expr.
id() == ID_zero_extend)
2574 else if(expr.
id() == ID_function_application)
2578 if(function_application_expr.arguments().empty())
2586 for(
auto &op : function_application_expr.arguments())
2594 else if(expr.
id() == ID_cond)
2602 "smt2_convt::convert_expr should not be applied to unsupported "
2612 if(dest_type.
id()==ID_c_enum_tag)
2616 if(src_type.
id()==ID_c_enum_tag)
2619 if(dest_type.
id()==ID_bool)
2622 if(src_type.
id()==ID_signedbv ||
2623 src_type.
id()==ID_unsignedbv ||
2624 src_type.
id()==ID_c_bool ||
2625 src_type.
id()==ID_fixedbv ||
2626 src_type.
id()==ID_pointer ||
2627 src_type.
id()==ID_integer)
2635 else if(src_type.
id()==ID_floatbv)
2639 out <<
"(not (fp.isZero ";
2651 else if(dest_type.
id()==ID_c_bool)
2660 out <<
" (_ bv1 " << to_width <<
")";
2661 out <<
" (_ bv0 " << to_width <<
")";
2664 else if(dest_type.
id()==ID_signedbv ||
2665 dest_type.
id()==ID_unsignedbv ||
2666 dest_type.
id()==ID_c_enum ||
2667 dest_type.
id()==ID_bv)
2671 if(src_type.
id()==ID_signedbv ||
2672 src_type.
id()==ID_unsignedbv ||
2673 src_type.
id()==ID_c_bool ||
2674 src_type.
id()==ID_c_enum ||
2675 src_type.
id()==ID_bv)
2679 if(from_width==to_width)
2681 else if(from_width<to_width)
2683 if(src_type.
id()==ID_signedbv)
2684 out <<
"((_ sign_extend ";
2686 out <<
"((_ zero_extend ";
2688 out << (to_width-from_width)
2695 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2700 else if(src_type.
id()==ID_fixedbv)
2704 std::size_t from_width=fixedbv_type.
get_width();
2711 out <<
"(let ((?tcop ";
2717 if(to_width>from_integer_bits)
2719 out <<
"((_ sign_extend "
2720 << (to_width-from_integer_bits) <<
") ";
2721 out <<
"((_ extract " << (from_width-1) <<
" "
2722 << from_fraction_bits <<
") ";
2728 out <<
"((_ extract " << (from_fraction_bits+to_width-1)
2729 <<
" " << from_fraction_bits <<
") ";
2734 out <<
" (ite (and ";
2737 out <<
"(not (= ((_ extract " << (from_fraction_bits-1) <<
" 0) ?tcop) "
2738 "(_ bv0 " << from_fraction_bits <<
")))";
2741 out <<
" (= ((_ extract " << (from_width-1) <<
" " << (from_width-1)
2746 out <<
" (_ bv1 " << to_width <<
") (_ bv0 " << to_width <<
"))";
2750 else if(src_type.
id()==ID_floatbv)
2752 if(dest_type.
id()==ID_bv)
2758 defined_expressionst::const_iterator it =
2769 else if(dest_type.
id()==ID_signedbv)
2773 "typecast unexpected "+src_type.
id_string()+
" -> "+
2776 else if(dest_type.
id()==ID_unsignedbv)
2780 "typecast unexpected "+src_type.
id_string()+
" -> "+
2784 else if(src_type.
id()==ID_bool)
2789 if(dest_type.
id()==ID_fixedbv)
2792 out <<
" (concat (_ bv1 "
2795 "(_ bv0 " << spec.
width <<
")";
2799 out <<
" (_ bv1 " << to_width <<
")";
2800 out <<
" (_ bv0 " << to_width <<
")";
2805 else if(src_type.
id()==ID_pointer)
2809 if(from_width<to_width)
2811 out <<
"((_ sign_extend ";
2812 out << (to_width-from_width)
2819 out <<
"((_ extract " << (to_width-1) <<
" 0) ";
2824 else if(src_type.
id()==ID_integer)
2830 out <<
"(_ bv" << i <<
" " << to_width <<
")";
2833 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2836 src_type.
id() == ID_struct ||
2837 src_type.
id() == ID_struct_tag)
2843 "bit vector with of source and destination type shall be equal");
2850 "bit vector with of source and destination type shall be equal");
2855 src_type.
id() == ID_union ||
2856 src_type.
id() == ID_union_tag)
2860 "bit vector with of source and destination type shall be equal");
2863 else if(src_type.
id()==ID_c_bit_field)
2867 if(from_width==to_width)
2878 std::ostringstream e_str;
2879 e_str << src_type.
id() <<
" -> " << dest_type.
id()
2880 <<
" src == " <<
format(src);
2884 else if(dest_type.
id()==ID_fixedbv)
2890 if(src_type.
id()==ID_unsignedbv ||
2891 src_type.
id()==ID_signedbv ||
2892 src_type.
id()==ID_c_enum)
2899 if(from_width==to_integer_bits)
2901 else if(from_width>to_integer_bits)
2904 out <<
"((_ extract " << (to_integer_bits-1) <<
" 0) ";
2912 from_width < to_integer_bits,
2913 "from_width should be smaller than to_integer_bits as other case "
2914 "have been handled above");
2915 if(dest_type.
id()==ID_unsignedbv)
2917 out <<
"(_ zero_extend "
2918 << (to_integer_bits-from_width) <<
") ";
2924 out <<
"((_ sign_extend "
2925 << (to_integer_bits-from_width) <<
") ";
2931 out <<
"(_ bv0 " << to_fraction_bits <<
")";
2934 else if(src_type.
id()==ID_bool)
2936 out <<
"(concat (concat"
2937 <<
" (_ bv0 " << (to_integer_bits-1) <<
") ";
2943 else if(src_type.
id()==ID_fixedbv)
2948 std::size_t from_width=from_fixedbv_type.
get_width();
2950 out <<
"(let ((?tcop ";
2956 if(to_integer_bits<=from_integer_bits)
2958 out <<
"((_ extract "
2959 << (from_fraction_bits+to_integer_bits-1) <<
" "
2960 << from_fraction_bits
2966 to_integer_bits > from_integer_bits,
2967 "to_integer_bits should be greater than from_integer_bits as the"
2968 "other case has been handled above");
2969 out <<
"((_ sign_extend "
2970 << (to_integer_bits-from_integer_bits)
2972 << (from_width-1) <<
" "
2973 << from_fraction_bits
2979 if(to_fraction_bits<=from_fraction_bits)
2981 out <<
"((_ extract "
2982 << (from_fraction_bits-1) <<
" "
2983 << (from_fraction_bits-to_fraction_bits)
2989 to_fraction_bits > from_fraction_bits,
2990 "to_fraction_bits should be greater than from_fraction_bits as the"
2991 "other case has been handled above");
2992 out <<
"(concat ((_ extract "
2993 << (from_fraction_bits-1) <<
" 0) ";
2996 <<
" (_ bv0 " << to_fraction_bits-from_fraction_bits
3005 else if(dest_type.
id()==ID_pointer)
3009 if(src_type.
id()==ID_pointer)
3015 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
3016 src_type.
id() == ID_bv)
3022 if(from_width==to_width)
3024 else if(from_width<to_width)
3026 out <<
"((_ sign_extend "
3027 << (to_width-from_width)
3034 out <<
"((_ extract " << to_width <<
" 0) ";
3042 else if(dest_type.
id()==ID_range)
3045 const auto dest_size =
3046 dest_range_type.get_to() - dest_range_type.get_from() + 1;
3048 if(src_type.
id() == ID_range)
3051 const auto src_size =
3052 src_range_type.get_to() - src_range_type.get_from() + 1;
3054 if(src_width < dest_width)
3056 out <<
"((_ zero_extend " << dest_width - src_width <<
") ";
3060 else if(src_width > dest_width)
3062 out <<
"((_ extract " << dest_width - 1 <<
" 0) ";
3074 else if(dest_type.
id()==ID_floatbv)
3083 if(src_type.
id()==ID_bool)
3093 else if(src_type.
id()==ID_c_bool)
3099 else if(src_type.
id() == ID_bv)
3108 out <<
"((_ to_fp " << dest_floatbv_type.get_e() <<
" "
3109 << dest_floatbv_type.get_f() + 1 <<
") ";
3119 else if(dest_type.
id()==ID_integer)
3121 if(src_type.
id()==ID_bool)
3130 else if(dest_type.
id()==ID_c_bit_field)
3135 if(from_width==to_width)
3156 if(dest_type.
id()==ID_floatbv)
3158 if(src_type.
id()==ID_floatbv)
3185 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3186 << dst.
get_f() + 1 <<
") ";
3195 else if(src_type.
id()==ID_unsignedbv)
3216 out <<
"((_ to_fp_unsigned " << dst.
get_e() <<
" "
3217 << dst.
get_f() + 1 <<
") ";
3226 else if(src_type.
id()==ID_signedbv)
3234 out <<
"((_ to_fp " << dst.
get_e() <<
" "
3235 << dst.
get_f() + 1 <<
") ";
3244 else if(src_type.
id()==ID_c_enum_tag)
3258 else if(dest_type.
id()==ID_signedbv)
3263 out <<
"((_ fp.to_sbv " << dest_width <<
") ";
3272 else if(dest_type.
id()==ID_unsignedbv)
3277 out <<
"((_ fp.to_ubv " << dest_width <<
") ";
3300 out <<
"(fp.roundToIntegral ";
3313 expr.
type().
id() == ID_struct_tag
3321 components.size() == expr.
operands().size(),
3322 "number of struct components as indicated by the struct type shall be equal"
3323 "to the number of operands of the struct expression");
3325 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
3329 const std::string &smt_typename =
datatype_map.at(struct_type);
3332 out <<
"(mk-" << smt_typename;
3335 for(struct_typet::componentst::const_iterator
3336 it=components.begin();
3337 it!=components.end();
3350 auto convert_operand = [
this](
const exprt &op) {
3354 else if(op.type().id() == ID_bool)
3361 std::size_t n_concat = 0;
3362 for(std::size_t i = components.size(); i > 1; i--)
3372 convert_operand(expr.
operands()[i - 1]);
3378 convert_operand(expr.
op0());
3380 out << std::string(n_concat,
')');
3388 const auto &size_expr = array_type.
size();
3394 out <<
"(let ((?far ";
3402 out <<
"(select ?far ";
3424 if(total_width==member_width)
3432 total_width > member_width,
3433 "total_width should be greater than member_width as member_width can be"
3434 "at most as large as total_width and the other case has been handled "
3438 << (total_width-member_width) <<
") ";
3448 if(expr_type.
id()==ID_unsignedbv ||
3449 expr_type.
id()==ID_signedbv ||
3450 expr_type.
id()==ID_bv ||
3451 expr_type.
id()==ID_c_enum ||
3452 expr_type.
id()==ID_c_enum_tag ||
3453 expr_type.
id()==ID_c_bool ||
3454 expr_type.
id()==ID_c_bit_field)
3460 out <<
"(_ bv" << value
3461 <<
" " << width <<
")";
3463 else if(expr_type.
id()==ID_fixedbv)
3469 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
3471 else if(expr_type.
id()==ID_floatbv)
3484 size_t e=floatbv_type.
get_e();
3485 size_t f=floatbv_type.
get_f()+1;
3491 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3497 out <<
"(_ NaN " << e <<
" " << f <<
")";
3502 out <<
"(_ -oo " << e <<
" " << f <<
")";
3504 out <<
"(_ +oo " << e <<
" " << f <<
")";
3514 <<
"#b" << binaryString.substr(0, 1) <<
" "
3515 <<
"#b" << binaryString.substr(1, e) <<
" "
3516 <<
"#b" << binaryString.substr(1+e, f-1) <<
")";
3524 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3527 else if(expr_type.
id()==ID_pointer)
3541 out <<
"(_ bv" << value <<
" " << width <<
")";
3544 else if(expr_type.
id()==ID_bool)
3553 else if(expr_type.
id()==ID_array)
3559 else if(expr_type.
id()==ID_rational)
3562 const bool negative =
has_prefix(value,
"-");
3567 size_t pos=value.find(
"/");
3569 if(
pos==std::string::npos)
3570 out << value <<
".0";
3573 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3574 << value.substr(
pos+1) <<
".0)";
3580 else if(expr_type.
id()==ID_integer)
3586 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3590 else if(expr_type.
id() == ID_range)
3593 const auto size = range_type.get_to() - range_type.get_from() + 1;
3596 out <<
"(_ bv" << (value_int - range_type.get_from()) <<
" " << width
3605 if(expr.
type().
id() == ID_integer)
3615 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3620 if(expr.
type().
id()==ID_unsignedbv ||
3621 expr.
type().
id()==ID_signedbv)
3623 if(expr.
type().
id()==ID_unsignedbv)
3639 std::vector<mp_integer> dynamic_objects;
3642 if(dynamic_objects.empty())
3648 out <<
"(let ((?obj ((_ extract "
3649 << pointer_width-1 <<
" "
3650 << pointer_width-
config.bv_encoding.object_bits <<
") ";
3654 if(dynamic_objects.size()==1)
3656 out <<
"(= (_ bv" << dynamic_objects.front()
3657 <<
" " <<
config.bv_encoding.object_bits <<
") ?obj)";
3663 for(
const auto &
object : dynamic_objects)
3664 out <<
" (= (_ bv" <<
object
3665 <<
" " <<
config.bv_encoding.object_bits <<
") ?obj)";
3679 op_type.
id() == ID_unsignedbv || op_type.
id() == ID_bv ||
3680 op_type.
id() == ID_range)
3684 if(expr.
id()==ID_le)
3686 else if(expr.
id()==ID_lt)
3688 else if(expr.
id()==ID_ge)
3690 else if(expr.
id()==ID_gt)
3699 else if(op_type.
id()==ID_signedbv ||
3700 op_type.
id()==ID_fixedbv)
3703 if(expr.
id()==ID_le)
3705 else if(expr.
id()==ID_lt)
3707 else if(expr.
id()==ID_ge)
3709 else if(expr.
id()==ID_gt)
3718 else if(op_type.
id()==ID_floatbv)
3723 if(expr.
id()==ID_le)
3725 else if(expr.
id()==ID_lt)
3727 else if(expr.
id()==ID_ge)
3729 else if(expr.
id()==ID_gt)
3741 else if(op_type.
id()==ID_rational ||
3742 op_type.
id()==ID_integer)
3753 else if(op_type.
id() == ID_pointer)
3761 if(expr.
id() == ID_le)
3763 else if(expr.
id() == ID_lt)
3765 else if(expr.
id() == ID_ge)
3767 else if(expr.
id() == ID_gt)
3786 expr.
type().
id() == ID_rational || expr.
type().
id() == ID_integer ||
3787 expr.
type().
id() == ID_real)
3792 for(
const auto &op : expr.
operands())
3801 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv ||
3802 expr.
type().
id() == ID_fixedbv)
3819 else if(expr.
type().
id() == ID_range)
3829 const auto size = range_type.get_to() - range_type.get_from() + 1;
3836 out <<
" (_ bv" << range_type.get_from() <<
' ' << width
3844 else if(expr.
type().
id() == ID_floatbv)
3851 else if(expr.
type().
id() == ID_pointer)
3857 if(p.
type().
id() != ID_pointer)
3861 p.
type().
id() == ID_pointer,
3862 "one of the operands should have pointer type");
3866 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
3869 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3873 out <<
"(let ((?pointerop ";
3879 const std::size_t offset_bits =
3880 pointer_width -
config.bv_encoding.object_bits;
3883 out <<
"((_ extract " << pointer_width - 1 <<
' ' << offset_bits
3884 <<
") ?pointerop) ";
3885 out <<
"(bvadd ((_ extract " << offset_bits - 1 <<
" 0) ?pointerop) ";
3887 if(element_size >= 2)
3889 out <<
"(bvmul ((_ extract " << offset_bits - 1 <<
" 0) ";
3891 out <<
") (_ bv" << element_size <<
" " << offset_bits <<
"))";
3895 out <<
"((_ extract " << offset_bits - 1 <<
" 0) ";
3934 out <<
"roundNearestTiesToEven";
3936 out <<
"roundTowardNegative";
3938 out <<
"roundTowardPositive";
3940 out <<
"roundTowardZero";
3942 out <<
"roundNearestTiesToAway";
3946 "Rounding mode should have value 0, 1, 2, 3, or 4",
3954 out <<
"(ite (= (_ bv0 " << width <<
") ";
3956 out <<
") roundNearestTiesToEven ";
3958 out <<
"(ite (= (_ bv1 " << width <<
") ";
3960 out <<
") roundTowardNegative ";
3962 out <<
"(ite (= (_ bv2 " << width <<
") ";
3964 out <<
") roundTowardPositive ";
3966 out <<
"(ite (= (_ bv3 " << width <<
") ";
3968 out <<
") roundTowardZero ";
3971 out <<
"roundNearestTiesToAway";
3982 type.
id() == ID_floatbv ||
3983 (type.
id() == ID_complex &&
3988 if(type.
id()==ID_floatbv)
3998 else if(type.
id()==ID_complex)
4005 "type should not be one of the unsupported types",
4014 if(expr.
type().
id()==ID_integer)
4022 else if(expr.
type().
id()==ID_unsignedbv ||
4023 expr.
type().
id()==ID_signedbv ||
4024 expr.
type().
id()==ID_fixedbv)
4026 if(expr.
op0().
type().
id()==ID_pointer &&
4032 base_type.id() != ID_empty,
"no pointer arithmetic over void pointers");
4034 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
4037 if(element_size >= 2)
4042 "bitvector width of operand shall be equal to the bitvector width of "
4051 if(element_size >= 2)
4064 else if(expr.
type().
id()==ID_floatbv)
4071 else if(expr.
type().
id()==ID_pointer)
4075 (expr.
op1().
type().
id() == ID_unsignedbv ||
4087 else if(expr.
type().
id() == ID_range)
4093 const auto size = range_type.get_to() - range_type.get_from() + 1;
4096 out <<
"(bvsub (bvsub ";
4100 out <<
") (_ bv" << range_type.get_from() <<
' ' << width
4110 expr.
type().
id() == ID_floatbv,
4111 "type of ieee floating point expression shall be floatbv");
4129 if(expr.
type().
id()==ID_unsignedbv ||
4130 expr.
type().
id()==ID_signedbv)
4132 if(expr.
type().
id()==ID_unsignedbv)
4142 else if(expr.
type().
id()==ID_fixedbv)
4147 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
4152 out <<
" (_ bv0 " << fraction_bits <<
")) ";
4154 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4160 else if(expr.
type().
id()==ID_floatbv)
4174 expr.
type().
id() == ID_floatbv,
4175 "type of ieee floating point expression shall be floatbv");
4206 "expression should have been converted to a variant with two operands");
4208 if(expr.
type().
id()==ID_unsignedbv ||
4209 expr.
type().
id()==ID_signedbv)
4220 else if(expr.
type().
id()==ID_floatbv)
4227 else if(expr.
type().
id()==ID_fixedbv)
4232 out <<
"((_ extract "
4233 << spec.
width+fraction_bits-1 <<
" "
4234 << fraction_bits <<
") ";
4238 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4242 out <<
"((_ sign_extend " << fraction_bits <<
") ";
4248 else if(expr.
type().
id()==ID_rational ||
4249 expr.
type().
id()==ID_integer ||
4250 expr.
type().
id()==ID_real)
4254 for(
const auto &op : expr.
operands())
4269 expr.
type().
id() == ID_floatbv,
4270 "type of ieee floating point expression shall be floatbv");
4289 expr.
type().
id() == ID_floatbv,
4290 "type of ieee floating point expression shall be floatbv");
4304 "smt2_convt::convert_floatbv_rem to be implemented when not using "
4315 std::size_t s=expr.
operands().size();
4330 "with expression should have been converted to a version with three "
4335 if(expr_type.
id()==ID_array)
4359 out <<
"(let ((distance? ";
4360 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4364 if(array_width>index_width)
4366 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4372 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4382 out <<
"(bvshl (_ bv" <<
power(2, sub_width) - 1 <<
" " << array_width
4384 out <<
"distance?)) ";
4388 out <<
"((_ zero_extend " << array_width-sub_width <<
") ";
4390 out <<
") distance?)))";
4393 else if(expr_type.
id() == ID_struct || expr_type.
id() == ID_struct_tag)
4396 expr_type.
id() == ID_struct_tag
4403 const irep_idt &component_name=index.
get(ID_component_name);
4407 "struct should have accessed component");
4411 const std::string &smt_typename =
datatype_map.at(expr_type);
4413 out <<
"(update-" << smt_typename <<
"." << component_name <<
" ";
4427 out <<
"(let ((?withop ";
4431 if(m.
width==struct_width)
4441 <<
"((_ extract " << (struct_width-1) <<
" "
4442 << m.
width <<
") ?withop) ";
4451 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
4456 out <<
"(concat (concat "
4457 <<
"((_ extract " << (struct_width-1) <<
" "
4460 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
4467 else if(expr_type.
id() == ID_union || expr_type.
id() == ID_union_tag)
4475 if(total_width==member_width)
4482 total_width > member_width,
4483 "total width should be greater than member_width as member_width is at "
4484 "most as large as total_width and the other case has been handled "
4487 out <<
"((_ extract "
4489 <<
" " << member_width <<
") ";
4496 else if(expr_type.
id()==ID_bv ||
4497 expr_type.
id()==ID_unsignedbv ||
4498 expr_type.
id()==ID_signedbv)
4513 "with expects struct, union, or array type, but got "+
4521 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4538 if(array_op_type.
id()==ID_array)
4573 out <<
"((_ extract " << sub_width-1 <<
" 0) ";
4577 out <<
"(bvmul (_ bv" << sub_width <<
" " << array_width <<
") ";
4581 if(array_width>index_width)
4583 out <<
"((_ zero_extend " << array_width-index_width <<
") ";
4589 out <<
"((_ extract " << array_width-1 <<
" 0) ";
4601 false,
"index with unsupported array type: " + array_op_type.
id_string());
4608 const typet &struct_op_type = struct_op.
type();
4611 if(struct_op_type.
id() == ID_struct || struct_op_type.
id() == ID_struct_tag)
4614 struct_op_type.
id() == ID_struct_tag
4619 struct_type.
has_component(name),
"struct should have accessed component");
4623 const std::string &smt_typename =
datatype_map.at(struct_type);
4625 out <<
"(" << smt_typename <<
"."
4636 if(expr.
type().
id() == ID_bool)
4642 if(expr.
type().
id() == ID_bool)
4647 struct_op_type.
id() == ID_union || struct_op_type.
id() == ID_union_tag)
4651 width != 0,
"failed to get union member width");
4657 out <<
"((_ extract " << (width - 1) <<
" 0) ";
4665 out <<
"((_ extract " << (width - 1) <<
" 0) ";
4672 "convert_member on an unexpected type "+struct_op_type.
id_string());
4679 if(type.
id()==ID_bool)
4685 else if(type.
id()==ID_array)
4696 std::size_t n_concat = 0;
4710 out << std::string(n_concat,
')');
4715 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4728 std::size_t n_concat = 0;
4729 for(std::size_t i=components.size(); i>1; i--)
4749 out << std::string(n_concat,
')');
4754 else if(type.
id()==ID_floatbv)
4758 "floatbv expressions should be flattened when using FPA theory");
4771 if(type.
id()==ID_bool)
4778 else if(type.
id() == ID_array)
4783 out <<
"(let ((?ufop" << nesting <<
" ";
4794 "cannot unflatten arrays of non-constant size");
4801 out <<
"((as const ";
4806 out <<
"((_ extract " << subtype_width - 1 <<
" "
4807 <<
"0) ?ufop" << nesting <<
")";
4811 std::size_t offset = subtype_width;
4812 for(
mp_integer i = 1; i < size; ++i, offset += subtype_width)
4817 out <<
"((_ extract " << offset + subtype_width - 1 <<
" " << offset
4818 <<
") ?ufop" << nesting <<
")";
4826 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
4832 out <<
"(let ((?ufop" << nesting <<
" ";
4837 const std::string &smt_typename =
datatype_map.at(type);
4839 out <<
"(mk-" << smt_typename;
4848 std::size_t offset=0;
4851 for(struct_typet::componentst::const_iterator
4852 it=components.begin();
4853 it!=components.end();
4863 out <<
"((_ extract " << offset+member_width-1 <<
" "
4864 << offset <<
") ?ufop" << nesting <<
")";
4866 offset+=member_width;
4887 if(expr.
id()==ID_and && value)
4889 for(
const auto &op : expr.
operands())
4894 if(expr.
id()==ID_or && !value)
4896 for(
const auto &op : expr.
operands())
4901 if(expr.
id()==ID_not)
4911 if(expr.
id() == ID_equal && value)
4920 if(equal_expr.
lhs().
id()==ID_symbol)
4927 equal_expr.
lhs() != equal_expr.
rhs())
4939 out <<
"; set_to true (equal)\n";
4941 if(equal_expr.
lhs().
type().
id() == ID_mathematical_function)
4945 out <<
"(declare-fun " << smt2_identifier;
4947 auto &mathematical_function_type =
4953 for(
auto &t : mathematical_function_type.domain())
4967 out <<
"(assert (= " << smt2_identifier <<
' ';
4969 out <<
')' <<
')' <<
'\n';
4973 out <<
"(define-fun " << smt2_identifier;
4978 equal_expr.
lhs().
type().
id() != ID_array ||
5006 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
5017 out << found_literal->second;
5040 exprt lowered_expr = expr;
5047 it->id() == ID_byte_extract_little_endian ||
5048 it->id() == ID_byte_extract_big_endian)
5053 it->id() == ID_byte_update_little_endian ||
5054 it->id() == ID_byte_update_big_endian)
5060 return lowered_expr;
5077 "lower_byte_operators should remove all byte operators");
5084 auto prophecy_r_or_w_ok =
5088 it.mutate() = lowered;
5089 it.next_sibling_or_parent();
5092 auto prophecy_pointer_in_range =
5096 it.mutate() = lowered;
5097 it.next_sibling_or_parent();
5106 return lowered_expr;
5117 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
5119 std::unordered_map<irep_idt, std::optional<identifiert>> shadowed_syms;
5124 for(
const auto &symbol : q_expr.variables())
5126 const auto identifier = symbol.get_identifier();
5129 shadowed_syms.insert(
5131 id_entry.second ? std::nullopt
5132 : std::optional{id_entry.first->second}});
5135 for(
const auto &[
id, shadowed_val] : shadowed_syms)
5138 if(!shadowed_val.has_value())
5141 previous_entry->second = std::move(*shadowed_val);
5147 for(
const auto &op : expr.
operands())
5150 if(expr.
id()==ID_symbol ||
5151 expr.
id()==ID_nondet_symbol)
5154 if(expr.
type().
id()==ID_code)
5159 if(expr.
id()==ID_symbol)
5162 identifier=
"nondet_"+
5173 out <<
"; find_symbols\n";
5174 out <<
"(declare-fun " << smt2_identifier;
5176 if(expr.
type().
id() == ID_mathematical_function)
5178 auto &mathematical_function_type =
5183 for(
auto &type : mathematical_function_type.domain())
5204 else if(expr.
id() == ID_array_of)
5211 const auto &array_type = array_of.type();
5215 out <<
"; the following is a substitute for lambda i. x\n";
5216 out <<
"(declare-fun " <<
id <<
" () ";
5223 out <<
"(assert (forall ((i ";
5225 out <<
")) (= (select " <<
id <<
" i) ";
5243 else if(expr.
id() == ID_array_comprehension)
5250 const auto &array_type = array_comprehension.type();
5251 const auto &array_size = array_type.size();
5255 out <<
"(declare-fun " <<
id <<
" () ";
5259 out <<
"; the following is a substitute for lambda i . x(i)\n";
5260 out <<
"; universally quantified initialization of the array\n";
5261 out <<
"(assert (forall ((";
5265 out <<
")) (=> (and (bvule (_ bv0 " <<
boolbv_width(array_size.type())
5272 out <<
")) (= (select " <<
id <<
" ";
5291 else if(expr.
id()==ID_array)
5298 out <<
"; the following is a substitute for an array constructor" <<
"\n";
5299 out <<
"(declare-fun " <<
id <<
" () ";
5305 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5307 out <<
"(assert (= (select " <<
id <<
" ";
5328 else if(expr.
id()==ID_string_constant)
5338 out <<
"; the following is a substitute for a string" <<
"\n";
5339 out <<
"(declare-fun " <<
id <<
" () ";
5343 for(std::size_t i=0; i<tmp.
operands().size(); i++)
5345 out <<
"(assert (= (select " <<
id <<
' ';
5349 out <<
"))" <<
"\n";
5362 out <<
"(declare-fun " <<
id <<
" () ";
5373 (expr.
id() == ID_floatbv_plus ||
5374 expr.
id() == ID_floatbv_minus ||
5375 expr.
id() == ID_floatbv_mult ||
5376 expr.
id() == ID_floatbv_div ||
5377 expr.
id() == ID_floatbv_typecast ||
5378 expr.
id() == ID_ieee_float_equal ||
5379 expr.
id() == ID_ieee_float_notequal ||
5380 ((expr.
id() == ID_lt ||
5381 expr.
id() == ID_gt ||
5382 expr.
id() == ID_le ||
5383 expr.
id() == ID_ge ||
5384 expr.
id() == ID_isnan ||
5385 expr.
id() == ID_isnormal ||
5386 expr.
id() == ID_isfinite ||
5387 expr.
id() == ID_isinf ||
5388 expr.
id() == ID_sign ||
5389 expr.
id() == ID_unary_minus ||
5390 expr.
id() == ID_typecast ||
5391 expr.
id() == ID_abs) &&
5398 if(
bvfp_set.insert(function).second)
5400 out <<
"; this is a model for " << expr.
id() <<
" : "
5403 <<
"(define-fun " << function <<
" (";
5405 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5409 out <<
"(op" << i <<
' ';
5419 for(std::size_t i = 0; i < tmp1.
operands().size(); i++)
5435 expr.
type().
id() == ID_bv)
5445 out <<
"(declare-fun " <<
id <<
" () ";
5451 out <<
"(assert (= ";
5452 out <<
"((_ to_fp " << floatbv_type.get_e() <<
" "
5453 << floatbv_type.get_f() + 1 <<
") " <<
id <<
')';
5461 else if(expr.
id() == ID_initial_state)
5463 irep_idt function =
"initial-state";
5467 out <<
"(declare-fun " << function <<
" (";
5474 else if(expr.
id() == ID_evaluate)
5480 out <<
"(declare-fun " << function <<
" (";
5490 expr.
id() == ID_state_is_cstring ||
5491 expr.
id() == ID_state_is_dynamic_object ||
5492 expr.
id() == ID_state_live_object || expr.
id() == ID_state_writeable_object)
5495 expr.
id() == ID_state_is_cstring ?
"state-is-cstring"
5496 : expr.
id() == ID_state_is_dynamic_object ?
"state-is-dynamic-object"
5497 : expr.
id() == ID_state_live_object ?
"state-live-object"
5498 :
"state-writeable-object";
5502 out <<
"(declare-fun " << function <<
" (";
5512 expr.
id() == ID_state_r_ok || expr.
id() == ID_state_w_ok ||
5513 expr.
id() == ID_state_rw_ok)
5515 irep_idt function = expr.
id() == ID_state_r_ok ?
"state-r-ok"
5516 : expr.
id() == ID_state_w_ok ?
"state-w-ok"
5521 out <<
"(declare-fun " << function <<
" (";
5532 else if(expr.
id() == ID_update_state)
5539 out <<
"(declare-fun " << function <<
" (";
5550 else if(expr.
id() == ID_enter_scope_state)
5557 out <<
"(declare-fun " << function <<
" (";
5568 else if(expr.
id() == ID_exit_scope_state)
5575 out <<
"(declare-fun " << function <<
" (";
5584 else if(expr.
id() == ID_allocate)
5590 out <<
"(declare-fun " << function <<
" (";
5599 else if(expr.
id() == ID_reallocate)
5605 out <<
"(declare-fun " << function <<
" (";
5616 else if(expr.
id() == ID_deallocate_state)
5622 out <<
"(declare-fun " << function <<
" (";
5631 else if(expr.
id() == ID_object_address)
5633 irep_idt function =
"object-address";
5637 out <<
"(declare-fun " << function <<
" (String) ";
5642 else if(expr.
id() == ID_field_address)
5648 out <<
"(declare-fun " << function <<
" (";
5657 else if(expr.
id() == ID_element_address)
5663 out <<
"(declare-fun " << function <<
" (";
5682 if(expr.
id() == ID_with)
5690 if(type.
id()==ID_array)
5704 out <<
"(_ BitVec 1)";
5710 else if(type.
id()==ID_bool)
5714 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
5724 out <<
"(_ BitVec " << width <<
")";
5727 else if(type.
id()==ID_code)
5734 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
5741 union_type.
components().empty() || width != 0,
5742 "failed to get width of union");
5744 out <<
"(_ BitVec " << width <<
")";
5746 else if(type.
id()==ID_pointer)
5751 else if(type.
id()==ID_bv ||
5752 type.
id()==ID_fixedbv ||
5753 type.
id()==ID_unsignedbv ||
5754 type.
id()==ID_signedbv ||
5755 type.
id()==ID_c_bool)
5760 else if(type.
id()==ID_c_enum)
5767 else if(type.
id()==ID_c_enum_tag)
5771 else if(type.
id()==ID_floatbv)
5776 out <<
"(_ FloatingPoint "
5777 << floatbv_type.
get_e() <<
" "
5778 << floatbv_type.
get_f() + 1 <<
")";
5783 else if(type.
id()==ID_rational ||
5786 else if(type.
id()==ID_integer)
5788 else if(type.
id()==ID_complex)
5798 out <<
"(_ BitVec " << width <<
")";
5801 else if(type.
id()==ID_c_bit_field)
5805 else if(type.
id() == ID_state)
5809 else if(type.
id() == ID_range)
5812 mp_integer size = range_type.get_to() - range_type.get_from() + 1;
5825 std::set<irep_idt> recstack;
5831 std::set<irep_idt> &recstack)
5833 if(type.
id()==ID_array)
5839 else if(type.
id()==ID_complex)
5846 const std::string smt_typename =
5850 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5851 <<
"(((mk-" << smt_typename;
5853 out <<
" (" << smt_typename <<
".imag ";
5857 out <<
" (" << smt_typename <<
".real ";
5864 else if(type.
id() == ID_struct)
5867 bool need_decl=
false;
5871 const std::string smt_typename =
5886 const std::string &smt_typename =
datatype_map.at(type);
5897 out <<
"(declare-datatypes ((" << smt_typename <<
" 0)) "
5898 <<
"(((mk-" << smt_typename <<
" ";
5905 out <<
"(" << smt_typename <<
"." <<
component.get_name()
5911 out <<
"))))" <<
"\n";
5928 for(struct_union_typet::componentst::const_iterator
5929 it=components.begin();
5930 it!=components.end();
5937 out <<
"(define-fun update-" << smt_typename <<
"."
5939 <<
"((s " << smt_typename <<
") "
5942 out <<
")) " << smt_typename <<
" "
5943 <<
"(mk-" << smt_typename
5946 for(struct_union_typet::componentst::const_iterator
5947 it2=components.begin();
5948 it2!=components.end();
5955 out <<
"(" << smt_typename <<
"."
5956 << it2->get_name() <<
" s) ";
5960 out <<
"))" <<
"\n";
5966 else if(type.
id() == ID_union)
5974 else if(type.
id()==ID_code)
5978 for(
const auto ¶m : parameters)
5983 else if(type.
id()==ID_pointer)
5987 else if(type.
id() == ID_struct_tag)
5990 const irep_idt &
id = struct_tag.get_identifier();
5992 if(recstack.find(
id) == recstack.end())
5994 const auto &base_struct =
ns.follow_tag(struct_tag);
5995 recstack.insert(
id);
6000 else if(type.
id() == ID_union_tag)
6003 const irep_idt &
id = union_tag.get_identifier();
6005 if(recstack.find(
id) == recstack.end())
6007 recstack.insert(
id);
6011 else if(type.
id() == ID_state)
6016 out <<
"(declare-sort state 0)\n";
6019 else if(type.
id() == ID_mathematical_function)
6021 const auto &mathematical_function_type =
6023 for(
auto &d_type : mathematical_function_type.domain())
API to expression classes for bitvectors.
const onehot0_exprt & to_onehot0_expr(const exprt &expr)
Cast an exprt to a onehot0_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
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.
const onehot_exprt & to_onehot_expr(const exprt &expr)
Cast an exprt to a onehot_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.
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 zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_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
The byte swap expression.
std::size_t get_bits_per_byte() const
std::vector< parametert > parameterst
const parameterst & parameters() const
A constant literal expression.
const irep_idt & get_value() const
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
resultt
Result of running the decision procedure.
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
Round a floating-point number to an integral value considering the given rounding mode.
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
An IEEE 754 floating-point value, including specificiation.
static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
static ieee_float_valuet one(const floatbv_typet &)
constant_exprt to_expr() const
static ieee_float_valuet zero(const floatbv_typet &type)
static ieee_float_valuet NaN(const ieee_float_spect &_spec)
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
The trinary if-then-else operator.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
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.
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 convert_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
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
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.
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)
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
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
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 floatbv_round_to_integral_exprt & to_floatbv_round_to_integral_expr(const exprt &expr)
Cast an exprt to a floatbv_round_to_integral_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)
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &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)
#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 cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_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 range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
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)