Branch data     Line data    Source code

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