Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer, Tim King, Morgan Deters
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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::internal {
      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                 :          0 : 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                 :          0 :     out << t;
      66                 :            :   }
      67                 :            :   else
      68                 :            :   {
      69                 :            :     out << "\"" << t << "\"";
      70                 :            :   }
      71                 :          0 : }
      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                 :        122 : void toSExpr(std::ostream& out, const std::pair<T1, T2>& p)
      82                 :            : {
      83                 :        122 :   out << "(";
      84                 :        122 :   toSExpr(out, p.first);
      85                 :        122 :   out << " ";
      86                 :        122 :   toSExpr(out, p.second);
      87                 :        122 :   out << ")";
      88                 :        122 : }
      89                 :            : 
      90                 :            : /**
      91                 :            :  * Render an arbitrary iterator range to an s-expression string.
      92                 :            :  */
      93                 :            : template <typename Iterator>
      94                 :          2 : void toSExpr(std::ostream& out, Iterator begin, Iterator end)
      95                 :            : {
      96                 :          2 :   out << "(";
      97         [ +  + ]:        124 :   for (auto it = begin; it != end; ++it)
      98                 :            :   {
      99         [ +  + ]:        122 :     if (it != begin)
     100                 :            :     {
     101                 :        120 :       out << " ";
     102                 :            :     }
     103                 :        122 :     toSExpr(out, *it);
     104                 :            :   }
     105                 :          2 :   out << ")";
     106                 :          2 : }
     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                 :          0 : void toSExpr(std::ostream& out, const std::vector<T>& v)
     114                 :            : {
     115                 :          0 :   toSExpr(out, v.begin(), v.end());
     116                 :          0 : }
     117                 :            : 
     118                 :            : /**
     119                 :            :  * Convert arbitrary data to an s-expression string.
     120                 :            :  */
     121                 :            : template <typename T>
     122                 :        225 : std::string toSExpr(const T& t)
     123                 :            : {
     124                 :        450 :   std::stringstream ss;
     125                 :        225 :   toSExpr(ss, t);
     126                 :        450 :   return ss.str();
     127                 :            : }
     128                 :            : 
     129                 :            : /**
     130                 :            :  * Convert an arbitrary iterator range to an s-expression string.
     131                 :            :  */
     132                 :            : template <typename Iterator>
     133                 :          2 : std::string toSExpr(Iterator begin, Iterator end)
     134                 :            : {
     135                 :          4 :   std::stringstream ss;
     136                 :          2 :   toSExpr(ss, begin, end);
     137                 :          4 :   return ss.str();
     138                 :            : }
     139                 :            : 
     140                 :            : }  // namespace cvc5::internal
     141                 :            : 
     142                 :            : #endif /* CVC5__SEXPR_H */