cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
smt2irep.cpp
Go to the documentation of this file.
1
2
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
}
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
smt2_parser_error_containingt::expected_error
std::string expected_error
Definition
smt2irep.h:34
smt2_parser_error_containingt::smt2_parser_error_containingt
smt2_parser_error_containingt(std::string expected_error)
Definition
smt2irep.cpp:39
smt2_parser_error_containingt::match
bool match(const smt2_parser_test_resultt &exception) const override
Definition
smt2irep.cpp:45
smt2_parser_error_containingt::describe
std::string describe() const override
Definition
smt2irep.cpp:52
stream_message_handlert
Definition
message.h:110
std
STL namespace.
smt2irep
std::optional< 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:92
smt2irep.h
message.h
smt2_parser_test_resultt
Definition
smt2irep.h:14
smt2_parser_test_resultt::parsed_output
std::optional< irept > parsed_output
Definition
smt2irep.h:15
smt2_parser_test_resultt::messages
std::string messages
Definition
smt2irep.h:16
operator==
bool operator==(const smt2_parser_test_resultt &left, const smt2_parser_test_resultt &right)
Author: Diffblue Ltd.
Definition
smt2irep.cpp:10
operator<<
std::ostream & operator<<(std::ostream &output_stream, const smt2_parser_test_resultt &test_result)
Definition
smt2irep.cpp:26
smt2_parser_success
smt2_parser_test_resultt smt2_parser_success(irept parse_tree)
Definition
smt2irep.cpp:58
smt2irep.h
unit
testing-utils
smt2irep.cpp
Generated by
1.17.0