28 if(token == smt2_tokenizert::OPEN)
30 else if(token == smt2_tokenizert::CLOSE)
39 if(
next_token() == smt2_tokenizert::END_OF_FILE)
56 throw error(
"command must start with '('");
61 throw error(
"expected symbol as command");
68 case smt2_tokenizert::END_OF_FILE:
70 "expected closing parenthesis at end of command,"
73 case smt2_tokenizert::CLOSE:
77 case smt2_tokenizert::OPEN:
78 case smt2_tokenizert::SYMBOL:
79 case smt2_tokenizert::NUMERAL:
80 case smt2_tokenizert::STRING_LITERAL:
81 case smt2_tokenizert::NONE:
82 case smt2_tokenizert::KEYWORD:
83 throw error(
"expected ')' at end of command");
90 std::size_t parentheses=0;
95 case smt2_tokenizert::OPEN:
100 case smt2_tokenizert::CLOSE:
108 case smt2_tokenizert::END_OF_FILE:
109 throw error(
"unexpected EOF in command");
111 case smt2_tokenizert::SYMBOL:
112 case smt2_tokenizert::NUMERAL:
113 case smt2_tokenizert::STRING_LITERAL:
114 case smt2_tokenizert::NONE:
115 case smt2_tokenizert::KEYWORD:
146 std::piecewise_construct,
147 std::forward_as_tuple(new_id),
148 std::forward_as_tuple(kind, expr))
161 std::piecewise_construct,
162 std::forward_as_tuple(
id),
163 std::forward_as_tuple(idt::VARIABLE, expr))
167 throw error() <<
"identifier '" <<
id <<
"' defined twice";
184 throw error(
"expected bindings after let");
186 std::vector<std::pair<irep_idt, exprt>> bindings;
193 throw error(
"expected symbol in binding");
201 throw error(
"expected ')' after value in binding");
204 std::pair<irep_idt, exprt>(identifier, value));
208 throw error(
"expected ')' at end of bindings");
214 for(
auto &b : bindings)
217 b.first =
add_fresh_id(b.first, idt::BINDING, b.second);
223 throw error(
"expected ')' after let");
228 for(
const auto &b : bindings)
230 variables.push_back(
symbol_exprt(b.first, b.second.type()));
231 values.push_back(b.second);
240 return let_exprt(variables, values, where);
246 throw error() <<
"expected bindings after " << id;
248 std::vector<symbol_exprt> bindings;
255 throw error(
"expected symbol in binding");
262 throw error(
"expected ')' after sort in binding");
268 throw error(
"expected ')' at end of bindings");
274 for(
auto &b : bindings)
279 b.set_identifier(
id);
285 throw error() <<
"expected ')' after " << id;
290 for(
const auto &b : bindings)
291 id_map.erase(b.get_identifier());
297 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
313 if(op.size() != function_type.domain().size())
314 throw error(
"wrong number of arguments for function");
316 for(std::size_t i=0; i<op.size(); i++)
318 if(op[i].type() != function_type.domain()[i])
319 throw error(
"wrong type for arguments for function");
329 for(
auto &expr : result)
331 if(expr.type().id() == ID_signedbv)
334 else if(expr.type().id() != ID_unsignedbv)
336 throw error(
"expected unsigned bitvector");
350 if(expr.
type().
id()==ID_unsignedbv)
353 if(expr.
type().
id()!=ID_signedbv)
354 throw error(
"expected signed bitvector");
363 throw error(
"expression must have at least one operand");
365 for(std::size_t i = 1; i < op.size(); i++)
367 if(op[i].type() != op[0].type())
369 throw error() <<
"expression must have operands with matching types,"
376 exprt result(
id, op[0].type());
384 throw error(
"expression must have two operands");
386 if(op[0].type() != op[1].type())
388 throw error() <<
"expression must have operands with matching types,"
400 throw error(
"expression must have one operand");
408 throw error(
"expression must have two operands");
410 if(op[0].type() != op[1].type())
411 throw error(
"expression must have operands with matching types");
420 throw error() <<
"FloatingPoint equality takes two operands";
422 if(op[0].type().
id() != ID_floatbv || op[1].type().
id() != ID_floatbv)
423 throw error() <<
"FloatingPoint equality takes FloatingPoint operands";
425 if(op[0].type() != op[1].type())
427 throw error() <<
"FloatingPoint equality takes FloatingPoint operands with "
428 <<
"matching sort, but got " <<
smt2_format(op[0].type())
440 throw error() <<
id <<
" takes three operands";
442 if(op[1].type().
id() != ID_floatbv || op[2].type().
id() != ID_floatbv)
443 throw error() <<
id <<
" takes FloatingPoint operands";
445 if(op[1].type() != op[2].type())
447 throw error() <<
id <<
" takes FloatingPoint operands with matching sort, "
448 <<
"but got " <<
smt2_format(op[1].type()) <<
" vs "
454 id ==
"fp.add" ? ID_floatbv_plus :
455 id ==
"fp.sub" ? ID_floatbv_minus :
456 id ==
"fp.mul" ? ID_floatbv_mult :
457 id ==
"fp.div" ? ID_floatbv_div :
458 throw error(
"unsupported floating-point operation");
468 throw error(
"fp takes three operands");
470 if(op[0].type().
id() != ID_unsignedbv)
471 throw error(
"fp takes BitVec as first operand");
473 if(op[1].type().
id() != ID_unsignedbv)
474 throw error(
"fp takes BitVec as second operand");
476 if(op[2].type().
id() != ID_unsignedbv)
477 throw error(
"fp takes BitVec as third operand");
480 throw error(
"fp takes BitVec of size 1 as first operand");
495 case smt2_tokenizert::SYMBOL:
500 throw error(
"expected symbol after '_'");
508 throw error(
"expected numeral as bitvector literal width");
513 throw error(
"expected ')' after bitvector literal");
519 throw error() <<
"unknown indexed identifier "
534 if(term.type().id() != ID_bool)
535 throw error(
"named terms must be Boolean");
545 throw error(
"invalid name attribute, expected symbol");
548 throw error(
"unknown term attribute");
552 throw error(
"expected ')' at end of term attribute");
562 return e_it->second();
569 auto id_it =
id_map.find(final_id);
572 if(id_it->second.type.id() == ID_mathematical_function)
581 throw error() <<
"unknown function symbol '" <<
id <<
'\'';
585 case smt2_tokenizert::OPEN:
593 throw error(
"expected symbol after '_'");
600 throw error(
"expected numeral after extract");
605 throw error(
"expected two numerals after extract");
610 throw error(
"expected ')' after extract");
615 throw error(
"extract takes one operand");
621 throw error(
"extract got bad indices");
627 else if(
id==
"rotate_left" ||
628 id==
"rotate_right" ||
634 throw error() <<
"expected numeral after " << id;
639 throw error() <<
"expected ')' after " <<
id <<
" index";
644 throw error() <<
id <<
" takes one operand";
646 if(
id==
"rotate_left")
651 else if(
id==
"rotate_right")
656 else if(
id==
"sign_extend")
670 else if(
id==
"zero_extend")
677 else if(
id == ID_repeat)
688 throw error() <<
"unknown indexed identifier '"
701 throw error(
"mismatched parentheses in an expression");
716 throw error(
"mismatched parentheses in an expression");
723 case smt2_tokenizert::CLOSE:
724 case smt2_tokenizert::NUMERAL:
725 case smt2_tokenizert::STRING_LITERAL:
726 case smt2_tokenizert::END_OF_FILE:
727 case smt2_tokenizert::NONE:
728 case smt2_tokenizert::KEYWORD:
732 throw error(
"mismatched parentheses in an expression");
744 case smt2_tokenizert::SYMBOL:
751 return e_it->second();
755 auto id_it =
id_map.find(final_id);
760 symbol_expr.
set(ID_C_quoted,
true);
761 return std::move(symbol_expr);
765 throw error() <<
"unknown expression '" << identifier <<
'\'';
768 case smt2_tokenizert::NUMERAL:
771 if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'x')
775 const std::size_t width = 4 * (buffer.size() - 2);
780 else if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'b')
784 const std::size_t width = buffer.size() - 2;
795 case smt2_tokenizert::OPEN:
798 case smt2_tokenizert::END_OF_FILE:
799 throw error(
"EOF in an expression");
801 case smt2_tokenizert::CLOSE:
802 case smt2_tokenizert::STRING_LITERAL:
803 case smt2_tokenizert::NONE:
804 case smt2_tokenizert::KEYWORD:
805 throw error(
"unexpected token in an expression");
822 throw error(
"unsupported rounding mode");
909 return unary(ID_unary_minus, op);
911 return binary(ID_minus, op);
945 const std::size_t total_width =
946 std::accumulate(op_width.begin(), op_width.end(), 0);
958 std::vector<exprt> pairwise_constraints;
959 for(std::size_t i = 0; i < op.size(); i++)
961 for(std::size_t j = i; j < op.size(); j++)
964 pairwise_constraints.push_back(
968 return multi_ary(ID_and, pairwise_constraints);
976 throw error(
"ite takes three operands");
978 if(op[0].type().
id() != ID_bool)
979 throw error(
"ite takes a boolean as first operand");
981 if(op[1].type() != op[2].type())
982 throw error(
"ite needs matching types");
984 return if_exprt(op[0], op[1], op[2]);
996 throw error(
"select takes two operands");
998 if(op[0].type().
id() != ID_array)
999 throw error(
"select expects array operand");
1009 throw error(
"store takes three operands");
1011 if(op[0].type().
id() != ID_array)
1012 throw error(
"store expects array operand");
1015 throw error(
"store expects value that matches array element type");
1024 throw error(
"fp.isNaN takes one operand");
1026 if(op[0].type().
id() != ID_floatbv)
1027 throw error(
"fp.isNaN takes FloatingPoint operand");
1036 throw error(
"fp.isInf takes one operand");
1038 if(op[0].type().
id() != ID_floatbv)
1039 throw error(
"fp.isInf takes FloatingPoint operand");
1048 throw error(
"fp.isNormal takes one operand");
1050 if(op[0].type().
id() != ID_floatbv)
1051 throw error(
"fp.isNormal takes FloatingPoint operand");
1101 case smt2_tokenizert::SYMBOL:
1104 case smt2_tokenizert::OPEN:
1106 throw error(
"expected symbol after '(' in a sort ");
1111 throw error(
"expected symbol after '_' in a sort");
1115 case smt2_tokenizert::CLOSE:
1116 case smt2_tokenizert::NUMERAL:
1117 case smt2_tokenizert::STRING_LITERAL:
1118 case smt2_tokenizert::NONE:
1119 case smt2_tokenizert::KEYWORD:
1120 throw error() <<
"unexpected token in a sort: '"
1123 case smt2_tokenizert::END_OF_FILE:
1124 throw error() <<
"unexpected end-of-file in a sort";
1130 const auto s_it =
sorts.find(token);
1132 if(s_it ==
sorts.end())
1133 throw error() <<
"unexpected sort: '" << token <<
'\'';
1135 return s_it->second();
1144 sorts[
"BitVec"] = [
this] {
1146 throw error(
"expected numeral as bit-width");
1152 throw error(
"expected ')' at end of sort");
1157 sorts[
"FloatingPoint"] = [
this] {
1159 throw error(
"expected numeral as bit-width");
1164 throw error(
"expected numeral as bit-width");
1170 throw error(
"expected ')' at end of sort");
1175 sorts[
"Array"] = [
this] {
1177 auto domain =
sort();
1178 auto range =
sort();
1182 throw error(
"expected ')' at end of Array sort");
1186 if(domain.id() == ID_unsignedbv)
1189 throw error(
"unsupported array sort");
1197 throw error(
"expected '(' at beginning of signature");
1207 std::vector<irep_idt> parameters;
1212 throw error(
"expected '(' at beginning of parameter");
1215 throw error(
"expected symbol in parameter");
1218 domain.push_back(
sort());
1220 parameters.push_back(
1224 throw error(
"expected ')' at end of parameter");
1238 throw error(
"expected '(' at beginning of signature");
1249 domain.push_back(
sort());
1272 commands[
"declare-const"] = [
this]() {
1276 throw error() <<
"expected a symbol after " << s;
1288 commands[
"declare-fun"] = [
this]() {
1290 throw error(
"expected a symbol after declare-fun");
1298 commands[
"define-const"] = [
this]() {
1300 throw error(
"expected a symbol after define-const");
1304 const auto type =
sort();
1308 if(value.type() != type)
1310 throw error() <<
"type mismatch in constant definition: expected '"
1319 commands[
"define-fun"] = [
this]() {
1321 throw error(
"expected a symbol after define-fun");
1335 if(signature.type.id() == ID_mathematical_function)
1338 if(body.type() != f_signature.codomain())
1340 throw error() <<
"type mismatch in function definition: expected '"
1341 <<
smt2_format(f_signature.codomain()) <<
"' but got '"
1345 else if(body.type() != signature.type)
1347 throw error() <<
"type mismatch in function definition: expected '"
1355 id_map.at(
id).type = signature.type;
1356 id_map.at(
id).parameters = signature.parameters;
API to expression classes for bitvectors.
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.
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)...
class floatbv_typet to_type() const
The trinary if-then-else operator.
An expression denoting infinity.
Unbounded, signed integers (mathematical integers, not bitvectors)
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & id() const
Evaluates to true if the operand is a normal number.
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
A base class for quantifier expressions.
Unbounded, signed real numbers.
Fixed-width bit-vector with two's complement interpretation.
irep_idt add_fresh_id(const irep_idt &, idt::kindt, const exprt &)
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()
renaming_mapt renaming_map
exprt binary(irep_idt, const exprt::operandst &)
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
std::unordered_map< std::string, std::function< exprt()> > expressions
void add_unique_id(const irep_idt &, const exprt &)
typet function_signature_declaration()
std::unordered_map< std::string, std::function< void()> > commands
exprt function_application()
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 &)
irep_idt rename_id(const irep_idt &) const
std::map< irep_idt, irep_idt > renaming_mapt
exprt quantifier_expression(irep_idt)
exprt function_application_ieee_float_eq(const exprt::operandst &)
signature_with_parameter_idst function_signature_definition()
exprt function_application_fp(const exprt::operandst &)
renaming_counterst renaming_counters
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_errort error()
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 signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
enum { VARIABLE, BINDING, PARAMETER } kindt