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

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

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:

[dependencies]
cvc5-rs = "0.1"

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:

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

Example: Linear Integer Arithmetic

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():

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.