AWS SMT IR

https://docs.rs/aws-smt-ir/0.3.0
Admin
AWS SMT IR is an intermediate representation for SMT-LIB formulas.
Tokens:440,916
Snippets:3,600
Trust Score:9.1
Update:4 months ago
Show doc for...
Tokens:
Raw
### Get Info Command

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/parser.rs.html

Parses and handles the get-info command, which retrieves information about the solver.

```Rust
command ::= LeftParen GetInfo keyword(x) RightParen { extra.0.visit_get_info(x)? }
```

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

### Get Proof Command

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/parser.rs.html

Parses and handles the get-proof command, which retrieves the proof of unsatisfiability.

```Rust
command ::= LeftParen GetProof RightParen { extra.0.visit_get_proof()? }
```

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

### Vector Capacity Example

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Demonstrates how to check the capacity of a vector. A vector with zero-sized elements has a capacity of usize::MAX.

```rust
let mut vec: Vec<i32> = Vec::with_capacity(10);
vec.push(42);
assert!(vec.capacity() >= 10);
```

```rust
#[derive(Clone)]
struct ZeroSized;

fn main() {
    assert_eq!(std::mem::size_of::<ZeroSized>(), 0);
    let v = vec![ZeroSized; 0];
    assert_eq!(v.capacity(), usize::MAX);
}
```

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

### Get Proof Rewriter

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/rewriter.rs.html

Rewrites a `get-proof` command by visiting it and processing the resulting command.

```rust
fn visit_get_proof(&mut self) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> {
            let value = self.visitor().visit_get_proof()?;
            self.process_command(value)
        }
```

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

### Visit Get Unsat Core

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/renaming/struct.SymbolNormalizer.html

Handles the 'get-unsat-core' command in SMT-LIB 2.

```rust
fn visit_get_unsat_core( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>
```

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

### Get Info Rewriter

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/rewriter.rs.html

Rewrites a `get-info` command by visiting it and processing the resulting command.

```rust
fn visit_get_info(
            &mut self,
            flag: <Self::V as Smt2Visitor>::Keyword,
        ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> {
            let value = self.visitor().visit_get_info(flag)?;
            self.process_command(value)
        }
```

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

### Getting Mutable Reference to First Element

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Shows how to get a mutable reference to the first element of a slice using `first_mut()`, returning `None` if the slice is empty. The example demonstrates modifying the first element.

```rust
let x = &mut [0, 1, 2];

if let Some(first) = x.first_mut() {
    *first = 5;
}
assert_eq!(x, &[5, 1, 2]);

let y: &mut [i32] = &mut [];
assert_eq!(None, y.first_mut());
```

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

### SMT-LIB Command Structure Example

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/rewriter.rs.html

Illustrates the structure of an SMT-LIB command, specifically an assertion involving a variable 'x' and constants '2' and '3'. This is used for testing the rewriter.

```rust
    let command2 = Command::Assert
        {
            term: Box::new(Term::Application {
                qual_identifier: QualIdentifier::Simple {
                    identifier: Identifier::Simple {
                        symbol: Symbol("=__".into()),
                    },
                },
                arguments: vec![Term::QualIdentifier(QualIdentifier::Simple {
                    identifier: Identifier::Simple {
                        symbol: Symbol("x__".into()),
                    },
                }), Term::Constant(Constant::Numeral(num::BigUint::from(3u32)))]
            })
        };

    let command3 = Command::Assert
        {
            term: Box::new(Term::Application {
                qual_identifier: QualIdentifier::Simple {
                    identifier: Identifier::Simple {
                        symbol: Symbol("=__".into()),
                    },
                },
                arguments: vec![Term::QualIdentifier(QualIdentifier::Simple {
                    identifier: Identifier::Simple {
                        symbol: Symbol("x__".into()),
                    },
                }), Term::Constant(Constant::Numeral(num::BigUint::from(3u32)))]
            })
        };
```

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

### Rust Slice Subslice Range Example

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Demonstrates using `subslice_range` to get the range of elements between delimiters in a slice. Requires the `substr_range` feature.

```rust
#![feature(substr_range)]
use core::range::Range;

let nums = &[0, 5, 10, 0, 0, 5];

let mut iter = nums
    .split(|t| *t == 0)
    .map(|n| nums.subslice_range(n).unwrap());

assert_eq!(iter.next(), Some(Range { start: 0, end: 0 }));
assert_eq!(iter.next(), Some(Range { start: 1, end: 3 }));
assert_eq!(iter.next(), Some(Range { start: 4, end: 4 }));
assert_eq!(iter.next(), Some(Range { start: 5, end: 6 }));

```

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

### Example: Adding Asserts to a Script

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/script.rs.html

Demonstrates how to parse an SMT script, add new assertions, and verify the script's content. Requires `aws_smt_ir` and `Term` types.

```rust
# fn main() -> Result<(), Box<dyn std::error::Error>> {
use aws_smt_ir::{Script, Term, logic::ALL};
let smt = "(assert true) (check-sat)".as_bytes();
let mut script: Script<Term> = Script::parse(smt)?;
script.add_asserts([Term::from(false)]);
let expected = Script::parse("(assert true) (assert false) (check-sat)".as_bytes())?;
assert_eq!(script, expected);
# Ok(())
# }
```

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

