tiny.pluck.toplevel.json

1const std = @import("std");2const pretty = @import("pretty");3const result_owner = @import("result.zig");4const top_types = @import("types.zig");56const QueryResult = result_owner.QueryResult;7const QueryOutcome = top_types.QueryOutcome;8const Span = top_types.SourceSpan;9const pretty_json = pretty.json;1011pub fn writeQueryResult(result: *const QueryResult, writer: anytype) !void {12    var stream = pretty_json.Writer.init(writer, .minified);13    const object = try stream.object();14    try writeQueryResultFields(result, object);15    try object.endLine();16}1718pub fn writeQueryResultFields(result: *const QueryResult, object: pretty_json.Object) !void {19    const status: []const u8 = if (result.program_error)20        "error"21    else if (result.limit_reason != null)22        "partial"23    else if (result.outcomes.len == 0)24        "error"25    else26        "success";2728    const outcomes = try object.array("outcomes");29    for (result.outcomes) |outcome| {30        const outcome_object = try outcomes.object();31        try outcome_object.field("value", outcome.value_str);32        try outcome_object.print("probability", "{d}", .{outcome.probability});33        try outcome_object.end();34    }35    try outcomes.end();3637    const stats = try object.object("stats");38    try stats.field("time_ns", result.stats.time_ns);39    try stats.field("wmc_time_ns", result.stats.wmc_time_ns);40    try stats.field("refinement_time_ns", result.stats.refinement_time_ns);41    try stats.field("refinement_count", result.stats.refinement_count);42    if (result.stats.num_forward_calls > 0) {43        try stats.field("forward_calls", result.stats.num_forward_calls);44    }45    if (result.stats.num_recursive_calls > 0) {46        try stats.field("recursive_calls", result.stats.num_recursive_calls);47    }48    if (result.stats.variable_count > 0) {49        try stats.field("bdd_variables", result.stats.variable_count);50    }51    if (result.stats.node_count > 0) {52        try stats.field("bdd_nodes", result.stats.node_count);53    }54    const total_cache = result.stats.ite_cache_hits + result.stats.ite_cache_misses;55    if (total_cache > 0) {56        try stats.field("ite_cache_hits", result.stats.ite_cache_hits);57        try stats.field("ite_cache_misses", result.stats.ite_cache_misses);58    }59    if (result.stats.unique_table_grows > 0) {60        try stats.field("bdd_unique_table_grows", result.stats.unique_table_grows);61    }62    if (result.stats.ite_cache_grows > 0) {63        try stats.field("ite_cache_grows", result.stats.ite_cache_grows);64    }65    const total_thunks = result.stats.thunk_reuse_hits + result.stats.thunk_reuse_misses;66    if (total_thunks > 0) {67        try stats.field("thunk_reuse_hits", result.stats.thunk_reuse_hits);68        try stats.field("thunk_reuse_misses", result.stats.thunk_reuse_misses);69    }70    if (result.stats.thunk_evaluations > 0) {71        try stats.field("thunk_evaluations", result.stats.thunk_evaluations);72        try stats.field("thunk_cache_hits", result.stats.thunk_cache_hits);73    }74    if (result.stats.bdd_samples_len > 0) {75        const samples = try stats.array("bdd_samples");76        var i: usize = 0;77        while (i < @as(usize, result.stats.bdd_samples_len)) : (i += 1) {78            const sample = try samples.object();79            try sample.field("forward_calls", result.stats.bdd_samples_forward_calls[i]);80            try sample.field("bdd_variables", result.stats.bdd_samples_vars[i]);81            try sample.field("bdd_nodes", result.stats.bdd_samples_nodes[i]);82            try sample.end();83        }84        try samples.end();85    }86    try stats.end();87    try object.field("program_error", result.program_error);88    if (result.limit_reason) |reason| {89        try object.field("limit_reason", @tagName(reason));90    }91    try object.field("status", status);92}9394pub const JsonError = struct {95    type: []const u8,96    message: []const u8,97    file: ?[]const u8 = null,98    span: ?Span = null,99100    pub fn write(self: JsonError, writer: anytype) !void {101        var stream = pretty_json.Writer.init(writer, .minified);102        const object = try stream.object();103        try object.field("type", self.type);104        try object.field("message", self.message);105        if (self.file) |f| {106            try object.field("file", f);107        }108        if (self.span) |s| {109            const span = try object.object("span");110            const start = try span.object("start");111            try start.field("line", s.start.line);112            try start.field("column", s.start.column);113            try start.field("offset", s.start.offset);114            try start.end();115            const end = try span.object("end");116            try end.field("line", s.end.line);117            try end.field("column", s.end.column);118            try end.field("offset", s.end.offset);119            try end.end();120            try span.end();121        }122        try object.endLine();123    }124};125126test "writeQueryResult includes bdd stats and samples" {127    const allocator = std.testing.allocator;128    const outcomes = try allocator.alloc(QueryOutcome, 1);129    outcomes[0] = .{130        .value_str = try allocator.dupe(u8, "True"),131        .probability = 0.5,132    };133134    var result = QueryResult{135        .outcomes = outcomes,136        .stats = .{137            .time_ns = 123,138            .wmc_time_ns = 100,139            .refinement_time_ns = 50,140            .refinement_count = 2,141            .num_forward_calls = 4,142            .num_recursive_calls = 8,143            .variable_count = 3,144            .node_count = 10,145            .ite_cache_hits = 5,146            .ite_cache_misses = 2,147            .bdd_samples_len = 1,148        },149        .limit_reason = null,150        .program_error = false,151        .allocator = allocator,152    };153    result.stats.bdd_samples_forward_calls[0] = 4;154    result.stats.bdd_samples_vars[0] = 3;155    result.stats.bdd_samples_nodes[0] = 10;156    defer result.deinit();157158    var out_buf: [1024]u8 = undefined;159    var out_stream = std.Io.Writer.fixed(&out_buf);160    try writeQueryResult(&result, &out_stream);161    const written = out_stream.buffered();162163    try std.testing.expect(std.mem.indexOf(u8, written, "\"wmc_time_ns\":100") != null);164    try std.testing.expect(std.mem.indexOf(u8, written, "\"bdd_nodes\":10") != null);165    try std.testing.expect(std.mem.indexOf(u8, written, "\"bdd_samples\"") != null);166}167168test "writeQueryResult includes program_error and limit_reason fields" {169    const allocator = std.testing.allocator;170    const outcomes = try allocator.alloc(QueryOutcome, 1);171    outcomes[0] = .{172        .value_str = try allocator.dupe(u8, "True"),173        .probability = 1.0,174    };175176    var result = QueryResult{177        .outcomes = outcomes,178        .stats = .{},179        .limit_reason = .factor_weight_too_complex,180        .program_error = false,181        .allocator = allocator,182    };183    defer result.deinit();184185    var out_buf: [1024]u8 = undefined;186    var out_stream = std.Io.Writer.fixed(&out_buf);187    try writeQueryResult(&result, &out_stream);188    const written = out_stream.buffered();189190    try std.testing.expect(std.mem.indexOf(u8, written, "\"program_error\":false") != null);191    try std.testing.expect(std.mem.indexOf(u8, written, "\"limit_reason\":\"factor_weight_too_complex\"") != null);192    try std.testing.expect(std.mem.indexOf(u8, written, "\"status\":\"partial\"") != null);193}194195test "JsonError includes span when present" {196    var buf: [512]u8 = undefined;197    var writer = std.Io.Writer.fixed(&buf);198199    const span = Span{200        .start = .{ .line = 0, .column = 1, .offset = 2 },201        .end = .{ .line = 0, .column = 2, .offset = 3 },202    };203204    const err = JsonError{205        .type = "eval_error",206        .message = "oops\n\"quoted\"",207        .span = span,208    };209210    try err.write(&writer);211    try std.testing.expectEqualStrings(212        "{\"type\":\"eval_error\",\"message\":\"oops\\n\\\"quoted\\\"\",\"span\":{\"start\":{\"line\":0,\"column\":1,\"offset\":2},\"end\":{\"line\":0,\"column\":2,\"offset\":3}}}\n",213        writer.buffered(),214    );215}

1pub const json = @import("json.zig");