lib/smt/src/bitvec.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

   1 //! Decides formulas over Booleans, fixed-width bit-vectors, arrays and uninterpreted functions by
   2 //! turning them into clauses for a SAT solver, and reads a satisfying assignment back as a value
   3 //! 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 a
   7 //! 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 to
  10 //! become Boolean relations between single bits. An array with an index of w bits has 2 to the
  11 //! power w cells, so its size doubles with each index bit. An uninterpreted function has no
  12 //! 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 or
  17 //! a logical right shift by at least the width gives zero, and an arithmetic right shift by at
  18 //! 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 significant
  21 //! 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 per
  23 //! bit, and division finds its quotient one bit at a time from the most significant bit down. One
  24 //! variable fixed true by a unit clause stands for true, and its negation stands for false, so
  25 //! 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 index
  28 //! wider than eight bits with `ArrayIndexTooWide` and an array has at most 256 cells. Two arrays
  29 //! 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 whenever
  32 //! their arguments are equal. The encoder writes these clauses once, the first time a caller
  33 //! 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 and
  37 //! `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`: one
  41 //! value per named constant and one entry per encoded function application. A model value holds at
  42 //! most 128 bits, and a wider named constant, function argument, function result or array cell
  43 //! fails with `ModelValueTooWide`.
  44 //!
  45 //! A caller builds an `Encoder` over a `Context` and a `sat.Solver`, asserts terms with
  46 //! `assertTerm`, assumes terms with `assumeTerm`, and calls `solve`. On a satisfiable answer it
  47 //! reads `model`, and on an unsatisfiable one it asks the solver for the unsat core and the proof.
  48 const std = @import("std");
  49 const sat = @import("sat/root.zig");
  50 const term = @import("term.zig");
  51 
  52 /// The errors the encoder and `Encoder.model` return besides the solver's and the allocator's, for
  53 /// code that reports why a formula could not be encoded or read back. The encoder's functions
  54 /// return `Error`, which is `anyerror`, so the compiler does not check a switch on these tags for
  55 /// completeness.
  56 pub const EncodeError = error{
  57     /// A term used as a condition, such as an assertion, an assumption or an operand of `and`, has
  58     /// 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's
  63     /// argument count differs from its declaration.
  64     SortMismatch,
  65     /// The term is an integer term or `distinct`, which the encoder does not support, or it
  66     /// 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 was
  69     /// never encoded. The error follows a model read before a satisfiable answer, or of a constant
  70     /// 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 a
  77     /// 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 };
  86 
  87 /// The error set of the encoder's functions: any error, returned by every public function of the
  88 /// encoder, so a caller can absorb it into its own error set. The set covers `EncodeError`, the
  89 /// solver's errors, `error.OutOfMemory` and the errors of `Context.sortOf`. Because it is
  90 /// `anyerror`, the compiler cannot list the errors a call returns.
  91 pub const Error = anyerror;
  92 
  93 const max_native_array_index_width = 8;
  94 
  95 const ArrayValue = struct {
  96     index_width: u32,
  97     element_width: u32,
  98     cells: [][]sat.Literal,
  99 };
 100 
 101 const Value = union(enum) {
 102     none,
 103     bool: sat.Literal,
 104     bits: []sat.Literal,
 105     array: ArrayValue,
 106 };
 107 
 108 /// The value of a constant, a function argument or a function result in a model: a Boolean, a
 109 /// bit-vector or an array, for code that reads one from a `Model` to print it or compare it with an
 110 /// expected value. A value that holds an array owns its cells, so its owner calls `deinit`.
 111 pub 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 its
 115     /// 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 for
 121     /// 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     },
 127 
 128     /// 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 Boolean
 130     /// 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     }
 138 
 139     /// Writes the value in SMT-LIB syntax: `true` or `false`, `(_ bvV W)`, or an array as
 140     /// `(array (_ BitVec i) (_ BitVec e) 0->(_ bvV e) ...)` with one index and value per cell, for
 141     /// `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 };
 156 
 157 /// One named constant of a model and its value, for code that walks a `Model`.
 158 pub 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 };
 164 
 165 /// One application of an uninterpreted function in a model: its argument values and its result
 166 /// value, for code that checks a function's model.
 167 pub 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,
 172 
 173     /// Frees every argument value, the argument slice and the result value with `allocator`, for
 174     /// `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 };
 184 
 185 /// The model of one uninterpreted function: its name and one entry per application the encoder
 186 /// encoded, returned by `Model.getFunction` so code can check each application of one function. The
 187 /// model lists the applications in the formula, and it gives no value for other arguments.
 188 pub 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 equal
 192     /// arguments give two entries with equal results.
 193     entries: std.ArrayList(FunctionModelEntry) = .empty,
 194 
 195     /// Frees the name, every entry and the entry list with `allocator`, for `Model.deinit` to call
 196     /// 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 };
 206 
 207 /// The values a satisfying assignment gives: one per named constant, and one entry per encoded
 208 /// 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 model
 210 /// owns every name and value in it, and its owner frees them all with `deinit`.
 211 pub const Model = struct {
 212     allocator: std.mem.Allocator,
 213     /// The named constants and their values, in the order the constants were built. Two constants
 214     /// 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,
 218 
 219     /// Returns an empty model that allocates with `allocator`. A caller makes one to build an
 220     /// 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     }
 224 
 225     /// Frees every name, every value and every function model. The owner calls it once when done
 226     /// with the values. A value returned by `get` and a pointer returned by `getFunction` are
 227     /// 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     }
 240 
 241     /// Adds the constant `name` with value `value`. `Encoder.model` calls it once per named
 242     /// constant. The call copies `name` and takes ownership of `value`, and on failure it frees
 243     /// `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     }
 251 
 252     /// Returns the value of the first constant named `name`, or `null` when the model has none. A
 253     /// caller reads with it a constant's value after a satisfiable answer, as every encoder test
 254     /// does. An array value's cells stay owned by the model, so the caller does not free them. The
 255     /// 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     }
 262 
 263     /// Adds an entry with argument values `arguments` and result value `result` to the model of the
 264     /// function `name`, and creates that function's model on first use. `Encoder.model` calls it
 265     /// once per encoded application. The call takes ownership of `arguments` and `result`, and on
 266     /// 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     }
 279 
 280     /// Returns the model of the function `name`, or `null` when no application of it was encoded. A
 281     /// 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     }
 289 
 290     /// Writes one `name: value` line per constant, then per function a `name:` line followed by one
 291     /// indented `(arguments) -> result` line per entry, with each value in the syntax of
 292     /// `ModelValue.write`. A caller prints a model for a person to read with it. The call returns
 293     /// 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     }
 314 
 315     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 };
 325 
 326 const BitwiseKind = enum {
 327     and_,
 328     or_,
 329     xor,
 330 };
 331 
 332 const ShiftKind = enum {
 333     left,
 334     right,
 335 };
 336 
 337 const RotateKind = enum {
 338     left,
 339     right,
 340 };
 341 
 342 const DivRemResult = struct {
 343     quotient: []sat.Literal,
 344     remainder: []sat.Literal,
 345 };
 346 
 347 const ExtendKind = enum {
 348     zero,
 349     sign,
 350 };
 351 
 352 /// Turns the terms of one `Context` into clauses of one `sat.Solver`, and reads the solver's
 353 /// assignment back as a `Model`. A caller builds one per solve, over the `Context` that holds its
 354 /// terms and the solver that will decide them. The encoder borrows the `Context` and the solver, so
 355 /// both have to outlive it. The encoder encodes each term once and remembers the result, and the
 356 /// clauses it adds stay in the solver.
 357 pub 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,
 365 
 366     /// Returns an encoder over `ctx` and `solver` that allocates with `allocator`. A caller builds
 367     /// the encoder once the formula's terms exist and before asserting any of them. The call adds
 368     /// one variable to the solver and a unit clause that fixes it true, and the encoder uses it as
 369     /// the constant true. The encoder sizes its table of encoded terms to the terms of `ctx` at
 370     /// 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     }
 386 
 387     /// Frees the bits and array cells of every encoded term and the table that held them. The owner
 388     /// calls it once when done with the encoder. The clauses already added to the solver stay
 389     /// 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     }
 401 
 402     /// Encodes the Boolean term `assertion` and adds a unit clause that makes it true in every
 403     /// later solve. A caller states with it each part of the formula that has to hold, as a caller
 404     /// does for every assertion of a `Script`. The first call of `assertTerm`, `assumeTerm` or
 405     /// `solve` also adds the equal-arguments clauses for every function application of the
 406     /// `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     }
 412 
 413     /// Encodes the Boolean term `assumption`, adds its literal to the solver's active assumptions
 414     /// and returns that literal. A caller calls it to test a condition without asserting it for
 415     /// good, and matches the returned literal against the solver's unsat core, a set of tested
 416     /// conditions that the formula refutes together. The assumption holds in every solve until the
 417     /// caller pops its assumption frame or clears the assumptions. The clauses that encode the term
 418     /// 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 function
 420     /// 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     }
 427 
 428     /// Encodes every named constant of the `Context`, adds the equal-arguments clauses if no
 429     /// earlier call did, and solves under the active assumptions. A caller decides the formula with
 430     /// 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, a
 432     /// single integer constant in the `Context` makes the call fail with `UnsupportedTerm`, even if
 433     /// 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     }
 439 
 440     /// 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 the
 442     /// 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     }
 449 
 450     /// Encodes the bit-vector term `id` and returns one literal per bit, least significant bit
 451     /// first. A caller that builds its own clauses over a bit-vector's bits gets them with it. The
 452     /// encoder owns the returned slice, which stays valid until `deinit`. The call returns
 453     /// `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     }
 460 
 461     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     }
 467 
 468     /// Encodes every named constant of the `Context`, so that `model` finds a value for each one. A
 469     /// caller that calls `sat.Solver.solve` directly, as the encoder's tests do, calls it first so
 470     /// 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     }
 479 
 480     /// Returns a `Model` that allocates with `allocator`, with the value of every named constant
 481     /// and one entry per encoded function application. A caller reads the satisfying values with it
 482     /// after a satisfiable answer. The caller owns the model and frees it with `Model.deinit`. The
 483     /// call returns `ModelUnavailable` when a constant has no value, as before a satisfiable answer
 484     /// or before `encodeSymbols`, `ModelValueTooWide` for a value above 128 bits, and
 485     /// `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     }
 500 
 501     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     }
 564 
 565     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     }
 573 
 574     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     }
 583 
 584     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     }
 606 
 607     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     }
 638 
 639     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     }
 654 
 655     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     }
 660 
 661     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     }
 678 
 679     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     }
 702 
 703     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     }
 722 
 723     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     }
 732 
 733     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     }
 740 
 741     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     }
 749 
 750     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     }
 764 
 765     fn freeArray(self: *Encoder, array: ArrayValue) void {
 766         for (array.cells) |cell| self.allocator.free(cell);
 767         self.allocator.free(array.cells);
 768     }
 769 
 770     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     }
 778 
 779     fn freshLiteral(self: *Encoder) Error!sat.Literal {
 780         return sat.Literal.positive(try self.solver.addVariable());
 781     }
 782 
 783     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     }
 798 
 799     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     }
 815 
 816     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     }
 832 
 833     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     }
 846 
 847     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     }
 850 
 851     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     }
 861 
 862     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     }
 865 
 866     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     }
 874 
 875     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     }
 883 
 884     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     }
 895 
 896     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     }
 908 
 909     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     }
 923 
 924     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     }
 945 
 946     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     }
 971 
 972     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     }
 982 
 983     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     }
 990 
 991     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     }
