GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/sexpr.h Lines: 23 29 79.3 %
Date: 2021-05-24 Branches: 12 54 22.2 %

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