z3rs 0.0.8

A pure-Rust port of the Z3 theorem prover, free of third-party and native dependencies
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139

name: CI

on:
  push:
    branches: [master]
  pull_request:

permissions:
  contents: read

env:
  CARGO_TERM_COLOR: always

jobs:
  test:
    name: Test & lint (${{ matrix.os }})
    runs-on: ${{ matrix.os }}
    strategy:
      fail-fast: false
      matrix:
        os: [ubuntu-latest, windows-latest, macos-latest]
    steps:
      - uses: actions/checkout@v6

      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable
        with:
          components: rustfmt, clippy

      - name: Cache
        uses: Swatinem/rust-cache@v2
        with:
          key: ${{ matrix.os }}

      - name: Format
        if: runner.os == 'Linux' # formatting is platform-independent
        run: cargo fmt --all --check

      - name: Clippy (all features, warnings denied)
        run: cargo clippy --all-targets --all-features -- -D warnings

      - name: Test (all features)
        run: cargo test --all-features

  no_std:
    name: no_std builds (${{ matrix.target }})
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        # thumbv7em-none-eabi is a 32-bit bare-metal target with no std at all:
        # it catches both accidental `std` dependencies and 64-bit-only
        # arithmetic (e.g. a `usize` shift that overflows when usize is 32 bits).
        target: [x86_64-unknown-linux-gnu, thumbv7em-none-eabi]
    steps:
      - uses: actions/checkout@v6

      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable
        with:
          targets: ${{ matrix.target }}

      - name: Cache
        uses: Swatinem/rust-cache@v2
        with:
          key: ${{ matrix.target }}

      # z3rs is no_std by default (`default = []`). The library must build for a
      # bare-metal target; the `z3rs` binary links std itself, so only the lib is
      # built here.
      - name: Build no_std library (default = no_std)
        run: cargo build --lib --target ${{ matrix.target }}

  msrv:
    name: MSRV (Rust 1.88)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v6

      # Keep this pin in sync with `rust-version` in Cargo.toml. Compiling on the
      # declared minimum guards against accidentally using a std/library or
      # language feature newer than 1.88 (behavior is covered by the stable `test`
      # job, so this is compile-only).
      - name: Install Rust 1.88 (declared MSRV)
        uses: dtolnay/rust-toolchain@1.88

      - name: Cache
        uses: Swatinem/rust-cache@v2
        with:
          key: msrv

      - name: cargo check --all-features --all-targets
        run: cargo check --all-features --all-targets

  c_abi:
    name: C ABI smoke test
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v6

      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable

      - name: Cache
        uses: Swatinem/rust-cache@v2

      - name: Build the C library (static + shared)
        run: |
          cargo rustc --lib --release --features ffi --crate-type staticlib
          cargo rustc --lib --release --features ffi --crate-type cdylib

      - name: Compile and run the C smoke test
        run: |
          cc tests/ffi_smoke.c -I include target/release/libz3rs.a \
             -lpthread -ldl -lm -o ffi_smoke
          ./ffi_smoke

  docs:
    name: Docs build (warnings denied)
    runs-on: ubuntu-latest
    env:
      RUSTDOCFLAGS: -D warnings -D rustdoc::broken-intra-doc-links
    steps:
      - uses: actions/checkout@v6

      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable

      - name: Cache
        uses: Swatinem/rust-cache@v2

      - name: cargo doc --no-deps --all-features
        run: cargo doc --no-deps --all-features

# Sibling workflows (matching puremp's CI):
#   * fuzz.yml             — weekly cargo-fuzz over the SMT-LIB / DIMACS parsers
#   * release-plz.yml      — crates.io publishing + GitHub releases
#   * release-binaries.yml — cross-built `z3rs` CLI attached to each release
#                            (the C library will be added once the C ABI lands, Phase 9)