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");
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)
196 throw error(
"expected ')' after let");
201 for(
const auto &
b : bindings)
204 values.push_back(
b.second);
208 for(
const auto &
binding : bindings)
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()}});
265 throw error() <<
"expected ')' after " << id;
268 for(
const auto &
b : bindings)
269 id_map.erase(
b.get_identifier());
275 return {std::move(bindings), std::move(expr)};
288 if(!
binding.second.is_boolean())
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)
324 throw error(
"expected unsigned bitvector");
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";
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";
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 "
445 throw error(
"unsupported floating-point operation");
455 throw error(
"fp takes three operands");
458 throw error(
"fp takes BitVec as first operand");
461 throw error(
"fp takes BitVec as second operand");
464 throw error(
"fp takes BitVec as third operand");
467 throw error(
"fp takes BitVec of size 1 as first operand");
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.is_boolean())
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();
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")
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");
752 if(
dot_pos == std::string::npos)
777 a.from_base10(significand, exponent);
782 <<
"to_fp for non-constant real expressions is not implemented";
801 throw error() <<
"unexpected sort given as operand to to_fp";
803 else if(
id ==
"to_fp_unsigned")
806 throw error(
"expected number after to_fp_unsigned");
811 throw error(
"expected second number after to_fp_unsigned");
816 throw error(
"expected ')' after to_fp_unsigned");
826 throw error(
"expected ')' at the end of to_fp_unsigned");
837 <<
"unexpected sort given as operand to to_fp_unsigned";
839 else if(
id ==
"fp.to_sbv" ||
id ==
"fp.to_ubv")
843 throw error() <<
"expected number after " << id;
848 throw error() <<
"expected ')' after " << id;
853 throw error() <<
id <<
" takes two operands";
856 throw error() <<
id <<
" takes a FloatingPoint operand";
858 if(
id ==
"fp.to_sbv")
868 throw error() <<
"unknown indexed identifier '"
885 <<
"unexpected 'as const' expression expects array type";
891 throw error() <<
"expecting ')' after sort in 'as const'";
896 throw error() <<
"unexpected 'as const' with wrong element type";
899 throw error() <<
"expecting ')' at the end of 'as const'";
904 throw error() <<
"unexpected 'as' expression";
915 throw error(
"mismatched parentheses in an expression");
930 throw error(
"mismatched parentheses in an expression");
937 case smt2_tokenizert::CLOSE:
938 case smt2_tokenizert::NUMERAL:
939 case smt2_tokenizert::STRING_LITERAL:
940 case smt2_tokenizert::END_OF_FILE:
941 case smt2_tokenizert::NONE:
942 case smt2_tokenizert::KEYWORD:
946 throw error(
"mismatched parentheses in an expression");
959 throw error() <<
"bitvector division expects two operands";
986 throw error() <<
"bitvector modulo expects two operands";
1007 {dividend, divisor},
1016 case smt2_tokenizert::SYMBOL:
1023 return e_it->second();
1032 return std::move(symbol_expr);
1036 throw error() <<
"unknown expression '" << identifier <<
'\'';
1039 case smt2_tokenizert::NUMERAL:
1042 if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'x')
1046 const std::size_t width = 4 * (buffer.size() - 2);
1051 else if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'b')
1055 const std::size_t width = buffer.size() - 2;
1066 case smt2_tokenizert::OPEN:
1069 case smt2_tokenizert::END_OF_FILE:
1070 throw error(
"EOF in an expression");
1072 case smt2_tokenizert::CLOSE:
1073 case smt2_tokenizert::STRING_LITERAL:
1074 case smt2_tokenizert::NONE:
1075 case smt2_tokenizert::KEYWORD:
1076 throw error(
"unexpected token in an expression");
1093 throw error(
"unsupported rounding mode");
1212 const std::size_t total_width =
1226 for(std::size_t i = 0; i < op.size(); i++)
1228 for(std::size_t j = i; j < op.size(); j++)
1243 throw error(
"ite takes three operands");
1245 if(!op[0].is_boolean())
1246 throw error(
"ite takes a boolean as first operand");
1248 if(op[1].type() != op[2].type())
1249 throw error(
"ite needs matching types");
1251 return if_exprt(op[0], op[1], op[2]);
1263 throw error(
"select takes two operands");
1266 throw error(
"select expects array operand");
1276 throw error(
"store takes three operands");
1279 throw error(
"store expects array operand");
1281 if(
to_array_type(op[0].type()).element_type() != op[2].type())
1282 throw error(
"store expects value that matches array element type");
1291 throw error(
"fp.abs takes one operand");
1294 throw error(
"fp.abs takes FloatingPoint operand");
1303 throw error(
"fp.isNaN takes one operand");
1306 throw error(
"fp.isNaN takes FloatingPoint operand");
1315 throw error(
"fp.isInfinite takes one operand");
1318 throw error(
"fp.isInfinite takes FloatingPoint operand");
1327 throw error(
"fp.isNormal takes one operand");
1330 throw error(
"fp.isNormal takes FloatingPoint operand");
1339 throw error(
"fp.isZero takes one operand");
1342 throw error(
"fp.isZero takes FloatingPoint operand");
1370 throw error() <<
"fp.rem takes three operands";
1373 throw error() <<
"fp.rem takes FloatingPoint operands";
1375 if(op[0].type() != op[1].type())
1378 <<
"fp.rem takes FloatingPoint operands with matching sort, "
1379 <<
"but got " <<
smt2_format(op[0].type()) <<
" vs "
1407 std::vector<typet>
sorts;
1415 throw error() <<
"unexpected end-of-file in a function sort";
1422 if(
sorts.size() < 2)
1423 throw error() <<
"expected function sort to have at least 2 type arguments";
1425 auto codomain = std::move(
sorts.back());
1439 case smt2_tokenizert::SYMBOL:
1442 case smt2_tokenizert::OPEN:
1444 throw error(
"expected symbol after '(' in a sort ");
1449 throw error(
"expected symbol after '_' in a sort");
1453 case smt2_tokenizert::CLOSE:
1454 case smt2_tokenizert::NUMERAL:
1455 case smt2_tokenizert::STRING_LITERAL:
1456 case smt2_tokenizert::NONE:
1457 case smt2_tokenizert::KEYWORD:
1458 throw error() <<
"unexpected token in a sort: '"
1461 case smt2_tokenizert::END_OF_FILE:
1462 throw error() <<
"unexpected end-of-file in a sort";
1471 throw error() <<
"unexpected sort: '" << token <<
'\'';
1473 return s_it->second();
1482 sorts[
"Float16"] = [] {
1485 sorts[
"Float32"] = [] {
1488 sorts[
"Float64"] = [] {
1491 sorts[
"Float128"] = [] {
1495 sorts[
"BitVec"] = [
this] {
1497 throw error(
"expected numeral as bit-width");
1503 throw error(
"expected ')' at end of sort");
1508 sorts[
"FloatingPoint"] = [
this] {
1510 throw error(
"expected numeral as bit-width");
1515 throw error(
"expected numeral as bit-width");
1521 throw error(
"expected ')' at end of sort");
1526 sorts[
"Array"] = [
this] {
1528 auto domain =
sort();
1529 auto range =
sort();
1533 throw error(
"expected ')' at end of Array sort");
1540 throw error(
"unsupported array sort");
1550 throw error(
"expected '(' at beginning of signature");
1560 std::vector<irep_idt> parameters;
1565 throw error(
"expected '(' at beginning of parameter");
1568 throw error(
"expected symbol in parameter");
1571 domain.push_back(
sort());
1572 parameters.push_back(
id);
1575 throw error(
"expected ')' at end of parameter");
1589 throw error(
"expected '(' at beginning of signature");
1600 domain.push_back(
sort());
1623 commands[
"declare-const"] = [
this]() {
1627 throw error() <<
"expected a symbol after " << s;
1639 commands[
"declare-fun"] = [
this]() {
1641 throw error(
"expected a symbol after declare-fun");
1649 commands[
"define-const"] = [
this]() {
1651 throw error(
"expected a symbol after define-const");
1655 const auto type =
sort();
1659 if(value.type() != type)
1661 throw error() <<
"type mismatch in constant definition: expected '"
1670 commands[
"define-fun"] = [
this]() {
1672 throw error(
"expected a symbol after define-fun");
1679 std::vector<std::pair<irep_idt, idt>>
hidden_ids;
1681 for(
const auto &
pair : signature.ids_and_types())
1697 for(
auto &
id : signature.parameters)
1710 throw error() <<
"type mismatch in function definition: expected '"
1715 else if(body.type() != signature.type)
1717 throw error() <<
"type mismatch in function definition: expected '"
1723 if(!signature.parameters.empty())
1724 body =
lambda_exprt(signature.binding_variables(), body);
API to expression classes for bitvectors.
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
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()
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.
An expression denoting infinity.
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 &)
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?