1004 
1005     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     }
1028 
1029     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     }
1049 
1050     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     }
1063 
1064     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     }
1105 
1106     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     }
1121 
1122     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     }
1136 
1137     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     }
1164 
1165     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     }
1171 
1172     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     }
1181 
1182     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     }
1201 
1202     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     }
1222 
1223     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     }
1229 
1230     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     }
1240 
1241     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     }
1256 
1257     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     }
1265 
1266     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     }
1273 
1274     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     }
1281 
1282     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     }
1290 
1291     fn xnorGate(self: *Encoder, a: sat.Literal, b: sat.Literal) Error!sat.Literal {
1292         return (try self.xorGate(a, b)).negated();
1293     }
1294 
1295     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     }
1298 
1299     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 };
1309 
1310 fn 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 }
1319 
1320 fn 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 }
1324 
1325 test "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 }
1337 
1338 test "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 }
1350 
1351 test "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 }
1376 
1377 test "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 }
1408 
1409 test "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 }
1425 
1426 test "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 }
1442 
1443 test "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 }
1470 
1471 test "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 }
1526 
1527 test "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 }
1544 
1545 test "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 }
1561 
1562 test "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 }
1581 
1582 test "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 }
1620 
1621 test "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 }
1638 
1639 test "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 }
1659 
1660 test "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 }
1671 
1672 test "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 }
1686 
1687 test "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 }
1715 
1716 test "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 }
1732 
1733 test "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 }
1747 
1748 test "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 }
1794 
1795 test "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 }
1821 
1822 test "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 }
1838 
1839 test "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 }
1853 
1854 test "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 }
1870 
1871 test "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 }
1887 
1888 test "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 }
1904 
1905 test "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 }
1921 
1922 test "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 }
1938 
1939 test "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 }
1953 
1954 test "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 }
1970 
1971 test "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 }
1987 
1988 test "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 }
2017 
2018 test "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 }
2031 
2032 test "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 }
2061 
2062 test "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 }
2078 
2079 test "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 }
2115 
2116 test "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 }
2134 
2135 test "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 }
2163 
2164 test "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 }
2176 
2177 test "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 }
2190 
2191 test "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 }
2217 
2218 test "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 }
2252 
2253 test "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 }