1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
/******************************************************************************
* Top contributors (to current version):
* Tim King, Morgan Deters, Mathias Preiner
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Simple stateless conversion to s-expressions.
*
* This file contains a collection of conversion routines from various data to
* s-expressions as strings. The actual conversion is provided by methods of
* the following form, where T is some type:
*
* toSExpr(std::ostream& out, const T& t)
*
* A fallback is provided where T is a template type that forwards to the
* generic streaming operator `operator<<()` for T.
* To make usage easier, `std::string toSExpr(const T&)` is provided as well.
* For containers, an overload that accepts two iterators is available.
*/
#include "cvc5_private.h"
#ifndef CVC5__SEXPR_H
#define CVC5__SEXPR_H
#include <iostream>
#include <memory>
#include <sstream>
#include <string>
#include <type_traits>
#include <utility>
#include <vector>
namespace cvc5 {
// Forward declarations
struct StatisticBaseValue;
// Non-templated overloads that live in the source file
void toSExpr(std::ostream& out, const std::string& s);
void toSExpr(std::ostream& out, const std::unique_ptr<StatisticBaseValue>& sbv);
/**
* Fallback overload for basic types.
*
* Prints Boolean values as `true` and `false`, integral numbers as numbers and
* all other types using their respective streaming operators, enclosed with
* double quotes.
*/
template <typename T>
void toSExpr(std::ostream& out, const T& t)
{
if constexpr (std::is_same_v<T, bool>)
{
out << (t ? "true" : "false");
}
if constexpr (std::is_integral_v<T>)
{
out << t;
}
else
{
out << "\"" << t << "\"";
}
}
// Forward declarations of templated overloads
template <typename T>
void toSExpr(std::ostream& out, const std::vector<T>& v);
/**
* Render an `std::pair` to an s-expression string.
*/
template <typename T1, typename T2>
void toSExpr(std::ostream& out, const std::pair<T1, T2>& p)
{
out << "(";
toSExpr(out, p.first);
out << " ";
toSExpr(out, p.second);
out << ")";
}
/**
* Render an arbitrary iterator range to an s-expression string.
*/
template <typename Iterator>
void toSExpr(std::ostream& out, Iterator begin, Iterator end)
{
out << "(";
for (auto it = begin; it != end; ++it)
{
if (it != begin)
{
out << " ";
}
toSExpr(out, *it);
}
out << ")";
}
/**
* Render a vector to an s-expression string.
* Convenience wrapper for `std::vector` around the overload using iterators.
*/
template <typename T>
void toSExpr(std::ostream& out, const std::vector<T>& v)
{
toSExpr(out, v.begin(), v.end());
}
/**
* Convert arbitrary data to an s-expression string.
*/
template <typename T>
std::string toSExpr(const T& t)
{
std::stringstream ss;
toSExpr(ss, t);
return ss.str();
}
/**
* Convert an arbitrary iterator range to an s-expression string.
*/
template <typename Iterator>
std::string toSExpr(Iterator begin, Iterator end)
{
std::stringstream ss;
toSExpr(ss, begin, end);
return ss.str();
}
} // namespace cvc5
#endif /* CVC5__SEXPR_H */
|
