tiny.smt.term

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

1//! The formulas the package solves are trees of typed expressions over Booleans, integers,2//! bit-vectors and arrays, with named constants and uninterpreted functions, and each expression3//! has a sort.4//!5//! A caller builds a formula one operator at a time and needs each piece to be a small value it can6//! reuse as an operand of larger pieces. The encoder and the SMT-LIB writer walk every expression7//! and read its operator, its operands and its sort.8//!9//! Formulas share subexpressions, as `x` appears in both `x + 1` and `x < x + 1`, so the pieces10//! refer to one another and need one owner. Each operator accepts operands of particular sorts, and11//! a formula with a mismatched operand has no meaning.12//!13//! [SMT-LIB](https://smt-lib.org/) defines the sorts and operators of its theories: Booleans with14//! equality, integers, fixed-size bit-vectors, arrays and uninterpreted functions. The term kinds15//! here carry SMT-LIB's operator names, and the SMT-LIB writer and parser map each kind to its16//! standard operator.17//!18//! Every term lives in one table that owns every term and function declaration it holds, a19//! *context* (`Context`), and each term is its 32-bit index in that table (`Term`). Building a term20//! appends one entry and returns its index, so an index stays valid until the table is freed, and21//! building one expression twice gives two indexes.22//!23//! The builders copy the names and operand lists they receive, so a caller may free its own slices24//! after the call. The builders check no sorts, except that `function` refuses a second declaration25//! of one name with other sorts and `apply` checks its arguments against the declaration. `sortOf`26//! computes a term's sort on demand and reports a mismatch. A builder stores operand indexes as27//! given, so an index that names no earlier term leaves a term on which `sortOf` fails or recurses28//! without end.29//!30//! Arrays map a bit-vector index to a bit-vector element, and their sort records the two widths31//! (`ArraySort`). Integer terms can be built, sorted and written as SMT-LIB, and the bit-vector32//! encoder refuses them. The SMT-LIB parser returns, and the writer reads, a logic name with the33//! list of terms asserted over one table, a *script* (`Script`). Freeing the table frees every34//! term, name and operand list at once, and nothing frees a single term.35const std = @import("std");3637/// The shape of an array sort: the width of its bit-vector index and the width of its bit-vector38/// element. Code that declares an array constant builds one to give the array's shape, as the39/// encoder's array tests do. The bit-vector encoder accepts an index of at most eight bits.40pub const ArraySort = struct {41    /// The width of the index in bits. The index of every read or write of the array has this42    /// width.43    index_width: u32,44    /// The width of each element in bits. A read of the array is a bit-vector of this width.45    element_width: u32,46};4748/// The sort of a term: Boolean, integer, a bit-vector of a given width, or an array from49/// bit-vectors to bit-vectors. Code declares every constant and function with a sort, and `sortOf`50/// returns one for every term.51pub const Sort = union(enum) {52    /// The Boolean sort. SMT-LIB writes it `Bool`.53    bool,54    /// The sort of mathematical integers. SMT-LIB writes it `Int`. The bit-vector encoder refuses55    /// terms of this sort with `UnsupportedTerm`.56    int,57    /// A bit-vector sort, with its width in bits as the payload. SMT-LIB writes it `(_ BitVec n)`.58    /// Any width is accepted, 0 and widths above 128 included. A bit-vector constant wider than 12859    /// bits makes the encoder panic. A named constant wider than 128 bits encodes, and60    /// `Encoder.model` returns `ModelValueTooWide` for it.61    bitvec: u32,62    /// An array sort, with its index and element widths as the payload. SMT-LIB writes it63    /// `(Array (_ BitVec i) (_ BitVec e))`.64    array: ArraySort,6566    /// Writes the sort in SMT-LIB syntax: `Bool`, `Int`, `(_ BitVec n)` or67    /// `(Array (_ BitVec i) (_ BitVec e))`. The SMT-LIB writer calls it to print the sort of every68    /// declaration. The function returns only the writer's errors.69    pub fn write(self: Sort, writer: *std.Io.Writer) std.Io.Writer.Error!void {70        switch (self) {71            .bool => try writer.writeAll("Bool"),72            .int => try writer.writeAll("Int"),73            .bitvec => |width| try writer.print("(_ BitVec {d})", .{width}),74            .array => |array| try writer.print(75                "(Array (_ BitVec {d}) (_ BitVec {d}))",76                .{ array.index_width, array.element_width },77            ),78        }79    }8081    /// Returns true when the two sorts have the same kind and the same widths. `sortOf` and82    /// `function` call it to compare the sort an operator needs with the sort it got.83    pub fn eql(self: Sort, other: Sort) bool {84        return std.meta.eql(self, other);85    }86};8788/// A term, named by its index in the table of the `Context` that built it. Every builder returns89/// one and every operand is one, so callers pass terms around as plain integers. The index means90/// nothing in another `Context`. The index stays valid until its `Context` is freed.91pub const Term = u32;92/// A function declaration, named by its index in the declaration table of the `Context` that holds93/// it. `function` returns one, and `apply` takes one to build an application.94pub const Function = u32;9596/// The payload of a named constant: its name and its sort. Code that walks terms reads it from a97/// `.symbol` term to learn a constant's name and sort.98pub const SymbolExpr = struct {99    /// The constant's name, a copy the `Context` owns and frees. Two constants may share a name,100    /// because every call to `symbol` builds a new term.101    name: []const u8,102    /// The constant's sort.103    sort: Sort,104};105106/// The payload of a function application: the declared function and its argument terms. Code that107/// walks terms reads it from an `.apply` term to learn which function is applied to which108/// arguments.109pub const ApplyExpr = struct {110    /// The applied function's index in the declaration table.111    function: Function,112    /// The argument terms in declaration order, a copy the `Context` owns and frees.113    args: []const Term,114};115116/// The payload of a bit-vector constant: its value and its width. Code that walks terms reads it117/// from a `.bitvec` term to learn a constant's bits.118pub const BitVecExpr = struct {119    /// The constant's bits as an unsigned number: bit i of the number is bit i of the vector,120    /// counted from the least significant. Nothing checks the value against the width, and the121    /// encoder reads only the low `width` bits.122    value: u128,123    /// The constant's width in bits. A width above 128 makes the encoder panic.124    width: u32,125};126127/// The payload of a two-operand term: the left operand term `lhs` and the right operand term `rhs`.128/// Code that walks terms reads it from every two-operand term, such as `.eq`, `.bvadd` or `.bvult`.129pub const BinaryOperands = struct {130    lhs: Term,131    rhs: Term,132};133134/// The payload of an array read: the array term `array` and the index term `index`. Code that walks135/// terms reads it from an `.array_select` term.136pub const ArraySelectExpr = struct {137    array: Term,138    index: Term,139};140141/// The payload of an array write: the array term `array`, the index term `index` and the element142/// term `value` stored there. Code that walks terms reads it from an `.array_store` term.143pub const ArrayStoreExpr = struct {144    array: Term,145    index: Term,146    value: Term,147};148149/// The payload of a bit range taken from the bit-vector term `operand`, between two bit positions.150/// Code that walks terms reads it from a `.bvextract` term.151pub const BitVecExtractExpr = struct {152    operand: Term,153    /// The position of the highest bit taken, counted from 0 at the least significant bit. The154    /// position has to be below the operand's width, or `sortOf` and the encoder report155    /// `InvalidBitVectorRange`.156    high: u32,157    /// The position of the lowest bit taken, counted from 0 at the least significant bit. The158    /// position has to be at most `high`, or `sortOf` and the encoder report159    /// `InvalidBitVectorRange`.160    low: u32,161};162163/// The payload of a widening of the bit-vector term `operand`. Code that walks terms reads it from164/// a `.bvzeroext` or `.bvsignext` term.165pub const BitVecExtendExpr = struct {166    operand: Term,167    /// The number of bits added above the operand's most significant bit.168    extra: u32,169};170171/// The payload of a rotation of the bit-vector term `operand` by a fixed number of bits. Code that172/// walks terms reads it from a `.bvrotl` or `.bvrotr` term.173pub const BitVecRotateExpr = struct {174    operand: Term,175    /// The number of positions to rotate. The encoder takes it modulo the operand's width, so 5 on176    /// a 4-bit operand rotates by 1.177    amount: u32,178};179180/// One declared function: its name, the sorts of its arguments and the sort of its result. Code181/// that walks the declarations reads one per function, as the SMT-LIB writer does for each182/// `declare-fun`.183pub const FunctionDecl = struct {184    /// The function's name, a copy the `Context` owns and frees. The name is unique among the185    /// declarations of one `Context`.186    name: []const u8,187    /// The sorts of the arguments in order, a copy the `Context` owns and frees. The slice length188    /// is the function's arity: 0 declares a constant function.189    params: []const Sort,190    /// The sort of every application's result.191    result: Sort,192};193194/// One term: a tag naming its operator and a payload holding its operands. Code that walks a195/// formula switches on it, as the encoder and the SMT-LIB writer do for every term. The `Context`196/// stores one per term, and a term's index is its position in that table. A tag named after an197/// SMT-LIB operator reads and writes as that operator, and each tag whose name differs gives its198/// SMT-LIB spelling. The bit-vector encoder refuses the integer tags (`int`, `add`, `mul`, `le`,199/// `lt`, `ge`, `gt`) and `distinct` with `UnsupportedTerm`.200pub const Expr = union(enum) {201    /// A named constant, with its name and sort as the payload. The encoder gives it fresh202    /// variables, one per bit.203    symbol: SymbolExpr,204    /// A function application, with the function and its arguments as the payload. Its sort is the205    /// function's result sort.206    apply: ApplyExpr,207    /// A Boolean constant. SMT-LIB writes it `true` or `false`.208    bool: bool,209    /// An integer constant, a signed 128-bit value. The bit-vector encoder refuses it.210    int: i128,211    /// A bit-vector constant, with its value and width as the payload. SMT-LIB writes it212    /// `(_ bvV W)`.213    bitvec: BitVecExpr,214    /// The negation of one Boolean operand.215    not: Term,216    /// The conjunction of any number of Boolean operands. With no operands it is true. SMT-LIB217    /// writes it `and`.218    and_: []const Term,219    /// The disjunction of any number of Boolean operands. With no operands it is false. SMT-LIB220    /// writes it `or`.221    or_: []const Term,222    /// `lhs` implies `rhs`, both Boolean. SMT-LIB writes it `=>`.223    implies: BinaryOperands,224    /// `lhs` equals `rhs`, a Boolean term over two operands of one sort. Two arrays are equal when225    /// every cell is equal. SMT-LIB writes it `=`.226    eq: BinaryOperands,227    /// True when all operands differ from one another, over operands of one sort. The bit-vector228    /// encoder refuses it.229    distinct: []const Term,230    /// The integer sum of any number of integer operands. SMT-LIB writes it `+`. The bit-vector231    /// encoder refuses it.232    add: []const Term,233    /// The integer product of any number of integer operands. SMT-LIB writes it `*`. The bit-vector234    /// encoder refuses it.235    mul: []const Term,236    /// `lhs` is at most `rhs`, as integers. SMT-LIB writes it `<=`. The bit-vector encoder refuses237    /// it.238    le: BinaryOperands,239    /// `lhs` is less than `rhs`, as integers. SMT-LIB writes it `<`. The bit-vector encoder refuses240    /// it.241    lt: BinaryOperands,242    /// `lhs` is at least `rhs`, as integers. SMT-LIB writes it `>=`. The bit-vector encoder refuses243    /// it.244    ge: BinaryOperands,245    /// `lhs` is greater than `rhs`, as integers. SMT-LIB writes it `>`. The bit-vector encoder246    /// refuses it.247    gt: BinaryOperands,248    /// `lhs` is at most `rhs`, as unsigned bit-vectors of one width.249    bvule: BinaryOperands,250    /// `lhs` is less than `rhs`, as unsigned bit-vectors of one width.251    bvult: BinaryOperands,252    /// `lhs` is at most `rhs`, as two's-complement bit-vectors of one width.253    bvsle: BinaryOperands,254    /// `lhs` is less than `rhs`, as two's-complement bit-vectors of one width.255    bvslt: BinaryOperands,256    /// True when the unsigned sum of `lhs` and `rhs` does not fit their width.257    bvuaddo: BinaryOperands,258    /// True when the two's-complement sum of `lhs` and `rhs` does not fit their width: both have259    /// one sign and the sum has the other.260    bvsaddo: BinaryOperands,261    /// True when the two's-complement difference `lhs` minus `rhs` does not fit their width.262    bvssubo: BinaryOperands,263    /// True when the unsigned product of `lhs` and `rhs` does not fit their width.264    bvumulo: BinaryOperands,265    /// True when the two's-complement product of `lhs` and `rhs` does not fit their width.266    bvsmulo: BinaryOperands,267    /// The bitwise complement of one bit-vector operand, of the same width.268    bvnot: Term,269    /// The bitwise and of two bit-vectors of one width.270    bvand: BinaryOperands,271    /// The bitwise or of two bit-vectors of one width.272    bvor: BinaryOperands,273    /// The bitwise exclusive or of two bit-vectors of one width.274    bvxor: BinaryOperands,275    /// `lhs` shifted toward its most significant bit by the value of `rhs`, with zeros shifted in,276    /// over two bit-vectors of one width. A shift amount at or above the width gives zero.277    bvshl: BinaryOperands,278    /// `lhs` shifted toward its least significant bit by the value of `rhs`, with zeros shifted in.279    /// A shift amount at or above the width gives zero.280    bvlshr: BinaryOperands,281    /// `lhs` shifted toward its least significant bit by the value of `rhs`, with copies of its282    /// sign bit shifted in. A shift amount at or above the width fills every bit with the sign bit.283    bvashr: BinaryOperands,284    /// The unsigned quotient of `lhs` by `rhs`, rounded down. Division by zero gives all ones.285    bvudiv: BinaryOperands,286    /// The unsigned remainder of `lhs` by `rhs`. The remainder by zero is `lhs`.287    bvurem: BinaryOperands,288    /// The two's-complement quotient of `lhs` by `rhs`, rounded toward zero. Division by zero gives289    /// 1 for a negative `lhs` and all ones otherwise.290    bvsdiv: BinaryOperands,291    /// The two's-complement remainder of `lhs` by `rhs`, with the sign of `lhs`. The remainder by292    /// zero is `lhs`.293    bvsrem: BinaryOperands,294    /// The two's-complement modulo of `lhs` by `rhs`, with the sign of `rhs`. The modulo by zero is295    /// `lhs`.296    bvsmod: BinaryOperands,297    /// The element of an array at an index, a bit-vector of the element width. The index has the298    /// array's index width. SMT-LIB writes it `select`.299    array_select: ArraySelectExpr,300    /// An array equal to its operand everywhere except at one index, which holds the new element.301    /// The term's sort is the operand's array sort. SMT-LIB writes it `store`.302    array_store: ArrayStoreExpr,303    /// The bits of `lhs` above the bits of `rhs`, one bit-vector as wide as the two together.304    /// SMT-LIB writes it `concat`.305    bvconcat: BinaryOperands,306    /// The bits from position `high` down to position `low` of one bit-vector, both included, so307    /// the result has `high - low + 1` bits. SMT-LIB writes it `((_ extract high low) x)`.308    bvextract: BitVecExtractExpr,309    /// A bit-vector widened by `extra` zero bits above its most significant bit. SMT-LIB writes it310    /// `((_ zero_extend extra) x)`.311    bvzeroext: BitVecExtendExpr,312    /// A bit-vector widened by `extra` copies of its sign bit. SMT-LIB writes it313    /// `((_ sign_extend extra) x)`.314    bvsignext: BitVecExtendExpr,315    /// A bit-vector rotated toward its most significant bit by a fixed number of positions, with316    /// the top bits wrapping to the bottom. SMT-LIB writes it `((_ rotate_left amount) x)`.317    bvrotl: BitVecRotateExpr,318    /// A bit-vector rotated toward its least significant bit by a fixed number of positions, with319    /// the bottom bits wrapping to the top. SMT-LIB writes it `((_ rotate_right amount) x)`.320    bvrotr: BitVecRotateExpr,321    /// The sum of two bit-vectors of one width, modulo 2 to the power of the width.322    bvadd: BinaryOperands,323    /// The difference `lhs` minus `rhs` of two bit-vectors of one width, modulo 2 to the power of324    /// the width.325    bvsub: BinaryOperands,326    /// The product of two bit-vectors of one width, modulo 2 to the power of the width.327    bvmul: BinaryOperands,328};329330/// One table that owns every term and function declaration it holds. Every formula starts here: a331/// caller makes one, builds its terms with the builders, and frees them all at once with `deinit`.332/// Each builder appends one term and returns its index. The builders check no sorts, except333/// `function` and `apply`, and `sortOf` checks a term's sort when a caller asks. Every builder can334/// fail with `error.OutOfMemory`, and a failed builder leaves the table as it was. A `Script`, a335/// parser and an encoder borrow the `Context` and have to be freed before it.336pub const Context = struct {337    /// The allocator for every term, name, operand list and declaration. A `Script` over this table338    /// and the SMT-LIB parser allocate with it too.339    allocator: std.mem.Allocator,340    /// Every term in the order it was built: entry i is the term whose index is i. The encoder and341    /// the SMT-LIB writer read it to walk every named constant.342    nodes: std.ArrayList(Expr) = .empty,343    /// Every function declaration in the order it was declared: entry i is the function whose index344    /// is i.345    functions: std.ArrayList(FunctionDecl) = .empty,346347    /// Returns an empty table that allocates with `allocator`, so a caller makes one before348    /// building any term. The call allocates nothing.349    pub fn init(allocator: std.mem.Allocator) Context {350        return .{ .allocator = allocator };351    }352353    /// Frees every term's name and operand list, every declaration and both tables, so the owner354    /// calls it once after every `Script`, parser and encoder built over the table is done with its355    /// terms. Every `Term` and `Function` index from this table is invalid afterward.356    pub fn deinit(self: *Context) void {357        for (self.nodes.items) |node| {358            switch (node) {359                .symbol => |sym| self.allocator.free(sym.name),360                .apply => |item| self.allocator.free(item.args),361                .and_, .or_, .distinct, .add, .mul => |items| self.allocator.free(items),362                else => {},363            }364        }365        for (self.functions.items) |decl| {366            self.allocator.free(decl.name);367            self.allocator.free(decl.params);368        }369        self.functions.deinit(self.allocator);370        self.nodes.deinit(self.allocator);371        self.* = undefined;372    }373374    /// Appends a named constant of the given sort and returns its term, so code declares each free375    /// variable of a formula with it, as the SMT-LIB parser does for every `declare-const`. The376    /// builder copies `name`, so the caller may free its own copy. The builder builds a new term on377    /// every call, even for a name used before.378    pub fn symbol(self: *Context, name: []const u8, sort: Sort) !Term {379        const owned_name = try self.allocator.dupe(u8, name);380        errdefer self.allocator.free(owned_name);381        return try self.append(.{ .symbol = .{ .name = owned_name, .sort = sort } });382    }383384    /// Declares a function by name, argument sorts and result sort, and returns its index, so code385    /// declares each uninterpreted function with it, as the SMT-LIB parser does for every386    /// `declare-fun`. A second call with the same name and the same sorts returns the first index.387    /// A second call with the same name and other sorts returns `error.DuplicateFunction`. The388    /// builder copies `name` and `params`.389    pub fn function(390        self: *Context,391        name: []const u8,392        params: []const Sort,393        result: Sort,394    ) !Function {395        for (self.functions.items, 0..) |decl, index| {396            if (!std.mem.eql(u8, decl.name, name)) continue;397            if (!sortListsEqual(decl.params, params) or !decl.result.eql(result)) {398                return error.DuplicateFunction;399            }400            return @intCast(index);401        }402        const owned_name = try self.allocator.dupe(u8, name);403        errdefer self.allocator.free(owned_name);404        const owned_params = try self.allocator.dupe(Sort, params);405        errdefer self.allocator.free(owned_params);406        const id: Function = @intCast(self.functions.items.len);407        try self.functions.append(self.allocator, .{408            .name = owned_name,409            .params = owned_params,410            .result = result,411        });412        return id;413    }414415    /// Appends the application of the function `function_id` to `args` and returns its term, so416    /// code applies a declared function to arguments with it. The call returns417    /// `error.UnknownFunction` for an index past the declarations, `error.FunctionArityMismatch`418    /// for the wrong number of arguments, and `error.FunctionArgumentSortMismatch` for an argument419    /// of the wrong sort. The builder computes each argument's sort with `sortOf`, so the call also420    /// returns the errors of `sortOf` for an argument that has no sort. The builder copies `args`.421    pub fn apply(self: *Context, function_id: Function, args: []const Term) !Term {422        if (function_id >= self.functions.items.len) return error.UnknownFunction;423        const decl = self.functions.items[function_id];424        if (decl.params.len != args.len) return error.FunctionArityMismatch;425        for (args, decl.params) |arg, expected| {426            if (!(try self.sortOf(arg)).eql(expected)) return error.FunctionArgumentSortMismatch;427        }428        const owned = try self.allocator.dupe(Term, args);429        errdefer self.allocator.free(owned);430        return try self.append(.{ .apply = .{ .function = function_id, .args = owned } });431    }432433    /// Returns the sort of term `id`, checking every operand below it against the sorts its434    /// operator accepts, so code checks a formula's sorts before encoding or writing, and the435    /// encoder reads each function argument's sort with it. The call returns `error.TermOutOfRange`436    /// for an index past the table, `error.SortMismatch` for an operand of the wrong sort,437    /// `error.InvalidBitVectorRange` for a bad extract range, and the errors of `apply` for a bad438    /// application. The function allocates nothing, and the call walks the whole term below `id` on439    /// every call. The recursion has no depth bound, and a term that refers to itself makes the440    /// call recurse without end.441    pub fn sortOf(self: *const Context, id: Term) anyerror!Sort {442        if (id >= self.nodes.items.len) return error.TermOutOfRange;443        return switch (self.nodes.items[id]) {444            .symbol => |sym| sym.sort,445            .apply => |item| try self.sortOfApply(item),446            .bool => .bool,447            .int => .int,448            .bitvec => |value| .{ .bitvec = value.width },449            .not => |operand| try self.expectBoolResult(operand),450            .and_, .or_ => |operands| try self.expectBoolList(operands),451            .implies => |pair| try self.expectBoolPair(pair.lhs, pair.rhs),452            .eq => |pair| try self.expectSameSortPair(pair.lhs, pair.rhs),453            .distinct => |operands| try self.expectSameSortList(operands),454            .add, .mul => |operands| try self.expectIntList(operands),455            .le => |pair| try self.expectIntPair(pair.lhs, pair.rhs),456            .lt => |pair| try self.expectIntPair(pair.lhs, pair.rhs),457            .ge => |pair| try self.expectIntPair(pair.lhs, pair.rhs),458            .gt => |pair| try self.expectIntPair(pair.lhs, pair.rhs),459            .bvule => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),460            .bvult => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),461            .bvsle => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),462            .bvslt => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),463            .bvuaddo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),464            .bvsaddo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),465            .bvssubo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),466            .bvumulo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),467            .bvsmulo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),468            .bvnot => |operand| try self.expectBitVecResult(operand),469            .bvand => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),470            .bvor => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),471            .bvxor => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),472            .bvshl => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),473            .bvlshr => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),474            .bvashr => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),475            .bvudiv => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),476            .bvurem => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),477            .bvsdiv => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),478            .bvsrem => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),479            .bvsmod => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),480            .bvadd => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),481            .bvsub => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),482            .bvmul => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),483            .array_select => |item| try self.sortOfArraySelect(item.array, item.index),484            .array_store => |item| try self.sortOfArrayStore(item.array, item.index, item.value),485            .bvconcat => |pair| try self.sortOfConcat(pair.lhs, pair.rhs),486            .bvextract => |item| try self.sortOfExtract(item.operand, item.high, item.low),487            .bvzeroext => |item| try self.sortOfExtend(item.operand, item.extra),488            .bvsignext => |item| try self.sortOfExtend(item.operand, item.extra),489            .bvrotl => |item| try self.expectBitVecResult(item.operand),490            .bvrotr => |item| try self.expectBitVecResult(item.operand),491        };492    }493494    /// Appends the constant `value` and returns its term, so code builds the Boolean constants with495    /// it.496    pub fn boolValue(self: *Context, value: bool) !Term {497        return try self.append(.{ .bool = value });498    }499500    /// Appends the integer constant `value` and returns its term, so code builds integer constants501    /// with it, as the SMT-LIB parser does for every numeral.502    pub fn intValue(self: *Context, value: i128) !Term {503        return try self.append(.{ .int = value });504    }505506    /// Appends the constant with bits `value` and width `width` and returns its term, so code507    /// builds bit-vector constants with it, as the SMT-LIB parser does for every `(_ bvV W)`. The508    /// builder checks neither the value against the width nor the width. A width above 128 makes509    /// the encoder panic.510    pub fn bitvecValue(self: *Context, value: u128, width: u32) !Term {511        return try self.append(.{ .bitvec = .{ .value = value, .width = width } });512    }513514    /// Appends the negation of `operand` and returns its term, so code negates a Boolean term with515    /// it.516    pub fn not(self: *Context, operand: Term) !Term {517        return try self.append(.{ .not = operand });518    }519520    /// Appends the conjunction of `operands` and returns its term, so code calls it to join Boolean521    /// terms that must all hold. The builder copies `operands`.522    pub fn and_(self: *Context, operands: []const Term) !Term {523        return try self.appendList(.and_, operands);524    }525526    /// Appends the disjunction of `operands` and returns its term, so code calls it to join Boolean527    /// terms of which one must hold. The builder copies `operands`.528    pub fn or_(self: *Context, operands: []const Term) !Term {529        return try self.appendList(.or_, operands);530    }531532    /// Appends `lhs` implies `rhs` and returns its term, so code states that one Boolean term533    /// implies another with it.534    pub fn implies(self: *Context, lhs: Term, rhs: Term) !Term {535        return try self.append(.{ .implies = .{ .lhs = lhs, .rhs = rhs } });536    }537538    /// Appends `lhs` equals `rhs` and returns its term, so code calls it to state that two terms539    /// are equal.540    pub fn eq(self: *Context, lhs: Term, rhs: Term) !Term {541        return try self.append(.{ .eq = .{ .lhs = lhs, .rhs = rhs } });542    }543544    /// Appends the claim that `operands` all differ and returns its term, so code states that terms545    /// all differ with it. The builder copies `operands`. The bit-vector encoder refuses the term.546    pub fn distinct(self: *Context, operands: []const Term) !Term {547        return try self.appendList(.distinct, operands);548    }549550    /// Appends the integer sum of `operands` and returns its term, so code adds integer terms with551    /// it. The builder copies `operands`. The bit-vector encoder refuses the term.552    pub fn add(self: *Context, operands: []const Term) !Term {553        return try self.appendList(.add, operands);554    }555556    /// Appends the integer product of `operands` and returns its term, so code multiplies integer557    /// terms with it. The builder copies `operands`. The bit-vector encoder refuses the term.558    pub fn mul(self: *Context, operands: []const Term) !Term {559        return try self.appendList(.mul, operands);560    }561562    /// Appends the two-operand term of kind `tag` over `lhs` and `rhs` and returns its term, so the563    /// SMT-LIB parser calls it with the tag of each two-operand operator it reads, and one call564    /// covers every such operator. The parameter `tag` names a kind whose payload is565    /// `BinaryOperands`, or `.array_select`, which the builder builds with `arraySelect`. Any other566    /// tag is a compile error.567    pub fn binary(self: *Context, comptime tag: std.meta.Tag(Expr), lhs: Term, rhs: Term) !Term {568        return switch (tag) {569            .implies,570            .eq,571            .le,572            .lt,573            .ge,574            .gt,575            .bvule,576            .bvult,577            .bvsle,578            .bvslt,579            .bvuaddo,580            .bvsaddo,581            .bvssubo,582            .bvumulo,583            .bvsmulo,584            .bvand,585            .bvor,586            .bvxor,587            .bvshl,588            .bvlshr,589            .bvashr,590            .bvudiv,591            .bvurem,592            .bvsdiv,593            .bvsrem,594            .bvsmod,595            .bvconcat,596            .bvadd,597            .bvsub,598            .bvmul,599            => try self.appendPair(tag, lhs, rhs),600            .array_select => try self.arraySelect(lhs, rhs),601            else => unreachable,602        };603    }604605    /// Appends `lhs` at most `rhs`, as integers, and returns its term, so code compares integer606    /// terms with it. The bit-vector encoder refuses the term.607    pub fn le(self: *Context, lhs: Term, rhs: Term) !Term {608        return try self.append(.{ .le = .{ .lhs = lhs, .rhs = rhs } });609    }610611    /// Appends `lhs` less than `rhs`, as integers, and returns its term, so code compares integer612    /// terms with it. The bit-vector encoder refuses the term.613    pub fn lt(self: *Context, lhs: Term, rhs: Term) !Term {614        return try self.append(.{ .lt = .{ .lhs = lhs, .rhs = rhs } });615    }616617    /// Appends `lhs` at least `rhs`, as integers, and returns its term, so code compares integer618    /// terms with it. The bit-vector encoder refuses the term.619    pub fn ge(self: *Context, lhs: Term, rhs: Term) !Term {620        return try self.append(.{ .ge = .{ .lhs = lhs, .rhs = rhs } });621    }622623    /// Appends `lhs` greater than `rhs`, as integers, and returns its term, so code compares624    /// integer terms with it. The bit-vector encoder refuses the term.625    pub fn gt(self: *Context, lhs: Term, rhs: Term) !Term {626        return try self.append(.{ .gt = .{ .lhs = lhs, .rhs = rhs } });627    }628629    /// Appends `lhs` at most `rhs`, as unsigned bit-vectors, and returns its term, so code compares630    /// bit-vectors as unsigned numbers with it.631    pub fn bvule(self: *Context, lhs: Term, rhs: Term) !Term {632        return try self.append(.{ .bvule = .{ .lhs = lhs, .rhs = rhs } });633    }634635    /// Appends `lhs` less than `rhs`, as unsigned bit-vectors, and returns its term, so code636    /// compares bit-vectors as unsigned numbers with it, as the SMT-LIB round-trip test does.637    pub fn bvult(self: *Context, lhs: Term, rhs: Term) !Term {638        return try self.append(.{ .bvult = .{ .lhs = lhs, .rhs = rhs } });639    }640641    /// Appends `lhs` at most `rhs`, as two's-complement bit-vectors, and returns its term, so code642    /// compares bit-vectors as two's-complement numbers with it.643    pub fn bvsle(self: *Context, lhs: Term, rhs: Term) !Term {644        return try self.append(.{ .bvsle = .{ .lhs = lhs, .rhs = rhs } });645    }646647    /// Appends `lhs` less than `rhs`, as two's-complement bit-vectors, and returns its term, so648    /// code compares bit-vectors as two's-complement numbers with it.649    pub fn bvslt(self: *Context, lhs: Term, rhs: Term) !Term {650        return try self.append(.{ .bvslt = .{ .lhs = lhs, .rhs = rhs } });651    }652653    /// Appends the claim that the unsigned sum of `lhs` and `rhs` overflows their width and returns654    /// its term. Code asks with it whether an unsigned addition can overflow.655    pub fn bvuaddo(self: *Context, lhs: Term, rhs: Term) !Term {656        return try self.append(.{ .bvuaddo = .{ .lhs = lhs, .rhs = rhs } });657    }658659    /// Appends the claim that the two's-complement sum of `lhs` and `rhs` overflows their width and660    /// returns its term. Code asks with it whether a two's-complement addition can overflow.661    pub fn bvsaddo(self: *Context, lhs: Term, rhs: Term) !Term {662        return try self.append(.{ .bvsaddo = .{ .lhs = lhs, .rhs = rhs } });663    }664665    /// Appends the claim that the two's-complement difference `lhs` minus `rhs` overflows their666    /// width and returns its term. Code asks with it whether a two's-complement subtraction can667    /// overflow.668    pub fn bvssubo(self: *Context, lhs: Term, rhs: Term) !Term {669        return try self.append(.{ .bvssubo = .{ .lhs = lhs, .rhs = rhs } });670    }671672    /// Appends the claim that the unsigned product of `lhs` and `rhs` overflows their width and673    /// returns its term. Code asks with it whether an unsigned multiplication can overflow.674    pub fn bvumulo(self: *Context, lhs: Term, rhs: Term) !Term {675        return try self.append(.{ .bvumulo = .{ .lhs = lhs, .rhs = rhs } });676    }677678    /// Appends the claim that the two's-complement product of `lhs` and `rhs` overflows their width679    /// and returns its term. Code asks with it whether a two's-complement multiplication can680    /// overflow.681    pub fn bvsmulo(self: *Context, lhs: Term, rhs: Term) !Term {682        return try self.append(.{ .bvsmulo = .{ .lhs = lhs, .rhs = rhs } });683    }684685    /// Appends the bitwise complement of `operand` and returns its term. Code complements every bit686    /// of a bit-vector with it.687    pub fn bvnot(self: *Context, operand: Term) !Term {688        return try self.append(.{ .bvnot = operand });689    }690691    /// Appends the bitwise and of `lhs` and `rhs` and returns its term. Code masks bit-vectors with692    /// it.693    pub fn bvand(self: *Context, lhs: Term, rhs: Term) !Term {694        return try self.append(.{ .bvand = .{ .lhs = lhs, .rhs = rhs } });695    }696697    /// Appends the bitwise or of `lhs` and `rhs` and returns its term. Code sets bits of a698    /// bit-vector with it.699    pub fn bvor(self: *Context, lhs: Term, rhs: Term) !Term {700        return try self.append(.{ .bvor = .{ .lhs = lhs, .rhs = rhs } });701    }702703    /// Appends the bitwise exclusive or of `lhs` and `rhs` and returns its term. Code flips bits of704    /// a bit-vector with it.705    pub fn bvxor(self: *Context, lhs: Term, rhs: Term) !Term {706        return try self.append(.{ .bvxor = .{ .lhs = lhs, .rhs = rhs } });707    }708709    /// Appends `lhs` shifted toward its most significant bit by the value of `rhs` and returns its710    /// term. Code shifts a bit-vector left with it.711    pub fn bvshl(self: *Context, lhs: Term, rhs: Term) !Term {712        return try self.append(.{ .bvshl = .{ .lhs = lhs, .rhs = rhs } });713    }714715    /// Appends `lhs` shifted toward its least significant bit by the value of `rhs`, with zeros716    /// shifted in, and returns its term. Code shifts with it a bit-vector right with zero fill.717    pub fn bvlshr(self: *Context, lhs: Term, rhs: Term) !Term {718        return try self.append(.{ .bvlshr = .{ .lhs = lhs, .rhs = rhs } });719    }720721    /// Appends `lhs` shifted toward its least significant bit by the value of `rhs`, with copies of722    /// its sign bit shifted in, and returns its term. Code shifts a two's-complement bit-vector723    /// right with it.724    pub fn bvashr(self: *Context, lhs: Term, rhs: Term) !Term {725        return try self.append(.{ .bvashr = .{ .lhs = lhs, .rhs = rhs } });726    }727728    /// Appends the unsigned quotient of `lhs` by `rhs` and returns its term. Code divides729    /// bit-vectors as unsigned numbers with it.730    pub fn bvudiv(self: *Context, lhs: Term, rhs: Term) !Term {731        return try self.append(.{ .bvudiv = .{ .lhs = lhs, .rhs = rhs } });732    }733734    /// Appends the unsigned remainder of `lhs` by `rhs` and returns its term. Code takes the735    /// unsigned remainder of bit-vectors with it.736    pub fn bvurem(self: *Context, lhs: Term, rhs: Term) !Term {737        return try self.append(.{ .bvurem = .{ .lhs = lhs, .rhs = rhs } });738    }739740    /// Appends the two's-complement quotient of `lhs` by `rhs`, rounded toward zero, and returns741    /// its term. Code divides bit-vectors as two's-complement numbers with it.742    pub fn bvsdiv(self: *Context, lhs: Term, rhs: Term) !Term {743        return try self.append(.{ .bvsdiv = .{ .lhs = lhs, .rhs = rhs } });744    }745746    /// Appends the remainder of `lhs` by `rhs` with the sign of `lhs` and returns its term. Code747    /// takes the two's-complement remainder of bit-vectors with it.748    pub fn bvsrem(self: *Context, lhs: Term, rhs: Term) !Term {749        return try self.append(.{ .bvsrem = .{ .lhs = lhs, .rhs = rhs } });750    }751752    /// Appends the modulo of `lhs` by `rhs` with the sign of `rhs` and returns its term. Code takes753    /// the two's-complement modulo of bit-vectors with it.754    pub fn bvsmod(self: *Context, lhs: Term, rhs: Term) !Term {755        return try self.append(.{ .bvsmod = .{ .lhs = lhs, .rhs = rhs } });756    }757758    /// Appends the element of `array` at `index` and returns its term. Code reads an array at an759    /// index with it.760    pub fn arraySelect(self: *Context, array: Term, index: Term) !Term {761        return try self.append(.{ .array_select = .{ .array = array, .index = index } });762    }763764    /// Appends the array equal to `array` except that `index` holds `value`, and returns its term.765    /// Code writes an element into an array with it.766    pub fn arrayStore(self: *Context, array: Term, index: Term, value: Term) !Term {767        return try self.append(.{ .array_store = .{768            .array = array,769            .index = index,770            .value = value,771        } });772    }773774    /// Appends the bits of `lhs` above the bits of `rhs` and returns its term. Code joins two775    /// bit-vectors into a wider one with it.776    pub fn bvconcat(self: *Context, lhs: Term, rhs: Term) !Term {777        return try self.append(.{ .bvconcat = .{ .lhs = lhs, .rhs = rhs } });778    }779780    /// Appends the bits from position `high` down to position `low` of `operand`, both included,781    /// and returns its term. Code takes a range of bits from a bit-vector with it. It checks no782    /// range: `sortOf` and the encoder report `InvalidBitVectorRange` when `low` is above `high` or783    /// `high` is at or above the width.784    pub fn bvextract(self: *Context, operand: Term, high: u32, low: u32) !Term {785        return try self.append(.{ .bvextract = .{ .operand = operand, .high = high, .low = low } });786    }787788    /// Appends `operand` widened by `extra` zero bits above its most significant bit and returns789    /// its term. Code widens an unsigned bit-vector with it.790    pub fn bvzeroext(self: *Context, operand: Term, extra: u32) !Term {791        return try self.append(.{ .bvzeroext = .{ .operand = operand, .extra = extra } });792    }793794    /// Appends `operand` widened by `extra` copies of its sign bit and returns its term. Code795    /// widens a two's-complement bit-vector with it.796    pub fn bvsignext(self: *Context, operand: Term, extra: u32) !Term {797        return try self.append(.{ .bvsignext = .{ .operand = operand, .extra = extra } });798    }799800    /// Appends `operand` rotated toward its most significant bit by `amount` positions and returns801    /// its term. Code rotates a bit-vector left by a fixed amount with it.802    pub fn bvrotl(self: *Context, operand: Term, amount: u32) !Term {803        return try self.append(.{ .bvrotl = .{ .operand = operand, .amount = amount } });804    }805806    /// Appends `operand` rotated toward its least significant bit by `amount` positions and returns807    /// its term. Code rotates a bit-vector right by a fixed amount with it.808    pub fn bvrotr(self: *Context, operand: Term, amount: u32) !Term {809        return try self.append(.{ .bvrotr = .{ .operand = operand, .amount = amount } });810    }811812    /// Appends the sum of `lhs` and `rhs`, modulo 2 to the power of their width, and returns its813    /// term. Code adds bit-vectors with it.814    pub fn bvadd(self: *Context, lhs: Term, rhs: Term) !Term {815        return try self.append(.{ .bvadd = .{ .lhs = lhs, .rhs = rhs } });816    }817818    /// Appends `lhs` minus `rhs`, modulo 2 to the power of their width, and returns its term. Code819    /// subtracts bit-vectors with it.820    pub fn bvsub(self: *Context, lhs: Term, rhs: Term) !Term {821        return try self.append(.{ .bvsub = .{ .lhs = lhs, .rhs = rhs } });822    }823824    /// Appends the product of `lhs` and `rhs`, modulo 2 to the power of their width, and returns825    /// its term. Code multiplies bit-vectors with it.826    pub fn bvmul(self: *Context, lhs: Term, rhs: Term) !Term {827        return try self.append(.{ .bvmul = .{ .lhs = lhs, .rhs = rhs } });828    }829830    fn sortOfApply(self: *const Context, item: ApplyExpr) !Sort {831        if (item.function >= self.functions.items.len) return error.UnknownFunction;832        const decl = self.functions.items[item.function];833        if (decl.params.len != item.args.len) return error.FunctionArityMismatch;834        for (item.args, decl.params) |arg, expected| {835            if (!(try self.sortOf(arg)).eql(expected)) return error.FunctionArgumentSortMismatch;836        }837        return decl.result;838    }839840    fn expectBoolResult(self: *const Context, operand: Term) !Sort {841        if (!(try self.sortOf(operand)).eql(.bool)) return error.SortMismatch;842        return .bool;843    }844845    fn expectBoolPair(self: *const Context, lhs: Term, rhs: Term) !Sort {846        if (!(try self.sortOf(lhs)).eql(.bool) or !(try self.sortOf(rhs)).eql(.bool)) {847            return error.SortMismatch;848        }849        return .bool;850    }851852    fn expectBoolList(self: *const Context, operands: []const Term) !Sort {853        for (operands) |operand| {854            if (!(try self.sortOf(operand)).eql(.bool)) return error.SortMismatch;855        }856        return .bool;857    }858859    fn expectIntPair(self: *const Context, lhs: Term, rhs: Term) !Sort {860        if (!(try self.sortOf(lhs)).eql(.int) or !(try self.sortOf(rhs)).eql(.int)) {861            return error.SortMismatch;862        }863        return .bool;864    }865866    fn expectIntList(self: *const Context, operands: []const Term) !Sort {867        for (operands) |operand| {868            if (!(try self.sortOf(operand)).eql(.int)) return error.SortMismatch;869        }870        return .int;871    }872873    fn expectSameSortPair(self: *const Context, lhs: Term, rhs: Term) !Sort {874        if (!(try self.sortOf(lhs)).eql(try self.sortOf(rhs))) return error.SortMismatch;875        return .bool;876    }877878    fn expectSameSortList(self: *const Context, operands: []const Term) !Sort {879        if (operands.len == 0) return .bool;880        const expected = try self.sortOf(operands[0]);881        for (operands[1..]) |operand| {882            if (!(try self.sortOf(operand)).eql(expected)) return error.SortMismatch;883        }884        return .bool;885    }886887    fn expectBitVecPair(self: *const Context, lhs: Term, rhs: Term) !Sort {888        _ = try self.expectBitVecPairResult(lhs, rhs);889        return .bool;890    }891892    fn expectBitVecResult(self: *const Context, operand: Term) !Sort {893        return switch (try self.sortOf(operand)) {894            .bitvec => |width| .{ .bitvec = width },895            else => error.SortMismatch,896        };897    }898899    fn expectBitVecPairResult(self: *const Context, lhs: Term, rhs: Term) !Sort {900        return switch (try self.sortOf(lhs)) {901            .bitvec => |lhs_width| switch (try self.sortOf(rhs)) {902                .bitvec => |rhs_width| {903                    if (lhs_width != rhs_width) return error.SortMismatch;904                    return .{ .bitvec = lhs_width };905                },906                else => error.SortMismatch,907            },908            else => error.SortMismatch,909        };910    }911912    fn sortOfArraySelect(self: *const Context, array: Term, index: Term) !Sort {913        const array_sort = try self.sortOf(array);914        const index_sort = try self.sortOf(index);915        return switch (array_sort) {916            .array => |shape| switch (index_sort) {917                .bitvec => |width| {918                    if (width != shape.index_width) return error.SortMismatch;919                    return .{ .bitvec = shape.element_width };920                },921                else => error.SortMismatch,922            },923            else => error.SortMismatch,924        };925    }926927    fn sortOfArrayStore(self: *const Context, array: Term, index: Term, value: Term) !Sort {928        const array_sort = try self.sortOf(array);929        const index_sort = try self.sortOf(index);930        const value_sort = try self.sortOf(value);931        return switch (array_sort) {932            .array => |shape| switch (index_sort) {933                .bitvec => |index_width| switch (value_sort) {934                    .bitvec => |element_width| {935                        if (index_width != shape.index_width or936                            element_width != shape.element_width)937                        {938                            return error.SortMismatch;939                        }940                        return array_sort;941                    },942                    else => error.SortMismatch,943                },944                else => error.SortMismatch,945            },946            else => error.SortMismatch,947        };948    }949950    fn sortOfConcat(self: *const Context, lhs: Term, rhs: Term) !Sort {951        return switch (try self.sortOf(lhs)) {952            .bitvec => |lhs_width| switch (try self.sortOf(rhs)) {953                .bitvec => |rhs_width| .{ .bitvec = try std.math.add(u32, lhs_width, rhs_width) },954                else => error.SortMismatch,955            },956            else => error.SortMismatch,957        };958    }959960    fn sortOfExtract(self: *const Context, operand: Term, high: u32, low: u32) !Sort {961        return switch (try self.sortOf(operand)) {962            .bitvec => |width| {963                if (low > high or high >= width) return error.InvalidBitVectorRange;964                return .{ .bitvec = high - low + 1 };965            },966            else => error.SortMismatch,967        };968    }969970    fn sortOfExtend(self: *const Context, operand: Term, extra: u32) !Sort {971        return switch (try self.sortOf(operand)) {972            .bitvec => |width| .{ .bitvec = try std.math.add(u32, width, extra) },973            else => error.SortMismatch,974        };975    }976977    fn append(self: *Context, expr: Expr) !Term {978        const id: Term = @intCast(self.nodes.items.len);979        try self.nodes.append(self.allocator, expr);980        return id;981    }982983    fn appendPair(self: *Context, comptime tag: std.meta.Tag(Expr), lhs: Term, rhs: Term) !Term {984        return try self.append(@unionInit(Expr, @tagName(tag), .{ .lhs = lhs, .rhs = rhs }));985    }986987    fn appendList(self: *Context, comptime tag: std.meta.Tag(Expr), operands: []const Term) !Term {988        const owned = try self.allocator.dupe(Term, operands);989        errdefer self.allocator.free(owned);990        return switch (tag) {991            .and_ => try self.append(.{ .and_ = owned }),992            .or_ => try self.append(.{ .or_ = owned }),993            .distinct => try self.append(.{ .distinct = owned }),994            .add => try self.append(.{ .add = owned }),995            .mul => try self.append(.{ .mul = owned }),996            else => unreachable,997        };998    }999};10001001fn sortListsEqual(lhs: []const Sort, rhs: []const Sort) bool {1002    if (lhs.len != rhs.len) return false;1003    for (lhs, rhs) |left, right| {1004        if (!left.eql(right)) return false;1005    }1006    return true;1007}10081009/// A logic name and the list of terms asserted over one `Context`. `smtlib.parseScript` returns1010/// one, `smtlib.writeScript` prints one, and code that solves a script asserts each of its terms1011/// with the encoder. It borrows the `Context` and allocates its list with the `Context`'s1012/// allocator.1013pub const Script = struct {1014    /// The `Context` whose terms the script asserts.1015    ctx: *Context,1016    /// The logic name, such as `QF_BV`, that `set-logic` gives. The script borrows it: a script1017    /// from `smtlib.parseScript` points into the parsed text, which has to outlive the script.1018    logic: []const u8,1019    /// The asserted terms in the order they were asserted.1020    assertions: std.ArrayList(Term) = .empty,10211022    /// Returns a script over `ctx` with logic `logic` and no assertions. Code makes an empty script1023    /// before asserting terms, as the SMT-LIB writer's tests do. It copies neither and allocates1024    /// nothing.1025    pub fn init(ctx: *Context, logic: []const u8) Script {1026        return .{ .ctx = ctx, .logic = logic };1027    }10281029    /// Frees the list of assertions and leaves the terms to the `Context`. The owner calls it1030    /// before freeing the `Context`.1031    pub fn deinit(self: *Script) void {1032        self.assertions.deinit(self.ctx.allocator);1033        self.* = undefined;1034    }10351036    /// Appends `assertion` to the list. Code adds one assertion to a script with it. It checks1037    /// nothing, including whether the term is Boolean.1038    pub fn assertTerm(self: *Script, assertion: Term) !void {1039        try self.assertions.append(self.ctx.allocator, assertion);1040    }1041};10421043test "term context stores structured arithmetic expression" {1044    var ctx = Context.init(std.testing.allocator);1045    defer ctx.deinit();1046    const x = try ctx.symbol("x", .int);1047    const one = try ctx.intValue(1);1048    const sum = try ctx.add(&.{ x, one });1049    const zero = try ctx.intValue(0);1050    _ = try ctx.gt(sum, zero);1051    try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);1052}10531054test "term context stores function applications" {1055    var ctx = Context.init(std.testing.allocator);1056    defer ctx.deinit();1057    const bv4 = Sort{ .bitvec = 4 };1058    const x = try ctx.symbol("x", bv4);1059    const y = try ctx.symbol("y", bv4);1060    const flag = try ctx.symbol("flag", .bool);1061    const f = try ctx.function("f", &.{bv4}, bv4);1062    const fx = try ctx.apply(f, &.{x});1063    _ = try ctx.apply(f, &.{y});1064    try std.testing.expectEqual(@as(usize, 1), ctx.functions.items.len);1065    try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);1066    try std.testing.expect((try ctx.sortOf(fx)).eql(bv4));1067    try std.testing.expectEqual(f, try ctx.function("f", &.{bv4}, bv4));1068    try std.testing.expectError(error.DuplicateFunction, ctx.function("f", &.{bv4}, .bool));1069    try std.testing.expectError(error.FunctionArgumentSortMismatch, ctx.apply(f, &.{flag}));1070}10711072test "term context infers composite sorts" {1073    var ctx = Context.init(std.testing.allocator);1074    defer ctx.deinit();1075    const bv4 = Sort{ .bitvec = 4 };1076    const high = try ctx.symbol("high", bv4);1077    const low = try ctx.symbol("low", bv4);1078    const word = try ctx.bvconcat(high, low);1079    const upper = try ctx.bvextract(word, 7, 4);1080    const lower = try ctx.bvextract(word, 3, 0);1081    const memory = try ctx.symbol("memory", .{ .array = .{1082        .index_width = 2,1083        .element_width = 4,1084    } });1085    const index = try ctx.symbol("index", .{ .bitvec = 2 });1086    const read = try ctx.arraySelect(memory, index);1087    try std.testing.expect((try ctx.sortOf(word)).eql(.{ .bitvec = 8 }));1088    try std.testing.expect((try ctx.sortOf(upper)).eql(bv4));1089    try std.testing.expect((try ctx.sortOf(lower)).eql(bv4));1090    try std.testing.expect((try ctx.sortOf(try ctx.eq(upper, lower))).eql(.bool));1091    try std.testing.expect((try ctx.sortOf(read)).eql(bv4));1092}10931094test "term context stores bit-vector overflow predicates" {1095    var ctx = Context.init(std.testing.allocator);1096    defer ctx.deinit();1097    const x = try ctx.symbol("x", .{ .bitvec = 8 });1098    const y = try ctx.symbol("y", .{ .bitvec = 8 });1099    _ = try ctx.bvuaddo(x, y);1100    _ = try ctx.bvsaddo(x, y);1101    _ = try ctx.bvssubo(x, y);1102    _ = try ctx.bvumulo(x, y);1103    _ = try ctx.bvsmulo(x, y);1104    try std.testing.expectEqual(@as(usize, 7), ctx.nodes.items.len);1105}11061107test "term context stores signed bit-vector comparisons" {1108    var ctx = Context.init(std.testing.allocator);1109    defer ctx.deinit();1110    const x = try ctx.symbol("x", .{ .bitvec = 8 });1111    const y = try ctx.symbol("y", .{ .bitvec = 8 });1112    const difference = try ctx.bvsub(x, y);1113    _ = try ctx.bvslt(difference, y);1114    _ = try ctx.bvsle(x, y);1115    try std.testing.expect((try ctx.sortOf(difference)).eql(.{ .bitvec = 8 }));1116    try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);1117}11181119test "term context stores bit-vector bitwise operators" {1120    var ctx = Context.init(std.testing.allocator);1121    defer ctx.deinit();1122    const x = try ctx.symbol("x", .{ .bitvec = 8 });1123    const y = try ctx.symbol("y", .{ .bitvec = 8 });1124    _ = try ctx.bvnot(x);1125    _ = try ctx.bvand(x, y);1126    _ = try ctx.bvor(x, y);1127    _ = try ctx.bvxor(x, y);1128    try std.testing.expectEqual(@as(usize, 6), ctx.nodes.items.len);1129}11301131test "term context stores bit-vector shift operators" {1132    var ctx = Context.init(std.testing.allocator);1133    defer ctx.deinit();1134    const x = try ctx.symbol("x", .{ .bitvec = 8 });1135    const amount = try ctx.symbol("amount", .{ .bitvec = 8 });1136    _ = try ctx.bvshl(x, amount);1137    _ = try ctx.bvlshr(x, amount);1138    _ = try ctx.bvashr(x, amount);1139    _ = try ctx.bvudiv(x, amount);1140    _ = try ctx.bvurem(x, amount);1141    _ = try ctx.bvsdiv(x, amount);1142    _ = try ctx.bvsrem(x, amount);1143    _ = try ctx.bvsmod(x, amount);1144    try std.testing.expectEqual(@as(usize, 10), ctx.nodes.items.len);1145}11461147test "term context stores bit-vector width-changing operators" {1148    var ctx = Context.init(std.testing.allocator);1149    defer ctx.deinit();1150    const high = try ctx.symbol("high", .{ .bitvec = 4 });1151    const low = try ctx.symbol("low", .{ .bitvec = 4 });1152    const word = try ctx.bvconcat(high, low);1153    _ = try ctx.bvextract(word, 7, 4);1154    _ = try ctx.bvzeroext(high, 4);1155    _ = try ctx.bvsignext(low, 4);1156    try std.testing.expectEqual(@as(usize, 6), ctx.nodes.items.len);1157}11581159test "term context stores bit-vector rotate operators" {1160    var ctx = Context.init(std.testing.allocator);1161    defer ctx.deinit();1162    const x = try ctx.symbol("x", .{ .bitvec = 8 });1163    _ = try ctx.bvrotl(x, 3);1164    _ = try ctx.bvrotr(x, 5);1165    try std.testing.expectEqual(@as(usize, 3), ctx.nodes.items.len);1166}11671168test "term context stores finite bit-vector array operators" {1169    var ctx = Context.init(std.testing.allocator);1170    defer ctx.deinit();1171    const memory = try ctx.symbol("memory", .{ .array = .{1172        .index_width = 2,1173        .element_width = 4,1174    } });1175    const index = try ctx.symbol("index", .{ .bitvec = 2 });1176    const value = try ctx.symbol("value", .{ .bitvec = 4 });1177    const written = try ctx.arrayStore(memory, index, value);1178    _ = try ctx.arraySelect(written, index);1179    try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);1180}