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;
196 throw error(
"expected ')' after let");
204 values.push_back(
b.second);
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;
252 id_map.insert({
b.get_identifier(),
idt{idt::BINDING,
b.type()}});
265 throw error() <<
"expected ')' after " << id;
269 id_map.erase(
b.get_identifier());
275 return {std::move(
bindings), std::move(expr)};
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.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();
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";
805 throw error() <<
"unknown indexed identifier '"
822 <<
"unexpected 'as const' expression expects array type";
828 throw error() <<
"expecting ')' after sort in 'as const'";
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";
923 throw error() <<
"bitvector modulo expects two operands";
953 case smt2_tokenizert::SYMBOL:
960 return e_it->second();
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");
1149 const std::size_t total_width =
1163 for(std::size_t
i = 0;
i < op.size();
i++)
1165 for(std::size_t
j =
i;
j < op.size();
j++)
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");
1203 throw error(
"select expects array operand");
1213 throw error(
"store takes three operands");
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");
1231 throw error(
"fp.abs takes FloatingPoint operand");
1240 throw error(
"fp.isNaN takes one operand");
1243 throw error(
"fp.isNaN takes FloatingPoint operand");
1252 throw error(
"fp.isInf takes one operand");
1255 throw error(
"fp.isInf takes FloatingPoint operand");
1264 throw error(
"fp.isNormal takes one operand");
1267 throw error(
"fp.isNormal takes FloatingPoint operand");
1295 throw error() <<
"fp.rem takes three operands";
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";
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");
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())
1622 for(
auto &
id : signature.parameters)
1635 throw error() <<
"type mismatch in function definition: expected '"
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 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
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()
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.
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 &)
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?