tiny.smt.bitvec

1//! Decides formulas over Booleans, fixed-width bit-vectors, arrays and uninterpreted functions by2//! turning them into clauses for a SAT solver, and reads a satisfying assignment back as a value3//! for each constant.4//!5//! A caller holds a formula and needs to know whether some values of its constants make it true,6//! and which values do. A caller also tests a condition without asserting it for good, and after a7//! contradiction learns a set of its tested conditions that the formula refutes together.8//!9//! A SAT solver accepts only clauses over Boolean variables, so every bit-vector operation has to10//! become Boolean relations between single bits. An array with an index of w bits has 2 to the11//! power w cells, so its size doubles with each index bit. An uninterpreted function has no12//! definition: the only thing known about it is that equal arguments give equal results.13//!14//! [SMT-LIB](https://smt-lib.org/) defines the fixed-size bit-vector operators on every input,15//! division by zero and shifts past the width included. The encoder follows those definitions:16//! unsigned division by zero gives all ones, the remainder by zero is the dividend, a left shift or17//! a logical right shift by at least the width gives zero, and an arithmetic right shift by at18//! least the width copies the sign bit into every bit.19//!20//! The encoder (`Encoder`) gives each bit-vector one Boolean variable per bit, least significant21//! bit first, and each operator the clauses of and, or and exclusive-or gates over those bits.22//! Addition carries from each bit to the next, multiplication adds one shifted partial product per23//! bit, and division finds its quotient one bit at a time from the most significant bit down. One24//! variable fixed true by a unit clause stands for true, and its negation stands for false, so25//! every bit of a Boolean constant or a bit-vector constant is one of those two literals.26//!27//! An array becomes one cell of element bits for each index value, so the encoder refuses an index28//! wider than eight bits with `ArrayIndexTooWide` and an array has at most 256 cells. Two arrays29//! are equal when every pair of cells is equal.30//!31//! For each pair of applications of one function, one clause makes their results equal whenever32//! their arguments are equal. The encoder writes these clauses once, the first time a caller33//! asserts, assumes or solves, over every application in the `Context`, asserted or not.34//!35//! The encoder encodes each term once and remembers the result, in a table sized to the `Context`36//! at `Encoder.init`, so a term built after `init` fails with `TermOutOfRange`. Integer terms and37//! `distinct` fail with `UnsupportedTerm`. `solve` encodes every named constant of the `Context`,38//! so a single integer constant fails every solve.39//!40//! After a satisfiable answer, `Encoder.model` reads the solver's assignment into a `Model`: one41//! value per named constant and one entry per encoded function application. A model value holds at42//! most 128 bits, and a wider named constant, function argument, function result or array cell43//! fails with `ModelValueTooWide`.44//!45//! A caller builds an `Encoder` over a `Context` and a `sat.Solver`, asserts terms with46//! `assertTerm`, assumes terms with `assumeTerm`, and calls `solve`. On a satisfiable answer it47//! reads `model`, and on an unsatisfiable one it asks the solver for the unsat core and the proof.48const std = @import("std");49const sat = @import("sat/root.zig");50const term = @import("term.zig");5152/// The errors the encoder and `Encoder.model` return besides the solver's and the allocator's, for53/// code that reports why a formula could not be encoded or read back. The encoder's functions54/// return `Error`, which is `anyerror`, so the compiler does not check a switch on these tags for55/// completeness.56pub const EncodeError = error{57    /// A term used as a condition, such as an assertion, an assumption or an operand of `and`, has58    /// another sort.59    ExpectedBool,60    /// A term used as a bit-vector operand has another sort.61    ExpectedBitVec,62    /// The operands of an operator have different widths or different kinds, or an application's63    /// argument count differs from its declaration.64    SortMismatch,65    /// The term is an integer term or `distinct`, which the encoder does not support, or it66    /// compares two values that were never encoded.67    UnsupportedTerm,68    /// `Encoder.model` found a constant with no value: the solver has not assigned it, or it was69    /// never encoded. The error follows a model read before a satisfiable answer, or of a constant70    /// that `encodeSymbols` has not reached.71    ModelUnavailable,72    /// `Encoder.model` found a value wider than 128 bits.73    ModelValueTooWide,74    /// The term's index is past the terms that existed when the `Encoder` was built.75    TermOutOfRange,76    /// An extract range lies outside its operand, or an operator that needs at least one bit got a77    /// bit-vector of width 0.78    InvalidBitVectorRange,79    /// A term used as an array has another sort.80    ExpectedArray,81    /// An array's index is wider than eight bits.82    ArrayIndexTooWide,83    /// An application names a function past the declarations of the `Context`.84    FunctionOutOfRange,85};8687/// The error set of the encoder's functions: any error, returned by every public function of the88/// encoder, so a caller can absorb it into its own error set. The set covers `EncodeError`, the89/// solver's errors, `error.OutOfMemory` and the errors of `Context.sortOf`. Because it is90/// `anyerror`, the compiler cannot list the errors a call returns.91pub const Error = anyerror;9293const max_native_array_index_width = 8;9495const ArrayValue = struct {96    index_width: u32,97    element_width: u32,98    cells: [][]sat.Literal,99};100101const Value = union(enum) {102    none,103    bool: sat.Literal,104    bits: []sat.Literal,105    array: ArrayValue,106};107108/// The value of a constant, a function argument or a function result in a model: a Boolean, a109/// bit-vector or an array, for code that reads one from a `Model` to print it or compare it with an110/// expected value. A value that holds an array owns its cells, so its owner calls `deinit`.111pub const ModelValue = union(enum) {112    /// A Boolean value.113    bool: bool,114    /// A bit-vector value: its bits as an unsigned number, least significant bit as bit 0, and its115    /// width.116    bitvec: struct {117        value: u128,118        width: u32,119    },120    /// An array value: its index width, its element width and one number per cell, the cell for121    /// index i at position i. The cells are a slice the value owns.122    array: struct {123        index_width: u32,124        element_width: u32,125        cells: []u128,126    },127128    /// Frees an array value's cells with `allocator`, which has to be the allocator that made them,129    /// for a caller that holds a value outside a `Model`. The function frees nothing for a Boolean130    /// or a bit-vector.131    pub fn deinit(self: *ModelValue, allocator: std.mem.Allocator) void {132        switch (self.*) {133            .array => |array| allocator.free(array.cells),134            else => {},135        }136        self.* = undefined;137    }138139    /// Writes the value in SMT-LIB syntax: `true` or `false`, `(_ bvV W)`, or an array as140    /// `(array (_ BitVec i) (_ BitVec e) 0->(_ bvV e) ...)` with one index and value per cell, for141    /// `Model.write` to call for every value. The function returns only the writer's errors.142    pub fn write(self: ModelValue, writer: *std.Io.Writer) std.Io.Writer.Error!void {143        switch (self) {144            .bool => |value| try writer.writeAll(if (value) "true" else "false"),145            .bitvec => |value| try writer.print("(_ bv{d} {d})", .{ value.value, value.width }),146            .array => |value| {147                try writer.print("(array (_ BitVec {d}) (_ BitVec {d})", .{ value.index_width, value.element_width });148                for (value.cells, 0..) |cell, index| {149                    try writer.print(" {d}->(_ bv{d} {d})", .{ index, cell, value.element_width });150                }151                try writer.writeAll(")");152            },153        }154    }155};156157/// One named constant of a model and its value, for code that walks a `Model`.158pub const ModelEntry = struct {159    /// The constant's name, a copy the `Model` owns and frees.160    name: []u8,161    /// The constant's value, which the `Model` owns and frees.162    value: ModelValue,163};164165/// One application of an uninterpreted function in a model: its argument values and its result166/// value, for code that checks a function's model.167pub const FunctionModelEntry = struct {168    /// The argument values in declaration order, a slice the entry owns.169    arguments: []ModelValue,170    /// The value of the application's result, which the entry owns.171    result: ModelValue,172173    /// Frees every argument value, the argument slice and the result value with `allocator`, for174    /// `FunctionModel.deinit` to call for each entry.175    pub fn deinit(self: *FunctionModelEntry, allocator: std.mem.Allocator) void {176        for (self.arguments) |*argument| {177            argument.deinit(allocator);178        }179        allocator.free(self.arguments);180        self.result.deinit(allocator);181        self.* = undefined;182    }183};184185/// The model of one uninterpreted function: its name and one entry per application the encoder186/// encoded, returned by `Model.getFunction` so code can check each application of one function. The187/// model lists the applications in the formula, and it gives no value for other arguments.188pub const FunctionModel = struct {189    /// The function's name, a copy the model owns.190    name: []u8,191    /// The entries in the order of their applications in the `Context`. Two applications with equal192    /// arguments give two entries with equal results.193    entries: std.ArrayList(FunctionModelEntry) = .empty,194195    /// Frees the name, every entry and the entry list with `allocator`, for `Model.deinit` to call196    /// for each function.197    pub fn deinit(self: *FunctionModel, allocator: std.mem.Allocator) void {198        allocator.free(self.name);199        for (self.entries.items) |*entry| {200            entry.deinit(allocator);201        }202        self.entries.deinit(allocator);203        self.* = undefined;204    }205};206207/// The values a satisfying assignment gives: one per named constant, and one entry per encoded208/// application of each uninterpreted function. A caller reads a constant's value from it with `get`209/// or prints it with `write` after `Encoder.model` returns one for a satisfiable answer. The model210/// owns every name and value in it, and its owner frees them all with `deinit`.211pub const Model = struct {212    allocator: std.mem.Allocator,213    /// The named constants and their values, in the order the constants were built. Two constants214    /// built with one name give two entries, and `get` returns the first.215    entries: std.ArrayList(ModelEntry) = .empty,216    /// The model of each uninterpreted function with an encoded application, one per function name.217    functions: std.ArrayList(FunctionModel) = .empty,218219    /// Returns an empty model that allocates with `allocator`. A caller makes one to build an220    /// expected model by hand, and `Encoder.model` makes one. The call allocates nothing.221    pub fn init(allocator: std.mem.Allocator) Model {222        return .{ .allocator = allocator };223    }224225    /// Frees every name, every value and every function model. The owner calls it once when done226    /// with the values. A value returned by `get` and a pointer returned by `getFunction` are227    /// invalid afterward.228    pub fn deinit(self: *Model) void {229        for (self.entries.items) |*entry| {230            self.allocator.free(entry.name);231            entry.value.deinit(self.allocator);232        }233        self.entries.deinit(self.allocator);234        for (self.functions.items) |*function| {235            function.deinit(self.allocator);236        }237        self.functions.deinit(self.allocator);238        self.* = undefined;239    }240241    /// Adds the constant `name` with value `value`. `Encoder.model` calls it once per named242    /// constant. The call copies `name` and takes ownership of `value`, and on failure it frees243    /// `value`.244    pub fn append(self: *Model, name: []const u8, value: ModelValue) !void {245        var owned_value = value;246        errdefer owned_value.deinit(self.allocator);247        const owned_name = try self.allocator.dupe(u8, name);248        errdefer self.allocator.free(owned_name);249        try self.entries.append(self.allocator, .{ .name = owned_name, .value = owned_value });250    }251252    /// Returns the value of the first constant named `name`, or `null` when the model has none. A253    /// caller reads with it a constant's value after a satisfiable answer, as every encoder test254    /// does. An array value's cells stay owned by the model, so the caller does not free them. The255    /// lookup checks each entry in turn.256    pub fn get(self: *const Model, name: []const u8) ?ModelValue {257        for (self.entries.items) |entry| {258            if (std.mem.eql(u8, entry.name, name)) return entry.value;259        }260        return null;261    }262263    /// Adds an entry with argument values `arguments` and result value `result` to the model of the264    /// function `name`, and creates that function's model on first use. `Encoder.model` calls it265    /// once per encoded application. The call takes ownership of `arguments` and `result`, and on266    /// failure it frees them.267    pub fn appendFunctionApplication(self: *Model, name: []const u8, arguments: []ModelValue, result: ModelValue) !void {268        var owned_result = result;269        errdefer {270            for (arguments) |*argument| {271                argument.deinit(self.allocator);272            }273            self.allocator.free(arguments);274            owned_result.deinit(self.allocator);275        }276        const function = try self.functionModel(name);277        try function.entries.append(self.allocator, .{ .arguments = arguments, .result = owned_result });278    }279280    /// Returns the model of the function `name`, or `null` when no application of it was encoded. A281    /// caller checks the values an uninterpreted function took with it. The model keeps ownership,282    /// and the pointer is valid until the model changes or is freed.283    pub fn getFunction(self: *const Model, name: []const u8) ?*const FunctionModel {284        for (self.functions.items) |*function| {285            if (std.mem.eql(u8, function.name, name)) return function;286        }287        return null;288    }289290    /// Writes one `name: value` line per constant, then per function a `name:` line followed by one291    /// indented `(arguments) -> result` line per entry, with each value in the syntax of292    /// `ModelValue.write`. A caller prints a model for a person to read with it. The call returns293    /// only the writer's errors.294    pub fn write(self: *const Model, writer: *std.Io.Writer) std.Io.Writer.Error!void {295        for (self.entries.items) |entry| {296            try writer.print("{s}: ", .{entry.name});297            try entry.value.write(writer);298            try writer.writeAll("\n");299        }300        for (self.functions.items) |function| {301            try writer.print("{s}:\n", .{function.name});302            for (function.entries.items) |entry| {303                try writer.writeAll("  (");304                for (entry.arguments, 0..) |argument, index| {305                    if (index > 0) try writer.writeAll(", ");306                    try argument.write(writer);307                }308                try writer.writeAll(") -> ");309                try entry.result.write(writer);310                try writer.writeAll("\n");311            }312        }313    }314315    fn functionModel(self: *Model, name: []const u8) !*FunctionModel {316        for (self.functions.items) |*item| {317            if (std.mem.eql(u8, item.name, name)) return item;318        }319        const owned_name = try self.allocator.dupe(u8, name);320        errdefer self.allocator.free(owned_name);321        try self.functions.append(self.allocator, .{ .name = owned_name });322        return &self.functions.items[self.functions.items.len - 1];323    }324};325326const BitwiseKind = enum {327    and_,328    or_,329    xor,330};331332const ShiftKind = enum {333    left,334    right,335};336337const RotateKind = enum {338    left,339    right,340};341342const DivRemResult = struct {343    quotient: []sat.Literal,344    remainder: []sat.Literal,345};346347const ExtendKind = enum {348    zero,349    sign,350};351352/// Turns the terms of one `Context` into clauses of one `sat.Solver`, and reads the solver's353/// assignment back as a `Model`. A caller builds one per solve, over the `Context` that holds its354/// terms and the solver that will decide them. The encoder borrows the `Context` and the solver, so355/// both have to outlive it. The encoder encodes each term once and remembers the result, and the356/// clauses it adds stay in the solver.357pub const Encoder = struct {358    allocator: std.mem.Allocator,359    ctx: *const term.Context,360    solver: *sat.Solver,361    cache: []Value,362    true_literal: sat.Literal,363    false_literal: sat.Literal,364    function_congruence_encoded: bool = false,365366    /// Returns an encoder over `ctx` and `solver` that allocates with `allocator`. A caller builds367    /// the encoder once the formula's terms exist and before asserting any of them. The call adds368    /// one variable to the solver and a unit clause that fixes it true, and the encoder uses it as369    /// the constant true. The encoder sizes its table of encoded terms to the terms of `ctx` at370    /// this call, so a term built later fails with `TermOutOfRange`.371    pub fn init(allocator: std.mem.Allocator, ctx: *const term.Context, solver: *sat.Solver) Error!Encoder {372        const true_variable = try solver.addVariable();373        const true_literal = sat.Literal.positive(true_variable);374        try solver.addClause(&.{true_literal});375        const cache = try allocator.alloc(Value, ctx.nodes.items.len);376        @memset(cache, .none);377        return .{378            .allocator = allocator,379            .ctx = ctx,380            .solver = solver,381            .cache = cache,382            .true_literal = true_literal,383            .false_literal = true_literal.negated(),384        };385    }386387    /// Frees the bits and array cells of every encoded term and the table that held them. The owner388    /// calls it once when done with the encoder. The clauses already added to the solver stay389    /// there.390    pub fn deinit(self: *Encoder) void {391        for (self.cache) |value| {392            switch (value) {393                .bits => |bits| self.allocator.free(bits),394                .array => |array| self.freeArray(array),395                else => {},396            }397        }398        self.allocator.free(self.cache);399        self.* = undefined;400    }401402    /// Encodes the Boolean term `assertion` and adds a unit clause that makes it true in every403    /// later solve. A caller states with it each part of the formula that has to hold, as a caller404    /// does for every assertion of a `Script`. The first call of `assertTerm`, `assumeTerm` or405    /// `solve` also adds the equal-arguments clauses for every function application of the406    /// `Context`. The call returns `ExpectedBool` for a term of another sort.407    pub fn assertTerm(self: *Encoder, assertion: term.Term) Error!void {408        const literal = try self.encodeBool(assertion);409        try self.solver.addClause(&.{literal});410        try self.encodeFunctionCongruence();411    }412413    /// Encodes the Boolean term `assumption`, adds its literal to the solver's active assumptions414    /// and returns that literal. A caller calls it to test a condition without asserting it for415    /// good, and matches the returned literal against the solver's unsat core, a set of tested416    /// conditions that the formula refutes together. The assumption holds in every solve until the417    /// caller pops its assumption frame or clears the assumptions. The clauses that encode the term418    /// stay in the solver after the assumption is removed. The first call of `assertTerm`,419    /// `assumeTerm` or `solve` also adds the equal-arguments clauses for every function420    /// application. The call returns `ExpectedBool` for a term of another sort.421    pub fn assumeTerm(self: *Encoder, assumption: term.Term) Error!sat.Literal {422        const literal = try self.encodeBool(assumption);423        try self.solver.assume(literal);424        try self.encodeFunctionCongruence();425        return literal;426    }427428    /// Encodes every named constant of the `Context`, adds the equal-arguments clauses if no429    /// earlier call did, and solves under the active assumptions. A caller decides the formula with430    /// it after asserting and assuming its terms. The call returns the solver's answer:431    /// satisfiable, unsatisfiable or unknown. Because the encoder encodes every named constant, a432    /// single integer constant in the `Context` makes the call fail with `UnsupportedTerm`, even if433    /// no assertion uses it.434    pub fn solve(self: *Encoder) Error!sat.Status {435        try self.encodeSymbols();436        try self.encodeFunctionCongruence();437        return try self.solver.solveWithActiveAssumptions();438    }439440    /// Encodes the Boolean term `id` and returns the literal that is true exactly when the term is.441    /// A caller that builds its own clauses around a term, or checks one term's value, gets the442    /// term's literal with it. The call returns `ExpectedBool` for a term of another sort.443    pub fn encodeBool(self: *Encoder, id: term.Term) Error!sat.Literal {444        switch (try self.encode(id)) {445            .bool => |literal| return literal,446            else => return EncodeError.ExpectedBool,447        }448    }449450    /// Encodes the bit-vector term `id` and returns one literal per bit, least significant bit451    /// first. A caller that builds its own clauses over a bit-vector's bits gets them with it. The452    /// encoder owns the returned slice, which stays valid until `deinit`. The call returns453    /// `ExpectedBitVec` for a term of another sort.454    pub fn encodeBits(self: *Encoder, id: term.Term) Error![]const sat.Literal {455        switch (try self.encode(id)) {456            .bits => |bits| return bits,457            else => return EncodeError.ExpectedBitVec,458        }459    }460461    fn encodeArray(self: *Encoder, id: term.Term) Error!ArrayValue {462        switch (try self.encode(id)) {463            .array => |array| return array,464            else => return EncodeError.ExpectedArray,465        }466    }467468    /// Encodes every named constant of the `Context`, so that `model` finds a value for each one. A469    /// caller that calls `sat.Solver.solve` directly, as the encoder's tests do, calls it first so470    /// that every constant has a value to read. `solve` calls it.471    pub fn encodeSymbols(self: *Encoder) Error!void {472        for (self.ctx.nodes.items, 0..) |node, index| {473            switch (node) {474                .symbol => _ = try self.encode(@intCast(index)),475                else => {},476            }477        }478    }479480    /// Returns a `Model` that allocates with `allocator`, with the value of every named constant481    /// and one entry per encoded function application. A caller reads the satisfying values with it482    /// after a satisfiable answer. The caller owns the model and frees it with `Model.deinit`. The483    /// call returns `ModelUnavailable` when a constant has no value, as before a satisfiable answer484    /// or before `encodeSymbols`, `ModelValueTooWide` for a value above 128 bits, and485    /// `UnsupportedTerm` for an integer constant.486    pub fn model(self: *const Encoder, allocator: std.mem.Allocator) Error!Model {487        var result = Model.init(allocator);488        errdefer result.deinit();489        for (self.ctx.nodes.items, 0..) |node, index| {490            switch (node) {491                .symbol => |symbol| try result.append(symbol.name, try self.modelValueFor(allocator, @intCast(index), symbol.sort)),492                .apply => |application| {493                    if (self.cache[index] != .none) try self.appendFunctionApplicationModel(allocator, &result, @intCast(index), application);494                },495                else => {},496            }497        }498        return result;499    }500501    fn encode(self: *Encoder, id: term.Term) Error!Value {502        if (id >= self.cache.len) return EncodeError.TermOutOfRange;503        if (self.cache[id] != .none) return self.cache[id];504        const node = self.ctx.nodes.items[id];505        const value = switch (node) {506            .symbol => |symbol| try self.encodeSymbol(symbol.sort),507            .apply => |item| try self.encodeApply(item),508            .bool => |value| Value{ .bool = if (value) self.true_literal else self.false_literal },509            .int => return EncodeError.UnsupportedTerm,510            .bitvec => |value| Value{ .bits = try self.constantBits(value.value, value.width) },511            .not => |operand| Value{ .bool = (try self.encodeBool(operand)).negated() },512            .and_ => |operands| Value{ .bool = try self.encodeBoolNary(operands, true) },513            .or_ => |operands| Value{ .bool = try self.encodeBoolNary(operands, false) },514            .implies => |pair| Value{ .bool = try self.orGate((try self.encodeBool(pair.lhs)).negated(), try self.encodeBool(pair.rhs)) },515            .eq => |pair| try self.encodeEq(pair.lhs, pair.rhs),516            .add => return EncodeError.UnsupportedTerm,517            .mul => return EncodeError.UnsupportedTerm,518            .le, .lt, .ge, .gt => return EncodeError.UnsupportedTerm,519            .distinct => return EncodeError.UnsupportedTerm,520            .bvadd => |pair| Value{ .bits = try self.encodeAdd(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },521            .bvsub => |pair| Value{ .bits = try self.encodeSub(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },522            .bvmul => |pair| Value{ .bits = try self.encodeMul(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },523            .bvule => |pair| Value{ .bool = try self.encodeUle(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },524            .bvult => |pair| Value{ .bool = try self.encodeUlt(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },525            .bvsle => |pair| Value{ .bool = try self.encodeSle(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },526            .bvslt => |pair| Value{ .bool = try self.encodeSlt(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },527            .bvuaddo => |pair| Value{ .bool = try self.encodeUaddOverflow(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },528            .bvsaddo => |pair| Value{ .bool = try self.encodeSaddOverflow(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },529            .bvssubo => |pair| Value{ .bool = try self.encodeSsubOverflow(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },530            .bvumulo => |pair| Value{ .bool = try self.encodeUmulOverflow(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },531            .bvsmulo => |pair| Value{ .bool = try self.encodeSmulOverflow(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },532            .bvnot => |operand| Value{ .bits = try self.encodeBitwiseNot(try self.encodeBits(operand)) },533            .bvand => |pair| Value{ .bits = try self.encodeBitwiseBinary(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs), .and_) },534            .bvor => |pair| Value{ .bits = try self.encodeBitwiseBinary(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs), .or_) },535            .bvxor => |pair| Value{ .bits = try self.encodeBitwiseBinary(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs), .xor) },536            .bvshl => |pair| Value{ .bits = try self.encodeShift(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs), .left) },537            .bvlshr => |pair| Value{ .bits = try self.encodeShift(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs), .right) },538            .bvashr => |pair| Value{ .bits = try self.encodeArithmeticShiftRight(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },539            .bvrotl => |item| Value{ .bits = try self.encodeRotate(try self.encodeBits(item.operand), item.amount, .left) },540            .bvrotr => |item| Value{ .bits = try self.encodeRotate(try self.encodeBits(item.operand), item.amount, .right) },541            .bvudiv => |pair| blk: {542                const result = try self.encodeUnsignedDivRem(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs));543                self.allocator.free(result.remainder);544                break :blk Value{ .bits = result.quotient };545            },546            .bvurem => |pair| blk: {547                const result = try self.encodeUnsignedDivRem(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs));548                self.allocator.free(result.quotient);549                break :blk Value{ .bits = result.remainder };550            },551            .bvsdiv => |pair| Value{ .bits = try self.encodeSignedDiv(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },552            .bvsrem => |pair| Value{ .bits = try self.encodeSignedRem(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },553            .bvsmod => |pair| Value{ .bits = try self.encodeSignedMod(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },554            .array_select => |item| Value{ .bits = try self.encodeArraySelect(try self.encodeArray(item.array), try self.encodeBits(item.index)) },555            .array_store => |item| Value{ .array = try self.encodeArrayStore(try self.encodeArray(item.array), try self.encodeBits(item.index), try self.encodeBits(item.value)) },556            .bvconcat => |pair| Value{ .bits = try self.encodeConcat(try self.encodeBits(pair.lhs), try self.encodeBits(pair.rhs)) },557            .bvextract => |item| Value{ .bits = try self.encodeExtract(try self.encodeBits(item.operand), item.high, item.low) },558            .bvzeroext => |item| Value{ .bits = try self.encodeExtend(try self.encodeBits(item.operand), item.extra, .zero) },559            .bvsignext => |item| Value{ .bits = try self.encodeExtend(try self.encodeBits(item.operand), item.extra, .sign) },560        };561        self.cache[id] = value;562        return value;563    }564565    fn encodeSymbol(self: *Encoder, sort: term.Sort) Error!Value {566        return switch (sort) {567            .bool => .{ .bool = try self.freshLiteral() },568            .bitvec => |width| .{ .bits = try self.freshBits(width) },569            .array => |array| .{ .array = try self.freshArray(array.index_width, array.element_width) },570            .int => EncodeError.UnsupportedTerm,571        };572    }573574    fn encodeApply(self: *Encoder, item: term.ApplyExpr) Error!Value {575        if (item.function >= self.ctx.functions.items.len) return EncodeError.FunctionOutOfRange;576        const decl = self.ctx.functions.items[item.function];577        if (decl.params.len != item.args.len) return EncodeError.SortMismatch;578        for (item.args) |argument| {579            _ = try self.encode(argument);580        }581        return try self.encodeSymbol(decl.result);582    }583584    fn modelValueFor(self: *const Encoder, allocator: std.mem.Allocator, id: term.Term, sort: term.Sort) Error!ModelValue {585        if (id >= self.cache.len) return EncodeError.TermOutOfRange;586        return switch (sort) {587            .bool => switch (self.cache[id]) {588                .bool => |literal| switch (self.solver.literalValue(literal)) {589                    .true => .{ .bool = true },590                    .false => .{ .bool = false },591                    .unset => EncodeError.ModelUnavailable,592                },593                else => EncodeError.ModelUnavailable,594            },595            .bitvec => |width| switch (self.cache[id]) {596                .bits => |bits| .{ .bitvec = .{ .value = try modelValue(self.solver, bits), .width = width } },597                else => EncodeError.ModelUnavailable,598            },599            .array => switch (self.cache[id]) {600                .array => |array| try self.modelArrayValue(allocator, array),601                else => EncodeError.ModelUnavailable,602            },603            .int => EncodeError.UnsupportedTerm,604        };605    }606607    fn appendFunctionApplicationModel(608        self: *const Encoder,609        allocator: std.mem.Allocator,610        model_result: *Model,611        id: term.Term,612        application: term.ApplyExpr,613    ) Error!void {614        if (application.function >= self.ctx.functions.items.len) return EncodeError.FunctionOutOfRange;615        const decl = self.ctx.functions.items[application.function];616        const arguments = try self.modelArguments(allocator, application.args);617        var arguments_handled = false;618        errdefer {619            if (!arguments_handled) {620                for (arguments) |*argument| {621                    argument.deinit(allocator);622                }623                allocator.free(arguments);624            }625        }626        const value = try self.modelValueFor(allocator, id, decl.result);627        var value_handled = false;628        errdefer {629            if (!value_handled) {630                var owned_value = value;631                owned_value.deinit(allocator);632            }633        }634        arguments_handled = true;635        value_handled = true;636        try model_result.appendFunctionApplication(decl.name, arguments, value);637    }638639    fn modelArguments(self: *const Encoder, allocator: std.mem.Allocator, arguments: []const term.Term) Error![]ModelValue {640        const values = try allocator.alloc(ModelValue, arguments.len);641        var initialized: usize = 0;642        errdefer {643            for (values[0..initialized]) |*value| {644                value.deinit(allocator);645            }646            allocator.free(values);647        }648        for (arguments, 0..) |argument, index| {649            values[index] = try self.modelValueFor(allocator, argument, try self.ctx.sortOf(argument));650            initialized += 1;651        }652        return values;653    }654655    fn encodeEq(self: *Encoder, lhs: term.Term, rhs: term.Term) Error!Value {656        const lhs_value = try self.encode(lhs);657        const rhs_value = try self.encode(rhs);658        return .{ .bool = try self.encodeValueEqual(lhs_value, rhs_value) };659    }660661    fn encodeValueEqual(self: *Encoder, lhs_value: Value, rhs_value: Value) Error!sat.Literal {662        return switch (lhs_value) {663            .bool => |lhs_literal| switch (rhs_value) {664                .bool => |rhs_literal| try self.xnorGate(lhs_literal, rhs_literal),665                else => EncodeError.SortMismatch,666            },667            .bits => |lhs_bits| switch (rhs_value) {668                .bits => |rhs_bits| try self.bitsEqual(lhs_bits, rhs_bits),669                else => EncodeError.SortMismatch,670            },671            .array => |lhs_array| switch (rhs_value) {672                .array => |rhs_array| try self.arraysEqual(lhs_array, rhs_array),673                else => EncodeError.SortMismatch,674            },675            .none => EncodeError.UnsupportedTerm,676        };677    }678679    fn encodeFunctionCongruence(self: *Encoder) Error!void {680        if (self.function_congruence_encoded) return;681        for (self.ctx.nodes.items, 0..) |node, index| {682            switch (node) {683                .apply => |application| {684                    const id: term.Term = @intCast(index);685                    _ = try self.encode(id);686                    var previous_index: usize = 0;687                    while (previous_index < index) : (previous_index += 1) {688                        switch (self.ctx.nodes.items[previous_index]) {689                            .apply => |previous| {690                                if (previous.function != application.function) continue;691                                try self.encodeApplicationCongruence(previous, @intCast(previous_index), application, id);692                            },693                            else => {},694                        }695                    }696                },697                else => {},698            }699        }700        self.function_congruence_encoded = true;701    }702703    fn encodeApplicationCongruence(704        self: *Encoder,705        lhs_application: term.ApplyExpr,706        lhs: term.Term,707        rhs_application: term.ApplyExpr,708        rhs: term.Term,709    ) Error!void {710        if (lhs_application.args.len != rhs_application.args.len) return EncodeError.SortMismatch;711        const clause = try self.allocator.alloc(sat.Literal, lhs_application.args.len + 1);712        defer self.allocator.free(clause);713        for (lhs_application.args, rhs_application.args, 0..) |lhs_arg, rhs_arg, index| {714            clause[index] = switch (try self.encodeEq(lhs_arg, rhs_arg)) {715                .bool => |literal| literal.negated(),716                else => return EncodeError.ExpectedBool,717            };718        }719        clause[lhs_application.args.len] = try self.encodeValueEqual(try self.encode(lhs), try self.encode(rhs));720        try self.solver.addClause(clause);721    }722723    fn encodeBoolNary(self: *Encoder, operands: []const term.Term, comptime is_and: bool) Error!sat.Literal {724        if (operands.len == 0) return if (is_and) self.true_literal else self.false_literal;725        var result = try self.encodeBool(operands[0]);726        for (operands[1..]) |operand| {727            const rhs = try self.encodeBool(operand);728            result = if (is_and) try self.andGate(result, rhs) else try self.orGate(result, rhs);729        }730        return result;731    }732733    fn constantBits(self: *Encoder, value: u128, width: u32) Error![]sat.Literal {734        const bits = try self.allocator.alloc(sat.Literal, width);735        for (bits, 0..) |*bit, index| {736            bit.* = if (((value >> @intCast(index)) & 1) == 1) self.true_literal else self.false_literal;737        }738        return bits;739    }740741    fn freshBits(self: *Encoder, width: u32) Error![]sat.Literal {742        const bits = try self.allocator.alloc(sat.Literal, width);743        errdefer self.allocator.free(bits);744        for (bits) |*bit| {745            bit.* = try self.freshLiteral();746        }747        return bits;748    }749750    fn freshArray(self: *Encoder, index_width: u32, element_width: u32) Error!ArrayValue {751        const cell_count = try arrayCellCount(index_width);752        const cells = try self.allocator.alloc([]sat.Literal, cell_count);753        var initialized: usize = 0;754        errdefer {755            for (cells[0..initialized]) |cell| self.allocator.free(cell);756            self.allocator.free(cells);757        }758        for (cells) |*cell| {759            cell.* = try self.freshBits(element_width);760            initialized += 1;761        }762        return .{ .index_width = index_width, .element_width = element_width, .cells = cells };763    }764765    fn freeArray(self: *Encoder, array: ArrayValue) void {766        for (array.cells) |cell| self.allocator.free(cell);767        self.allocator.free(array.cells);768    }769770    fn modelArrayValue(self: *const Encoder, allocator: std.mem.Allocator, array: ArrayValue) Error!ModelValue {771        const cells = try allocator.alloc(u128, array.cells.len);772        errdefer allocator.free(cells);773        for (cells, array.cells) |*target, bits| {774            target.* = try modelValue(self.solver, bits);775        }776        return .{ .array = .{ .index_width = array.index_width, .element_width = array.element_width, .cells = cells } };777    }778779    fn freshLiteral(self: *Encoder) Error!sat.Literal {780        return sat.Literal.positive(try self.solver.addVariable());781    }782783    fn encodeAdd(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error![]sat.Literal {784        if (lhs.len != rhs.len) return EncodeError.SortMismatch;785        const out = try self.allocator.alloc(sat.Literal, lhs.len);786        errdefer self.allocator.free(out);787        var carry = self.false_literal;788        for (lhs, rhs, 0..) |a, b, index| {789            const sum_ab = try self.xorGate(a, b);790            out[index] = try self.xorGate(sum_ab, carry);791            const carry_ab = try self.andGate(a, b);792            const carry_ac = try self.andGate(a, carry);793            const carry_bc = try self.andGate(b, carry);794            carry = try self.orGate(try self.orGate(carry_ab, carry_ac), carry_bc);795        }796        return out;797    }798799    fn encodeSub(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error![]sat.Literal {800        if (lhs.len != rhs.len) return EncodeError.SortMismatch;801        const out = try self.allocator.alloc(sat.Literal, lhs.len);802        errdefer self.allocator.free(out);803        var carry = self.true_literal;804        for (lhs, rhs, 0..) |a, b, index| {805            const not_b = b.negated();806            const sum_ab = try self.xorGate(a, not_b);807            out[index] = try self.xorGate(sum_ab, carry);808            const carry_ab = try self.andGate(a, not_b);809            const carry_ac = try self.andGate(a, carry);810            const carry_bc = try self.andGate(not_b, carry);811            carry = try self.orGate(try self.orGate(carry_ab, carry_ac), carry_bc);812        }813        return out;814    }815816    fn encodeMul(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error![]sat.Literal {817        if (lhs.len != rhs.len) return EncodeError.SortMismatch;818        var result = try self.constantBits(0, @intCast(lhs.len));819        errdefer self.allocator.free(result);820        for (rhs, 0..) |rhs_bit, shift| {821            const partial = try self.allocator.alloc(sat.Literal, lhs.len);822            defer self.allocator.free(partial);823            for (partial, 0..) |*bit, index| {824                bit.* = if (index < shift) self.false_literal else try self.andGate(lhs[index - shift], rhs_bit);825            }826            const next = try self.encodeAdd(result, partial);827            self.allocator.free(result);828            result = next;829        }830        return result;831    }832833    fn encodeUlt(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {834        if (lhs.len != rhs.len) return EncodeError.SortMismatch;835        var equal_prefix = self.true_literal;836        var less = self.false_literal;837        var index = lhs.len;838        while (index > 0) {839            index -= 1;840            const bit_less = try self.andGate(lhs[index].negated(), rhs[index]);841            less = try self.orGate(less, try self.andGate(equal_prefix, bit_less));842            equal_prefix = try self.andGate(equal_prefix, try self.xnorGate(lhs[index], rhs[index]));843        }844        return less;845    }846847    fn encodeUle(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {848        return try self.orGate(try self.encodeUlt(lhs, rhs), try self.bitsEqual(lhs, rhs));849    }850851    fn encodeSlt(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {852        if (lhs.len != rhs.len) return EncodeError.SortMismatch;853        if (lhs.len == 0) return EncodeError.InvalidBitVectorRange;854        const lhs_sign = lhs[lhs.len - 1];855        const rhs_sign = rhs[rhs.len - 1];856        const signs_differ = try self.xorGate(lhs_sign, rhs_sign);857        const lhs_negative_rhs_positive = try self.andGate(lhs_sign, rhs_sign.negated());858        const same_sign_less = try self.andGate(signs_differ.negated(), try self.encodeUlt(lhs, rhs));859        return try self.orGate(lhs_negative_rhs_positive, same_sign_less);860    }861862    fn encodeSle(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {863        return try self.orGate(try self.encodeSlt(lhs, rhs), try self.bitsEqual(lhs, rhs));864    }865866    fn bitsEqual(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {867        if (lhs.len != rhs.len) return EncodeError.SortMismatch;868        var result = self.true_literal;869        for (lhs, rhs) |a, b| {870            result = try self.andGate(result, try self.xnorGate(a, b));871        }872        return result;873    }874875    fn arraysEqual(self: *Encoder, lhs: ArrayValue, rhs: ArrayValue) Error!sat.Literal {876        if (lhs.index_width != rhs.index_width or lhs.element_width != rhs.element_width or lhs.cells.len != rhs.cells.len) return EncodeError.SortMismatch;877        var result = self.true_literal;878        for (lhs.cells, rhs.cells) |lhs_cell, rhs_cell| {879            result = try self.andGate(result, try self.bitsEqual(lhs_cell, rhs_cell));880        }881        return result;882    }883884    fn encodeUaddOverflow(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {885        if (lhs.len != rhs.len) return EncodeError.SortMismatch;886        var carry = self.false_literal;887        for (lhs, rhs) |a, b| {888            const carry_ab = try self.andGate(a, b);889            const carry_ac = try self.andGate(a, carry);890            const carry_bc = try self.andGate(b, carry);891            carry = try self.orGate(try self.orGate(carry_ab, carry_ac), carry_bc);892        }893        return carry;894    }895896    fn encodeSaddOverflow(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {897        if (lhs.len != rhs.len) return EncodeError.SortMismatch;898        if (lhs.len == 0) return EncodeError.InvalidBitVectorRange;899        const sum = try self.encodeAdd(lhs, rhs);900        defer self.allocator.free(sum);901        const lhs_sign = lhs[lhs.len - 1];902        const rhs_sign = rhs[rhs.len - 1];903        const sum_sign = sum[sum.len - 1];904        const same_input_sign = (try self.xorGate(lhs_sign, rhs_sign)).negated();905        const result_sign_changed = try self.xorGate(lhs_sign, sum_sign);906        return try self.andGate(same_input_sign, result_sign_changed);907    }908909    fn encodeSsubOverflow(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {910        if (lhs.len != rhs.len) return EncodeError.SortMismatch;911        if (lhs.len == 0) return EncodeError.InvalidBitVectorRange;912        const negated_rhs = try self.encodeNeg(rhs);913        defer self.allocator.free(negated_rhs);914        const difference = try self.encodeAdd(lhs, negated_rhs);915        defer self.allocator.free(difference);916        const lhs_sign = lhs[lhs.len - 1];917        const rhs_sign = rhs[rhs.len - 1];918        const difference_sign = difference[difference.len - 1];919        const input_signs_differ = try self.xorGate(lhs_sign, rhs_sign);920        const result_sign_changed = try self.xorGate(lhs_sign, difference_sign);921        return try self.andGate(input_signs_differ, result_sign_changed);922    }923924    fn encodeUmulOverflow(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {925        if (lhs.len != rhs.len) return EncodeError.SortMismatch;926        const double_width = lhs.len * 2;927        const lhs_extended = try self.allocator.alloc(sat.Literal, double_width);928        defer self.allocator.free(lhs_extended);929        const rhs_extended = try self.allocator.alloc(sat.Literal, double_width);930        defer self.allocator.free(rhs_extended);931        for (lhs, 0..) |bit, index| {932            lhs_extended[index] = bit;933        }934        for (rhs, 0..) |bit, index| {935            rhs_extended[index] = bit;936        }937        for (lhs.len..double_width) |index| {938            lhs_extended[index] = self.false_literal;939            rhs_extended[index] = self.false_literal;940        }941        const product = try self.encodeMul(lhs_extended, rhs_extended);942        defer self.allocator.free(product);943        return try self.orLiterals(product[lhs.len..]);944    }945946    fn encodeSmulOverflow(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error!sat.Literal {947        if (lhs.len != rhs.len) return EncodeError.SortMismatch;948        if (lhs.len == 0) return EncodeError.InvalidBitVectorRange;949        const double_width = lhs.len * 2;950        const lhs_extended = try self.allocator.alloc(sat.Literal, double_width);951        defer self.allocator.free(lhs_extended);952        const rhs_extended = try self.allocator.alloc(sat.Literal, double_width);953        defer self.allocator.free(rhs_extended);954        @memcpy(lhs_extended[0..lhs.len], lhs);955        @memcpy(rhs_extended[0..rhs.len], rhs);956        for (lhs_extended[lhs.len..]) |*bit| {957            bit.* = lhs[lhs.len - 1];958        }959        for (rhs_extended[rhs.len..]) |*bit| {960            bit.* = rhs[rhs.len - 1];961        }962        const product = try self.encodeMul(lhs_extended, rhs_extended);963        defer self.allocator.free(product);964        const result_sign = product[lhs.len - 1];965        var representable = self.true_literal;966        for (product[lhs.len..]) |upper_bit| {967            representable = try self.andGate(representable, try self.xnorGate(upper_bit, result_sign));968        }969        return representable.negated();970    }971972    fn encodeNeg(self: *Encoder, bits: []const sat.Literal) Error![]sat.Literal {973        if (bits.len == 0) return EncodeError.InvalidBitVectorRange;974        const inverted = try self.encodeBitwiseNot(bits);975        errdefer self.allocator.free(inverted);976        const one = try self.constantBits(1, @intCast(bits.len));977        defer self.allocator.free(one);978        const result = try self.encodeAdd(inverted, one);979        self.allocator.free(inverted);980        return result;981    }982983    fn encodeBitwiseNot(self: *Encoder, bits: []const sat.Literal) Error![]sat.Literal {984        const out = try self.allocator.alloc(sat.Literal, bits.len);985        for (out, bits) |*target, bit| {986            target.* = bit.negated();987        }988        return out;989    }990991    fn encodeBitwiseBinary(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal, kind: BitwiseKind) Error![]sat.Literal {992        if (lhs.len != rhs.len) return EncodeError.SortMismatch;993        const out = try self.allocator.alloc(sat.Literal, lhs.len);994        errdefer self.allocator.free(out);995        for (out, lhs, rhs) |*target, a, b| {996            target.* = switch (kind) {997                .and_ => try self.andGate(a, b),998                .or_ => try self.orGate(a, b),999                .xor => try self.xorGate(a, b),1000            };1001        }1002        return out;1003    }10041005    fn encodeShift(self: *Encoder, value: []const sat.Literal, amount: []const sat.Literal, kind: ShiftKind) Error![]sat.Literal {1006        if (value.len != amount.len) return EncodeError.SortMismatch;1007        const selectors = try self.allocator.alloc(sat.Literal, value.len);1008        defer self.allocator.free(selectors);1009        for (selectors, 0..) |*selector, shift| {1010            selector.* = try self.bitsEqualConstant(amount, shift);1011        }1012        const out = try self.allocator.alloc(sat.Literal, value.len);1013        errdefer self.allocator.free(out);1014        for (out, 0..) |*target, output_index| {1015            var result = self.false_literal;1016            for (selectors, 0..) |selector, shift| {1017                const source = switch (kind) {1018                    .left => if (output_index >= shift) value[output_index - shift] else self.false_literal,1019                    .right => if (output_index + shift < value.len) value[output_index + shift] else self.false_literal,1020                };1021                if (source.raw == self.false_literal.raw) continue;1022                result = try self.orGate(result, try self.andGate(selector, source));1023            }1024            target.* = result;1025        }1026        return out;1027    }10281029    fn encodeArithmeticShiftRight(self: *Encoder, value: []const sat.Literal, amount: []const sat.Literal) Error![]sat.Literal {1030        if (value.len != amount.len) return EncodeError.SortMismatch;1031        if (value.len == 0) return EncodeError.InvalidBitVectorRange;1032        const logical = try self.encodeShift(value, amount, .right);1033        errdefer self.allocator.free(logical);1034        const inverted = try self.encodeBitwiseNot(value);1035        defer self.allocator.free(inverted);1036        const shifted_inverted = try self.encodeShift(inverted, amount, .right);1037        defer self.allocator.free(shifted_inverted);1038        const negative = try self.encodeBitwiseNot(shifted_inverted);1039        defer self.allocator.free(negative);1040        const sign = value[value.len - 1];1041        const out = try self.allocator.alloc(sat.Literal, value.len);1042        errdefer self.allocator.free(out);1043        for (out, logical, negative) |*target, positive_bit, negative_bit| {1044            target.* = try self.muxGate(sign, negative_bit, positive_bit);1045        }1046        self.allocator.free(logical);1047        return out;1048    }10491050    fn encodeRotate(self: *Encoder, bits: []const sat.Literal, amount: u32, kind: RotateKind) Error![]sat.Literal {1051        if (bits.len == 0) return EncodeError.InvalidBitVectorRange;1052        const shift = @as(usize, @intCast(amount)) % bits.len;1053        const out = try self.allocator.alloc(sat.Literal, bits.len);1054        for (out, 0..) |*target, index| {1055            const source_index = switch (kind) {1056                .left => if (index >= shift) index - shift else bits.len - (shift - index),1057                .right => if (index >= bits.len - shift) index - (bits.len - shift) else index + shift,1058            };1059            target.* = bits[source_index];1060        }1061        return out;1062    }10631064    fn encodeUnsignedDivRem(self: *Encoder, dividend: []const sat.Literal, divisor: []const sat.Literal) Error!DivRemResult {1065        if (dividend.len != divisor.len) return EncodeError.SortMismatch;1066        if (dividend.len == 0) return EncodeError.InvalidBitVectorRange;1067        const width = dividend.len;1068        const extended_width = std.math.add(usize, width, 1) catch return EncodeError.InvalidBitVectorRange;1069        var remainder = try self.allocator.alloc(sat.Literal, extended_width);1070        errdefer self.allocator.free(remainder);1071        @memset(remainder, self.false_literal);1072        const divisor_extended = try self.allocator.alloc(sat.Literal, extended_width);1073        defer self.allocator.free(divisor_extended);1074        @memcpy(divisor_extended[0..width], divisor);1075        divisor_extended[width] = self.false_literal;1076        const quotient = try self.allocator.alloc(sat.Literal, width);1077        errdefer self.allocator.free(quotient);1078        var index = width;1079        while (index > 0) {1080            index -= 1;1081            const shifted = try self.allocator.alloc(sat.Literal, extended_width);1082            errdefer self.allocator.free(shifted);1083            shifted[0] = dividend[index];1084            @memcpy(shifted[1..], remainder[0..width]);1085            const can_subtract = try self.encodeUle(divisor_extended, shifted);1086            const difference = try self.encodeSub(shifted, divisor_extended);1087            errdefer self.allocator.free(difference);1088            const next_remainder = try self.allocator.alloc(sat.Literal, extended_width);1089            errdefer self.allocator.free(next_remainder);1090            for (next_remainder, shifted, difference) |*target, shifted_bit, difference_bit| {1091                target.* = try self.muxGate(can_subtract, difference_bit, shifted_bit);1092            }1093            quotient[index] = can_subtract;1094            self.allocator.free(remainder);1095            self.allocator.free(shifted);1096            self.allocator.free(difference);1097            remainder = next_remainder;1098        }1099        const result_remainder = try self.allocator.alloc(sat.Literal, width);1100        errdefer self.allocator.free(result_remainder);1101        @memcpy(result_remainder, remainder[0..width]);1102        self.allocator.free(remainder);1103        return .{ .quotient = quotient, .remainder = result_remainder };1104    }11051106    fn encodeSignedDiv(self: *Encoder, dividend: []const sat.Literal, divisor: []const sat.Literal) Error![]sat.Literal {1107        if (dividend.len != divisor.len) return EncodeError.SortMismatch;1108        if (dividend.len == 0) return EncodeError.InvalidBitVectorRange;1109        const abs_dividend = try self.encodeAbs(dividend);1110        defer self.allocator.free(abs_dividend);1111        const abs_divisor = try self.encodeAbs(divisor);1112        defer self.allocator.free(abs_divisor);1113        const result = try self.encodeUnsignedDivRem(abs_dividend, abs_divisor);1114        defer self.allocator.free(result.quotient);1115        defer self.allocator.free(result.remainder);1116        const negated_quotient = try self.encodeNeg(result.quotient);1117        defer self.allocator.free(negated_quotient);1118        const negative = try self.xorGate(dividend[dividend.len - 1], divisor[divisor.len - 1]);1119        return try self.muxBits(negative, negated_quotient, result.quotient);1120    }11211122    fn encodeSignedRem(self: *Encoder, dividend: []const sat.Literal, divisor: []const sat.Literal) Error![]sat.Literal {1123        if (dividend.len != divisor.len) return EncodeError.SortMismatch;1124        if (dividend.len == 0) return EncodeError.InvalidBitVectorRange;1125        const abs_dividend = try self.encodeAbs(dividend);1126        defer self.allocator.free(abs_dividend);1127        const abs_divisor = try self.encodeAbs(divisor);1128        defer self.allocator.free(abs_divisor);1129        const result = try self.encodeUnsignedDivRem(abs_dividend, abs_divisor);1130        defer self.allocator.free(result.quotient);1131        defer self.allocator.free(result.remainder);1132        const negated_remainder = try self.encodeNeg(result.remainder);1133        defer self.allocator.free(negated_remainder);1134        return try self.muxBits(dividend[dividend.len - 1], negated_remainder, result.remainder);1135    }11361137    fn encodeSignedMod(self: *Encoder, dividend: []const sat.Literal, divisor: []const sat.Literal) Error![]sat.Literal {1138        if (dividend.len != divisor.len) return EncodeError.SortMismatch;1139        if (dividend.len == 0) return EncodeError.InvalidBitVectorRange;1140        const abs_dividend = try self.encodeAbs(dividend);1141        defer self.allocator.free(abs_dividend);1142        const abs_divisor = try self.encodeAbs(divisor);1143        defer self.allocator.free(abs_divisor);1144        const result = try self.encodeUnsignedDivRem(abs_dividend, abs_divisor);1145        defer self.allocator.free(result.quotient);1146        defer self.allocator.free(result.remainder);1147        const zero = try self.constantBits(0, @intCast(dividend.len));1148        defer self.allocator.free(zero);1149        const remainder_is_zero = try self.bitsEqual(result.remainder, zero);1150        const negated_remainder = try self.encodeNeg(result.remainder);1151        defer self.allocator.free(negated_remainder);1152        const negative_plus_divisor = try self.encodeAdd(negated_remainder, divisor);1153        defer self.allocator.free(negative_plus_divisor);1154        const positive_plus_divisor = try self.encodeAdd(result.remainder, divisor);1155        defer self.allocator.free(positive_plus_divisor);1156        const lhs_positive_branch = try self.muxBits(divisor[divisor.len - 1], positive_plus_divisor, result.remainder);1157        defer self.allocator.free(lhs_positive_branch);1158        const lhs_negative_branch = try self.muxBits(divisor[divisor.len - 1], negated_remainder, negative_plus_divisor);1159        defer self.allocator.free(lhs_negative_branch);1160        const adjusted = try self.muxBits(dividend[dividend.len - 1], lhs_negative_branch, lhs_positive_branch);1161        defer self.allocator.free(adjusted);1162        return try self.muxBits(remainder_is_zero, result.remainder, adjusted);1163    }11641165    fn encodeAbs(self: *Encoder, bits: []const sat.Literal) Error![]sat.Literal {1166        if (bits.len == 0) return EncodeError.InvalidBitVectorRange;1167        const negated = try self.encodeNeg(bits);1168        defer self.allocator.free(negated);1169        return try self.muxBits(bits[bits.len - 1], negated, bits);1170    }11711172    fn bitsEqualConstant(self: *Encoder, bits: []const sat.Literal, value: usize) Error!sat.Literal {1173        var result = self.true_literal;1174        for (bits, 0..) |bit, index| {1175            const bit_is_set = index < @bitSizeOf(usize) and ((value >> @intCast(index)) & 1) == 1;1176            const selected = if (bit_is_set) bit else bit.negated();1177            result = try self.andGate(result, selected);1178        }1179        return result;1180    }11811182    fn encodeArraySelect(self: *Encoder, array: ArrayValue, index: []const sat.Literal) Error![]sat.Literal {1183        const index_width: usize = @intCast(array.index_width);1184        const element_width: usize = @intCast(array.element_width);1185        if (index.len != index_width) return EncodeError.SortMismatch;1186        const cell_count = try arrayCellCount(array.index_width);1187        if (array.cells.len != cell_count) return EncodeError.SortMismatch;1188        const out = try self.allocator.alloc(sat.Literal, element_width);1189        errdefer self.allocator.free(out);1190        @memset(out, self.false_literal);1191        for (array.cells, 0..) |cell, cell_index| {1192            if (cell.len != element_width) return EncodeError.SortMismatch;1193            const selector = try self.bitsEqualConstant(index, cell_index);1194            for (out, cell) |*target, bit| {1195                if (bit.raw == self.false_literal.raw) continue;1196                target.* = try self.orGate(target.*, try self.andGate(selector, bit));1197            }1198        }1199        return out;1200    }12011202    fn encodeArrayStore(self: *Encoder, array: ArrayValue, index: []const sat.Literal, value: []const sat.Literal) Error!ArrayValue {1203        const index_width: usize = @intCast(array.index_width);1204        const element_width: usize = @intCast(array.element_width);1205        if (index.len != index_width or value.len != element_width) return EncodeError.SortMismatch;1206        const cell_count = try arrayCellCount(array.index_width);1207        if (array.cells.len != cell_count) return EncodeError.SortMismatch;1208        const cells = try self.allocator.alloc([]sat.Literal, cell_count);1209        var initialized: usize = 0;1210        errdefer {1211            for (cells[0..initialized]) |cell| self.allocator.free(cell);1212            self.allocator.free(cells);1213        }1214        for (cells, array.cells, 0..) |*target, cell, cell_index| {1215            if (cell.len != element_width) return EncodeError.SortMismatch;1216            const selector = try self.bitsEqualConstant(index, cell_index);1217            target.* = try self.muxBits(selector, value, cell);1218            initialized += 1;1219        }1220        return .{ .index_width = array.index_width, .element_width = array.element_width, .cells = cells };1221    }12221223    fn encodeConcat(self: *Encoder, lhs: []const sat.Literal, rhs: []const sat.Literal) Error![]sat.Literal {1224        const out = try self.allocator.alloc(sat.Literal, lhs.len + rhs.len);1225        @memcpy(out[0..rhs.len], rhs);1226        @memcpy(out[rhs.len..], lhs);1227        return out;1228    }12291230    fn encodeExtract(self: *Encoder, bits: []const sat.Literal, high: u32, low: u32) Error![]sat.Literal {1231        if (low > high or high >= bits.len) return EncodeError.InvalidBitVectorRange;1232        const width = high - low + 1;1233        const out = try self.allocator.alloc(sat.Literal, width);1234        const base: usize = @intCast(low);1235        for (out, 0..) |*target, index| {1236            target.* = bits[base + index];1237        }1238        return out;1239    }12401241    fn encodeExtend(self: *Encoder, bits: []const sat.Literal, extra: u32, kind: ExtendKind) Error![]sat.Literal {1242        if (bits.len == 0) return EncodeError.InvalidBitVectorRange;1243        const extra_len: usize = @intCast(extra);1244        const width = std.math.add(usize, bits.len, extra_len) catch return EncodeError.InvalidBitVectorRange;1245        const out = try self.allocator.alloc(sat.Literal, width);1246        @memcpy(out[0..bits.len], bits);1247        const extension = switch (kind) {1248            .zero => self.false_literal,1249            .sign => bits[bits.len - 1],1250        };1251        for (out[bits.len..]) |*target| {1252            target.* = extension;1253        }1254        return out;1255    }12561257    fn orLiterals(self: *Encoder, literals: []const sat.Literal) Error!sat.Literal {1258        if (literals.len == 0) return self.false_literal;1259        var result = literals[0];1260        for (literals[1..]) |literal| {1261            result = try self.orGate(result, literal);1262        }1263        return result;1264    }12651266    fn andGate(self: *Encoder, a: sat.Literal, b: sat.Literal) Error!sat.Literal {1267        const out = try self.freshLiteral();1268        try self.solver.addClause(&.{ a.negated(), b.negated(), out });1269        try self.solver.addClause(&.{ a, out.negated() });1270        try self.solver.addClause(&.{ b, out.negated() });1271        return out;1272    }12731274    fn orGate(self: *Encoder, a: sat.Literal, b: sat.Literal) Error!sat.Literal {1275        const out = try self.freshLiteral();1276        try self.solver.addClause(&.{ a, b, out.negated() });1277        try self.solver.addClause(&.{ a.negated(), out });1278        try self.solver.addClause(&.{ b.negated(), out });1279        return out;1280    }12811282    fn xorGate(self: *Encoder, a: sat.Literal, b: sat.Literal) Error!sat.Literal {1283        const out = try self.freshLiteral();1284        try self.solver.addClause(&.{ a, b, out.negated() });1285        try self.solver.addClause(&.{ a.negated(), b.negated(), out.negated() });1286        try self.solver.addClause(&.{ a, b.negated(), out });1287        try self.solver.addClause(&.{ a.negated(), b, out });1288        return out;1289    }12901291    fn xnorGate(self: *Encoder, a: sat.Literal, b: sat.Literal) Error!sat.Literal {1292        return (try self.xorGate(a, b)).negated();1293    }12941295    fn muxGate(self: *Encoder, selector: sat.Literal, when_true: sat.Literal, when_false: sat.Literal) Error!sat.Literal {1296        return try self.orGate(try self.andGate(selector, when_true), try self.andGate(selector.negated(), when_false));1297    }12981299    fn muxBits(self: *Encoder, selector: sat.Literal, when_true: []const sat.Literal, when_false: []const sat.Literal) Error![]sat.Literal {1300        if (when_true.len != when_false.len) return EncodeError.SortMismatch;1301        const out = try self.allocator.alloc(sat.Literal, when_true.len);1302        errdefer self.allocator.free(out);1303        for (out, when_true, when_false) |*target, true_bit, false_bit| {1304            target.* = try self.muxGate(selector, true_bit, false_bit);1305        }1306        return out;1307    }1308};13091310fn modelValue(solver: *const sat.Solver, bits: []const sat.Literal) Error!u128 {1311    if (bits.len > 128) return EncodeError.ModelValueTooWide;1312    var value: u128 = 0;1313    for (bits, 0..) |bit, index| {1314        const bit_value = solver.literalValue(bit);1315        if (bit_value == .true) value |= @as(u128, 1) << @intCast(index);1316    }1317    return value;1318}13191320fn arrayCellCount(index_width: u32) Error!usize {1321    if (index_width > max_native_array_index_width) return EncodeError.ArrayIndexTooWide;1322    return @as(usize, 1) << @intCast(index_width);1323}13241325test "bit-vector encoder proves unsigned self-less-than impossible" {1326    var ctx = term.Context.init(std.testing.allocator);1327    defer ctx.deinit();1328    const x = try ctx.symbol("x", .{ .bitvec = 4 });1329    const assertion = try ctx.bvult(x, x);1330    var solver = sat.Solver.init(std.testing.allocator);1331    defer solver.deinit();1332    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1333    defer encoder.deinit();1334    try encoder.assertTerm(assertion);1335    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1336}13371338test "bit-vector encoder proves signed self-less-than impossible" {1339    var ctx = term.Context.init(std.testing.allocator);1340    defer ctx.deinit();1341    const x = try ctx.symbol("x", .{ .bitvec = 4 });1342    const assertion = try ctx.bvslt(x, x);1343    var solver = sat.Solver.init(std.testing.allocator);1344    defer solver.deinit();1345    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1346    defer encoder.deinit();1347    try encoder.assertTerm(assertion);1348    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1349}13501351test "bit-vector encoder solves with Boolean term assumptions" {1352    var ctx = term.Context.init(std.testing.allocator);1353    defer ctx.deinit();1354    const p = try ctx.symbol("p", .bool);1355    const q = try ctx.symbol("q", .bool);1356    const r = try ctx.symbol("r", .bool);1357    const operands = [_]term.Term{ p, q };1358    const disjunction = try ctx.or_(&operands);1359    const not_p = try ctx.not(p);1360    const not_q = try ctx.not(q);1361    var solver = sat.Solver.init(std.testing.allocator);1362    defer solver.deinit();1363    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1364    defer encoder.deinit();1365    try encoder.assertTerm(disjunction);1366    const not_p_literal = try encoder.assumeTerm(not_p);1367    _ = try encoder.assumeTerm(r);1368    const not_q_literal = try encoder.assumeTerm(not_q);1369    try std.testing.expectEqual(sat.Status.unsat, try encoder.solve());1370    try std.testing.expectEqualSlices(sat.Literal, &.{ not_p_literal, not_q_literal }, solver.lastUnsatCore());1371    var artifact = (try solver.lastProofArtifact(std.testing.allocator)).?;1372    defer artifact.deinit();1373    try std.testing.expectEqualSlices(sat.Literal, &.{ not_p_literal, not_q_literal }, artifact.assumptions.items);1374    try std.testing.expect(try artifact.valid());1375}13761377test "bit-vector encoder solves signed comparison model" {1378    var ctx = term.Context.init(std.testing.allocator);1379    defer ctx.deinit();1380    const negative = try ctx.symbol("negative", .{ .bitvec = 4 });1381    const positive = try ctx.symbol("positive", .{ .bitvec = 4 });1382    const minus_one = try ctx.bitvecValue(0xf, 4);1383    const one = try ctx.bitvecValue(0x1, 4);1384    const min_value = try ctx.bitvecValue(0x8, 4);1385    const negative_is_minus_one = try ctx.eq(negative, minus_one);1386    const positive_is_one = try ctx.eq(positive, one);1387    const negative_less_positive = try ctx.bvslt(negative, positive);1388    const negative_less_equal_negative = try ctx.bvsle(negative, negative);1389    const min_less_negative = try ctx.bvslt(min_value, negative);1390    const positive_not_less_negative = try ctx.not(try ctx.bvslt(positive, negative));1391    var solver = sat.Solver.init(std.testing.allocator);1392    defer solver.deinit();1393    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1394    defer encoder.deinit();1395    try encoder.assertTerm(negative_is_minus_one);1396    try encoder.assertTerm(positive_is_one);1397    try encoder.assertTerm(negative_less_positive);1398    try encoder.assertTerm(negative_less_equal_negative);1399    try encoder.assertTerm(min_less_negative);1400    try encoder.assertTerm(positive_not_less_negative);1401    try encoder.encodeSymbols();1402    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1403    var model_result = try encoder.model(std.testing.allocator);1404    defer model_result.deinit();1405    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0xf, .width = 4 } }, model_result.get("negative").?);1406    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0x1, .width = 4 } }, model_result.get("positive").?);1407}14081409test "bit-vector encoder finds wrapped increment model" {1410    var ctx = term.Context.init(std.testing.allocator);1411    defer ctx.deinit();1412    const x = try ctx.symbol("x", .{ .bitvec = 4 });1413    const one = try ctx.bitvecValue(1, 4);1414    const zero = try ctx.bitvecValue(0, 4);1415    const assertion = try ctx.eq(try ctx.bvadd(x, one), zero);1416    var solver = sat.Solver.init(std.testing.allocator);1417    defer solver.deinit();1418    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1419    defer encoder.deinit();1420    try encoder.assertTerm(assertion);1421    const bits = try encoder.encodeBits(x);1422    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1423    try std.testing.expectEqual(@as(u128, 15), try modelValue(&solver, bits));1424}14251426test "bit-vector encoder solves subtraction model" {1427    var ctx = term.Context.init(std.testing.allocator);1428    defer ctx.deinit();1429    const x = try ctx.symbol("x", .{ .bitvec = 4 });1430    const three = try ctx.bitvecValue(3, 4);1431    const twelve = try ctx.bitvecValue(12, 4);1432    const assertion = try ctx.eq(try ctx.bvsub(x, three), twelve);1433    var solver = sat.Solver.init(std.testing.allocator);1434    defer solver.deinit();1435    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1436    defer encoder.deinit();1437    try encoder.assertTerm(assertion);1438    const bits = try encoder.encodeBits(x);1439    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1440    try std.testing.expectEqual(@as(u128, 15), try modelValue(&solver, bits));1441}14421443test "bit-vector encoder extracts named model values" {1444    var ctx = term.Context.init(std.testing.allocator);1445    defer ctx.deinit();1446    const x = try ctx.symbol("x", .{ .bitvec = 4 });1447    const flag = try ctx.symbol("flag", .bool);1448    const one = try ctx.bitvecValue(1, 4);1449    const zero = try ctx.bitvecValue(0, 4);1450    const assertion = try ctx.eq(try ctx.bvadd(x, one), zero);1451    var solver = sat.Solver.init(std.testing.allocator);1452    defer solver.deinit();1453    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1454    defer encoder.deinit();1455    try encoder.assertTerm(assertion);1456    try encoder.assertTerm(flag);1457    try encoder.encodeSymbols();1458    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1459    var model_result = try encoder.model(std.testing.allocator);1460    defer model_result.deinit();1461    try std.testing.expectEqual(@as(usize, 2), model_result.entries.items.len);1462    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 15, .width = 4 } }, model_result.get("x").?);1463    try std.testing.expectEqual(ModelValue{ .bool = true }, model_result.get("flag").?);1464    var buffer: [128]u8 = undefined;1465    var stream = std.Io.Writer.fixed(&buffer);1466    try model_result.write(&stream);1467    try std.testing.expect(std.mem.indexOf(u8, stream.buffered(), "x: (_ bv15 4)") != null);1468    try std.testing.expect(std.mem.indexOf(u8, stream.buffered(), "flag: true") != null);1469}14701471test "bit-vector encoder solves finite array store select model" {1472    var ctx = term.Context.init(std.testing.allocator);1473    defer ctx.deinit();1474    const memory = try ctx.symbol("memory", .{ .array = .{ .index_width = 2, .element_width = 4 } });1475    const index = try ctx.symbol("index", .{ .bitvec = 2 });1476    const other_index = try ctx.symbol("other_index", .{ .bitvec = 2 });1477    const value = try ctx.symbol("value", .{ .bitvec = 4 });1478    const other_value = try ctx.symbol("other_value", .{ .bitvec = 4 });1479    const index_one = try ctx.bitvecValue(1, 2);1480    const index_two = try ctx.bitvecValue(2, 2);1481    const ten = try ctx.bitvecValue(0xa, 4);1482    const five = try ctx.bitvecValue(0x5, 4);1483    const written = try ctx.arrayStore(memory, index, value);1484    const other_written = try ctx.arrayStore(written, other_index, other_value);1485    const index_is_one = try ctx.eq(index, index_one);1486    const other_index_is_two = try ctx.eq(other_index, index_two);1487    const value_is_ten = try ctx.eq(value, ten);1488    const other_value_is_five = try ctx.eq(other_value, five);1489    const stored_read = try ctx.eq(try ctx.arraySelect(written, index), value);1490    const preserved_read = try ctx.eq(try ctx.arraySelect(written, other_index), try ctx.arraySelect(memory, other_index));1491    const nested_stored_read = try ctx.eq(try ctx.arraySelect(other_written, index), value);1492    const nested_other_read = try ctx.eq(try ctx.arraySelect(other_written, other_index), other_value);1493    var solver = sat.Solver.init(std.testing.allocator);1494    defer solver.deinit();1495    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1496    defer encoder.deinit();1497    try encoder.assertTerm(index_is_one);1498    try encoder.assertTerm(other_index_is_two);1499    try encoder.assertTerm(value_is_ten);1500    try encoder.assertTerm(other_value_is_five);1501    try encoder.assertTerm(stored_read);1502    try encoder.assertTerm(preserved_read);1503    try encoder.assertTerm(nested_stored_read);1504    try encoder.assertTerm(nested_other_read);1505    try encoder.encodeSymbols();1506    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1507    var model_result = try encoder.model(std.testing.allocator);1508    defer model_result.deinit();1509    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 1, .width = 2 } }, model_result.get("index").?);1510    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 2, .width = 2 } }, model_result.get("other_index").?);1511    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0xa, .width = 4 } }, model_result.get("value").?);1512    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0x5, .width = 4 } }, model_result.get("other_value").?);1513    switch (model_result.get("memory").?) {1514        .array => |array| {1515            try std.testing.expectEqual(@as(u32, 2), array.index_width);1516            try std.testing.expectEqual(@as(u32, 4), array.element_width);1517            try std.testing.expectEqual(@as(usize, 4), array.cells.len);1518        },1519        else => return error.TestExpectedArrayModel,1520    }1521    var buffer: [512]u8 = undefined;1522    var stream = std.Io.Writer.fixed(&buffer);1523    try model_result.write(&stream);1524    try std.testing.expect(std.mem.indexOf(u8, stream.buffered(), "memory: (array (_ BitVec 2) (_ BitVec 4)") != null);1525}15261527test "bit-vector encoder rejects overwritten array read contradiction" {1528    var ctx = term.Context.init(std.testing.allocator);1529    defer ctx.deinit();1530    const memory = try ctx.symbol("memory", .{ .array = .{ .index_width = 2, .element_width = 4 } });1531    const index = try ctx.bitvecValue(1, 2);1532    const ten = try ctx.bitvecValue(0xa, 4);1533    const three = try ctx.bitvecValue(0x3, 4);1534    const written = try ctx.arrayStore(memory, index, ten);1535    const overwritten = try ctx.arrayStore(written, index, three);1536    const contradiction = try ctx.eq(try ctx.arraySelect(overwritten, index), ten);1537    var solver = sat.Solver.init(std.testing.allocator);1538    defer solver.deinit();1539    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1540    defer encoder.deinit();1541    try encoder.assertTerm(contradiction);1542    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1543}15441545test "bit-vector encoder compares finite arrays extensionally" {1546    var ctx = term.Context.init(std.testing.allocator);1547    defer ctx.deinit();1548    const lhs = try ctx.symbol("lhs", .{ .array = .{ .index_width = 2, .element_width = 4 } });1549    const rhs = try ctx.symbol("rhs", .{ .array = .{ .index_width = 2, .element_width = 4 } });1550    const index = try ctx.bitvecValue(2, 2);1551    const arrays_equal = try ctx.eq(lhs, rhs);1552    const reads_differ = try ctx.not(try ctx.eq(try ctx.arraySelect(lhs, index), try ctx.arraySelect(rhs, index)));1553    var solver = sat.Solver.init(std.testing.allocator);1554    defer solver.deinit();1555    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1556    defer encoder.deinit();1557    try encoder.assertTerm(arrays_equal);1558    try encoder.assertTerm(reads_differ);1559    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1560}15611562test "bit-vector encoder enforces uninterpreted function congruence" {1563    var ctx = term.Context.init(std.testing.allocator);1564    defer ctx.deinit();1565    const bv4 = term.Sort{ .bitvec = 4 };1566    const x = try ctx.symbol("x", bv4);1567    const y = try ctx.symbol("y", bv4);1568    const f = try ctx.function("f", &.{bv4}, bv4);1569    const fx = try ctx.apply(f, &.{x});1570    const fy = try ctx.apply(f, &.{y});1571    const arguments_equal = try ctx.eq(x, y);1572    const results_differ = try ctx.not(try ctx.eq(fx, fy));1573    var solver = sat.Solver.init(std.testing.allocator);1574    defer solver.deinit();1575    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1576    defer encoder.deinit();1577    try encoder.assertTerm(arguments_equal);1578    try encoder.assertTerm(results_differ);1579    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1580}15811582test "bit-vector encoder permits distinct uninterpreted function results" {1583    var ctx = term.Context.init(std.testing.allocator);1584    defer ctx.deinit();1585    const bv4 = term.Sort{ .bitvec = 4 };1586    const x = try ctx.symbol("x", bv4);1587    const y = try ctx.symbol("y", bv4);1588    const f = try ctx.function("f", &.{bv4}, bv4);1589    const fx = try ctx.apply(f, &.{x});1590    const fy = try ctx.apply(f, &.{y});1591    const one = try ctx.bitvecValue(1, 4);1592    const two = try ctx.bitvecValue(2, 4);1593    const three = try ctx.bitvecValue(3, 4);1594    const four = try ctx.bitvecValue(4, 4);1595    const x_is_one = try ctx.eq(x, one);1596    const y_is_two = try ctx.eq(y, two);1597    const fx_is_three = try ctx.eq(fx, three);1598    const fy_is_four = try ctx.eq(fy, four);1599    var solver = sat.Solver.init(std.testing.allocator);1600    defer solver.deinit();1601    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1602    defer encoder.deinit();1603    try encoder.assertTerm(x_is_one);1604    try encoder.assertTerm(y_is_two);1605    try encoder.assertTerm(fx_is_three);1606    try encoder.assertTerm(fy_is_four);1607    try encoder.encodeSymbols();1608    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1609    var model_result = try encoder.model(std.testing.allocator);1610    defer model_result.deinit();1611    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 1, .width = 4 } }, model_result.get("x").?);1612    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 2, .width = 4 } }, model_result.get("y").?);1613    const f_model = model_result.getFunction("f").?;1614    try std.testing.expectEqual(@as(usize, 2), f_model.entries.items.len);1615    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 1, .width = 4 } }, f_model.entries.items[0].arguments[0]);1616    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 3, .width = 4 } }, f_model.entries.items[0].result);1617    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 2, .width = 4 } }, f_model.entries.items[1].arguments[0]);1618    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 4, .width = 4 } }, f_model.entries.items[1].result);1619}16201621test "bit-vector model skips unused uninterpreted function applications" {1622    var ctx = term.Context.init(std.testing.allocator);1623    defer ctx.deinit();1624    const bv4 = term.Sort{ .bitvec = 4 };1625    const x = try ctx.symbol("x", bv4);1626    const f = try ctx.function("f", &.{bv4}, bv4);1627    _ = try ctx.apply(f, &.{x});1628    var solver = sat.Solver.init(std.testing.allocator);1629    defer solver.deinit();1630    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1631    defer encoder.deinit();1632    try encoder.encodeSymbols();1633    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1634    var model_result = try encoder.model(std.testing.allocator);1635    defer model_result.deinit();1636    try std.testing.expect(model_result.getFunction("f") == null);1637}16381639test "bit-vector encoder enforces bool-returning function congruence" {1640    var ctx = term.Context.init(std.testing.allocator);1641    defer ctx.deinit();1642    const bv4 = term.Sort{ .bitvec = 4 };1643    const x = try ctx.symbol("x", bv4);1644    const y = try ctx.symbol("y", bv4);1645    const p = try ctx.function("p", &.{bv4}, .bool);1646    const px = try ctx.apply(p, &.{x});1647    const py = try ctx.apply(p, &.{y});1648    const arguments_equal = try ctx.eq(x, y);1649    const py_false = try ctx.not(py);1650    var solver = sat.Solver.init(std.testing.allocator);1651    defer solver.deinit();1652    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1653    defer encoder.deinit();1654    try encoder.assertTerm(arguments_equal);1655    try encoder.assertTerm(px);1656    try encoder.assertTerm(py_false);1657    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1658}16591660test "bit-vector encoder rejects terms appended after initialization" {1661    var ctx = term.Context.init(std.testing.allocator);1662    defer ctx.deinit();1663    const x = try ctx.symbol("x", .{ .bitvec = 4 });1664    var solver = sat.Solver.init(std.testing.allocator);1665    defer solver.deinit();1666    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1667    defer encoder.deinit();1668    const zero = try ctx.bitvecValue(0, 4);1669    try std.testing.expectError(EncodeError.TermOutOfRange, encoder.assertTerm(try ctx.eq(x, zero)));1670}16711672test "bit-vector encoder multiplies exactly modulo width" {1673    var ctx = term.Context.init(std.testing.allocator);1674    defer ctx.deinit();1675    const x = try ctx.symbol("x", .{ .bitvec = 4 });1676    const three = try ctx.bitvecValue(3, 4);1677    const fifteen = try ctx.bitvecValue(15, 4);1678    const assertion = try ctx.eq(try ctx.bvmul(x, three), fifteen);1679    var solver = sat.Solver.init(std.testing.allocator);1680    defer solver.deinit();1681    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1682    defer encoder.deinit();1683    try encoder.assertTerm(assertion);1684    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1685}16861687test "bit-vector encoder solves unsigned division and remainder model" {1688    var ctx = term.Context.init(std.testing.allocator);1689    defer ctx.deinit();1690    const dividend = try ctx.symbol("dividend", .{ .bitvec = 4 });1691    const divisor = try ctx.symbol("divisor", .{ .bitvec = 4 });1692    const thirteen = try ctx.bitvecValue(13, 4);1693    const three = try ctx.bitvecValue(3, 4);1694    const four = try ctx.bitvecValue(4, 4);1695    const one = try ctx.bitvecValue(1, 4);1696    const dividend_is_thirteen = try ctx.eq(dividend, thirteen);1697    const divisor_is_three = try ctx.eq(divisor, three);1698    const quotient_is_four = try ctx.eq(try ctx.bvudiv(dividend, divisor), four);1699    const remainder_is_one = try ctx.eq(try ctx.bvurem(dividend, divisor), one);1700    var solver = sat.Solver.init(std.testing.allocator);1701    defer solver.deinit();1702    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1703    defer encoder.deinit();1704    try encoder.assertTerm(dividend_is_thirteen);1705    try encoder.assertTerm(divisor_is_three);1706    try encoder.assertTerm(quotient_is_four);1707    try encoder.assertTerm(remainder_is_one);1708    try encoder.encodeSymbols();1709    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1710    var model_result = try encoder.model(std.testing.allocator);1711    defer model_result.deinit();1712    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 13, .width = 4 } }, model_result.get("dividend").?);1713    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 3, .width = 4 } }, model_result.get("divisor").?);1714}17151716test "bit-vector encoder follows unsigned division by zero semantics" {1717    var ctx = term.Context.init(std.testing.allocator);1718    defer ctx.deinit();1719    const dividend = try ctx.bitvecValue(10, 4);1720    const zero = try ctx.bitvecValue(0, 4);1721    const all_ones = try ctx.bitvecValue(15, 4);1722    const quotient_is_all_ones = try ctx.eq(try ctx.bvudiv(dividend, zero), all_ones);1723    const remainder_is_dividend = try ctx.eq(try ctx.bvurem(dividend, zero), dividend);1724    var solver = sat.Solver.init(std.testing.allocator);1725    defer solver.deinit();1726    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1727    defer encoder.deinit();1728    try encoder.assertTerm(quotient_is_all_ones);1729    try encoder.assertTerm(remainder_is_dividend);1730    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1731}17321733test "bit-vector encoder rejects wrapped unsigned division quotient" {1734    var ctx = term.Context.init(std.testing.allocator);1735    defer ctx.deinit();1736    const one = try ctx.bitvecValue(1, 4);1737    const three = try ctx.bitvecValue(3, 4);1738    const eleven = try ctx.bitvecValue(11, 4);1739    const impossible = try ctx.eq(try ctx.bvudiv(one, three), eleven);1740    var solver = sat.Solver.init(std.testing.allocator);1741    defer solver.deinit();1742    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1743    defer encoder.deinit();1744    try encoder.assertTerm(impossible);1745    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1746}17471748test "bit-vector encoder solves signed division remainder and modulo" {1749    var ctx = term.Context.init(std.testing.allocator);1750    defer ctx.deinit();1751    const negative = try ctx.symbol("negative", .{ .bitvec = 4 });1752    const positive = try ctx.symbol("positive", .{ .bitvec = 4 });1753    const positive_divisor = try ctx.symbol("positive_divisor", .{ .bitvec = 4 });1754    const negative_divisor = try ctx.symbol("negative_divisor", .{ .bitvec = 4 });1755    const minus_seven = try ctx.bitvecValue(0b1001, 4);1756    const plus_seven = try ctx.bitvecValue(0b0111, 4);1757    const plus_three = try ctx.bitvecValue(0b0011, 4);1758    const minus_three = try ctx.bitvecValue(0b1101, 4);1759    const minus_two = try ctx.bitvecValue(0b1110, 4);1760    const minus_one = try ctx.bitvecValue(0b1111, 4);1761    const plus_one = try ctx.bitvecValue(0b0001, 4);1762    const plus_two = try ctx.bitvecValue(0b0010, 4);1763    const negative_is_minus_seven = try ctx.eq(negative, minus_seven);1764    const positive_is_plus_seven = try ctx.eq(positive, plus_seven);1765    const positive_divisor_is_plus_three = try ctx.eq(positive_divisor, plus_three);1766    const negative_divisor_is_minus_three = try ctx.eq(negative_divisor, minus_three);1767    const negative_quotient = try ctx.eq(try ctx.bvsdiv(negative, positive_divisor), minus_two);1768    const negative_remainder = try ctx.eq(try ctx.bvsrem(negative, positive_divisor), minus_one);1769    const negative_modulo = try ctx.eq(try ctx.bvsmod(negative, positive_divisor), plus_two);1770    const positive_quotient = try ctx.eq(try ctx.bvsdiv(positive, negative_divisor), minus_two);1771    const positive_remainder = try ctx.eq(try ctx.bvsrem(positive, negative_divisor), plus_one);1772    const positive_modulo = try ctx.eq(try ctx.bvsmod(positive, negative_divisor), minus_two);1773    var solver = sat.Solver.init(std.testing.allocator);1774    defer solver.deinit();1775    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1776    defer encoder.deinit();1777    try encoder.assertTerm(negative_is_minus_seven);1778    try encoder.assertTerm(positive_is_plus_seven);1779    try encoder.assertTerm(positive_divisor_is_plus_three);1780    try encoder.assertTerm(negative_divisor_is_minus_three);1781    try encoder.assertTerm(negative_quotient);1782    try encoder.assertTerm(negative_remainder);1783    try encoder.assertTerm(negative_modulo);1784    try encoder.assertTerm(positive_quotient);1785    try encoder.assertTerm(positive_remainder);1786    try encoder.assertTerm(positive_modulo);1787    try encoder.encodeSymbols();1788    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1789    var model_result = try encoder.model(std.testing.allocator);1790    defer model_result.deinit();1791    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0b1001, .width = 4 } }, model_result.get("negative").?);1792    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0b0111, .width = 4 } }, model_result.get("positive").?);1793}17941795test "bit-vector encoder follows signed division by zero semantics" {1796    var ctx = term.Context.init(std.testing.allocator);1797    defer ctx.deinit();1798    const negative = try ctx.bitvecValue(0b1001, 4);1799    const positive = try ctx.bitvecValue(0b0111, 4);1800    const zero = try ctx.bitvecValue(0, 4);1801    const one = try ctx.bitvecValue(1, 4);1802    const all_ones = try ctx.bitvecValue(0b1111, 4);1803    const negative_division = try ctx.eq(try ctx.bvsdiv(negative, zero), one);1804    const positive_division = try ctx.eq(try ctx.bvsdiv(positive, zero), all_ones);1805    const negative_remainder = try ctx.eq(try ctx.bvsrem(negative, zero), negative);1806    const positive_remainder = try ctx.eq(try ctx.bvsrem(positive, zero), positive);1807    const negative_modulo = try ctx.eq(try ctx.bvsmod(negative, zero), negative);1808    const positive_modulo = try ctx.eq(try ctx.bvsmod(positive, zero), positive);1809    var solver = sat.Solver.init(std.testing.allocator);1810    defer solver.deinit();1811    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1812    defer encoder.deinit();1813    try encoder.assertTerm(negative_division);1814    try encoder.assertTerm(positive_division);1815    try encoder.assertTerm(negative_remainder);1816    try encoder.assertTerm(positive_remainder);1817    try encoder.assertTerm(negative_modulo);1818    try encoder.assertTerm(positive_modulo);1819    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1820}18211822test "bit-vector encoder detects unsigned addition overflow" {1823    var ctx = term.Context.init(std.testing.allocator);1824    defer ctx.deinit();1825    const x = try ctx.symbol("x", .{ .bitvec = 4 });1826    const one = try ctx.bitvecValue(1, 4);1827    const fifteen = try ctx.bitvecValue(15, 4);1828    const is_fifteen = try ctx.eq(x, fifteen);1829    const overflow = try ctx.bvuaddo(x, one);1830    var solver = sat.Solver.init(std.testing.allocator);1831    defer solver.deinit();1832    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1833    defer encoder.deinit();1834    try encoder.assertTerm(is_fifteen);1835    try encoder.assertTerm(overflow);1836    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1837}18381839test "bit-vector encoder proves bounded unsigned addition does not overflow" {1840    var ctx = term.Context.init(std.testing.allocator);1841    defer ctx.deinit();1842    const x = try ctx.symbol("x", .{ .bitvec = 4 });1843    const one = try ctx.bitvecValue(1, 4);1844    const fifteen = try ctx.bitvecValue(15, 4);1845    const assertion = try ctx.and_(&.{ try ctx.bvult(x, fifteen), try ctx.bvuaddo(x, one) });1846    var solver = sat.Solver.init(std.testing.allocator);1847    defer solver.deinit();1848    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1849    defer encoder.deinit();1850    try encoder.assertTerm(assertion);1851    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1852}18531854test "bit-vector encoder detects signed addition overflow" {1855    var ctx = term.Context.init(std.testing.allocator);1856    defer ctx.deinit();1857    const x = try ctx.symbol("x", .{ .bitvec = 4 });1858    const seven = try ctx.bitvecValue(7, 4);1859    const one = try ctx.bitvecValue(1, 4);1860    const is_seven = try ctx.eq(x, seven);1861    const overflow = try ctx.bvsaddo(x, one);1862    var solver = sat.Solver.init(std.testing.allocator);1863    defer solver.deinit();1864    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1865    defer encoder.deinit();1866    try encoder.assertTerm(is_seven);1867    try encoder.assertTerm(overflow);1868    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1869}18701871test "bit-vector encoder proves signed addition inside range does not overflow" {1872    var ctx = term.Context.init(std.testing.allocator);1873    defer ctx.deinit();1874    const x = try ctx.symbol("x", .{ .bitvec = 4 });1875    const minus_one = try ctx.bitvecValue(15, 4);1876    const one = try ctx.bitvecValue(1, 4);1877    const is_minus_one = try ctx.eq(x, minus_one);1878    const overflow = try ctx.bvsaddo(x, one);1879    var solver = sat.Solver.init(std.testing.allocator);1880    defer solver.deinit();1881    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1882    defer encoder.deinit();1883    try encoder.assertTerm(is_minus_one);1884    try encoder.assertTerm(overflow);1885    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1886}18871888test "bit-vector encoder detects signed subtraction overflow" {1889    var ctx = term.Context.init(std.testing.allocator);1890    defer ctx.deinit();1891    const x = try ctx.symbol("x", .{ .bitvec = 4 });1892    const min = try ctx.bitvecValue(8, 4);1893    const one = try ctx.bitvecValue(1, 4);1894    const is_min = try ctx.eq(x, min);1895    const overflow = try ctx.bvssubo(x, one);1896    var solver = sat.Solver.init(std.testing.allocator);1897    defer solver.deinit();1898    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1899    defer encoder.deinit();1900    try encoder.assertTerm(is_min);1901    try encoder.assertTerm(overflow);1902    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1903}19041905test "bit-vector encoder proves signed subtraction inside range does not overflow" {1906    var ctx = term.Context.init(std.testing.allocator);1907    defer ctx.deinit();1908    const x = try ctx.symbol("x", .{ .bitvec = 4 });1909    const minus_one = try ctx.bitvecValue(15, 4);1910    const one = try ctx.bitvecValue(1, 4);1911    const is_minus_one = try ctx.eq(x, minus_one);1912    const overflow = try ctx.bvssubo(x, one);1913    var solver = sat.Solver.init(std.testing.allocator);1914    defer solver.deinit();1915    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1916    defer encoder.deinit();1917    try encoder.assertTerm(is_minus_one);1918    try encoder.assertTerm(overflow);1919    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1920}19211922test "bit-vector encoder detects unsigned multiplication overflow" {1923    var ctx = term.Context.init(std.testing.allocator);1924    defer ctx.deinit();1925    const x = try ctx.symbol("x", .{ .bitvec = 4 });1926    const six = try ctx.bitvecValue(6, 4);1927    const three = try ctx.bitvecValue(3, 4);1928    const is_six = try ctx.eq(x, six);1929    const overflow = try ctx.bvumulo(x, three);1930    var solver = sat.Solver.init(std.testing.allocator);1931    defer solver.deinit();1932    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1933    defer encoder.deinit();1934    try encoder.assertTerm(is_six);1935    try encoder.assertTerm(overflow);1936    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1937}19381939test "bit-vector encoder proves bounded unsigned multiplication does not overflow" {1940    var ctx = term.Context.init(std.testing.allocator);1941    defer ctx.deinit();1942    const x = try ctx.symbol("x", .{ .bitvec = 4 });1943    const five = try ctx.bitvecValue(5, 4);1944    const three = try ctx.bitvecValue(3, 4);1945    const assertion = try ctx.and_(&.{ try ctx.eq(x, five), try ctx.bvumulo(x, three) });1946    var solver = sat.Solver.init(std.testing.allocator);1947    defer solver.deinit();1948    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1949    defer encoder.deinit();1950    try encoder.assertTerm(assertion);1951    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1952}19531954test "bit-vector encoder detects signed multiplication overflow" {1955    var ctx = term.Context.init(std.testing.allocator);1956    defer ctx.deinit();1957    const x = try ctx.symbol("x", .{ .bitvec = 4 });1958    const minus_four = try ctx.bitvecValue(12, 4);1959    const three = try ctx.bitvecValue(3, 4);1960    const is_minus_four = try ctx.eq(x, minus_four);1961    const overflow = try ctx.bvsmulo(x, three);1962    var solver = sat.Solver.init(std.testing.allocator);1963    defer solver.deinit();1964    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1965    defer encoder.deinit();1966    try encoder.assertTerm(is_minus_four);1967    try encoder.assertTerm(overflow);1968    try std.testing.expectEqual(sat.Status.sat, try solver.solve());1969}19701971test "bit-vector encoder proves signed multiplication inside range does not overflow" {1972    var ctx = term.Context.init(std.testing.allocator);1973    defer ctx.deinit();1974    const x = try ctx.symbol("x", .{ .bitvec = 4 });1975    const minus_two = try ctx.bitvecValue(14, 4);1976    const three = try ctx.bitvecValue(3, 4);1977    const is_minus_two = try ctx.eq(x, minus_two);1978    const overflow = try ctx.bvsmulo(x, three);1979    var solver = sat.Solver.init(std.testing.allocator);1980    defer solver.deinit();1981    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);1982    defer encoder.deinit();1983    try encoder.assertTerm(is_minus_two);1984    try encoder.assertTerm(overflow);1985    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());1986}19871988test "bit-vector encoder solves bitwise mask model" {1989    var ctx = term.Context.init(std.testing.allocator);1990    defer ctx.deinit();1991    const x = try ctx.symbol("x", .{ .bitvec = 4 });1992    const ten = try ctx.bitvecValue(0b1010, 4);1993    const three = try ctx.bitvecValue(0b0011, 4);1994    const one = try ctx.bitvecValue(0b0001, 4);1995    const zero = try ctx.bitvecValue(0b0000, 4);1996    const eight = try ctx.bitvecValue(0b1000, 4);1997    const eleven = try ctx.bitvecValue(0b1011, 4);1998    const mask_assertion = try ctx.eq(try ctx.bvand(x, ten), eight);1999    const low_bit_assertion = try ctx.eq(try ctx.bvand(x, one), zero);2000    const or_assertion = try ctx.eq(try ctx.bvor(x, three), eleven);2001    const all_ones = try ctx.bitvecValue(0b1111, 4);2002    const not_assertion = try ctx.eq(try ctx.bvxor(x, all_ones), try ctx.bvnot(x));2003    var solver = sat.Solver.init(std.testing.allocator);2004    defer solver.deinit();2005    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2006    defer encoder.deinit();2007    try encoder.assertTerm(mask_assertion);2008    try encoder.assertTerm(low_bit_assertion);2009    try encoder.assertTerm(or_assertion);2010    try encoder.assertTerm(not_assertion);2011    try encoder.encodeSymbols();2012    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2013    var model_result = try encoder.model(std.testing.allocator);2014    defer model_result.deinit();2015    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 8, .width = 4 } }, model_result.get("x").?);2016}20172018test "bit-vector encoder proves xor self contradiction unsat" {2019    var ctx = term.Context.init(std.testing.allocator);2020    defer ctx.deinit();2021    const x = try ctx.symbol("x", .{ .bitvec = 4 });2022    const one = try ctx.bitvecValue(1, 4);2023    const assertion = try ctx.eq(try ctx.bvxor(x, x), one);2024    var solver = sat.Solver.init(std.testing.allocator);2025    defer solver.deinit();2026    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2027    defer encoder.deinit();2028    try encoder.assertTerm(assertion);2029    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());2030}20312032test "bit-vector encoder solves symbolic logical shift model" {2033    var ctx = term.Context.init(std.testing.allocator);2034    defer ctx.deinit();2035    const x = try ctx.symbol("x", .{ .bitvec = 4 });2036    const amount = try ctx.symbol("amount", .{ .bitvec = 4 });2037    const two = try ctx.bitvecValue(2, 4);2038    const three = try ctx.bitvecValue(3, 4);2039    const twelve = try ctx.bitvecValue(12, 4);2040    const shifted = try ctx.bvshl(x, amount);2041    const roundtrip = try ctx.bvlshr(shifted, amount);2042    const amount_is_two = try ctx.eq(amount, two);2043    const shifted_is_twelve = try ctx.eq(shifted, twelve);2044    const roundtrip_is_x = try ctx.eq(roundtrip, x);2045    const x_is_three = try ctx.eq(x, three);2046    var solver = sat.Solver.init(std.testing.allocator);2047    defer solver.deinit();2048    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2049    defer encoder.deinit();2050    try encoder.assertTerm(amount_is_two);2051    try encoder.assertTerm(shifted_is_twelve);2052    try encoder.assertTerm(roundtrip_is_x);2053    try encoder.assertTerm(x_is_three);2054    try encoder.encodeSymbols();2055    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2056    var model_result = try encoder.model(std.testing.allocator);2057    defer model_result.deinit();2058    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 3, .width = 4 } }, model_result.get("x").?);2059    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 2, .width = 4 } }, model_result.get("amount").?);2060}20612062test "bit-vector encoder treats large logical shift amounts as zero" {2063    var ctx = term.Context.init(std.testing.allocator);2064    defer ctx.deinit();2065    const one = try ctx.bitvecValue(1, 4);2066    const four = try ctx.bitvecValue(4, 4);2067    const zero = try ctx.bitvecValue(0, 4);2068    const shl_is_zero = try ctx.eq(try ctx.bvshl(one, four), zero);2069    const lshr_is_zero = try ctx.eq(try ctx.bvlshr(one, four), zero);2070    var solver = sat.Solver.init(std.testing.allocator);2071    defer solver.deinit();2072    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2073    defer encoder.deinit();2074    try encoder.assertTerm(shl_is_zero);2075    try encoder.assertTerm(lshr_is_zero);2076    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2077}20782079test "bit-vector encoder solves arithmetic shift model" {2080    var ctx = term.Context.init(std.testing.allocator);2081    defer ctx.deinit();2082    const negative = try ctx.symbol("negative", .{ .bitvec = 4 });2083    const positive = try ctx.symbol("positive", .{ .bitvec = 4 });2084    const amount = try ctx.symbol("amount", .{ .bitvec = 4 });2085    const minus_four = try ctx.bitvecValue(0b1100, 4);2086    const plus_six = try ctx.bitvecValue(0b0110, 4);2087    const one = try ctx.bitvecValue(1, 4);2088    const minus_two = try ctx.bitvecValue(0b1110, 4);2089    const plus_three = try ctx.bitvecValue(0b0011, 4);2090    const logical_negative = try ctx.bitvecValue(0b0110, 4);2091    const negative_is_minus_four = try ctx.eq(negative, minus_four);2092    const positive_is_plus_six = try ctx.eq(positive, plus_six);2093    const amount_is_one = try ctx.eq(amount, one);2094    const arithmetic_negative = try ctx.eq(try ctx.bvashr(negative, amount), minus_two);2095    const logical_negative_match = try ctx.eq(try ctx.bvlshr(negative, amount), logical_negative);2096    const arithmetic_positive = try ctx.eq(try ctx.bvashr(positive, amount), plus_three);2097    var solver = sat.Solver.init(std.testing.allocator);2098    defer solver.deinit();2099    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2100    defer encoder.deinit();2101    try encoder.assertTerm(negative_is_minus_four);2102    try encoder.assertTerm(positive_is_plus_six);2103    try encoder.assertTerm(amount_is_one);2104    try encoder.assertTerm(arithmetic_negative);2105    try encoder.assertTerm(logical_negative_match);2106    try encoder.assertTerm(arithmetic_positive);2107    try encoder.encodeSymbols();2108    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2109    var model_result = try encoder.model(std.testing.allocator);2110    defer model_result.deinit();2111    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0b1100, .width = 4 } }, model_result.get("negative").?);2112    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0b0110, .width = 4 } }, model_result.get("positive").?);2113    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 1, .width = 4 } }, model_result.get("amount").?);2114}21152116test "bit-vector encoder treats large arithmetic shift amounts as sign fill" {2117    var ctx = term.Context.init(std.testing.allocator);2118    defer ctx.deinit();2119    const negative = try ctx.bitvecValue(0b1001, 4);2120    const positive = try ctx.bitvecValue(0b0111, 4);2121    const four = try ctx.bitvecValue(4, 4);2122    const all_ones = try ctx.bitvecValue(0b1111, 4);2123    const zero = try ctx.bitvecValue(0, 4);2124    const negative_is_all_ones = try ctx.eq(try ctx.bvashr(negative, four), all_ones);2125    const positive_is_zero = try ctx.eq(try ctx.bvashr(positive, four), zero);2126    var solver = sat.Solver.init(std.testing.allocator);2127    defer solver.deinit();2128    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2129    defer encoder.deinit();2130    try encoder.assertTerm(negative_is_all_ones);2131    try encoder.assertTerm(positive_is_zero);2132    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2133}21342135test "bit-vector encoder solves fixed rotate model" {2136    var ctx = term.Context.init(std.testing.allocator);2137    defer ctx.deinit();2138    const x = try ctx.symbol("x", .{ .bitvec = 4 });2139    const nine = try ctx.bitvecValue(0b1001, 4);2140    const left_one = try ctx.bitvecValue(0b0011, 4);2141    const right_one = try ctx.bitvecValue(0b1100, 4);2142    const right_two = try ctx.bitvecValue(0b0110, 4);2143    const x_is_nine = try ctx.eq(x, nine);2144    const rotate_left_one = try ctx.eq(try ctx.bvrotl(x, 1), left_one);2145    const rotate_left_five = try ctx.eq(try ctx.bvrotl(x, 5), left_one);2146    const rotate_right_one = try ctx.eq(try ctx.bvrotr(x, 1), right_one);2147    const rotate_right_two = try ctx.eq(try ctx.bvrotr(x, 2), right_two);2148    var solver = sat.Solver.init(std.testing.allocator);2149    defer solver.deinit();2150    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2151    defer encoder.deinit();2152    try encoder.assertTerm(x_is_nine);2153    try encoder.assertTerm(rotate_left_one);2154    try encoder.assertTerm(rotate_left_five);2155    try encoder.assertTerm(rotate_right_one);2156    try encoder.assertTerm(rotate_right_two);2157    try encoder.encodeSymbols();2158    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2159    var model_result = try encoder.model(std.testing.allocator);2160    defer model_result.deinit();2161    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0b1001, .width = 4 } }, model_result.get("x").?);2162}21632164test "bit-vector encoder rejects impossible fixed rotate result" {2165    var ctx = term.Context.init(std.testing.allocator);2166    defer ctx.deinit();2167    const nine = try ctx.bitvecValue(0b1001, 4);2168    const impossible = try ctx.eq(try ctx.bvrotl(nine, 1), nine);2169    var solver = sat.Solver.init(std.testing.allocator);2170    defer solver.deinit();2171    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2172    defer encoder.deinit();2173    try encoder.assertTerm(impossible);2174    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());2175}21762177test "bit-vector encoder rejects impossible large shift result" {2178    var ctx = term.Context.init(std.testing.allocator);2179    defer ctx.deinit();2180    const one = try ctx.bitvecValue(1, 4);2181    const four = try ctx.bitvecValue(4, 4);2182    const impossible = try ctx.eq(try ctx.bvshl(one, four), one);2183    var solver = sat.Solver.init(std.testing.allocator);2184    defer solver.deinit();2185    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2186    defer encoder.deinit();2187    try encoder.assertTerm(impossible);2188    try std.testing.expectEqual(sat.Status.unsat, try solver.solve());2189}21902191test "bit-vector encoder solves concat and extract model" {2192    var ctx = term.Context.init(std.testing.allocator);2193    defer ctx.deinit();2194    const high = try ctx.symbol("high", .{ .bitvec = 4 });2195    const low = try ctx.symbol("low", .{ .bitvec = 4 });2196    const word = try ctx.bvconcat(high, low);2197    const high_value = try ctx.bitvecValue(0xa, 4);2198    const low_value = try ctx.bitvecValue(0x5, 4);2199    const packed_value = try ctx.bitvecValue(0xa5, 8);2200    const high_assertion = try ctx.eq(try ctx.bvextract(word, 7, 4), high_value);2201    const low_assertion = try ctx.eq(try ctx.bvextract(word, 3, 0), low_value);2202    const packed_assertion = try ctx.eq(word, packed_value);2203    var solver = sat.Solver.init(std.testing.allocator);2204    defer solver.deinit();2205    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2206    defer encoder.deinit();2207    try encoder.assertTerm(high_assertion);2208    try encoder.assertTerm(low_assertion);2209    try encoder.assertTerm(packed_assertion);2210    try encoder.encodeSymbols();2211    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2212    var model_result = try encoder.model(std.testing.allocator);2213    defer model_result.deinit();2214    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0xa, .width = 4 } }, model_result.get("high").?);2215    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0x5, .width = 4 } }, model_result.get("low").?);2216}22172218test "bit-vector encoder solves zero and sign extension model" {2219    var ctx = term.Context.init(std.testing.allocator);2220    defer ctx.deinit();2221    const positive = try ctx.symbol("positive", .{ .bitvec = 4 });2222    const negative = try ctx.symbol("negative", .{ .bitvec = 4 });2223    const positive_value = try ctx.bitvecValue(0x5, 4);2224    const negative_value = try ctx.bitvecValue(0xa, 4);2225    const zero_extended = try ctx.bvzeroext(positive, 4);2226    const positive_signed = try ctx.bvsignext(positive, 4);2227    const negative_signed = try ctx.bvsignext(negative, 4);2228    const zero_extended_value = try ctx.bitvecValue(0x05, 8);2229    const positive_signed_value = try ctx.bitvecValue(0x05, 8);2230    const negative_signed_value = try ctx.bitvecValue(0xfa, 8);2231    const positive_is_value = try ctx.eq(positive, positive_value);2232    const negative_is_value = try ctx.eq(negative, negative_value);2233    const zero_extended_is_value = try ctx.eq(zero_extended, zero_extended_value);2234    const positive_signed_is_value = try ctx.eq(positive_signed, positive_signed_value);2235    const negative_signed_is_value = try ctx.eq(negative_signed, negative_signed_value);2236    var solver = sat.Solver.init(std.testing.allocator);2237    defer solver.deinit();2238    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2239    defer encoder.deinit();2240    try encoder.assertTerm(positive_is_value);2241    try encoder.assertTerm(negative_is_value);2242    try encoder.assertTerm(zero_extended_is_value);2243    try encoder.assertTerm(positive_signed_is_value);2244    try encoder.assertTerm(negative_signed_is_value);2245    try encoder.encodeSymbols();2246    try std.testing.expectEqual(sat.Status.sat, try solver.solve());2247    var model_result = try encoder.model(std.testing.allocator);2248    defer model_result.deinit();2249    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0x5, .width = 4 } }, model_result.get("positive").?);2250    try std.testing.expectEqual(ModelValue{ .bitvec = .{ .value = 0xa, .width = 4 } }, model_result.get("negative").?);2251}22522253test "bit-vector encoder rejects invalid extract range" {2254    var ctx = term.Context.init(std.testing.allocator);2255    defer ctx.deinit();2256    const x = try ctx.symbol("x", .{ .bitvec = 4 });2257    const invalid = try ctx.bvextract(x, 4, 0);2258    var solver = sat.Solver.init(std.testing.allocator);2259    defer solver.deinit();2260    var encoder = try Encoder.init(std.testing.allocator, &ctx, &solver);2261    defer encoder.deinit();2262    try std.testing.expectError(EncodeError.InvalidBitVectorRange, encoder.encodeBits(invalid));2263}