### Core SMT Operations Enum

Source: https://github.com/awslabs/rust-smt-ir/blob/main/aws-smt-ir/README.md

A simplified Rust enum representing SMT-LIB Core operations. This structure allows for type-level encoding of function arity and properties.

```rust
enum CoreOp<Term> {
	Not(Term),
	And(Vec<Term>),
	Ite(Term, Term, Term),
}
```

--------------------------------

### SMT Term Representation

Source: https://github.com/awslabs/rust-smt-ir/blob/main/aws-smt-ir/README.md

Rust enum defining the structure of an SMT term within a specific logic `L`. It covers constants, variables, core operations, other operations, uninterpreted functions, let bindings, match expressions, and quantifiers.

```rust
enum Term<T: Logic> {
    /// A constant value.
    Constant(IConst),

    /// A variable representing a value.
    Variable(IVar<T::Var>),

    /// An operation in SMT-LIB's Core theory.
    CoreOp(ICoreOp<T>),

    /// A non-Core operation.
    OtherOp(IOp<T>),

    /// An uninterpreted function.
    UF(IUF<T>),

    /// Simultaneous let-binding e.g. `(let ((x true) (y false)) (and x y))`
    Let(ILet<T>),

    /// SMT-LIB `match` expression -- not yet supported
    Match(IMatch<T>),

    /// Quantified term.
    Quantifier(IQuantifier<T>),
}
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.