CBMC
smt2irep.cpp
Go to the documentation of this file.
1
3
#include <
testing-utils/smt2irep.h
>
4
5
#include <
solvers/smt2/smt2irep.h
>
6
#include <
util/message.h
>
7
8
#include <sstream>
9
10
bool
operator==
(
11
const
smt2_parser_test_resultt
&left,
12
const
smt2_parser_test_resultt
&right)
13
{
14
return
left.
parsed_output
== right.
parsed_output
&&
15
left.
messages
== right.
messages
;
16
}
17
18
smt2_parser_test_resultt
smt2irep
(
const
std::string &input)
19
{
20
std::stringstream in_stream(input);
21
std::stringstream out_stream;
22
stream_message_handlert
message_handler(out_stream);
23
return
{
smt2irep
(in_stream, message_handler), out_stream.str()};
24
}
25
26
std::ostream &
operator<<
(
27
std::ostream &output_stream,
28
const
smt2_parser_test_resultt
&test_result)
29
{
30
const
std::string printed_irep =
31
test_result.
parsed_output
.has_value()
32
?
'{'
+ test_result.
parsed_output
->pretty(0, 0) +
'}'
33
:
"empty optional irep"
;
34
output_stream <<
'{'
<< printed_irep <<
", \""
<< test_result.
messages
35
<<
"\"}"
;
36
return
output_stream;
37
}
38
39
smt2_parser_error_containingt::smt2_parser_error_containingt
(
40
std::string expected_error)
41
: expected_error{std::move(
expected_error
)}
42
{
43
}
44
45
bool
smt2_parser_error_containingt::match
(
46
const
smt2_parser_test_resultt
&result)
const
47
{
48
return
!result.
parsed_output
.has_value() &&
49
result.
messages
.find(
expected_error
) != std::string::npos;
50
}
51
52
std::string
smt2_parser_error_containingt::describe
()
const
53
{
54
return
"Expecting empty parse tree and \""
+
expected_error
+
55
"\" printed to output."
;
56
}
57
58
smt2_parser_test_resultt
smt2_parser_success
(
irept
parse_tree)
59
{
60
return
{std::move(parse_tree),
""
};
61
}
smt2irep
optionalt< irept > smt2irep(std::istream &in, message_handlert &message_handler)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
Definition:
smt2irep.cpp:91
smt2_parser_success
smt2_parser_test_resultt smt2_parser_success(irept parse_tree)
Definition:
smt2irep.cpp:58
smt2irep.h
smt2_parser_error_containingt::describe
std::string describe() const override
Definition:
smt2irep.cpp:52
smt2_parser_error_containingt::expected_error
std::string expected_error
Definition:
smt2irep.h:34
smt2_parser_test_resultt::parsed_output
optionalt< irept > parsed_output
Definition:
smt2irep.h:15
smt2_parser_error_containingt::match
bool match(const smt2_parser_test_resultt &exception) const override
Definition:
smt2irep.cpp:45
smt2_parser_test_resultt::messages
std::string messages
Definition:
smt2irep.h:16
smt2_parser_test_resultt
Definition:
smt2irep.h:13
smt2_parser_error_containingt::smt2_parser_error_containingt
smt2_parser_error_containingt(std::string expected_error)
Definition:
smt2irep.cpp:39
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition:
irep.h:359
message.h
operator<<
std::ostream & operator<<(std::ostream &output_stream, const smt2_parser_test_resultt &test_result)
Definition:
smt2irep.cpp:26
smt2irep.h
stream_message_handlert
Definition:
message.h:110
operator==
bool operator==(const smt2_parser_test_resultt &left, const smt2_parser_test_resultt &right)
Author: Diffblue Ltd.
Definition:
smt2irep.cpp:10
unit
testing-utils
smt2irep.cpp
Generated by
1.8.17