### Get Element Offset by Unaligned Reference

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Demonstrates that element_offset returns None for references not aligned to the start of an element. This method uses pointer arithmetic and does not compare elements.

```rust
let arr: &[[u32; 2]] = &[[0, 1], [2, 3]];
let flat_arr: &[u32] = arr.as_flattened();

let ok_elm: &[u32; 2] = flat_arr[0..2].try_into().unwrap();
let weird_elm: &[u32; 2] = flat_arr[1..3].try_into().unwrap();

assert_eq!(ok_elm, &[0, 1]);
assert_eq!(weird_elm, &[1, 2]);

assert_eq!(arr.element_offset(ok_elm), Some(0)); // Points to element 0
assert_eq!(arr.element_offset(weird_elm), None); // Points between element 0 and 1
```

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

### CloneToUninit

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/enum.QualIdentifier.html

This is a nightly-only experimental API for performing copy-assignment to uninitialized memory.

```APIDOC
## impl<T> CloneToUninit for T

### Description
This is a nightly-only experimental API for performing copy-assignment to uninitialized memory.

### Source
Source§

#### unsafe fn clone_to_uninit(&self, dest: *mut u8)
Performs copy-assignment from `self` to `dest`.
```

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

### Reverse Chunking of Slices

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `rchunks` to get an iterator over slices of `chunk_size` elements, starting from the end of the slice. The last chunk may be smaller if `chunk_size` does not divide the slice length.

```rust
let slice = [0, 1, 2, 3, 4];
let mut iter = slice.rchunks(2);
assert_eq!(iter.next().unwrap(), &[3, 4]);
assert_eq!(iter.next().unwrap(), &[1, 2]);
assert_eq!(iter.next().unwrap(), &[0]);
```

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

### Initialize and Check Length of Vec

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/type.Hexadecimal.html

Demonstrates basic Vec initialization and checking its length.

```rust
let a = vec![1, 2, 3];
assert_eq!(a.len(), 3);
```

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

### visit_get_proof

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/rewriter/trait.Rewriter.html

Visits a get-proof command, which requests the proof from the solver. Returns a Command.

