tiny.smt.Model

1/// The values a satisfying assignment gives: one per named constant, and one entry per encoded2/// application of each uninterpreted function. A caller reads a constant's value from it with `get`3/// or prints it with `write` after `Encoder.model` returns one for a satisfiable answer. The model4/// owns every name and value in it, and its owner frees them all with `deinit`.5pub const Model = struct {6    allocator: std.mem.Allocator,7    /// The named constants and their values, in the order the constants were built. Two constants8    /// built with one name give two entries, and `get` returns the first.9    entries: std.ArrayList(ModelEntry) = .empty,10    /// The model of each uninterpreted function with an encoded application, one per function name.11    functions: std.ArrayList(FunctionModel) = .empty,1213    /// Returns an empty model that allocates with `allocator`. A caller makes one to build an14    /// expected model by hand, and `Encoder.model` makes one. The call allocates nothing.15    pub fn init(allocator: std.mem.Allocator) Model {16        return .{ .allocator = allocator };17    }1819    /// Frees every name, every value and every function model. The owner calls it once when done20    /// with the values. A value returned by `get` and a pointer returned by `getFunction` are21    /// invalid afterward.22    pub fn deinit(self: *Model) void {23        for (self.entries.items) |*entry| {24            self.allocator.free(entry.name);25            entry.value.deinit(self.allocator);26        }27        self.entries.deinit(self.allocator);28        for (self.functions.items) |*function| {29            function.deinit(self.allocator);30        }31        self.functions.deinit(self.allocator);32        self.* = undefined;33    }3435    /// Adds the constant `name` with value `value`. `Encoder.model` calls it once per named36    /// constant. The call copies `name` and takes ownership of `value`, and on failure it frees37    /// `value`.38    pub fn append(self: *Model, name: []const u8, value: ModelValue) !void {39        var owned_value = value;40        errdefer owned_value.deinit(self.allocator);41        const owned_name = try self.allocator.dupe(u8, name);42        errdefer self.allocator.free(owned_name);43        try self.entries.append(self.allocator, .{ .name = owned_name, .value = owned_value });44    }4546    /// Returns the value of the first constant named `name`, or `null` when the model has none. A47    /// caller reads with it a constant's value after a satisfiable answer, as every encoder test48    /// does. An array value's cells stay owned by the model, so the caller does not free them. The49    /// lookup checks each entry in turn.50    pub fn get(self: *const Model, name: []const u8) ?ModelValue {51        for (self.entries.items) |entry| {52            if (std.mem.eql(u8, entry.name, name)) return entry.value;53        }54        return null;55    }5657    /// Adds an entry with argument values `arguments` and result value `result` to the model of the58    /// function `name`, and creates that function's model on first use. `Encoder.model` calls it59    /// once per encoded application. The call takes ownership of `arguments` and `result`, and on60    /// failure it frees them.61    pub fn appendFunctionApplication(self: *Model, name: []const u8, arguments: []ModelValue, result: ModelValue) !void {62        var owned_result = result;63        errdefer {64            for (arguments) |*argument| {65                argument.deinit(self.allocator);66            }67            self.allocator.free(arguments);68            owned_result.deinit(self.allocator);69        }70        const function = try self.functionModel(name);71        try function.entries.append(self.allocator, .{ .arguments = arguments, .result = owned_result });72    }7374    /// Returns the model of the function `name`, or `null` when no application of it was encoded. A75    /// caller checks the values an uninterpreted function took with it. The model keeps ownership,76    /// and the pointer is valid until the model changes or is freed.77    pub fn getFunction(self: *const Model, name: []const u8) ?*const FunctionModel {78        for (self.functions.items) |*function| {79            if (std.mem.eql(u8, function.name, name)) return function;80        }81        return null;82    }8384    /// Writes one `name: value` line per constant, then per function a `name:` line followed by one85    /// indented `(arguments) -> result` line per entry, with each value in the syntax of86    /// `ModelValue.write`. A caller prints a model for a person to read with it. The call returns87    /// only the writer's errors.88    pub fn write(self: *const Model, writer: *std.Io.Writer) std.Io.Writer.Error!void {89        for (self.entries.items) |entry| {90            try writer.print("{s}: ", .{entry.name});91            try entry.value.write(writer);92            try writer.writeAll("\n");93        }94        for (self.functions.items) |function| {95            try writer.print("{s}:\n", .{function.name});96            for (function.entries.items) |entry| {97                try writer.writeAll("  (");98                for (entry.arguments, 0..) |argument, index| {99                    if (index > 0) try writer.writeAll(", ");100                    try argument.write(writer);101                }102                try writer.writeAll(") -> ");103                try entry.result.write(writer);104                try writer.writeAll("\n");105            }106        }107    }108109    fn functionModel(self: *Model, name: []const u8) !*FunctionModel {110        for (self.functions.items) |*item| {111            if (std.mem.eql(u8, item.name, name)) return item;112        }113        const owned_name = try self.allocator.dupe(u8, name);114        errdefer self.allocator.free(owned_name);115        try self.functions.append(self.allocator, .{ .name = owned_name });116        return &self.functions.items[self.functions.items.len - 1];117    }118};

1pub const Model = bitvec.Model;