51#define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
54#define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
63 : use_FPA_theory(
false),
64 use_array_of_bool(
false),
66 use_check_sat_assuming(
false),
68 use_lambda_for_array(
false),
78 no_boolean_variables(0)
151 "variable number shall be within bounds");
157 out <<
"; SMT 2" <<
"\n";
165 out <<
"; Generated for the CPROVER SMT2 solver\n";
break;
174 out <<
"(set-info :source \"" <<
notes <<
"\")" <<
"\n";
176 out <<
"(set-option :produce-models true)" <<
"\n";
182 out <<
"(set-logic " <<
logic <<
")" <<
"\n";
195 out <<
"(check-sat-assuming (";
205 out <<
"; assumptions\n";
216 out <<
"(check-sat)\n";
224 out <<
"(get-value (|" <<
id <<
"|))"
232 out <<
"; end of SMT2 file"
244 std::size_t number = 0;
245 std::size_t
h=pointer_width-1;
250 const typet &type = o.type();
263 out <<
"(assert (=> (= "
264 <<
"((_ extract " <<
h <<
" " << l <<
") ";
290 return it->second.value;
300 return it->second.value;
323 else if(op.is_false())
333 element =
get(element);
368 if(s.size()>=2 && s[0]==
'#' && s[1]==
'b')
373 else if(s.size()>=2 && s[0]==
'#' && s[1]==
'x')
384 else if(src.
get_sub().size()==2 &&
389 else if(src.
get_sub().size()==3 &&
392 src.
get_sub()[1].id_string().substr(0, 2)==
"bv")
396 else if(src.
get_sub().size()==4 &&
420 else if(src.
get_sub().size()==4 &&
428 else if(src.
get_sub().size()==4 &&
436 else if(src.
get_sub().size()==4 &&
458 result.
type() = type;
475 "smt2_convt::parse_literal should not be of unsupported type " +
501 operands.emplace_back(
found_op->second);
514 operands.emplace_back(
found_op->second);
540 long index =
tempint.to_long();
544 else if(src.
get_sub().size() == 3 && src.
get_sub()[0].id() ==
"let")
552 else if(src.
get_sub().size()==2 &&
553 src.
get_sub()[0].get_sub().size()==3 &&
554 src.
get_sub()[0].get_sub()[0].id()==
"as" &&
555 src.
get_sub()[0].get_sub()[1].id()==
"const")
586 if(components.empty())
594 if(src.
get_sub().size()!=components.size()+1)
597 for(std::size_t
i=0;
i<components.size();
i++)
614 std::size_t offset=0;
616 for(std::size_t
i=0;
i<components.size();
i++)
622 "struct component bits shall be within struct bit vector");
758 "member expression operand shall have struct type");
790 "operand of address of expression should not be of kind " +
816 out <<
"; convert\n";
817 out <<
"; Converting var_no " << l.
var_no() <<
" with expr ID of "
824 std::string{
"|B"} + std::to_string(l.
var_no()) +
"|";
825 out <<
"(define-fun ";
888 for(std::size_t
i=0;
i<identifier.
size();
i++)
890 char ch=identifier[
i];
898 result+=std::to_string(
ch);
916 return "f"+std::to_string(spec.
width())+
"_"+std::to_string(spec.
f);
974 !expr.
operands().empty(),
"non-symbol expressions shall have operands");
976 out <<
"(|float_bv." << expr.
id()
1001 DATA_INVARIANT(!
id.empty(),
"nondet symbol must have identifier");
1034 "concatenation over a single operand should have matching types",
1048 "given expression should have at least two operands",
1089 out <<
"(let ((?vectorop ";
1154 out <<
"(let ((?vectorop ";
1196 out <<
"(fp.isNegative ";
1214 "sign should not be applied to unsupported type",
1235 "logical and, or, and xor expressions should have Boolean type");
1238 "logical and, or, and xor expressions should have at least two operands");
1240 out <<
"(" << expr.
id();
1254 "implies expression should have Boolean type");
1268 "not expression should have Boolean type");
1280 "operands of equal expression shall have same type");
1294 "operands of not equal expression shall have same type");
1311 "operands of float equal and not equal expressions shall have same type");
1394 "array of expression shall have array type");
1398 out <<
"((as const ";
1406 defined_expressionst::const_iterator it =
1418 "array_comprehension expression shall have array type");
1422 out <<
"(lambda ((";
1503 "unsupported distance type for " +
shift_expr.id_string() +
": " +
1510 "unsupported type for " +
shift_expr.id_string() +
": " +
1525 out <<
"((_ rotate_left";
1527 out <<
"((_ rotate_right";
1541 "distance type for " +
shift_expr.id_string() +
"must be constant");
1550 "unsupported type for " +
shift_expr.id_string() +
": " +
1571 "operand of pointer offset expression shall be of pointer type");
1598 "pointer object expressions should be of pointer type");
1604 out <<
"((_ zero_extend " <<
ext <<
") ";
1606 out <<
"((_ extract "
1607 << pointer_width-1 <<
" "
1623 out <<
"(= ((_ extract "
1624 << pointer_width-1 <<
" "
1645 out <<
"(= ((_ extract " <<
i <<
" " <<
i <<
") ";
1651 out <<
"(= ((_ extract 0 0) ";
1685 out <<
"(= ((_ extract 0 0) ";
1694 SMT2_TODO(
"smt2: extractbits with non-constant index");
1703 out <<
"((_ repeat " << times <<
") ";
1711 false,
"byte_extract ops should be lowered in prepare_for_convert_expr");
1717 false,
"byte_update ops should be lowered in prepare_for_convert_expr");
1729 out <<
"(ite (bvslt ";
1742 out <<
"(ite (bvslt ";
1777 out <<
"(fp.isNaN ";
1801 out <<
"(not (fp.isNaN ";
1805 out <<
"(not (fp.isInf ";
1829 out <<
"(fp.isInfinite ";
1851 out <<
"(fp.isNormal ";
1869 "overflow plus and overflow minus expressions shall be of Boolean type");
1878 out <<
"(let ((?sum (";
1879 out << (subtract?
"bvsub":
"bvadd");
1880 out <<
" ((_ sign_extend 1) ";
1883 out <<
" ((_ sign_extend 1) ";
1887 "((_ extract " << width <<
" " << width <<
") ?sum) "
1888 "((_ extract " << (width-1) <<
" " << (width-1) <<
") ?sum)";
1896 out <<
"((_ extract " << width <<
" " << width <<
") ";
1897 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1898 out <<
" ((_ zero_extend 1) ";
1901 out <<
" ((_ zero_extend 1) ";
1909 "overflow check should not be performed on unsupported type",
1919 "overflow mult expression shall be of Boolean type");
1929 out <<
"(let ( (prod (bvmul ((_ sign_extend " << width <<
") ";
1931 out <<
") ((_ sign_extend " << width <<
") ";
1934 out <<
"(or (bvsge prod (_ bv" <<
power(2, width-1) <<
" "
1936 out <<
" (bvslt prod (bvneg (_ bv" <<
power(2, width-1) <<
" "
1937 << width*2 <<
")))))";
1941 out <<
"(bvuge (bvmul ((_ zero_extend " << width <<
") ";
1943 out <<
") ((_ zero_extend " << width <<
") ";
1945 out <<
")) (_ bv" <<
power(2, width) <<
" " << width*2 <<
"))";
1950 "overflow check should not be performed on unsupported type",
1970 throw "MathSAT does not support quantifiers";
2001 "size indicated by type shall be equal to the number of operands");
2028 const auto &variables =
let_expr.variables();
2029 const auto &values =
let_expr.values();
2034 for(
auto &binding :
make_range(variables).zip(values))
2056 "smt2_convt::convert_expr: '" + expr.
id_string() +
2057 "' is not yet supported");
2065 "operand of byte swap expression shall have same type as the expression");
2068 out <<
"(let ((bswap_op ";
2076 const std::size_t width =
2084 "bit width indicated by type of bswap expression should be a multiple "
2085 "of the number of bits per byte");
2096 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2100 out <<
"(bswap_byte_" <<
byte <<
' ';
2111 for(std::size_t
byte = 0;
byte < bytes;
byte++)
2112 out <<
" bswap_byte_" <<
byte;
2146 "smt2_convt::convert_expr should not be applied to unsupported type",
2182 out <<
"(not (fp.isZero ";
2227 out <<
"((_ sign_extend ";
2229 out <<
"((_ zero_extend ";
2254 out <<
"(let ((?tcop ";
2262 out <<
"((_ sign_extend "
2277 out <<
" (ite (and ";
2316 "typecast unexpected "+
src_type.id_string()+
" -> "+
2323 "typecast unexpected "+
src_type.id_string()+
" -> "+
2335 out <<
" (concat (_ bv1 "
2338 "(_ bv0 " << spec.
width <<
")";
2354 out <<
"((_ sign_extend ";
2376 SMT2_TODO(
"can't convert non-constant integer to bitvector");
2386 "bit vector with of source and destination type shall be equal");
2393 "bit vector with of source and destination type shall be equal");
2403 "bit vector with of source and destination type shall be equal");
2421 std::ostringstream
e_str;
2423 <<
" src == " <<
format(src);
2456 "from_width should be smaller than to_integer_bits as other case "
2457 "have been handled above");
2460 out <<
"(_ zero_extend "
2467 out <<
"((_ sign_extend "
2479 out <<
"(concat (concat"
2493 out <<
"(let ((?tcop ";
2501 out <<
"((_ extract "
2510 "to_integer_bits should be greater than from_integer_bits as the"
2511 "other case has been handled above");
2512 out <<
"((_ sign_extend "
2524 out <<
"((_ extract "
2533 "to_fraction_bits should be greater than from_fraction_bits as the"
2534 "other case has been handled above");
2535 out <<
"(concat ((_ extract "
2569 out <<
"((_ sign_extend "
2613 a.build(significand, exponent);
2621 a.build(significand, exponent);
2719 out <<
"((_ to_fp " <<
dst.get_e() <<
" "
2720 <<
dst.get_f() + 1 <<
") ";
2750 out <<
"((_ to_fp_unsigned " <<
dst.get_e() <<
" "
2751 <<
dst.get_f() + 1 <<
") ";
2768 out <<
"((_ to_fp " <<
dst.get_e() <<
" "
2769 <<
dst.get_f() + 1 <<
") ";
2835 components.size() == expr.
operands().size(),
2836 "number of struct components as indicated by the struct type shall be equal"
2837 "to the number of operands of the struct expression");
2839 DATA_INVARIANT(!components.empty(),
"struct shall have struct components");
2849 for(struct_typet::componentst::const_iterator
2850 it=components.begin();
2851 it!=components.end();
2862 if(components.size()==1)
2867 for(std::size_t
i=components.size();
i>1;
i--)
2884 for(std::size_t
i=1;
i<components.size();
i++)
2900 out <<
"(let ((?far ";
2908 out <<
"(select ?far ";
2929 total_width != 0,
"failed to get union width for union");
2933 member_width != 0,
"failed to get union member width for union");
2944 "total_width should be greater than member_width as member_width can be"
2945 "at most as large as total_width and the other case has been handled "
2971 out <<
"(_ bv" << value
2972 <<
" " << width <<
")";
2980 out <<
"(_ bv" << v <<
" " << spec.
width <<
")";
3002 out <<
"((_ to_fp " << e <<
" " << f <<
")"
3008 out <<
"(_ NaN " << e <<
" " << f <<
")";
3013 out <<
"(_ -oo " << e <<
" " << f <<
")";
3015 out <<
"(_ +oo " << e <<
" " << f <<
")";
3035 out <<
"(_ bv" << v <<
" " << spec.
width() <<
")";
3073 size_t pos=value.find(
"/");
3075 if(
pos==std::string::npos)
3076 out << value <<
".0";
3079 out <<
"(/ " << value.substr(0,
pos) <<
".0 "
3080 << value.substr(
pos+1) <<
".0)";
3092 out <<
"(- " << value.substr(1, std::string::npos) <<
')';
3112 "unsupported type for euclidean_mod: " + expr.
type().
id_string());
3145 out <<
"(let ((?obj ((_ extract "
3146 << pointer_width-1 <<
" "
3161 out <<
" (= (_ bv" <<
object
3287 for(
const auto &op : expr.
operands())
3332 "one of the operands should have pointer type");
3393 for(
const auto &op : expr.
operands())
3434 out <<
"roundNearestTiesToEven";
3436 out <<
"roundTowardNegative";
3438 out <<
"roundTowardPositive";
3440 out <<
"roundTowardZero";
3444 "Rounding mode should have value 0, 1, 2, or 3",
3452 out <<
"(ite (= (_ bv0 " << width <<
") ";
3454 out <<
") roundNearestTiesToEven ";
3456 out <<
"(ite (= (_ bv1 " << width <<
") ";
3458 out <<
") roundTowardNegative ";
3460 out <<
"(ite (= (_ bv2 " << width <<
") ";
3462 out <<
") roundTowardPositive ";
3465 out <<
"roundTowardZero";
3505 "type should not be one of the unsupported types",
3539 "bitvector width of operand shall be equal to the bitvector width of "
3613 "type of ieee floating point expression shall be floatbv");
3649 out <<
"((_ extract " << spec.
width-1 <<
" 0) ";
3677 "type of ieee floating point expression shall be floatbv");
3700 tmp.operands().pop_back();
3708 "expression should have been converted to a variant with two operands");
3734 out <<
"((_ extract "
3772 "type of ieee floating point expression shall be floatbv");
3792 "type of ieee floating point expression shall be floatbv");
3806 "smt2_convt::convert_floatbv_rem to be implemented when not using "
3817 std::size_t s=expr.
operands().size();
3821 tmp.operands().resize(s-2);
3832 "with expression should have been converted to a version with three "
3861 out <<
"(let ((distance? ";
3886 out <<
"distance?)) ";
3892 out <<
") distance?)))";
3906 "struct should have accessed component");
3926 out <<
"(let ((?withop ";
3941 << m.
width <<
") ?withop) ";
3950 out <<
" ((_ extract " << (m.
offset - 1) <<
" 0) ?withop))";
3955 out <<
"(concat (concat "
3959 out <<
") ((_ extract " << (m.
offset-1) <<
" 0) ?withop)";
3974 total_width != 0,
"failed to get union width for with");
3978 member_width != 0,
"failed to get union member width for with");
3988 "total width should be greater than member_width as member_width is at "
3989 "most as large as total_width and the other case has been handled "
3992 out <<
"((_ extract "
4009 total_width != 0,
"failed to get total width");
4028 out <<
" (bvnot (bvshl";
4054 "with expects struct, union, or array type, but got "+
4062 SMT2_TODO(
"smt2_convt::convert_update to be implemented");
4144 SMT2_TODO(
"non-constant index on vectors");
4160 false,
"index with unsupported array type: " +
array_op_type.id_string());
4175 struct_type.has_component(name),
"struct should have accessed component");
4194 member_offset.has_value(),
"failed to get struct member offset");
4207 width != 0,
"failed to get union member width");
4211 out <<
"((_ extract "
4221 "convert_member on an unexpected type "+
struct_op_type.id_string());
4245 out <<
"(let ((?vflop ";
4274 out <<
"(let ((?sflop ";
4282 for(std::size_t
i=components.size();
i>1;
i--)
4285 << components[
i-1].get_name() <<
" ?sflop)";
4291 << components[0].get_name() <<
" ?sflop)";
4293 for(std::size_t
i=1;
i<components.size();
i++)
4305 "floatbv expressions should be flattened when using FPA theory");
4346 std::size_t offset=0;
4353 << offset <<
") ?ufop" <<
nesting <<
")";
4385 std::size_t offset=0;
4388 for(struct_typet::componentst::const_iterator
4389 it=components.begin();
4390 it!=components.end();
4398 << offset <<
") ?ufop" <<
nesting <<
")";
4428 if(expr.
id()==
ID_or && !value)
4473 out <<
"; set_to true (equal)\n";
4493 out <<
"; set_to " << (value?
"true":
"false") <<
"\n"
4564 "lower_byte_operators should remove all byte operators");
4582 for(
const auto &symbol :
q_expr.variables())
4584 const auto identifier = symbol.get_identifier();
4586 id.
type = symbol.type();
4609 identifier=
"nondet_"+
4614 if(
id.type.is_nil())
4621 out <<
"; find_symbols\n";
4622 out <<
"(declare-fun |"
4640 out <<
"; the following is a substitute for lambda i. x\n";
4641 out <<
"(declare-fun " <<
id <<
" () ";
4646 out <<
"(assert (forall ((i ";
4648 out <<
")) (= (select " <<
id <<
" i) ";
4677 out <<
"(declare-fun " <<
id <<
" () ";
4681 out <<
"; the following is a substitute for lambda i . x(i)\n";
4682 out <<
"; universally quantified initialization of the array\n";
4683 out <<
"(assert (forall ((";
4694 out <<
")) (= (select " <<
id <<
" ";
4720 out <<
"; the following is a substitute for an array constructor" <<
"\n";
4721 out <<
"(declare-fun " <<
id <<
" () ";
4725 for(std::size_t
i=0;
i<expr.
operands().size();
i++)
4727 out <<
"(assert (= (select " <<
id <<
" ";
4740 out <<
"))" <<
"\n";
4756 out <<
"; the following is a substitute for a string" <<
"\n";
4757 out <<
"(declare-fun " <<
id <<
" () ";
4761 for(std::size_t
i=0;
i<
tmp.operands().size();
i++)
4763 out <<
"(assert (= (select " << id;
4767 out <<
"))" <<
"\n";
4783 out <<
"(declare-fun |" <<
id <<
"| () ";
4819 if(
bvfp_set.insert(function).second)
4821 out <<
"; this is a model for " << expr.
id() <<
" : "
4824 <<
"(define-fun " << function <<
" (";
4826 for(std::size_t
i = 0;
i < expr.
operands().size();
i++)
4830 out <<
"(op" <<
i <<
' ';
4840 for(std::size_t
i = 0;
i <
tmp1.operands().size();
i++)
4891 out <<
"(_ BitVec 1)";
4911 width != 0,
"failed to get width of struct");
4913 out <<
"(_ BitVec " << width <<
")";
4926 width != 0,
"failed to get width of vector");
4928 out <<
"(_ BitVec " << width <<
")";
4943 "failed to get width of union");
4945 out <<
"(_ BitVec " << width <<
")";
4977 out <<
"(_ FloatingPoint "
4999 width != 0,
"failed to get width of complex");
5001 out <<
"(_ BitVec " << width <<
")";
5127 out <<
"))))" <<
"\n";
5144 for(struct_union_typet::componentst::const_iterator
5145 it=components.begin();
5146 it!=components.end();
5159 for(struct_union_typet::componentst::const_iterator
5160 it2=components.begin();
5161 it2!=components.end();
5169 <<
it2->get_name() <<
" s) ";
5173 out <<
"))" <<
"\n";
5191 for(
const auto &
param : parameters)
void base_type(typet &type, const namespacet &ns)
API to expression classes for bitvectors.
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 extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_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 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.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
bitvector_typet index_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.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
std::size_t get_width() const
const membert & get_member(const struct_typet &type, const irep_idt &member) const
The byte swap expression.
std::vector< parametert > parameterst
const parameterst & parameters() const
struct configt::bv_encodingt bv_encoding
A constant literal expression.
const irep_idt & get_value() const
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 is_true() const
Return whether the expression is a constant representing true.
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.
The Boolean constant false.
std::size_t get_fraction_bits() const
Fixed-width bit-vector with signed fixed-point interpretation.
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
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt NaN(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
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.
literalt get_literal() const
Extract member of struct or union.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_identifier() const
The plus expression Associativity is not specified.
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t get_invalid_object() const
numberingt< exprt, irep_hash > objects
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
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)
void convert_update(const exprt &expr)
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)
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
boolbv_widtht boolbv_width
void convert_constant(const constant_exprt &expr)
std::string floatbv_suffix(const exprt &) const
void flatten2bv(const exprt &)
void convert_div(const div_exprt &expr)
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
std::string type2id(const typet &) const
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
struct_exprt parse_struct(const irept &s, const struct_typet &type)
void convert_mult(const mult_exprt &expr)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
void define_object_size(const irep_idt &id, const exprt &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
datatype_mapt datatype_map
void convert_mod(const mod_exprt &expr)
static std::string convert_identifier(const irep_idt &identifier)
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
std::unordered_map< irep_idt, bool > set_values
The values which boolean identifiers have been smt2_convt::set_to or in other words those which are a...
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
void convert_member(const member_exprt &expr)
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
void convert_index(const index_exprt &expr)
pointer_logict pointer_logic
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
void walk_array_tree(std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)
This function walks the SMT output and populates a map with index/value pairs for the array.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
defined_expressionst object_sizes
exprt parse_rec(const irept &s, const typet &type)
void convert_union(const union_exprt &expr)
exprt parse_union(const irept &s, const union_typet &type)
exprt parse_array(const irept &s, const array_typet &type)
This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array ...
std::vector< bool > boolean_assignment
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
void convert_with(const with_exprt &expr)
std::vector< exprt > assumptions
void convert_plus(const plus_exprt &expr)
defined_expressionst defined_expressions
void pop() override
Currently, only implements a single stack element (no nested contexts)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
identifier_mapt identifier_map
void convert_minus(const minus_exprt &expr)
void convert_expr(const exprt &)
constant_exprt parse_literal(const irept &, const typet &type)
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
std::size_t no_boolean_variables
smt2_identifierst smt2_identifiers
void convert_floatbv(const exprt &expr)
resultt dec_solve() override
Run the decision procedure to solve the problem.
literalt convert(const exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const irep_idt & get_name() const
const componentst & components() const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
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.
Vector constructor from list of elements.
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
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 isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
static std::string binary(const constant_exprt &src)
bool is_true(const literalt &l)
literalt const_literal(bool value)
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const 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)
API to expression classes for Pointers.
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.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNEXPECTEDCASE(S)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
int solver(std::istream &in)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bool has_byte_operator(const exprt &src)
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
#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,...)
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 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 vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_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 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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_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.
std::size_t unsafe_string2size_t(const std::string &str, int base)
const string_constantt & to_string_constant(const exprt &expr)