tiny.smt.ModelValue

1/// The value of a constant, a function argument or a function result in a model: a Boolean, a2/// bit-vector or an array, for code that reads one from a `Model` to print it or compare it with an3/// expected value. A value that holds an array owns its cells, so its owner calls `deinit`.4pub const ModelValue = union(enum) {5    /// A Boolean value.6    bool: bool,7    /// A bit-vector value: its bits as an unsigned number, least significant bit as bit 0, and its8    /// width.9    bitvec: struct {10        value: u128,11        width: u32,12    },13    /// An array value: its index width, its element width and one number per cell, the cell for14    /// index i at position i. The cells are a slice the value owns.15    array: struct {16        index_width: u32,17        element_width: u32,18        cells: []u128,19    },2021    /// Frees an array value's cells with `allocator`, which has to be the allocator that made them,22    /// for a caller that holds a value outside a `Model`. The function frees nothing for a Boolean23    /// or a bit-vector.24    pub fn deinit(self: *ModelValue, allocator: std.mem.Allocator) void {25        switch (self.*) {26            .array => |array| allocator.free(array.cells),27            else => {},28        }29        self.* = undefined;30    }3132    /// Writes the value in SMT-LIB syntax: `true` or `false`, `(_ bvV W)`, or an array as33    /// `(array (_ BitVec i) (_ BitVec e) 0->(_ bvV e) ...)` with one index and value per cell, for34    /// `Model.write` to call for every value. The function returns only the writer's errors.35    pub fn write(self: ModelValue, writer: *std.Io.Writer) std.Io.Writer.Error!void {36        switch (self) {37            .bool => |value| try writer.writeAll(if (value) "true" else "false"),38            .bitvec => |value| try writer.print("(_ bv{d} {d})", .{ value.value, value.width }),39            .array => |value| {40                try writer.print("(array (_ BitVec {d}) (_ BitVec {d})", .{ value.index_width, value.element_width });41                for (value.cells, 0..) |cell, index| {42                    try writer.print(" {d}->(_ bv{d} {d})", .{ index, cell, value.element_width });43                }44                try writer.writeAll(")");45            },46        }47    }48};

1pub const ModelValue = bitvec.ModelValue;