tiny.smt.Expr

1/// One term: a tag naming its operator and a payload holding its operands. Code that walks a2/// formula switches on it, as the encoder and the SMT-LIB writer do for every term. The `Context`3/// stores one per term, and a term's index is its position in that table. A tag named after an4/// SMT-LIB operator reads and writes as that operator, and each tag whose name differs gives its5/// SMT-LIB spelling. The bit-vector encoder refuses the integer tags (`int`, `add`, `mul`, `le`,6/// `lt`, `ge`, `gt`) and `distinct` with `UnsupportedTerm`.7pub const Expr = union(enum) {8    /// A named constant, with its name and sort as the payload. The encoder gives it fresh9    /// variables, one per bit.10    symbol: SymbolExpr,11    /// A function application, with the function and its arguments as the payload. Its sort is the12    /// function's result sort.13    apply: ApplyExpr,14    /// A Boolean constant. SMT-LIB writes it `true` or `false`.15    bool: bool,16    /// An integer constant, a signed 128-bit value. The bit-vector encoder refuses it.17    int: i128,18    /// A bit-vector constant, with its value and width as the payload. SMT-LIB writes it19    /// `(_ bvV W)`.20    bitvec: BitVecExpr,21    /// The negation of one Boolean operand.22    not: Term,23    /// The conjunction of any number of Boolean operands. With no operands it is true. SMT-LIB24    /// writes it `and`.25    and_: []const Term,26    /// The disjunction of any number of Boolean operands. With no operands it is false. SMT-LIB27    /// writes it `or`.28    or_: []const Term,29    /// `lhs` implies `rhs`, both Boolean. SMT-LIB writes it `=>`.30    implies: BinaryOperands,31    /// `lhs` equals `rhs`, a Boolean term over two operands of one sort. Two arrays are equal when32    /// every cell is equal. SMT-LIB writes it `=`.33    eq: BinaryOperands,34    /// True when all operands differ from one another, over operands of one sort. The bit-vector35    /// encoder refuses it.36    distinct: []const Term,37    /// The integer sum of any number of integer operands. SMT-LIB writes it `+`. The bit-vector38    /// encoder refuses it.39    add: []const Term,40    /// The integer product of any number of integer operands. SMT-LIB writes it `*`. The bit-vector41    /// encoder refuses it.42    mul: []const Term,43    /// `lhs` is at most `rhs`, as integers. SMT-LIB writes it `<=`. The bit-vector encoder refuses44    /// it.45    le: BinaryOperands,46    /// `lhs` is less than `rhs`, as integers. SMT-LIB writes it `<`. The bit-vector encoder refuses47    /// it.48    lt: BinaryOperands,49    /// `lhs` is at least `rhs`, as integers. SMT-LIB writes it `>=`. The bit-vector encoder refuses50    /// it.51    ge: BinaryOperands,52    /// `lhs` is greater than `rhs`, as integers. SMT-LIB writes it `>`. The bit-vector encoder53    /// refuses it.54    gt: BinaryOperands,55    /// `lhs` is at most `rhs`, as unsigned bit-vectors of one width.56    bvule: BinaryOperands,57    /// `lhs` is less than `rhs`, as unsigned bit-vectors of one width.58    bvult: BinaryOperands,59    /// `lhs` is at most `rhs`, as two's-complement bit-vectors of one width.60    bvsle: BinaryOperands,61    /// `lhs` is less than `rhs`, as two's-complement bit-vectors of one width.62    bvslt: BinaryOperands,63    /// True when the unsigned sum of `lhs` and `rhs` does not fit their width.64    bvuaddo: BinaryOperands,65    /// True when the two's-complement sum of `lhs` and `rhs` does not fit their width: both have66    /// one sign and the sum has the other.67    bvsaddo: BinaryOperands,68    /// True when the two's-complement difference `lhs` minus `rhs` does not fit their width.69    bvssubo: BinaryOperands,70    /// True when the unsigned product of `lhs` and `rhs` does not fit their width.71    bvumulo: BinaryOperands,72    /// True when the two's-complement product of `lhs` and `rhs` does not fit their width.73    bvsmulo: BinaryOperands,74    /// The bitwise complement of one bit-vector operand, of the same width.75    bvnot: Term,76    /// The bitwise and of two bit-vectors of one width.77    bvand: BinaryOperands,78    /// The bitwise or of two bit-vectors of one width.79    bvor: BinaryOperands,80    /// The bitwise exclusive or of two bit-vectors of one width.81    bvxor: BinaryOperands,82    /// `lhs` shifted toward its most significant bit by the value of `rhs`, with zeros shifted in,83    /// over two bit-vectors of one width. A shift amount at or above the width gives zero.84    bvshl: BinaryOperands,85    /// `lhs` shifted toward its least significant bit by the value of `rhs`, with zeros shifted in.86    /// A shift amount at or above the width gives zero.87    bvlshr: BinaryOperands,88    /// `lhs` shifted toward its least significant bit by the value of `rhs`, with copies of its89    /// sign bit shifted in. A shift amount at or above the width fills every bit with the sign bit.90    bvashr: BinaryOperands,91    /// The unsigned quotient of `lhs` by `rhs`, rounded down. Division by zero gives all ones.92    bvudiv: BinaryOperands,93    /// The unsigned remainder of `lhs` by `rhs`. The remainder by zero is `lhs`.94    bvurem: BinaryOperands,95    /// The two's-complement quotient of `lhs` by `rhs`, rounded toward zero. Division by zero gives96    /// 1 for a negative `lhs` and all ones otherwise.97    bvsdiv: BinaryOperands,98    /// The two's-complement remainder of `lhs` by `rhs`, with the sign of `lhs`. The remainder by99    /// zero is `lhs`.100    bvsrem: BinaryOperands,101    /// The two's-complement modulo of `lhs` by `rhs`, with the sign of `rhs`. The modulo by zero is102    /// `lhs`.103    bvsmod: BinaryOperands,104    /// The element of an array at an index, a bit-vector of the element width. The index has the105    /// array's index width. SMT-LIB writes it `select`.106    array_select: ArraySelectExpr,107    /// An array equal to its operand everywhere except at one index, which holds the new element.108    /// The term's sort is the operand's array sort. SMT-LIB writes it `store`.109    array_store: ArrayStoreExpr,110    /// The bits of `lhs` above the bits of `rhs`, one bit-vector as wide as the two together.111    /// SMT-LIB writes it `concat`.112    bvconcat: BinaryOperands,113    /// The bits from position `high` down to position `low` of one bit-vector, both included, so114    /// the result has `high - low + 1` bits. SMT-LIB writes it `((_ extract high low) x)`.115    bvextract: BitVecExtractExpr,116    /// A bit-vector widened by `extra` zero bits above its most significant bit. SMT-LIB writes it117    /// `((_ zero_extend extra) x)`.118    bvzeroext: BitVecExtendExpr,119    /// A bit-vector widened by `extra` copies of its sign bit. SMT-LIB writes it120    /// `((_ sign_extend extra) x)`.121    bvsignext: BitVecExtendExpr,122    /// A bit-vector rotated toward its most significant bit by a fixed number of positions, with123    /// the top bits wrapping to the bottom. SMT-LIB writes it `((_ rotate_left amount) x)`.124    bvrotl: BitVecRotateExpr,125    /// A bit-vector rotated toward its least significant bit by a fixed number of positions, with126    /// the bottom bits wrapping to the top. SMT-LIB writes it `((_ rotate_right amount) x)`.127    bvrotr: BitVecRotateExpr,128    /// The sum of two bit-vectors of one width, modulo 2 to the power of the width.129    bvadd: BinaryOperands,130    /// The difference `lhs` minus `rhs` of two bit-vectors of one width, modulo 2 to the power of131    /// the width.132    bvsub: BinaryOperands,133    /// The product of two bit-vectors of one width, modulo 2 to the power of the width.134    bvmul: BinaryOperands,135};

1pub const Expr = term.Expr;