29 if(token == smt2_tokenizert::OPEN)
31 else if(token == smt2_tokenizert::CLOSE)
40 if(
next_token() == smt2_tokenizert::END_OF_FILE)
57 throw error(
"command must start with '('");
62 throw error(
"expected symbol as command");
69 case smt2_tokenizert::END_OF_FILE:
71 "expected closing parenthesis at end of command,"
74 case smt2_tokenizert::CLOSE:
78 case smt2_tokenizert::OPEN:
79 case smt2_tokenizert::SYMBOL:
80 case smt2_tokenizert::NUMERAL:
81 case smt2_tokenizert::STRING_LITERAL:
82 case smt2_tokenizert::NONE:
83 case smt2_tokenizert::KEYWORD:
84 throw error(
"expected ')' at end of command");
91 std::size_t parentheses=0;
96 case smt2_tokenizert::OPEN:
101 case smt2_tokenizert::CLOSE:
109 case smt2_tokenizert::END_OF_FILE:
110 throw error(
"unexpected EOF in command");
112 case smt2_tokenizert::SYMBOL:
113 case smt2_tokenizert::NUMERAL:
114 case smt2_tokenizert::STRING_LITERAL:
115 case smt2_tokenizert::NONE:
116 case smt2_tokenizert::KEYWORD:
138 std::piecewise_construct,
139 std::forward_as_tuple(
id),
140 std::forward_as_tuple(idt::VARIABLE, std::move(expr)))
144 throw error() <<
"identifier '" <<
id <<
"' defined twice";
151 throw error(
"expected bindings after let");
153 std::vector<std::pair<irep_idt, exprt>> bindings;
160 throw error(
"expected symbol in binding");
168 throw error(
"expected ')' after value in binding");
171 std::pair<irep_idt, exprt>(identifier, value));
175 throw error(
"expected ')' at end of bindings");
178 std::vector<std::pair<irep_idt, idt>> saved_ids;
181 for(
auto &b : bindings)
183 auto insert_result =
id_map.insert({b.first,
idt{idt::BINDING, b.second}});
184 if(!insert_result.second)
186 auto &id_entry = *insert_result.first;
187 saved_ids.emplace_back(id_entry.first, std::move(id_entry.second));
188 id_entry.second =
idt{idt::BINDING, b.second};
196 throw error(
"expected ')' after let");
201 for(
const auto &b : bindings)
203 variables.push_back(
symbol_exprt(b.first, b.second.type()));
204 values.push_back(b.second);
208 for(
const auto &
binding : bindings)
212 for(
auto &saved_id : saved_ids)
213 id_map.insert(std::move(saved_id));
215 return let_exprt(variables, values, where);
221 throw error() <<
"expected bindings after " << id;
230 throw error(
"expected symbol in binding");
237 throw error(
"expected ')' after sort in binding");
243 throw error(
"expected ')' at end of bindings");
246 std::vector<std::pair<irep_idt, idt>> saved_ids;
249 for(
auto &b : bindings)
252 id_map.insert({b.get_identifier(),
idt{idt::BINDING, b.
type()}});
253 if(!insert_result.second)
255 auto &id_entry = *insert_result.first;
256 saved_ids.emplace_back(id_entry.first, std::move(id_entry.second));
257 id_entry.second =
idt{idt::BINDING, b.
type()};
265 throw error() <<
"expected ')' after " << id;
268 for(
const auto &b : bindings)
269 id_map.erase(b.get_identifier());
272 for(
auto &saved_id : saved_ids)
273 id_map.insert(std::move(saved_id));
275 return {std::move(bindings), std::move(expr)};
288 if(
binding.second.type().id() != ID_bool)
289 throw error() <<
id <<
" expects a boolean term";
301 if(op.size() != function_type.domain().size())
302 throw error(
"wrong number of arguments for function");
304 for(std::size_t i=0; i<op.size(); i++)
306 if(op[i].type() != function_type.domain()[i])
307 throw error(
"wrong type for arguments for function");
317 for(
auto &expr : result)
319 if(expr.type().id() == ID_signedbv)
322 else if(expr.type().id() != ID_unsignedbv)
324 throw error(
"expected unsigned bitvector");
338 if(expr.
type().
id()==ID_unsignedbv)
341 if(expr.
type().
id()!=ID_signedbv)
342 throw error(
"expected signed bitvector");
351 for(std::size_t i = 1; i < op.size(); i++)
353 if(op[i].type() != op[0].type())
355 throw error() <<
"expression must have operands with matching types,"
366 throw error(
"expression must have at least one operand");
370 exprt result(
id, op[0].type());
378 throw error(
"expression must have two operands");
388 throw error(
"expression must have one operand");
396 throw error(
"expression must have two operands");
407 throw error() <<
"FloatingPoint equality takes two operands";
409 if(op[0].type().
id() != ID_floatbv || op[1].type().
id() != ID_floatbv)
410 throw error() <<
"FloatingPoint equality takes FloatingPoint operands";
412 if(op[0].type() != op[1].type())
414 throw error() <<
"FloatingPoint equality takes FloatingPoint operands with "
415 <<
"matching sort, but got " <<
smt2_format(op[0].type())
427 throw error() <<
id <<
" takes three operands";
429 if(op[1].type().
id() != ID_floatbv || op[2].type().
id() != ID_floatbv)
430 throw error() <<
id <<
" takes FloatingPoint operands";
432 if(op[1].type() != op[2].type())
434 throw error() <<
id <<
" takes FloatingPoint operands with matching sort, "
435 <<
"but got " <<
smt2_format(op[1].type()) <<
" vs "
441 id ==
"fp.add" ? ID_floatbv_plus :
442 id ==
"fp.sub" ? ID_floatbv_minus :
443 id ==
"fp.mul" ? ID_floatbv_mult :
444 id ==
"fp.div" ? ID_floatbv_div :
445 throw error(
"unsupported floating-point operation");
455 throw error(
"fp takes three operands");
457 if(op[0].type().
id() != ID_unsignedbv)
458 throw error(
"fp takes BitVec as first operand");
460 if(op[1].type().
id() != ID_unsignedbv)
461 throw error(
"fp takes BitVec as second operand");
463 if(op[2].type().
id() != ID_unsignedbv)
464 throw error(
"fp takes BitVec as third operand");
467 throw error(
"fp takes BitVec of size 1 as first operand");
477 const auto bv_type =
bv_typet(concat_type.get_width());
492 case smt2_tokenizert::SYMBOL:
497 throw error(
"expected symbol after '_'");
508 throw error(
"expected numeral as bitvector literal width");
513 throw error(
"expected ')' after bitvector literal");
517 else if(
id ==
"+oo" ||
id ==
"-oo" ||
id ==
"NaN")
522 throw error() <<
"expected number after " << id;
527 throw error() <<
"expected second number after " << id;
532 throw error() <<
"expected ')' after " << id;
546 throw error() <<
"unknown indexed identifier " << id;
560 if(term.type().id() != ID_bool)
561 throw error(
"named terms must be Boolean");
571 throw error(
"invalid name attribute, expected symbol");
574 throw error(
"unknown term attribute");
578 throw error(
"expected ')' at end of term attribute");
588 return e_it->second();
594 auto id_it =
id_map.find(
id);
597 if(id_it->second.type.id() == ID_mathematical_function)
605 throw error() <<
"unknown function symbol '" <<
id <<
'\'';
609 case smt2_tokenizert::OPEN:
617 throw error(
"expected symbol after '_'");
624 throw error(
"expected numeral after extract");
629 throw error(
"expected two numerals after extract");
634 throw error(
"expected ')' after extract");
639 throw error(
"extract takes one operand");
645 throw error(
"extract got bad indices");
651 else if(
id==
"rotate_left" ||
652 id==
"rotate_right" ||
658 throw error() <<
"expected numeral after " << id;
663 throw error() <<
"expected ')' after " <<
id <<
" index";
668 throw error() <<
id <<
" takes one operand";
670 if(
id==
"rotate_left")
675 else if(
id==
"rotate_right")
680 else if(
id==
"sign_extend")
694 else if(
id==
"zero_extend")
701 else if(
id == ID_repeat)
710 else if(
id ==
"to_fp")
713 throw error(
"expected number after to_fp");
718 throw error(
"expected second number after to_fp");
723 throw error(
"expected ')' after to_fp");
733 throw error(
"expected ')' at the end of to_fp");
740 source_op.type().id() == ID_real ||
741 source_op.type().id() == ID_integer)
745 if(source_op.id() == ID_constant)
749 const auto &real_number =
751 auto dot_pos = real_number.find(
'.');
752 if(dot_pos == std::string::npos)
760 std::string significand_str;
761 significand_str.reserve(real_number.size());
762 for(
auto ch : real_number)
765 significand_str += ch;
782 <<
"to_fp for non-constant real expressions is not implemented";
784 else if(source_op.type().id() == ID_unsignedbv)
795 else if(source_op.type().id() == ID_floatbv)
798 source_op, rounding_mode, spec.
to_type());
801 throw error() <<
"unexpected sort given as operand to to_fp";
805 throw error() <<
"unknown indexed identifier '"
822 <<
"unexpected 'as const' expression expects array type";
828 throw error() <<
"expecting ')' after sort in 'as const'";
832 if(value.type() != array_sort.element_type())
833 throw error() <<
"unexpected 'as const' with wrong element type";
836 throw error() <<
"expecting ')' at the end of 'as const'";
841 throw error() <<
"unexpected 'as' expression";
852 throw error(
"mismatched parentheses in an expression");
867 throw error(
"mismatched parentheses in an expression");
874 case smt2_tokenizert::CLOSE:
875 case smt2_tokenizert::NUMERAL:
876 case smt2_tokenizert::STRING_LITERAL:
877 case smt2_tokenizert::END_OF_FILE:
878 case smt2_tokenizert::NONE:
879 case smt2_tokenizert::KEYWORD:
883 throw error(
"mismatched parentheses in an expression");
896 throw error() <<
"bitvector division expects two operands";
903 exprt division_result;
917 if_exprt(divisor_is_zero, all_ones, division_result));
923 throw error() <<
"bitvector modulo expects two operands";
941 mod_result =
mod_exprt(dividend, divisor);
946 if_exprt(divisor_is_zero, dividend, mod_result));
953 case smt2_tokenizert::SYMBOL:
960 return e_it->second();
963 auto id_it =
id_map.find(identifier);
966 symbol_exprt symbol_expr(identifier, id_it->second.type);
968 symbol_expr.
set(ID_C_quoted,
true);
969 return std::move(symbol_expr);
973 throw error() <<
"unknown expression '" << identifier <<
'\'';
976 case smt2_tokenizert::NUMERAL:
979 if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'x')
983 const std::size_t width = 4 * (buffer.size() - 2);
988 else if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'b')
992 const std::size_t width = buffer.size() - 2;
1003 case smt2_tokenizert::OPEN:
1006 case smt2_tokenizert::END_OF_FILE:
1007 throw error(
"EOF in an expression");
1009 case smt2_tokenizert::CLOSE:
1010 case smt2_tokenizert::STRING_LITERAL:
1011 case smt2_tokenizert::NONE:
1012 case smt2_tokenizert::KEYWORD:
1013 throw error(
"unexpected token in an expression");
1030 throw error(
"unsupported rounding mode");
1118 return unary(ID_unary_minus, op);
1120 return binary(ID_minus, op);
1149 const std::size_t total_width =
1150 std::accumulate(op_width.begin(), op_width.end(), 0);
1162 std::vector<exprt> pairwise_constraints;
1163 for(std::size_t i = 0; i < op.size(); i++)
1165 for(std::size_t j = i; j < op.size(); j++)
1168 pairwise_constraints.push_back(
1172 return multi_ary(ID_and, pairwise_constraints);
1180 throw error(
"ite takes three operands");
1182 if(op[0].type().
id() != ID_bool)
1183 throw error(
"ite takes a boolean as first operand");
1185 if(op[1].type() != op[2].type())
1186 throw error(
"ite needs matching types");
1188 return if_exprt(op[0], op[1], op[2]);
1200 throw error(
"select takes two operands");
1202 if(op[0].type().
id() != ID_array)
1203 throw error(
"select expects array operand");
1213 throw error(
"store takes three operands");
1215 if(op[0].type().
id() != ID_array)
1216 throw error(
"store expects array operand");
1218 if(
to_array_type(op[0].type()).element_type() != op[2].type())
1219 throw error(
"store expects value that matches array element type");
1228 throw error(
"fp.abs takes one operand");
1230 if(op[0].type().
id() != ID_floatbv)
1231 throw error(
"fp.abs takes FloatingPoint operand");
1240 throw error(
"fp.isNaN takes one operand");
1242 if(op[0].type().
id() != ID_floatbv)
1243 throw error(
"fp.isNaN takes FloatingPoint operand");
1252 throw error(
"fp.isInf takes one operand");
1254 if(op[0].type().
id() != ID_floatbv)
1255 throw error(
"fp.isInf takes FloatingPoint operand");
1264 throw error(
"fp.isNormal takes one operand");
1266 if(op[0].type().
id() != ID_floatbv)
1267 throw error(
"fp.isNormal takes FloatingPoint operand");
1295 throw error() <<
"fp.rem takes three operands";
1297 if(op[0].type().
id() != ID_floatbv || op[1].type().
id() != ID_floatbv)
1298 throw error() <<
"fp.rem takes FloatingPoint operands";
1300 if(op[0].type() != op[1].type())
1303 <<
"fp.rem takes FloatingPoint operands with matching sort, "
1304 <<
"but got " <<
smt2_format(op[0].type()) <<
" vs "
1332 std::vector<typet>
sorts;
1340 throw error() <<
"unexpected end-of-file in a function sort";
1347 if(
sorts.size() < 2)
1348 throw error() <<
"expected function sort to have at least 2 type arguments";
1350 auto codomain = std::move(
sorts.back());
1364 case smt2_tokenizert::SYMBOL:
1367 case smt2_tokenizert::OPEN:
1369 throw error(
"expected symbol after '(' in a sort ");
1374 throw error(
"expected symbol after '_' in a sort");
1378 case smt2_tokenizert::CLOSE:
1379 case smt2_tokenizert::NUMERAL:
1380 case smt2_tokenizert::STRING_LITERAL:
1381 case smt2_tokenizert::NONE:
1382 case smt2_tokenizert::KEYWORD:
1383 throw error() <<
"unexpected token in a sort: '"
1386 case smt2_tokenizert::END_OF_FILE:
1387 throw error() <<
"unexpected end-of-file in a sort";
1393 const auto s_it =
sorts.find(token);
1395 if(s_it ==
sorts.end())
1396 throw error() <<
"unexpected sort: '" << token <<
'\'';
1398 return s_it->second();
1407 sorts[
"Float16"] = [] {
1410 sorts[
"Float32"] = [] {
1413 sorts[
"Float64"] = [] {
1416 sorts[
"Float128"] = [] {
1420 sorts[
"BitVec"] = [
this] {
1422 throw error(
"expected numeral as bit-width");
1428 throw error(
"expected ')' at end of sort");
1433 sorts[
"FloatingPoint"] = [
this] {
1435 throw error(
"expected numeral as bit-width");
1440 throw error(
"expected numeral as bit-width");
1446 throw error(
"expected ')' at end of sort");
1451 sorts[
"Array"] = [
this] {
1453 auto domain =
sort();
1454 auto range =
sort();
1458 throw error(
"expected ')' at end of Array sort");
1462 if(domain.id() == ID_unsignedbv)
1465 throw error(
"unsupported array sort");
1475 throw error(
"expected '(' at beginning of signature");
1485 std::vector<irep_idt> parameters;
1490 throw error(
"expected '(' at beginning of parameter");
1493 throw error(
"expected symbol in parameter");
1496 domain.push_back(
sort());
1497 parameters.push_back(
id);
1500 throw error(
"expected ')' at end of parameter");
1514 throw error(
"expected '(' at beginning of signature");
1525 domain.push_back(
sort());
1548 commands[
"declare-const"] = [
this]() {
1552 throw error() <<
"expected a symbol after " << s;
1564 commands[
"declare-fun"] = [
this]() {
1566 throw error(
"expected a symbol after declare-fun");
1574 commands[
"define-const"] = [
this]() {
1576 throw error(
"expected a symbol after define-const");
1580 const auto type =
sort();
1584 if(value.type() != type)
1586 throw error() <<
"type mismatch in constant definition: expected '"
1595 commands[
"define-fun"] = [
this]() {
1597 throw error(
"expected a symbol after define-fun");
1604 std::vector<std::pair<irep_idt, idt>> hidden_ids;
1606 for(
const auto &pair : signature.ids_and_types())
1608 auto insert_result =
1609 id_map.insert({pair.first,
idt{idt::PARAMETER, pair.second}});
1610 if(!insert_result.second)
1612 auto &id_entry = *insert_result.first;
1613 hidden_ids.emplace_back(id_entry.first, std::move(id_entry.second));
1614 id_entry.second =
idt{idt::PARAMETER, pair.second};
1622 for(
auto &
id : signature.parameters)
1626 for(
auto &hidden_id : hidden_ids)
1627 id_map.insert(std::move(hidden_id));
1630 if(signature.type.id() == ID_mathematical_function)
1633 if(body.type() != f_signature.codomain())
1635 throw error() <<
"type mismatch in function definition: expected '"
1636 <<
smt2_format(f_signature.codomain()) <<
"' but got '"
1640 else if(body.type() != signature.type)
1642 throw error() <<
"type mismatch in function definition: expected '"
1648 if(!signature.parameters.empty())
1649 body =
lambda_exprt(signature.binding_variables(), body);
API to expression classes for bitvectors.
Pre-defined bitvector types.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Array constructor from single element.
A base class for binary expressions.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
std::vector< symbol_exprt > variablest
std::size_t get_width() const
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
The Boolean constant false.
Semantic type conversion from/to floating-point formats.
Application of (mathematical) function.
IEEE-floating-point equality.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
static ieee_float_spect half_precision()
static ieee_float_spect single_precision()
static ieee_float_spect quadruple_precision()
class floatbv_typet to_type() const
static ieee_float_spect double_precision()
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt NaN(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
The trinary if-then-else operator.
An expression denoting infinity.
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
Unbounded, signed integers (mathematical integers, not bitvectors)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
Evaluates to true if the operand is a normal number.
A (mathematical) lambda expression.
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
A base class for quantifier expressions.
Unbounded, signed real numbers.
Fixed-width bit-vector with two's complement interpretation.
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
std::size_t parenthesis_level
void command(const std::string &)
exprt::operandst operands()
exprt bv_mod(const exprt::operandst &, bool is_signed)
exprt binary(irep_idt, const exprt::operandst &)
exprt bv_division(const exprt::operandst &, bool is_signed)
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
std::unordered_map< std::string, std::function< exprt()> > expressions
exprt lambda_expression()
typet function_signature_declaration()
std::unordered_map< std::string, std::function< void()> > commands
exprt function_application()
void add_unique_id(irep_idt, exprt)
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt quantifier_expression(irep_idt)
std::pair< binding_exprt::variablest, exprt > binding(irep_idt)
exprt function_application_ieee_float_eq(const exprt::operandst &)
void check_matching_operand_types(const exprt::operandst &) const
signature_with_parameter_idst function_signature_definition()
exprt function_application_fp(const exprt::operandst &)
smt2_tokenizert::smt2_errort error() const
exprt binary_predicate(irep_idt, const exprt::operandst &)
smt2_tokenizert::tokent next_token()
std::unordered_map< std::string, std::function< typet()> > sorts
smt2_tokenizert smt2_tokenizer
exprt unary(irep_idt, const exprt::operandst &)
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
const std::string & get_buffer() const
bool token_is_quoted_symbol() const
Expression to hold a symbol (variable)
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.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
API to expression classes for floating-point arithmetic.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
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)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
bool is_signed(const typet &t)
Convenience function – is the type signed?