tiny.smt.smtlib.write

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

1//! Prints a script or a single term as SMT-LIB text. A caller hands a formula it built to another2//! solver, or stores it, and needs text any SMT-LIB reader accepts.3//!4//! Each term kind prints as its SMT-LIB operator applied to its operands, and bit-vector constants5//! print as `(_ bvV W)`. A list operator with one operand prints as the operand alone, and an `and`6//! with none prints as `true` and an `or` with none as `false`. The same rule changes the meaning7//! of `distinct` with one operand, which prints as its operand, and of `+` and `*` with none, which8//! print as `false`. A negative integer prints as `-5`, which standard SMT-LIB readers refuse,9//! since SMT-LIB writes it `(- 5)`. The writer recurses once per level of the term, with no depth10//! bound.11const std = @import("std");12const smt = @import("../root.zig");1314const term = smt.term;1516/// Writes `(set-logic L)` with the script's logic, then one `declare-const` per named constant of17/// the `Context`, one `declare-fun` per function declaration, one `assert` per assertion of the18/// script, and `(check-sat)`, so code can hand a whole formula to another solver or read it back.19/// Declarations follow the order in which the `Context` built them. The call declares every20/// constant and function of the `Context`, including those no assertion uses. Two constants that21/// share a name print two `declare-const` lines with that name, which a reader refuses. The22/// function returns only the writer's errors.23pub fn writeScript(writer: *std.Io.Writer, script: *const term.Script) std.Io.Writer.Error!void {24    try writer.print("(set-logic {s})\n", .{script.logic});25    for (script.ctx.nodes.items) |node| {26        switch (node) {27            .symbol => |symbol| {28                try writer.print("(declare-const {s} ", .{symbol.name});29                try symbol.sort.write(writer);30                try writer.writeAll(")\n");31            },32            else => {},33        }34    }35    for (script.ctx.functions.items) |decl| {36        try writer.print("(declare-fun {s} (", .{decl.name});37        for (decl.params, 0..) |param, index| {38            if (index > 0) try writer.writeAll(" ");39            try param.write(writer);40        }41        try writer.writeAll(") ");42        try decl.result.write(writer);43        try writer.writeAll(")\n");44    }45    for (script.assertions.items) |assertion| {46        try writer.writeAll("(assert ");47        try writeTerm(writer, script.ctx, assertion);48        try writer.writeAll(")\n");49    }50    try writer.writeAll("(check-sat)\n");51}5253/// Writes the term `id` of `ctx` in SMT-LIB syntax, so code can print a single term for a message54/// or a log, and `writeScript` calls it for every assertion. A constant prints as its name, and an55/// application of a function with no arguments as the function's name alone. An `and` with no56/// operands prints as `true` and an `or` with none as `false`, and a list operator with one operand57/// prints the operand alone. `distinct` with one operand prints as its operand, `+` and `*` with no58/// operands print as `false`, and a negative integer prints as `-5`: each reads back as a different59/// term or fails in standard readers. An `id` past the terms of `ctx` makes the call panic. The60/// function returns only the writer's errors.61pub fn writeTerm(writer: *std.Io.Writer, ctx: *const term.Context, id: term.Term) std.Io.Writer.Error!void {62    const node = ctx.nodes.items[id];63    switch (node) {64        .symbol => |symbol| try writer.writeAll(symbol.name),65        .apply => |item| try writeApply(writer, ctx, item.function, item.args),66        .bool => |value| try writer.writeAll(if (value) "true" else "false"),67        .int => |value| try writer.print("{d}", .{value}),68        .bitvec => |value| try writer.print("(_ bv{d} {d})", .{ value.value, value.width }),69        .not => |operand| try writeUnary(writer, ctx, "not", operand),70        .and_ => |operands| try writeNary(writer, ctx, "and", operands),71        .or_ => |operands| try writeNary(writer, ctx, "or", operands),72        .implies => |pair| try writeBinary(writer, ctx, "=>", pair.lhs, pair.rhs),73        .eq => |pair| try writeBinary(writer, ctx, "=", pair.lhs, pair.rhs),74        .distinct => |operands| try writeNary(writer, ctx, "distinct", operands),75        .add => |operands| try writeNary(writer, ctx, "+", operands),76        .mul => |operands| try writeNary(writer, ctx, "*", operands),77        .le => |pair| try writeBinary(writer, ctx, "<=", pair.lhs, pair.rhs),78        .lt => |pair| try writeBinary(writer, ctx, "<", pair.lhs, pair.rhs),79        .ge => |pair| try writeBinary(writer, ctx, ">=", pair.lhs, pair.rhs),80        .gt => |pair| try writeBinary(writer, ctx, ">", pair.lhs, pair.rhs),81        .bvule => |pair| try writeBinary(writer, ctx, "bvule", pair.lhs, pair.rhs),82        .bvult => |pair| try writeBinary(writer, ctx, "bvult", pair.lhs, pair.rhs),83        .bvsle => |pair| try writeBinary(writer, ctx, "bvsle", pair.lhs, pair.rhs),84        .bvslt => |pair| try writeBinary(writer, ctx, "bvslt", pair.lhs, pair.rhs),85        .bvuaddo => |pair| try writeBinary(writer, ctx, "bvuaddo", pair.lhs, pair.rhs),86        .bvsaddo => |pair| try writeBinary(writer, ctx, "bvsaddo", pair.lhs, pair.rhs),87        .bvssubo => |pair| try writeBinary(writer, ctx, "bvssubo", pair.lhs, pair.rhs),88        .bvumulo => |pair| try writeBinary(writer, ctx, "bvumulo", pair.lhs, pair.rhs),89        .bvsmulo => |pair| try writeBinary(writer, ctx, "bvsmulo", pair.lhs, pair.rhs),90        .bvnot => |operand| try writeUnary(writer, ctx, "bvnot", operand),91        .bvand => |pair| try writeBinary(writer, ctx, "bvand", pair.lhs, pair.rhs),92        .bvor => |pair| try writeBinary(writer, ctx, "bvor", pair.lhs, pair.rhs),93        .bvxor => |pair| try writeBinary(writer, ctx, "bvxor", pair.lhs, pair.rhs),94        .bvshl => |pair| try writeBinary(writer, ctx, "bvshl", pair.lhs, pair.rhs),95        .bvlshr => |pair| try writeBinary(writer, ctx, "bvlshr", pair.lhs, pair.rhs),96        .bvashr => |pair| try writeBinary(writer, ctx, "bvashr", pair.lhs, pair.rhs),97        .bvudiv => |pair| try writeBinary(writer, ctx, "bvudiv", pair.lhs, pair.rhs),98        .bvurem => |pair| try writeBinary(writer, ctx, "bvurem", pair.lhs, pair.rhs),99        .bvsdiv => |pair| try writeBinary(writer, ctx, "bvsdiv", pair.lhs, pair.rhs),100        .bvsrem => |pair| try writeBinary(writer, ctx, "bvsrem", pair.lhs, pair.rhs),101        .bvsmod => |pair| try writeBinary(writer, ctx, "bvsmod", pair.lhs, pair.rhs),102        .array_select => |item| try writeBinary(writer, ctx, "select", item.array, item.index),103        .array_store => |item| try writeTernary(writer, ctx, "store", item.array, item.index, item.value),104        .bvconcat => |pair| try writeBinary(writer, ctx, "concat", pair.lhs, pair.rhs),105        .bvextract => |item| try writeExtract(writer, ctx, item.operand, item.high, item.low),106        .bvzeroext => |item| try writeExtension(writer, ctx, "zero_extend", item.operand, item.extra),107        .bvsignext => |item| try writeExtension(writer, ctx, "sign_extend", item.operand, item.extra),108        .bvrotl => |item| try writeExtension(writer, ctx, "rotate_left", item.operand, item.amount),109        .bvrotr => |item| try writeExtension(writer, ctx, "rotate_right", item.operand, item.amount),110        .bvadd => |pair| try writeBinary(writer, ctx, "bvadd", pair.lhs, pair.rhs),111        .bvsub => |pair| try writeBinary(writer, ctx, "bvsub", pair.lhs, pair.rhs),112        .bvmul => |pair| try writeBinary(writer, ctx, "bvmul", pair.lhs, pair.rhs),113    }114}115116fn writeApply(writer: *std.Io.Writer, ctx: *const term.Context, function_id: term.Function, args: []const term.Term) std.Io.Writer.Error!void {117    const decl = ctx.functions.items[function_id];118    if (args.len == 0) {119        try writer.writeAll(decl.name);120        return;121    }122    try writer.print("({s}", .{decl.name});123    for (args) |arg| {124        try writer.writeAll(" ");125        try writeTerm(writer, ctx, arg);126    }127    try writer.writeAll(")");128}129130fn writeUnary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, operand: term.Term) std.Io.Writer.Error!void {131    try writer.print("({s} ", .{name});132    try writeTerm(writer, ctx, operand);133    try writer.writeAll(")");134}135136fn writeBinary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, lhs: term.Term, rhs: term.Term) std.Io.Writer.Error!void {137    try writer.print("({s} ", .{name});138    try writeTerm(writer, ctx, lhs);139    try writer.writeAll(" ");140    try writeTerm(writer, ctx, rhs);141    try writer.writeAll(")");142}143144fn writeTernary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, first: term.Term, second: term.Term, third: term.Term) std.Io.Writer.Error!void {145    try writer.print("({s} ", .{name});146    try writeTerm(writer, ctx, first);147    try writer.writeAll(" ");148    try writeTerm(writer, ctx, second);149    try writer.writeAll(" ");150    try writeTerm(writer, ctx, third);151    try writer.writeAll(")");152}153154fn writeExtract(writer: *std.Io.Writer, ctx: *const term.Context, operand: term.Term, high: u32, low: u32) std.Io.Writer.Error!void {155    try writer.print("((_ extract {d} {d}) ", .{ high, low });156    try writeTerm(writer, ctx, operand);157    try writer.writeAll(")");158}159160fn writeExtension(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, operand: term.Term, extra: u32) std.Io.Writer.Error!void {161    try writer.print("((_ {s} {d}) ", .{ name, extra });162    try writeTerm(writer, ctx, operand);163    try writer.writeAll(")");164}165166fn writeNary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, operands: []const term.Term) std.Io.Writer.Error!void {167    if (operands.len == 0) {168        try writer.writeAll(if (std.mem.eql(u8, name, "and")) "true" else "false");169        return;170    }171    if (operands.len == 1) {172        try writeTerm(writer, ctx, operands[0]);173        return;174    }175    try writer.print("({s}", .{name});176    for (operands) |operand| {177        try writer.writeAll(" ");178        try writeTerm(writer, ctx, operand);179    }180    try writer.writeAll(")");181}182183test "SMT-LIB writer emits declarations and assertions" {184    var ctx = term.Context.init(std.testing.allocator);185    defer ctx.deinit();186    var script = term.Script.init(&ctx, "QF_LIA");187    defer script.deinit();188    const x = try ctx.symbol("x", .int);189    const zero = try ctx.intValue(0);190    try script.assertTerm(try ctx.ge(x, zero));191    var buffer: [512]u8 = undefined;192    var stream = std.Io.Writer.fixed(&buffer);193    try writeScript(&stream, &script);194    const text = stream.buffered();195    try std.testing.expect(std.mem.indexOf(u8, text, "(set-logic QF_LIA)\n") != null);196    try std.testing.expect(std.mem.indexOf(u8, text, "(declare-const x Int)\n") != null);197    try std.testing.expect(std.mem.indexOf(u8, text, "(assert (>= x 0))\n") != null);198}