```APIDOC
## fn visit_get_proof

### Description
Visits a get-proof command, which requests the proof from the solver. Returns a Command.

### Signature
`fn visit_get_proof( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>`
```

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

### Get Element Offset by Reference

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Finds the index of a given element reference within a slice. This method uses pointer arithmetic and does not compare elements. It returns None if the element reference does not point to the start of an element within the slice.

```rust
let nums: &[u32] = &[1, 7, 1, 1];
let num = &nums[2];

assert_eq!(num, &1);
assert_eq!(nums.element_offset(num), Some(2));
```

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

### Rust Vec Fill Example

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Fills a vector with cloned elements. Ensure the vector is initialized to the desired size.

```rust
let mut buf = vec![0; 10];
buf.fill(1);
assert_eq!(buf, vec![1; 10]);
```

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

### Strip prefix from a slice

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `strip_prefix` to get a subslice with a specified prefix removed. Returns `None` if the slice does not start with the prefix. An empty prefix returns the original slice, and a prefix equal to the slice returns an empty slice.

```rust
let v = &[10, 40, 30];
assert_eq!(v.strip_prefix(&[10]), Some(&[40, 30][..]));
assert_eq!(v.strip_prefix(&[10, 40]), Some(&[30][..]));
assert_eq!(v.strip_prefix(&[10, 40, 30]), Some(&[][..]));
assert_eq!(v.strip_prefix(&[50]), None);
assert_eq!(v.strip_prefix(&[10, 50]), None);
```

```rust
let prefix : &str = "he";
assert_eq!(b"hello".strip_prefix(prefix.as_bytes()),
           Some(b"llo".as_ref()));
```

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

### visit_get_info

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/rewriter/trait.Rewriter.html

Visits a get-info command, which retrieves information about the solver. It takes a keyword specifying the information to retrieve and returns a Command.

```APIDOC
## fn visit_get_info

### Description
Visits a get-info command, which retrieves information about the solver. It takes a keyword specifying the information to retrieve and returns a Command.

### Signature
`fn visit_get_info( &mut self, flag: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>`
```

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

### SMT-LIBv2 Command Parsing Logic

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/concrete.rs.html

This code block demonstrates the visitor pattern implementation for parsing various SMT-LIBv2 commands. It handles commands such as define-fun, define-sort, set-info, set-option, and others by dispatching to appropriate visitor methods.

```rust
impl<'a, V: Smt2Visitor<'a>> Smt2Visitor<'a> for V {
    type Error = Error;
    type Constant = Constant;
    type QualIdentifier = QualIdentifier;
    type Keyword = Keyword;
    type Sort = Sort;
    type SExpr = SExpr;
    type Symbol = Symbol;
    type Term = Term;
    type Command = Command;

    fn visit_command(&mut self, command: Command) -> Result<Self::Command, Self::Error> {
        match command {
            Command::Assert { term } => {
                let term = term.accept(self)?;
                self.visit_assert(term)
            }
            Command::CheckSat => self.visit_check_sat(),
            Command::DeclareConst { symbol } => {
                let symbol = self.visit_fresh_symbol(symbol.0, SymbolKind::Constant)?;
                self.visit_declare_const(symbol)
            }
            Command::DeclareFun { symbol, parameters, return_sort } => {
                let symbol = self.visit_fresh_symbol(symbol.0, SymbolKind::Function)?;
                let ps = parameters
                    .into_iter()
                    .map(|(s, sort)| {
                        let s = self.visit_fresh_symbol(s.0, SymbolKind::TypeVar)?;
                        let sort = sort.accept(self)?;
                        Ok((s, sort))
                    })
                    .collect::<Result<Vec<_>, Error>>()?;
                let return_sort = return_sort.accept(self)?;
                self.visit_declare_fun(symbol, ps, return_sort)
            }
            Command::DeclareSort { symbol, parameters } => {
                let symbol = self.visit_fresh_symbol(symbol.0, SymbolKind::Sort)?;
                let ps = parameters
                    .into_iter()
                    .map(|s| self.visit_fresh_symbol(s.0, SymbolKind::TypeVar))
                    .collect::<Result<Vec<_>, Error>>()?;
                self.visit_declare_sort(symbol, ps)
            }
            Command::DefineFun { symbol, parameters, return_sort, body } => {
                let symbol = self.visit_fresh_symbol(symbol.0, SymbolKind::Function)?;
                let ps = parameters
                    .into_iter()
                    .map(|(s, sort)| {
                        let s = self.visit_fresh_symbol(s.0, SymbolKind::TypeVar)?;
                        let sort = sort.accept(self)?;
                        Ok((s, sort))
                    })
                    .collect::<Result<Vec<_>, Error>>()?;
                let return_sort = return_sort.accept(self)?;
                let body = body.accept(self)?;
                self.visit_define_fun(symbol, ps, return_sort, body)
            }
            Command::DefineFunRec { funs } => {
                let funs = funs
                    .into_iter()
                    .map(|(symbol, parameters, return_sort, body)| {
                        let symbol = self.visit_fresh_symbol(symbol.0, SymbolKind::Function)?;
                        let ps = parameters
                            .into_iter()
                            .map(|(s, sort)| {
                                let s = self.visit_fresh_symbol(s.0, SymbolKind::TypeVar)?;
                                let sort = sort.accept(self)?;
                                Ok((s, sort))
                            })
                            .collect::<Result<Vec<_>, Error>>()?;
                        let return_sort = return_sort.accept(self)?;
                        let body = body.accept(self)?;
                        Ok((symbol, ps, return_sort, body))
                    })
                    .collect::<Result<_, E>>()?;
                visitor.visit_define_funs_rec(funs)
            }
            DefineSort {
                symbol,
                parameters,
                sort,
            } => {
                let symbol = visitor.visit_fresh_symbol(symbol.0, SymbolKind::Sort)?;
                let ps = parameters
                    .into_iter()
                    .map(|s| visitor.visit_fresh_symbol(s.0, SymbolKind::TypeVar))
                    .collect::<Result<Vec<_>, E>>()?;
                ps.iter().for_each(|s| visitor.bind_symbol(s));
                let sort = sort.accept(visitor)?;
                ps.iter().for_each(|s| visitor.unbind_symbol(s));
                visitor.bind_symbol(&symbol);
                visitor.visit_define_sort(symbol, ps, sort)
            }
            Echo { message } => visitor.visit_echo(message),
            Exit => visitor.visit_exit(),
            GetAssertions => visitor.visit_get_assertions(),
            GetAssignment => visitor.visit_get_assignment(),
            GetInfo { flag } => {
                let k = flag.accept(visitor)?;
                visitor.visit_get_info(k)
            }
            GetModel => visitor.visit_get_model(),
            GetOption { keyword } => {
                let k = keyword.accept(visitor)?;
                visitor.visit_get_option(k)
            }
            GetProof => visitor.visit_get_proof(),
            GetUnsatAssumptions => visitor.visit_get_unsat_assumptions(),
            GetUnsatCore => visitor.visit_get_unsat_core(),
            GetValue { terms } => {
                let ts = terms
                    .into_iter()
                    .map(|t| t.accept(visitor))
                    .collect::<Result<_, E>>()?;
                visitor.visit_get_value(ts)
            }
            Pop { level } => visitor.visit_pop(level),
            Push { level } => visitor.visit_push(level),
            Reset => visitor.visit_reset(),
            ResetAssertions => visitor.visit_reset_assertions(),
            SetInfo { keyword, value } => {
                let k = keyword.accept(visitor)?;
                let v = value.remap(
                    visitor,
                    |v, c: self::Constant| c.accept(v),
                    |v, s: Symbol| v.visit_bound_symbol(s.0),
                    |v, e: SExpr| e.accept(v),
                )?;
                visitor.visit_set_info(k, v)
            }
            SetLogic { symbol } => {
                let s = visitor.visit_bound_symbol(symbol.0)?;
                visitor.visit_set_logic(s)
            }
            SetOption { keyword, value } => {
                let k = keyword.accept(visitor)?;
                let v = value.remap(
                    visitor,
                    |v, c: self::Constant| c.accept(v),
                    |v, s: Symbol| v.visit_bound_symbol(s.0),
                    |v, e: SExpr| e.accept(v),
                )?;
                visitor.visit_set_option(k, v)
            }
        }
    }
}

```

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

### Extending Vec from a range (from start to index)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/type.Hexadecimal.html

Clones elements from a specified range (from start up to, but not including, index) and appends them to the Vec.

```Rust
let mut numbers = vec![0, 1, 2, 3, 4];
numbers.extend_from_within(..2);
assert_eq!(numbers, [0, 1, 2, 3, 4, 0, 1]);

```

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

### Dispatching SMT-LIB Commands with a Visitor

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/concrete.rs.html

Accepts a visitor and dispatches to the appropriate visit method based on the concrete command. This pattern allows for flexible command processing and extension.

```Rust
impl Command {
    /// Visit a concrete command.
    pub fn accept<V, T, E, S1, S2, S3, S4, S5, S6, S7>(self, visitor: &mut V) -> Result<T, E>
    where
        V: SortVisitor<S1, T = S2, E = E>
            + SymbolVisitor<T = S1, E = E>
            + QualIdentifierVisitor<Identifier<S1>, S2, T = S3, E = E>
            + ConstantVisitor<T = S4, E = E>
            + KeywordVisitor<T = S5, E = E>
            + SExprVisitor<S4, S1, S5, T = S6, E = E>
            + TermVisitor<S4, S3, S5, S6, S1, S2, T = S7, E = E>
            + CommandVisitor<S7, S1, S2, S5, S4, S6, T = T, E = E>,
    {
        use Command::*;
        match self {
            Assert { term } => {
                let t = term.accept(visitor)?;
                visitor.visit_assert(t)
            }
            CheckSat => visitor.visit_check_sat(),
            CheckSatAssuming { literals } => {
                let ls = literals
                    .into_iter()
                    .map(|(s, b)| Ok((visitor.visit_bound_symbol(s.0)?, b)))
                    .collect::<Result<_, E>>()?;
                visitor.visit_check_sat_assuming(ls)
            }
            DeclareConst { symbol, sort } => {
                let symb = visitor.visit_fresh_symbol(symbol.0, SymbolKind::Constant)?;
                let sort = sort.accept(visitor)?;
                visitor.bind_symbol(&symb);
                visitor.visit_declare_const(symb, sort)
            }
            DeclareDatatype { symbol, datatype } => {
                let s = visitor.visit_fresh_symbol(symbol.0, SymbolKind::Datatype)?;
                // Datatype may be recursive, so we bind the name early.
                visitor.bind_symbol(&s);
                let dt = datatype.remap(
                    visitor,
                    |_, _| panic!("unexpected type parameters in DeclareDatatype"),
                    |v, s| v.visit_fresh_symbol(s.0, SymbolKind::Constructor),
                    |v, s| v.visit_fresh_symbol(s.0, SymbolKind::Selector),
                    |v, sort| sort.accept(v),
                )?;
                // Bind constructor symbols and selectors.
                dt.constructors.iter().for_each(|c| {
                    visitor.bind_symbol(&c.symbol);
                    c.selectors.iter().for_each(|(s, _)| visitor.bind_symbol(s));
                });
                visitor.visit_declare_datatype(s, dt)
            }
            DeclareDatatypes { datatypes } => {
                let dts = datatypes
                    .into_iter()
                    .map(|(s, n, dt)| {
                        let s = visitor.visit_fresh_symbol(s.0, SymbolKind::Datatype)?;
                        // Datatype may be recursive, so we bind the names early.
                        visitor.bind_symbol(&s);
                        Ok((s, n, dt))
                    })
                    .collect::<Result<Vec<_>, E>>()?;
                let dts = dts
                    .into_iter()
                    .map(|(s, n, dt)| {
                        // ... (rest of the code omitted for brevity) ...
                    });
                    // ... (rest of the code omitted for brevity) ...
            }
            // ... other commands ...
        }
    }
}
```

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

### Get Constant Sort

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/struct.Ctx.html

Determines the type (sort) of a constant symbol. This is equivalent to getting the return sort of a nullary function.

```rust
pub fn const_sort(&self, sym: &ISymbol) -> Option<&ISort>
```

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

### Rust: Get Last Element

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `last` to get an optional reference to the last element of a slice. Returns `None` for empty slices.

```rust
let v = [10, 40, 30];
assert_eq!(Some(&30), v.last());

let w: &[i32] = &[];
assert_eq!(None, w.last());
```

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

### Test SMT2 Syntax Visitor

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/concrete.rs.html

Tests the SyntaxVisitor implementation by creating an SMT2 'assert' command with a 'let' binding and an equality comparison, then accepting the visitor to ensure it's processed correctly.

```rust
#[test]
fn test_syntax_visitor() {
    // (assert (let ((x (f x 2))) (= x 3)))
    let command = Command::Assert {
        term: Term::Let {
            var_bindings: vec![
                (
                    Symbol("x".into()),
                    Term::Application {
                        qual_identifier: QualIdentifier::Simple {
                            identifier: Identifier::Simple {
                                symbol: Symbol("f".into()),
                            },
                        },
                        arguments: vec![
                            Term::QualIdentifier(QualIdentifier::Simple {
                                identifier: Identifier::Simple {
                                    symbol: Symbol("x".into()),
                                },
                            }),
                            Term::Constant(Constant::Numeral(num::BigUint::from(2u32))),
                        ],
                    },
                )
            ],
            term: Box::new(Term::Application {
                qual_identifier: QualIdentifier::Simple {
                    identifier: Identifier::Simple {
                        symbol: Symbol("=".into()),
                    },
                },
                arguments: vec![
                    Term::QualIdentifier(QualIdentifier::Simple {
                        identifier: Identifier::Simple {
                            symbol: Symbol("x".into()),
                        },
                    }),
                    Term::Constant(Constant::Numeral(num::BigUint::from(3u32))),
                ],
            }),
        },
    };
    let mut builder = SyntaxBuilder;
    let command2 = command.clone().accept(&mut builder).unwrap();
    assert_eq!(command, command2);
}

```

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

### Getting First Element of Slice

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Illustrates how to safely get a reference to the first element of a slice using `first()`, returning `None` if the slice is empty.

```rust
let v = [10, 40, 30];
assert_eq!(Some(&10), v.first());

let w: &[i32] = &[];
assert_eq!(None, w.first());
```

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

### Implement CommandVisitor for Rewriter

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/rewriter.rs.html

Handles visiting and processing SMT-LIB2 commands. It delegates to the visitor's `visit_set_option` and then processes the command.

```rust
impl<R, V> CommandVisitor for R
where
    R: Rewriter<V = V>,
    V: Smt2Visitor,
{
    type T = V::Command;
    type E = R::Error;

    fn visit_set_option(
        &mut self,
        keyword: <Self::V as Smt2Visitor>::Keyword,
        value: AttributeValue<
            <Self::V as Smt2Visitor>::Constant,
            <Self::V as Smt2Visitor>::Symbol,
            <Self::V as Smt2Visitor>::SExpr,
        >,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> {
        let value = self.visitor().visit_set_option(keyword, value)?;
        self.process_command(value)
    }
}
```

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

### Rust: Get Last Element Mutably

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `last_mut` to get an optional mutable reference to the last element of a slice. Returns `None` for empty slices.

```rust
let x = &mut [0, 1, 2];

if let Some(last) = x.last_mut() {
    *last = 10;
}
assert_eq!(x, &[0, 1, 10]);

let y: &mut [i32] = &mut [];
assert_eq!(None, y.last_mut());
```

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

### Creating a Vec with Capacity and Pushing Elements

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/type.Binary.html

Demonstrates creating a vector with a specified initial capacity using a custom allocator and appending elements. It highlights how capacity is managed and when reallocations might occur.

```rust
#![feature(allocator_api)]

use std::alloc.System;

let mut vec = Vec::with_capacity_in(10, System);

// The vector contains no items, even though it has capacity for more
assert_eq!(vec.len(), 0);
assert!(vec.capacity() >= 10);

// These are all done without reallocating...
for i in 0..10 {
    vec.push(i);
}
assert_eq!(vec.len(), 10);
assert!(vec.capacity() >= 10);

// ...but this may make the vector reallocate
vec.push(11);
assert_eq!(vec.len(), 11);
assert!(vec.capacity() >= 11);

// A vector of a zero-sized type will always over-allocate, since no
// allocation is necessary
let vec_units = Vec::<(), System>::with_capacity_in(10, System);
assert_eq!(vec_units.capacity(), usize::MAX);

```

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

### Rust: Get Last Chunk of Slice

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `last_chunk::<N>` to get an array reference to the last `N` items. Returns `None` if the slice is shorter than `N`.

```rust
let u = [10, 40, 30];
assert_eq!(Some(&[40, 30]), u.last_chunk::<2>());

let v: &[i32] = &[10];
assert_eq!(None, v.last_chunk::<2>());

let w: &[i32] = &[];
assert_eq!(Some(&[]), w.last_chunk::<0>());
```

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

### Implement SortVisitor for Rewriter

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/rewriter.rs.html

Handles visiting SMT-LIB2 sorts, including simple and parameterized sorts. Each visit method delegates to the underlying visitor.

```rust
impl<R, V> SortVisitor<V::Symbol> for R
where
    R: Rewriter<V = V>,
    V: Smt2Visitor,
{
    type T = V::Sort;
    type E = R::Error;

    fn visit_simple_sort(&mut self, identifier: Identifier<V::Symbol>) -> Result<Self::T, Self::E> {
        self.visit_simple_sort(identifier)
    }

    fn visit_parameterized_sort(
        &mut self,
        identifier: Identifier<V::Symbol>,
        parameters: Vec<Self::T>,
    ) -> Result<Self::T, Self::E> {
        self.visit_parameterized_sort(identifier, parameters)
    }
}
```

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

### Rust: Get First Chunk of Slice

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `first_chunk::<N>` to get an array reference to the first `N` items. Returns `None` if the slice is shorter than `N`.

```rust
let u = [10, 40, 30];
assert_eq!(Some(&[10, 40]), u.first_chunk::<2>());

let v: &[i32] = &[10];
assert_eq!(None, v.first_chunk::<2>());

let w: &[i32] = &[];
assert_eq!(Some(&[]), w.first_chunk::<0>());
```

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

### Vec with Capacity in System Allocator

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/type.Hexadecimal.html

Demonstrates creating a Vec with a specific initial capacity using the System allocator and how push operations affect its length and capacity.

```rust
#![feature(allocator_api)]

use std::alloc::System;

let mut vec = Vec::with_capacity_in(10, System);

// The vector contains no items, even though it has capacity for more
assert_eq!(vec.len(), 0);
assert!(vec.capacity() >= 10);

// These are all done without reallocating...
for i in 0..10 {
    vec.push(i);
}
assert_eq!(vec.len(), 10);
assert!(vec.capacity() >= 10);

// ...but this may make the vector reallocate
vec.push(11);
assert_eq!(vec.len(), 11);
assert!(vec.capacity() >= 11);

// A vector of a zero-sized type will always over-allocate, since no
// allocation is necessary
let vec_units = Vec::<(), System>::with_capacity_in(10, System);
assert_eq!(vec_units.capacity(), usize::MAX);
```

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

### Rust: Get First Chunk Mutably

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `first_chunk_mut::<N>` to get a mutable array reference to the first `N` items. Returns `None` if the slice is shorter than `N`.

```rust
let x = &mut [0, 1, 2];

if let Some(first) = x.first_chunk_mut::<2>() {
    first[0] = 5;
    first[1] = 4;
}
assert_eq!(x, &[5, 4, 2]);

assert_eq!(None, x.first_chunk_mut::<4>());
```

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

### Appending an Element and Getting a Mutable Reference

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/type.Binary.html

Demonstrates using `push_mut` to append an element and immediately get a mutable reference to it. This is useful for modifying the newly added element in place.

```rust
let mut vec = vec![1, 2];
let last = vec.push_mut(3);
assert_eq!(*last, 3);
assert_eq!(vec, [1, 2, 3]);

let last = vec.push_mut(3);
*last += 1;
assert_eq!(vec, [1, 2, 3, 4]);

```

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

### Checking Vec Capacity

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/type.Hexadecimal.html

Shows how to create a Vec with a specified initial capacity and verify it.

```rust
let mut vec: Vec<i32> = Vec::with_capacity(10);
vec.push(42);
assert!(vec.capacity() >= 10);

```

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

### Get Element or Subslice by Index (Rust)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

The `get` method safely retrieves an element or subslice using various index types (position or range). It returns `None` if the index is out of bounds.

```rust
let v = [10, 40, 30];
assert_eq!(Some(&40), v.get(1));
assert_eq!(Some(&[10, 40][..]), v.get(0..2));
assert_eq!(None, v.get(3));
assert_eq!(None, v.get(0..4));
```

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

### Get Mutable Reference to Last N Elements (Rust)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `last_chunk_mut` to get a mutable reference to the last N elements of a slice. Returns `None` if the slice is shorter than N.

```rust
let x = &mut [0, 1, 2];

if let Some(last) = x.last_chunk_mut::<2>() {
    last[0] = 10;
    last[1] = 20;
}
assert_eq!(x, &[0, 10, 20]);

assert_eq!(None, x.last_chunk_mut::<4>());
```

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

### Rust SMT-2 Visitor: Set Info Command

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/smt2parser/renaming/struct.TesterModernizer.html

Handles the 'set-info' command in SMT-2, used to set information attributes.

```rust
fn visit_set_info( &mut self, keyword: <V as Smt2Visitor>::Keyword, value: AttributeValue<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::SExpr>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>
```

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

### Safe Get Multiple Disjoint Mutable References (RangeInclusive indices)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use this safe method to get mutable references to multiple sub-slices at once using RangeInclusive indices. It returns a Result, checking for out-of-bounds and overlapping indices.

```rust
if let Ok([a, b]) = v.get_disjoint_mut([1..=2, 0..=0]) {
    a[0] = 11;
    a[1] = 111;
    b[0] = 1;
}
assert_eq!(v, &[1, 11, 111]);
```

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

### Implement KeywordVisitor for Rewriter

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/rewriter.rs.html

Provides a method for visiting SMT-LIB2 keywords, delegating the call to the underlying visitor.

```rust
impl<R, V> KeywordVisitor for R
where
    R: Rewriter<V = V>,
    V: Smt2Visitor,
{
    type T = V::Keyword;
    type E = R::Error;

    fn visit_keyword(&mut self, value: String) -> Result<Self::T, Self::E> {
        self.visit_keyword(value)
    }
}
```

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

### visit_assert

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/concrete.rs.html

Visits an assert command, creating an SMT-IR Assert command.

```APIDOC
## visit_assert

### Description
Creates an SMT-IR `Command::Assert` from a given term.

### Method
`visit_assert`

### Parameters
- `term`: The term to be asserted.
```

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

### Safe Get Multiple Disjoint Mutable References (Range indices)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use this safe method to get mutable references to multiple sub-slices at once using Range indices. It returns a Result, checking for out-of-bounds and overlapping indices.

```rust
if let Ok([a, b]) = v.get_disjoint_mut([0..1, 1..3]) {
    a[0] = 8;
    b[0] = 88;
    b[1] = 888;
}
assert_eq!(v, &[8, 88, 888]);
```

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

### Safe Get Multiple Disjoint Mutable References (usize indices)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use this safe method to get mutable references to multiple elements at once using usize indices. It returns a Result, checking for out-of-bounds and overlapping indices.

```rust
let v = &mut [1, 2, 3];
if let Ok([a, b]) = v.get_disjoint_mut([0, 2]) {
    *a = 413;
    *b = 612;
}
assert_eq!(v, &[413, 2, 612]);
```

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

### Unsafe Get Multiple Disjoint Mutable References (RangeInclusive indices)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use this unsafe method to get mutable references to multiple sub-slices at once using RangeInclusive indices. It performs no checks, so overlapping or out-of-bounds indices result in undefined behavior.

```rust
let x = &mut [1, 2, 4];

unsafe {
    let [a, b] = x.get_disjoint_unchecked_mut([1..=2, 0..=0]);
    a[0] = 11;
    a[1] = 111;
    b[0] = 1;
}
assert_eq!(x, &[1, 11, 111]);
```

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

### SMT-LIB Token Matching in Rust

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/lexer.rs.html

Illustrates how different SMT-LIB tokens are matched and formatted within the lexer. This covers standard tokens like strings, parentheses, and various SMT commands.

```Rust
160            Token::String(s) => fmt_string(s, f),
161            Token::LeftParen => "(".fmt(f),
162            Token::RightParen => ")".fmt(f),
163            Token::Underscore(s) => s.fmt(f),
164            Token::Exclam(s) => s.fmt(f),
165            Token::As(s) => s.fmt(f),
166            Token::Let(s) => s.fmt(f),
167            Token::Exists(s) => s.fmt(f),
168            Token::Forall(s) => s.fmt(f),
169            Token::Match(s) => s.fmt(f),
170            Token::Par(s) => s.fmt(f),
171            Token::Assert(s) => s.fmt(f),
172            Token::CheckSat(s) => s.fmt(f),
173            Token::CheckSatAssuming(s) => s.fmt(f),
174            Token::DeclareConst(s) => s.fmt(f),
175            Token::DeclareDatatype(s) => s.fmt(f),
176            Token::DeclareDatatypes(s) => s.fmt(f),
177            Token::DeclareFun(s) => s.fmt(f),
178            Token::DeclareSort(s) => s.fmt(f),
179            Token::DefineFun(s) => s.fmt(f),
180            Token::DefineFunRec(s) => s.fmt(f),
181            Token::DefineFunsRec(s) => s.fmt(f),
182            Token::DefineSort(s) => s.fmt(f),
183            Token::Echo(s) => s.fmt(f),
184            Token::Exit(s) => s.fmt(f),
185            Token::GetAssertions(s) => s.fmt(f),
186            Token::GetAssignment(s) => s.fmt(f),
187            Token::GetInfo(s) => s.fmt(f),
188            Token::GetModel(s) => s.fmt(f),
189            Token::GetOption(s) => s.fmt(f),
190            Token::GetProof(s) => s.fmt(f),
191            Token::GetUnsatAssumptions(s) => s.fmt(f),
192            Token::GetUnsatCore(s) => s.fmt(f),
193            Token::GetValue(s) => s.fmt(f),
194            Token::Pop(s) => s.fmt(f),
195            Token::Push(s) => s.fmt(f),
196            Token::Reset(s) => s.fmt(f),
197            Token::ResetAssertions(s) => s.fmt(f),
198            Token::SetInfo(s) => s.fmt(f),
199            Token::SetLogic(s) => s.fmt(f),
200            Token::SetOption(s) => s.fmt(f),
201        }
202    }
203}
```

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

### Implement `Term::accept` for Visitor Pattern

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/concrete.rs.html

The `accept` method dispatches to the appropriate visitor method based on the `Term` variant. It handles symbol binding and unbinding for quantified and let expressions.

```rust
impl Term {
    /// Visit a concrete term.
    pub fn accept<V, T, E, S1, S2, S3, S4, S5, S6>(self, visitor: &mut V) -> Result<T, E>
    where
        V: SortVisitor<S1, T = S2, E = E>
            + SymbolVisitor<T = S1, E = E>
            + QualIdentifierVisitor<Identifier<S1>, S2, T = S3, E = E>
            + ConstantVisitor<T = S4, E = E>
            + KeywordVisitor<T = S5, E = E>
            + SExprVisitor<S4, S1, S5, T = S6, E = E>
            + TermVisitor<S4, S3, S5, S6, S1, S2, T = T, E = E>,
    {
        use Term::*;
        match self {
            Constant(value) => {
                let c = value.accept(visitor)?;
                visitor.visit_constant(c)
            }
            QualIdentifier(value) => {
                let qi = value.accept(visitor)?;
                visitor.visit_qual_identifier(qi)
            }
            Application {
                qual_identifier,
                arguments,
            } => {
                let qi = qual_identifier.accept(visitor)?;
                let mut ts = Vec::new();
                for t in arguments {
                    ts.push(t.accept(visitor)?);
                }
                visitor.visit_application(qi, ts)
            }
            Let { var_bindings, term } => {
                let bs = var_bindings
                    .into_iter()
                    .map(|(s, t)| {
                        Ok((
                            visitor.visit_fresh_symbol(s.0, SymbolKind::Variable)?,
                            t.accept(visitor)?,
                        ))
                    })
                    .collect::<Result<Vec<_>, E>>()?;
                bs.iter().for_each(|(s, _)| visitor.bind_symbol(s));
                let t = term.accept(visitor)?;
                bs.iter().for_each(|(s, _)| visitor.unbind_symbol(s));
                visitor.visit_let(bs, t)
            }
            Forall { vars, term } => {
                let vs = vars
                    .into_iter()
                    .map(|(v, s)| {
                        Ok((
                            visitor.visit_fresh_symbol(v.0, SymbolKind::Variable)?,
                            s.accept(visitor)?,
                        ))
                    })
                    .collect::<Result<Vec<_>, E>>()?;
                vs.iter().for_each(|(s, _)| visitor.bind_symbol(s));
                let t = term.accept(visitor)?;
                vs.iter().for_each(|(s, _)| visitor.unbind_symbol(s));
                visitor.visit_forall(vs, t)
            }
            Exists { vars, term } => {
                let vs = vars
                    .into_iter()
                    .map(|(v, s)| {
                        Ok((
                            visitor.visit_fresh_symbol(v.0, SymbolKind::Variable)?,
                            s.accept(visitor)?,
                        ))
                    })
                    .collect::<Result<Vec<_>, E>>()?;
                vs.iter().for_each(|(s, _)| visitor.bind_symbol(s));
                let t = term.accept(visitor)?;
                vs.iter().for_each(|(s, _)| visitor.unbind_symbol(s));
                visitor.visit_exists(vs, t)
            }
            Match { term, cases } => {
                let t = term.accept(visitor)?;
                let cs = cases
                    .into_iter()
                    .map(|(ss, t)| {
                        let mut symbols = Vec::new();
                        let mut ss = ss.into_iter();
                        let mut has_fresh_first_symbol = false;
                        if let Some(s) = ss.next() {
                            // First symbol may be a constructor.
                            symbols.push(visitor.visit_bound_symbol(s.0.clone()).or_else(
                                |_| {
                                    has_fresh_first_symbol = true;
                                    let s = visitor
                                        .visit_fresh_symbol(s.0.clone(), SymbolKind::Variable)?;
                                    visitor.bind_symbol(&s);
                                    Ok(s)
                                },
                            )?);
                        }
                        for s in ss {
                            let s = visitor.visit_fresh_symbol(s.0, SymbolKind::Variable)?;
                            visitor.bind_symbol(&s);
                            symbols.push(s);
                        }
                        Ok((symbols, t.accept(visitor)?))
                    })
                    .collect::<Result<Vec<_>, E>>()?;
                visitor.visit_match(t, cs)
            }
        }
    }
}
```

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

### Unsafe Get Multiple Disjoint Mutable References (Range indices)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use this unsafe method to get mutable references to multiple sub-slices at once using Range indices. It performs no checks, so overlapping or out-of-bounds indices result in undefined behavior.

```rust
let x = &mut [1, 2, 4];

unsafe {
    let [a, b] = x.get_disjoint_unchecked_mut([0..1, 1..3]);
    a[0] = 8;
    b[0] = 88;
    b[1] = 888;
}
assert_eq!(x, &[8, 88, 888]);
```

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

### Unsafe Get Multiple Disjoint Mutable References (usize indices)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use this unsafe method to get mutable references to multiple elements at once using usize indices. It performs no checks, so overlapping or out-of-bounds indices result in undefined behavior.

```rust
let x = &mut [1, 2, 4];

unsafe {
    let [a, b] = x.get_disjoint_unchecked_mut([0, 2]);
    *a *= 10;
    *b *= 100;
}
assert_eq!(x, &[10, 2, 400]);
```

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

### visit_get_info

Source: https://docs.rs/aws-smt-ir/0.3.0/src/aws_smt_ir/smt2parser/concrete.rs.html

Visits a get-info command, creating an SMT-IR GetInfo command.

```APIDOC
## visit_get_info

### Description
Creates an SMT-IR `Command::GetInfo` with a specified flag.

### Method
`visit_get_info`

### Parameters
- `flag`: The keyword flag for the get-info command.
```

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

### Get Mutable Raw Pointer to Slice Buffer (Rust)

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/types/struct.ISlice.html

Use `as_mut_ptr` to get a mutable raw pointer to the slice's buffer. The caller must ensure the slice outlives the pointer and manage memory safety, as modifications can invalidate pointers.

```rust
let x = &mut [1, 2, 4];
let x_ptr = x.as_mut_ptr();

unsafe {
    for i in 0..x.len() {
        *x_ptr.add(i) += 2;
    }
}
assert_eq!(x, &[3, 4, 6]);
```

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

### clone_to_uninit

Source: https://docs.rs/aws-smt-ir/0.3.0/aws_smt_ir/logic/bitvecs/enum.BvOp.html

This is a nightly-only experimental API. It performs copy-assignment from self to dest.

```APIDOC
## unsafe fn clone_to_uninit(&self, dest: *mut u8)

### Description
Performs copy-assignment from `self` to `dest`.

### Method
unsafe fn

### Parameters
#### Path Parameters
- **self**: `&self` - The source value.
- **dest**: `*mut u8` - A mutable pointer to the destination.

### Note
This is a nightly-only experimental API.
```
Tokens:
Raw