Adding `cvc5` library as a dependency

Run this command in a terminal, in your project's directory:

cargo add cvc5

To add it manually, edit your project's Cargo.toml file and add to the [dependencies] section:

cvc5 = "0.4.0"

The cvc5 library will be automatically available globally. Read the cvc5 library documentation.

Back to the crate overview.

Readme

cvc5-rs

Safe, high-level Rust bindings for the cvc5 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`	Safe, idiomatic Rust API (this crate)
`cvc5-sys`	Raw FFI bindings generated by bindgen

Version Correspondence

`cvc5` Version	`cvc5-sys` Version	`cvc5` Crate Version
1.3.1	>= 0.4 < 0.5	>= 0.4 < 0.5

Prerequisites

cvc5 1.3.1 (included as a git submodule in cvc5-sys/cvc5; built automatically by cvc5-sys when the static feature is enabled)

If building from source using the static feature, install:

A C/C++ compiler, CMake ≥ 3.16, and libclang (for bindgen)
Git (for automatic source download when installed from crates.io)

Quick Start

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 --features static

Usage

Add to your Cargo.toml:

[dependencies]
cvc5 = "0.4"

Enable the static feature to statically link cvc5 and build it from source automatically:

[dependencies]
cvc5 = { version = "0.4", features = ["static"] }

Without the static feature, cvc5 must be installed on the system or a path to shared library must be specified by CVC5_LIB_DIR. The build script discovers headers via CVC5_INCLUDE_DIR, CVC5_LIB_DIR/../include, or by asking the C compiler in this order.

Enable the parser feature for SMT-LIB parsing support:

[dependencies]
cvc5 = { version = "0.4", features = ["static", "parser"] }

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 (requires the static feature):

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

Linking Against a Prebuilt cvc5

If you already have cvc5 built and installed, you can skip the automatic build by setting CVC5_LIB_DIR to the directory containing the libraries:

CVC5_LIB_DIR=/path/to/cvc5/build/install/lib cargo build --features static

CVC5_LIB_DIR=/path/to/cvc5/build/install/lib cargo build

Headers are resolved in this order:

CVC5_INCLUDE_DIR environment variable (if set)
$CVC5_LIB_DIR/../include
Compiler discovery (the build script asks the C compiler to locate cvc5/c/cvc5.h)

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

Example: Linear Integer Arithmetic

use cvc5::{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::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, Stat — solver statistics.
OptionInfo, OptionInfoKind — solver option introspection.

Parser Types (parser feature)

InputParser — SMT-LIB input parser.
SymbolManager — symbol table for the parser.
Command — a parsed command.
InputLanguage — input language enum.

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., BooleanSort, IntegerSort, …)
RoundingMode — floating-point rounding modes
ProofRule, ProofRewriteRule — proof rules
ProofComponent, ProofFormat — proof output configuration
SkolemId — Skolem function identifiers
UnknownExplanation — reasons for unknown results
BlockModelsMode — model blocking modes
LearnedLitType — learned literal types
FindSynthTarget — synthesis targets
OptionCategory — option categories
Plugin — plugin interface

Configuration

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

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 for the full list of supported logics and options.

License

BSD-3-Clause — see LICENSE.

Adding cvc5 library as a dependency

Adding `cvc5` library as a dependency