fix bug in JSON output: JSON values that are decimals must be preceded by a 0

e.g. 0.5 is valid but .5 is not.
issue#70
Houtan Bastani 2018-10-23 14:00:36 +02:00
parent 9eaf39235e
commit 9968f5c971
1 changed files with 5 additions and 1 deletions

View File

@ -359,7 +359,11 @@ NumConstNode::writeOutput(ostream &output, ExprNodeOutputType output_type,
void
NumConstNode::writeJsonAST(ostream &output) const
{
output << "{\"node_type\" : \"NumConstNode\", \"value\" : " << datatree.num_constants.get(id) << "}";
output << "{\"node_type\" : \"NumConstNode\", \"value\" : ";
double testval = datatree.num_constants.getDouble(id);
if (testval < 1.0 && testval > -1.0 && testval != 0.0)
output << "0";
output << datatree.num_constants.get(id) << "}";
}
void