Logician

Type-safe SMT solver driver for Rust

Why Logician • Quick Start • Features • Philosophy • Sponsors

Logician is free forever. No paid tiers. No enterprise upsells. No asterisks.

Why Logician?

SMT solvers are powerful. Getting them into your Rust project shouldn't require a PhD.

What you get:

• Fluent Term API — Build formulas in Rust, not strings. Sort mismatches panic immediately with actionable diagnostics.
• Multi-solver fallback — Z3 timed out? Logician automatically retries on CVC5.
• Process watchdog — Hung solver? Dead. Entire process tree terminated cleanly.
• Optional async — Enable tokio feature when you need it.

// This panics immediately: "and requires Bool sort for other"
let bad = bool_var.and(int_var);

// This works and serializes to valid SMT-LIB
let good = x.and(y.or(z));

No silent failures. No malformed queries reaching the solver. No orphan processes.

Quick Start

[dependencies]
logician = "0.1"

You need an SMT solver in your PATH (e.g., Z3).

use logician::driver::Config;
use logician::solver::Solver;
use logician::parser::Response;
use logician::term::{Term, Sort};
use std::time::Duration;

fn main() -> Result<(), logician::term::LogicError> {
    let config = Config {
        program: "z3".into(),
        args: vec!["-in".into()],
        timeout: Duration::from_secs(30),
        trace: false,
    };
    
    let mut solver = Solver::new(config)?;
    
    solver.declare("x", &Sort::Bool)?;
    solver.declare("y", &Sort::Bool)?;
    
    let x = Term::Var("x".into(), Sort::Bool);
    let y = Term::Var("y".into(), Sort::Bool);
    let formula = x.and(y.not());
    
    solver.assert(&formula)?;
    
    match solver.check()? {
        Response::Sat => println!("Satisfiable!"),
        Response::Unsat => println!("Unsatisfiable!"),
        Response::Unknown => println!("Unknown"),
        _ => {}
    }
    
    Ok(())
}

Features

Type-Safe Terms

let a = Term::Var("a".into(), Sort::Bool);
let c = Term::Var("c".into(), Sort::Int);

// Works
let f1 = a.and(b);
let f2 = c.eq(Term::Int(42));

// Panics: "and requires Bool sort for other"
let bad = a.and(c);

Multi-Solver Fallback

use logician::multisolver::MultiSolver;

let mut ms = MultiSolver::new(vec![z3_config, cvc5_config]);

ms.declare("x", &Sort::Bool);
ms.assert(&Term::Var("x".into(), Sort::Bool));

// Tries Z3 first; if it fails, replays everything on CVC5
match ms.check() {
    Ok(Response::Sat) => println!("Found solution"),
    Err(e) => println!("All solvers failed: {:?}", e),
}

Process Watchdog

let config = Config {
    timeout: Duration::from_secs(5),  // Kill after 5 seconds
    // ...
};

Uses kill_tree to terminate the solver and all child processes.

SMT-LIB Tracing

let config = Config {
    trace: true,  // Writes to trace_<pid>.smt2
    // ...
};

Async Support

[dependencies]
logician = { version = "0.1", features = ["tokio"] }

let mut solver = Solver::new(config).await?;
solver.assert(&formula).await?;
let result = solver.check().await?;

Philosophy

The Invariant Superhighway

Logician doesn't just check for errors—it enforces architectural guarantees.

Every critical code path has runtime invariants that:

1. Record what was checked (for auditing)
2. Panic immediately on violations (no silent corruption)
3. Enable contract testing (verify the guards are watching)

// In code
assert_invariant!(term.sort() == Sort::Bool, "and requires Bool", "term_and_sort");

// In tests
let tags = get_invariant_tags();
assert!(tags.contains("term_and_sort"));

This is Predictive Property-Based Testing (PPT)—the same methodology used in high-reliability systems.

What Logician Is

• A driver for SMT solvers via subprocess (stdin/stdout)
• Type-safe term construction with sort enforcement
• Multi-solver orchestration with automatic fallback
• Process lifecycle management with timeout handling

What Logician Is Not

• Not FFI bindings (no C++ compilation required)
• Not a solver itself (you bring Z3, CVC5, Yices, etc.)
• Not a theorem prover framework
• Not pursuing advanced SMT-LIB features (arrays, bitvectors, quantifiers are not in scope)

See ROADMAP.md for the full scope definition and planned features.

Supported Solvers

Any SMT-LIB 2 compliant solver should work.

Testing

# Single-threaded (required for global invariant state)
cargo test -- --test-threads=1

# With coverage
cargo tarpaulin --out Html

Current: 24 tests, 90%+ coverage.

Sponsors

If Logician saves you time, consider sponsoring development.

Companies: Need invoicing? Email michaelallenkuykendall@gmail.com

See SPONSORS.md for the current sponsor list.

Contributing

Logician is open source but not open contribution. See CONTRIBUTING.md.

Bug reports via GitHub Issues are welcome. For security issues, see SECURITY.md.

License

MIT — see LICENSE.

Built with 🦀 by Michael A. Kuykendall