cvc5-rs 0.3.2

# cvc5-rs

Safe, high-level Rust bindings for the [cvc5](https://cvc5.github.io/) SMT solver.

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It supports a wide
range of theories including integers, reals, bit-vectors, strings, sequences, bags, sets, floating-point arithmetic,
algebraic datatypes, and more.

## Crate Structure

| Crate      | Description                           |
|------------|---------------------------------------|
| `cvc5-rs`  | Safe, idiomatic Rust API (this crate) |
| `cvc5-sys` | Raw FFI bindings generated by bindgen |

## Prerequisites

- Rust 2024 edition (1.85+)
- cvc5 1.3.1 source (included as a git submodule in `cvc5-sys/cvc5`; built automatically by `cvc5-sys` if needed)
- A C/C++ compiler, CMake ≥ 3.16, and libclang (for bindgen)
- Git (for automatic source download when installed from crates.io)

### Quick Start

```bash
git clone --recurse-submodules https://github.com/cvc5/cvc5-rs.git
cd cvc5-rs

# Build everything (cvc5 is compiled automatically on first run)
cargo build
```

## Usage

Add to your `Cargo.toml`:

```toml
[dependencies]
cvc5-rs = "0.3"
```

An application can set `CVC5_DIR` in its `.cargo/config.toml` to point to a local cvc5 checkout
so that `cvc5-sys` can build against it:

```toml
[env]
CVC5_DIR = { value = "cvc5", relative = true }
```

### Linking Against a Prebuilt cvc5

If you already have cvc5 built, you can skip the automatic build by setting `CVC5_LIB_DIR` to the
directory containing the static libraries (`libcvc5.a`, etc.):

```bash
CVC5_LIB_DIR=/path/to/cvc5/build/lib cargo build
```

Headers are expected at `$CVC5_LIB_DIR/../include` by default. To override, set `CVC5_INCLUDE_DIR`:

```bash
CVC5_LIB_DIR=/path/to/libs CVC5_INCLUDE_DIR=/path/to/include cargo build
```

### Example: Linear Integer Arithmetic

```rust
use cvc5_rs::{TermManager, Solver, Kind};

let tm = TermManager::new();
let mut solver = Solver::new( & tm);

solver.set_logic("QF_LIA");
solver.set_option("produce-models", "true");

let int_sort = tm.integer_sort();
let x = tm.mk_const(int_sort, "x");
let zero = tm.mk_integer(0);

let gt = tm.mk_term(Kind::CVC5_KIND_GT, & [x.clone(), zero]);
solver.assert_formula(gt);

let result = solver.check_sat();
assert!(result.is_sat());

let x_val = solver.get_value(x);
println!("x = {x_val}");
```

## API Overview

### Core Types

- `TermManager` — creates sorts, terms, and operators. Owns the underlying memory.
- `Solver` — the main solver interface. Tied to a `TermManager` lifetime.
- `Sort` — represents a type (Boolean, Integer, Real, BitVector, Array, Datatype, etc.).
- `Term` — represents an expression or formula.
- `Result` — the outcome of a `check_sat()` call (sat / unsat / unknown).

### Additional Types

- `Op` — parameterized operator (e.g., bit-vector extract with indices).
- `Datatype`, `DatatypeDecl`, `DatatypeConstructor`, `DatatypeConstructorDecl`, `DatatypeSelector` — algebraic datatype
  support.
- `Grammar` — for SyGuS (syntax-guided synthesis) problems.
- `SynthResult` — result of a synthesis query.
- `Proof` — proof objects when proof production is enabled.
- `Statistics` — solver statistics.

### Re-exported Enums

The following enums from `cvc5-sys` are re-exported for convenience:

- `Kind` — term kinds (e.g., `AND`, `OR`, `GT`, `PLUS`, …)
- `SortKind` — sort kinds (e.g., `BOOLEAN_SORT`, `INTEGER_SORT`, …)
- `RoundingMode` — floating-point rounding modes
- `ProofRule`, `ProofRewriteRule` — proof rules
- `SkolemId` — Skolem function identifiers
- `UnknownExplanation` — reasons for unknown results

## Configuration

The solver is configured through `set_logic()` and `set_option()`:

```rust
solver.set_logic("QF_BV");              // quantifier-free bit-vectors
solver.set_option("produce-models", "true");
solver.set_option("produce-proofs", "true");
```

See the [cvc5 documentation](https://cvc5.github.io/docs/) for the full list of supported logics and options.

## License

BSD-3-Clause — see [LICENSE](LICENSE).