Method convertDoubleToString

src/proofs/JsonWriter.cpp:334–344

}

String JsonWriter::convertDoubleToString( double value )
{
    std::stringstream s;
    s << std::fixed << std::setprecision( JSONWRITER_PRECISION ) << value;
    String str = String( s.str() ).trimZerosFromRight();

    // Add .0 for integers for some JSON parsers.
    if ( !str.contains( "." ) )
        str += String( ".0" );
    return str;
}

String JsonWriter::convertDoubleArrayToString( const double *arr, unsigned size )
{