SMT Server

SMT Server lets analysis tools build QF_BV formulas with small client libraries and delegate solving or simplification to a separate server.

It targets binary analysis, lifting, symbolic execution, and IR experiments where client projects need bit-vector queries but should avoid embedding solver build systems. A client constructs a flat binary DAG, sends a length-prefixed request, and receives a model, unsat core, optimum value, or simplified expression. The server owns the solver and simplifier integrations.

Clients

• C++: header-only C++17 package under cpp/.
• Python: dependency-free package under python/, installable with pip's #subdirectory=python support.
• Rust: smt-wire crate with an idiomatic Context/term/Client API; protocol internals are isolated for the server.

Backends

• Solve and optimize: z3, binbit, and the standalone qfbvsmtrs crate.
• Simplify: Rumba for supported 64-bit-or-smaller MBA expression islands.
• Text compatibility: SMT-LIB QF_BV scripts are parsed into the same binary IR used by binary clients.

The binary protocol is the main API. SMT-LIB support exists for tooling compatibility and test reuse.

Expression format

Expressions are stored as one contiguous binary buffer:

• nodes are fixed-size records in topological order;
• children are typed integer references into the node array;
• symbol names and wide constants live in a blob table;
• the buffer contains no pointers.

This layout makes requests cheap to copy, send, validate, hash, cache, and replay. The server validates the buffer and translates the flat DAG into backend-specific terms.

Scope is limited to quantifier-free bit-vectors and Booleans. That covers the formulas commonly emitted by lifters, binary-analysis tools, and symbolic-execution engines.

Build

cargo build --workspace

Run the server

cargo run -p smt-server -- 127.0.0.1:9123

If no address is provided, the server listens on 127.0.0.1:9123. Clients use SMT_SERVER_ADDRESS=<host>:<port> as their default connection target, falling back to 127.0.0.1:9123 when the variable is unset.

Requests use length-prefixed frames:

u32 little-endian payload length
payload bytes

Payload formats:

• binary SMTQ request produced by smt-wire or one of the clients;
• SMT-LIB script as UTF-8 text.

Python client example

The Python client can be installed with pip install 'git+https://github.com/LLVMParty/smt-server.git#subdirectory=python' or used directly by adding python/ to PYTHONPATH.

import smt_wire as smt

ctx = smt.Context()
x = ctx.bv_var("x", 8)
ctx.assert_(ctx.bv_eq(x, 42))

with smt.Client() as client:
    response = client.solve(ctx)  # want_model=True by default

print(response.status)       # Status.SAT
if response.model is not None:
    for var, value in response.model.items():
        print(f"{var.name} = {hex(int(value))}")

# Dump a self-contained SMT-LIB script for debugging or external solvers.
print(ctx.to_smt2())          # includes check-sat/get-model by default

Simplification example

SIMPLIFY requests send one expression root and return a typed term in a fresh result context:

import smt_wire as smt

ctx = smt.Context()
x = ctx.bv_var("x", 64)
target = x + 0

with smt.Client() as client:
    simplified = client.simplify(target)

if simplified.term is not None:
    print(simplified.term.to_smt2())  # full expansion by default

str(term) still prints a one-layer debug view; use term.to_smt2(depth=0) for the same depth-limited form explicitly.

SMT-LIB text example

A text frame can contain an SMT-LIB script:

(set-logic QF_BV)
(declare-const x (_ BitVec 8))
(assert (= x #x2a))
(check-sat)
(get-value (x))

The text frontend supports declarations, assertions, named assertions, check-sat, check-sat-assuming, get-model, get-value, get-unsat-core, let, and common bit-vector operations. It rejects stateful incremental commands such as push and pop.

with smt.Client() as client:
    print(client.smt2(script))

The full Python walkthrough is in python/example.py.

Rust client

use smt_wire::{Client, Context, Status};

let ctx = Context::new();
let x = ctx.bv_var("x", 8).unwrap();
ctx.assert_(&ctx.bv_eq(&x, 42u64).unwrap()).unwrap();

let mut client = Client::connect_default().unwrap();
let response = client.solve(&ctx).unwrap();
println!("{:?}", response.status);
if response.status == Status::Sat {
    if let Some(model) = response.model {
        println!("x = {:?}", model.get_bv(&x));
    }
}

A matching Rust walkthrough is in crates/smt-wire/examples/example.rs.

C++ client

The C++ helper is a dependency-free C++17 header:

#include <smt_wire/smt_wire.hpp>

smt_wire::Context ctx;
auto x = ctx.bv_var("x", 8);
ctx.assert_(ctx.bv_eq(x, 42u));

smt_wire::Client client;
auto response = client.solve(ctx);

A matching C++ walkthrough is in cpp/tests/example.cpp. On Windows/MSVC the header requests Ws2_32.lib automatically. With MinGW, link with -lws2_32 when using Client.

Standalone qfbvsmtrs CLI

cargo run -p qfbvsmtrs -- path/to/query.smt2

If no path is supplied, qfbvsmtrs reads SMT-LIB from stdin. The default SAT backend is splr (CDCL). varisat and the internal DPLL solver are selectable through Config::with_sat_backend.

Benchmark runner:

cargo run -p qfbvsmtrs --bin qfbvsmtrs_bench -- path/to/query.smt2

Test

cargo test --workspace
cargo clippy --workspace --all-targets -- -D warnings
python3 python/tests/test_python_client.py
cmake -S cpp -B target/cpp-cmake
cmake --build target/cpp-cmake

See docs/qfbvsmtrs-validation.md for maintainer validation gates and corpus-running notes.

Repository layout

• crates/smt-wire — Rust high-level client API plus server-side wire-format internals and validators.
• crates/qfbvsmtrs — standalone pure-Rust QF_BV bit-blasting solver crate and CLI.
• crates/smt-server — TCP server, Rumba simplifier integration, solver backend integration, SMT-LIB frontend.
• python — Python client package and tests.
• cpp — C++17 header-only package, CMake target, and tests.
• docs/architecture.md — current crate/server/backend architecture.
• docs/client-api.md — Python, C++, and Rust client API notes.
• docs/smt-wire-protocol.md — binary wire protocol reference.
• docs/smtlib-frontend.md — shared QF_BV SMT-LIB frontend behavior.
• docs/qfbvsmtrs-design.md — pure-Rust solver design.
• docs/qfbvsmtrs-validation.md — validation gates and latest corpus status.