54#define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
57#define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
66 : use_FPA_theory(
false),
67 use_array_of_bool(
false),
69 use_check_sat_assuming(
false),
71 use_lambda_for_array(
false),
81 no_boolean_variables(0)
172 "variable number shall be within bounds");
178 out <<
"; SMT 2" <<
"\n";
187 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
197 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
199 out <<
"(set-option :produce-models true)" <<
"\n";
205 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
218 out <<
"(check-sat-assuming (";
228 out <<
"; assumptions\n";
239 out <<
"(check-sat)\n";
247 out <<
"(get-value (" <<
id <<
"))"
255 out <<
"; end of SMT2 file"
293 std::size_t number = 0;
294 std::size_t
h=pointer_width-1;
299 const typet &type = o.type();
311 out <<
"(assert (=> (= "
312 <<
"((_ extract " <<
h <<
" " << l <<
") ";
315 <<
"(= " <<
id <<
" ";
347 return it->second.value;
357 return it->second.value;
372 else if(op.is_false())
420 if(!src.
id().empty())
424 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
429 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
436 std::size_t
pos = s.find(
".");
437 if(
pos != std::string::npos)
459 "smt2_convt::parse_literal parsed a number with a decimal point "
468 else if(src.
get_sub().size()==2 &&
473 else if(src.
get_sub().size()==3 &&
476 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
492 else if(src.
get_sub().size()==4 &&
516 else if(src.
get_sub().size()==4 &&
525 else if(src.
get_sub().size()==4 &&
534 else if(src.
get_sub().size()==4 &&
544 src.
get_sub()[0].id() ==
"root-obj")
552 src.
get_sub()[1].id().empty() && src.
get_sub()[1].get_sub().size() == 3 &&
553 src.
get_sub()[1].get_sub()[0].id() ==
"+" &&
555 "unexpected root-obj expression",
562 !
failed,
"failed to parse rational constant coefficient", src.
pretty());
566 sum_lhs.get_sub()[0].id() ==
"^" &&
sum_lhs.get_sub()[1].id() ==
"x",
567 "unexpected first operand to root-obj",
571 degree > 0,
"polynomial degree must be positive", src.
pretty());
572 std::vector<rationalt> coefficients{degree + 1,
rationalt{}};
592 result.
type() = type;
613 "smt2_convt::parse_literal should not be of unsupported type " +
639 operands.emplace_back(
found_op->second);
652 operands.emplace_back(
found_op->second);
678 long index =
tempint.to_long();
682 else if(src.
get_sub().size()==2 &&
683 src.
get_sub()[0].get_sub().size()==3 &&
684 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
685 src.
get_sub()[0].get_sub()[1].id()==
"const")
722 if(components.empty())
730 for(std::size_t i=0; i<components.size(); i++)
740 src.
get_sub().size() > j,
"insufficient number of component values");
757 std::size_t offset=0;
759 for(std::size_t i=0; i<components.size(); i++)
768 "struct component bits shall be within struct bit vector");
791 for(
const auto &binding : src.
get_sub()[1].get_sub())
793 const irep_idt &name = binding.get_sub()[0].id();
878 const std::size_t
max_objects = std::size_t(1) << object_bits;
884 "too many addressed objects: maximum number of objects is set to 2^n=" +
886 " (with n=" + std::to_string(object_bits) +
"); " +
887 "use the `--object-bits n` option to increase the maximum number"};
890 out <<
"(concat (_ bv" <<
object_id <<
" " << object_bits <<
")"
891 <<
" (_ bv0 " <<
boolbv_width(result_type) - object_bits <<
"))";
933 "member expression operand shall have struct type");
968 "operand of address of expression should not be of kind " +
1004 out <<
"; convert\n";
1005 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
1015 out <<
"(declare-fun ";
1017 out <<
" () Bool)\n";
1018 out <<
"(assert (= ";
1030 out <<
"(define-fun " << identifier <<
" () Bool ";
1058 const auto identifier =
1091 if(identifier.empty())
1116 std::string result =
"|";
1118 for(
auto ch : identifier)
1126 result+=std::to_string(
ch);
1146 return "f"+std::to_string(spec.
width())+
"_"+std::to_string(spec.
f);
1223 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
1229 for(
const auto &op : expr.
operands())
1271 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1308 "concatenation over a single operand should have matching types",
1319 "given expression should have at least two operands",
1337 for(
const auto &op : expr.
operands())
1368 else if(expr.
operands().size() == 1)
1374 else if(expr.
operands().size() >= 3)
1384 for(
const auto &op : expr.
operands())
1396 expr.
id_string() +
" should have at least one operand");
1410 const auto &type = expr.
type();
1464 out <<
"(fp.isNegative ";
1482 "sign should not be applied to unsupported type",
1529 "logical and, or, and xor expressions should have Boolean type");
1532 "logical and, or, and xor expressions should have at least two operands");
1534 out <<
"(" << expr.
id();
1535 for(
const auto &op : expr.
operands())
1546 "logical nand, nor, xnor expressions should have Boolean type");
1549 "logical nand, nor, xnor expressions should have at least one operand");
1565 for(
const auto &op : expr.
operands())
1579 implies_expr.is_boolean(),
"implies expression should have Boolean type");
1592 not_expr.is_boolean(),
"not expression should have Boolean type");
1604 "operands of equal expression shall have same type");
1625 "operands of not equal expression shall have same type");
1642 "operands of float equal and not equal expressions shall have same type");
1725 "array of expression shall have array type");
1729 out <<
"((as const ";
1737 defined_expressionst::const_iterator it =
1749 "array_comprehension expression shall have array type");
1753 out <<
"(lambda ((";
1835 "unsupported distance type for " +
shift_expr.id_string() +
": " +
1843 "unsupported type for " +
shift_expr.id_string() +
": " +
1858 out <<
"((_ rotate_left";
1860 out <<
"((_ rotate_right";
1874 "distance type for " +
shift_expr.id_string() +
"must be constant");
1883 "unsupported type for " +
shift_expr.id_string() +
": " +
1912 out <<
"(object-address ";
1955 "operand of pointer offset expression shall be of pointer type");
1982 "pointer object expressions should be of pointer type");
1988 out <<
"((_ zero_extend " <<
ext <<
") ";
1990 out <<
"((_ extract "
1991 << pointer_width-1 <<
" "
2007 out <<
"(= ((_ extract "
2008 << pointer_width-1 <<
" "
2029 out <<
"(= ((_ extract " << i <<
" " << i <<
") ";
2035 out <<
"(= ((_ extract 0 0) ";
2070 out <<
"(= ((_ extract 0 0) ";
2079 SMT2_TODO(
"smt2: extractbits with non-constant index");
2088 out <<
"((_ repeat " << times <<
") ";
2096 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
2102 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
2114 out <<
"(ite (bvslt ";
2127 out <<
"(ite (bvslt ";
2162 out <<
"(fp.isNaN ";
2186 out <<
"(not (fp.isNaN ";
2190 out <<
"(not (fp.isInfinite ";
2214 out <<
"(fp.isInfinite ";
2236 out <<
"(fp.isNormal ";
2259 "overflow plus and overflow minus expressions shall be of Boolean type");
2269 out <<
"(let ((?sum (";
2270 out << (subtract?
"bvsub":
"bvadd");
2271 out <<
" ((_ sign_extend 1) ";
2274 out <<
" ((_ sign_extend 1) ";
2289 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2294 "((_ extract " << width <<
" " << width <<
") ?sum) "
2295 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
2309 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2310 out <<
" ((_ zero_extend 1) ";
2313 out <<
" ((_ zero_extend 1) ";
2326 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2330 out <<
"((_ extract " << width <<
" " << width <<
") ?sum)";
2341 "overflow check should not be performed on unsupported type",
2355 "overflow mult expression shall be of Boolean type");
2365 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
2367 out <<
") ((_ sign_extend " << width <<
") ";
2382 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2386 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
2388 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width - 1) <<
" "
2389 << width * 2 <<
"))))";
2400 out <<
"(let ((prod (bvmul ((_ zero_extend " << width <<
") ";
2402 out <<
") ((_ zero_extend " << width <<
") ";
2417 out <<
" ((_ extract " << width - 1 <<
" 0) prod) ";
2421 out <<
"(bvuge prod (_ bv" <<
power(2, width) <<
" " << width * 2 <<
"))";
2433 "overflow check should not be performed on unsupported type",
2448 out <<
"(let ((?sum (";
2449 out << (subtract ?
"bvsub" :
"bvadd");
2450 out <<
" ((_ sign_extend 1) ";
2453 out <<
" ((_ sign_extend 1) ";
2460 << width <<
" " << width
2463 << (width - 1) <<
" " << (width - 1) <<
") ?sum)";
2467 out <<
"((_ extract " << width - 1 <<
" 0) ?sum) ";
2470 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2482 out <<
"(let ((?sum (" << (subtract ?
"bvsub" :
"bvadd");
2483 out <<
" ((_ zero_extend 1) ";
2486 out <<
" ((_ zero_extend 1) ";
2491 out <<
"(ite (= ((_ extract " << width <<
" " << width <<
") ?sum) #b0) ";
2494 out <<
" ((_ extract " << width - 1 <<
" 0) ?sum) ";
2508 "saturating_plus/minus on unsupported type",
2528 throw "MathSAT does not support quantifiers";
2563 const auto &variables =
let_expr.variables();
2564 const auto &values =
let_expr.values();
2569 for(
auto &binding :
make_range(variables).zip(values))
2591 "smt2_convt::convert_expr: '" + expr.
id_string() +
2592 "' is not yet supported");
2600 "operand of byte swap expression shall have same type as the expression");
2603 out <<
"(let ((bswap_op ";
2611 const std::size_t width =
2619 "bit width indicated by type of bswap expression should be a multiple "
2620 "of the number of bits per byte");
2631 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2635 out <<
"(bswap_byte_" <<
byte <<
' ';
2646 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2647 out <<
" bswap_byte_" <<
byte;
2710 "smt2_convt::convert_expr should not be applied to unsupported "
2747 out <<
"(not (fp.isZero ";
2792 out <<
"((_ sign_extend ";
2794 out <<
"((_ zero_extend ";
2819 out <<
"(let ((?tcop ";
2827 out <<
"((_ sign_extend "
2842 out <<
" (ite (and ";
2866 defined_expressionst::const_iterator it =
2881 "typecast unexpected "+
src_type.id_string()+
" -> "+
2888 "typecast unexpected "+
src_type.id_string()+
" -> "+
2900 out <<
" (concat (_ bv1 "
2903 "(_ bv0 " << spec.
width <<
")";
2919 out <<
"((_ sign_extend ";
2941 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2951 "bit vector with of source and destination type shall be equal");
2958 "bit vector with of source and destination type shall be equal");
2968 "bit vector with of source and destination type shall be equal");
2986 std::ostringstream
e_str;
2988 <<
" src == " <<
format(src);
3021 "from_width should be smaller than to_integer_bits as other case "
3022 "have been handled above");
3025 out <<
"(_ zero_extend "
3032 out <<
"((_ sign_extend "
3044 out <<
"(concat (concat"
3058 out <<
"(let ((?tcop ";
3066 out <<
"((_ extract "
3075 "to_integer_bits should be greater than from_integer_bits as the"
3076 "other case has been handled above");
3077 out <<
"((_ sign_extend "
3089 out <<
"((_ extract "
3098 "to_fraction_bits should be greater than from_fraction_bits as the"
3099 "other case has been handled above");
3100 out <<
"(concat ((_ extract "
3134 out <<
"((_ sign_extend "
3263 "Unknown typecast " +
src_type.id_string() +
" -> rational");
3306 out <<
"((_ to_fp " <<
dst.get_e() <<
" "
3307 <<
dst.get_f() + 1 <<
") ";
3337 out <<
"((_ to_fp_unsigned " <<
dst.get_e() <<
" "
3338 <<
dst.get_f() + 1 <<
") ";
3355 out <<
"((_ to_fp " <<
dst.get_e() <<
" "
3356 <<
dst.get_f() + 1 <<
") ";
3421 out <<
"(fp.roundToIntegral ";
3442 components.size() == expr.
operands().size(),
3443 "number of struct components as indicated by the struct type shall be equal"
3444 "to the number of operands of the struct expression");
3446 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
3456 for(struct_typet::componentst::const_iterator
3457 it=components.begin();
3458 it!=components.end();
3475 else if(op.type().id() ==
ID_bool)
3483 for(std::size_t i = components.size(); i > 1; i--)
3515 out <<
"(let ((?far ";
3523 out <<
"(select ?far ";
3554 "total_width should be greater than member_width as member_width can be"
3555 "at most as large as total_width and the other case has been handled "
3581 out <<
"(_ bv" << value
3582 <<
" " << width <<
")";
3590 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
3612 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3618 out <<
"(_ NaN " << e <<
" " << f <<
")";
3623 out <<
"(_ -oo " << e <<
" " << f <<
")";
3625 out <<
"(_ +oo " << e <<
" " << f <<
")";
3645 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3662 out <<
"(_ bv" << value <<
" " << width <<
")";
3688 value = value.substr(1);
3691 size_t pos=value.find(
"/");
3693 if(
pos==std::string::npos)
3694 out << value <<
".0";
3697 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3698 << value.substr(
pos+1) <<
".0)";
3708 if(value.find(
'.') == std::string::npos)
3717 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3750 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3783 out <<
"(let ((?obj ((_ extract "
3784 << pointer_width-1 <<
" "
3799 out <<
" (= (_ bv" <<
object
3928 for(
const auto &op : expr.
operands())
3998 "one of the operands should have pointer type");
4002 base_type.id() !=
ID_empty,
"no pointer arithmetic over void pointers");
4009 out <<
"(let ((?pointerop ";
4020 <<
") ?pointerop) ";
4021 out <<
"(bvadd ((_ extract " <<
offset_bits - 1 <<
" 0) ?pointerop) ";
4070 out <<
"roundNearestTiesToEven";
4072 out <<
"roundTowardNegative";
4074 out <<
"roundTowardPositive";
4076 out <<
"roundTowardZero";
4078 out <<
"roundNearestTiesToAway";
4082 "Rounding mode should have value 0, 1, 2, 3, or 4",
4090 out <<
"(ite (= (_ bv0 " << width <<
") ";
4092 out <<
") roundNearestTiesToEven ";
4094 out <<
"(ite (= (_ bv1 " << width <<
") ";
4096 out <<
") roundTowardNegative ";
4098 out <<
"(ite (= (_ bv2 " << width <<
") ";
4100 out <<
") roundTowardPositive ";
4102 out <<
"(ite (= (_ bv3 " << width <<
") ";
4104 out <<
") roundTowardZero ";
4107 out <<
"roundNearestTiesToAway";
4141 "type should not be one of the unsupported types",
4170 base_type.id() !=
ID_empty,
"no pointer arithmetic over void pointers");
4180 "bitvector width of operand shall be equal to the bitvector width of "
4234 out <<
"(bvsub (bvsub ";
4249 "type of ieee floating point expression shall be floatbv");
4285 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
4323 "type of ieee floating point expression shall be floatbv");
4346 tmp.operands().pop_back();
4354 "expression should have been converted to a variant with two operands");
4380 out <<
"((_ extract "
4402 for(
const auto &op : expr.
operands())
4418 "type of ieee floating point expression shall be floatbv");
4438 "type of ieee floating point expression shall be floatbv");
4452 "smt2_convt::convert_floatbv_rem to be implemented when not using "
4461 "with expression should have exactly three operands");
4489 out <<
"(let ((distance? ";
4514 out <<
"distance?)) ";
4520 out <<
") distance?)))";
4537 "struct should have accessed component");
4556 else if(op.type().id() ==
ID_bool)
4575 out <<
"(let ((?withop ";
4593 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
4598 out <<
"(concat (concat "
4602 out <<
") ((_ extract " << (m.
offset - 1) <<
" 0) ?withop)";
4626 "total width should be greater than member_width as member_width is at "
4627 "most as large as total_width and the other case has been handled "
4630 out <<
"((_ extract "
4656 "with expects struct, union, or array type, but got "+
4664 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4744 false,
"index with unsupported array type: " +
array_op_type.id_string());
4762 struct_type.has_component(name),
"struct should have accessed component");
4794 width != 0,
"failed to get union member width");
4800 out <<
"((_ extract " << (width - 1) <<
" 0) ";
4808 out <<
"((_ extract " << (width - 1) <<
" 0) ";
4815 "convert_member on an unexpected type "+
struct_op_type.id_string());
4872 for(std::size_t i=components.size(); i>1; i--)
4901 "floatbv expressions should be flattened when using FPA theory");
4937 "cannot unflatten arrays of non-constant size");
4944 out <<
"((as const ";
4950 <<
"0) ?ufop" <<
nesting <<
")";
4961 <<
") ?ufop" <<
nesting <<
")";
4991 std::size_t offset=0;
4994 for(struct_typet::componentst::const_iterator
4995 it=components.begin();
4996 it!=components.end();
5007 << offset <<
") ?ufop" <<
nesting <<
")";
5032 for(
const auto &op : expr.
operands())
5037 if(expr.
id()==
ID_or && !value)
5039 for(
const auto &op : expr.
operands())
5082 out <<
"; set_to true (equal)\n";
5112 out <<
')' <<
')' <<
'\n';
5149 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
5220 "lower_byte_operators should remove all byte operators");
5232 it.next_sibling_or_parent();
5240 it.next_sibling_or_parent();
5262 std::unordered_map<irep_idt, std::optional<identifiert>>
shadowed_syms;
5267 for(
const auto &symbol :
q_expr.variables())
5269 const auto identifier = symbol.get_identifier();
5275 : std::optional{
id_entry.first->second}});
5290 for(
const auto &op : expr.
operands())
5305 identifier=
"nondet_"+
5316 out <<
"; find_symbols\n";
5358 out <<
"; the following is a substitute for lambda i. x\n";
5359 out <<
"(declare-fun " <<
id <<
" () ";
5366 out <<
"(assert (forall ((i ";
5368 out <<
")) (= (select " <<
id <<
" i) ";
5398 out <<
"(declare-fun " <<
id <<
" () ";
5402 out <<
"; the following is a substitute for lambda i . x(i)\n";
5403 out <<
"; universally quantified initialization of the array\n";
5404 out <<
"(assert (forall ((";
5415 out <<
")) (= (select " <<
id <<
" ";
5441 out <<
"; the following is a substitute for an array constructor" <<
"\n";
5442 out <<
"(declare-fun " <<
id <<
" () ";
5448 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5450 out <<
"(assert (= (select " <<
id <<
" ";
5481 out <<
"; the following is a substitute for a string" <<
"\n";
5482 out <<
"(declare-fun " <<
id <<
" () ";
5486 for(std::size_t i=0; i<
tmp.operands().size(); i++)
5488 out <<
"(assert (= (select " <<
id <<
' ';
5492 out <<
"))" <<
"\n";
5505 out <<
"(declare-fun " <<
id <<
" () ";
5541 if(
bvfp_set.insert(function).second)
5543 out <<
"; this is a model for " << expr.
id() <<
" : "
5546 <<
"(define-fun " << function <<
" (";
5548 for(std::size_t i = 0; i < expr.
operands().size(); i++)
5552 out <<
"(op" << i <<
' ';
5562 for(std::size_t i = 0; i <
tmp1.operands().size(); i++)
5588 out <<
"(declare-fun " <<
id <<
" () ";
5594 out <<
"(assert (= ";
5606 irep_idt function =
"initial-state";
5610 out <<
"(declare-fun " << function <<
" (";
5623 out <<
"(declare-fun " << function <<
" (";
5641 :
"state-writeable-object";
5645 out <<
"(declare-fun " << function <<
" (";
5664 out <<
"(declare-fun " << function <<
" (";
5682 out <<
"(declare-fun " << function <<
" (";
5700 out <<
"(declare-fun " << function <<
" (";
5718 out <<
"(declare-fun " << function <<
" (";
5733 out <<
"(declare-fun " << function <<
" (";
5748 out <<
"(declare-fun " << function <<
" (";
5765 out <<
"(declare-fun " << function <<
" (";
5776 irep_idt function =
"object-address";
5780 out <<
"(declare-fun " << function <<
" (String) ";
5791 out <<
"(declare-fun " << function <<
" (";
5806 out <<
"(declare-fun " << function <<
" (";
5847 out <<
"(_ BitVec 1)";
5867 out <<
"(_ BitVec " << width <<
")";
5884 union_type.components().empty() || width != 0,
5885 "failed to get width of union");
5887 out <<
"(_ BitVec " << width <<
")";
5919 out <<
"(_ FloatingPoint "
5943 out <<
"(_ BitVec " << width <<
")";
6056 out <<
"))))" <<
"\n";
6073 for(struct_union_typet::componentst::const_iterator
6074 it=components.begin();
6075 it!=components.end();
6091 for(struct_union_typet::componentst::const_iterator
6092 it2=components.begin();
6093 it2!=components.end();
6101 <<
it2->get_name() <<
" s) ";
6105 out <<
"))" <<
"\n";
6123 for(
const auto &
param : parameters)
6161 out <<
"(declare-sort state 0)\n";
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)
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.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Represents real numbers as roots (zeros) of a polynomial with rational coefficients.
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.
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.
const membert & get_member(const struct_typet &type, const irep_idt &member) const
The byte swap expression.
std::vector< parametert > parameterst
struct configt::bv_encodingt bv_encoding
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.
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.
bool is_boolean() const
Return whether the expression represents a Boolean.
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.
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.
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 &)
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.
Extract member of struct or union.
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...
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 ...
A base class for quantifier expressions.
Unbounded, signed rational numbers.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
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)
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
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
The unary minus expression.
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Replaces a sub-range of a bit-vector operand.
exprt lower() const
A lowering to masking, shifting, or.
Replaces a sub-range of a bit-vector operand.
exprt lower() const
A lowering to masking, shifting, or.
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
Forward depth-first search iterators These iterators' copy operations are expensive,...
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
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.
double pow(double x, double y)
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 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)
static bool failed(bool error_indicator)