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

Version Correspondence

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

or

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

Headers are resolved in this order:

1. CVC5_INCLUDE_DIR environment variable (if set)
2. $CVC5_LIB_DIR/../include
3. 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.