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.

Approach	Setup	Type Safety	Multi-Solver	Watchdog
FFI Bindings	C++ toolchain, platform pain	Yes	Manual	Manual
String Builders	Easy	None—pray your strings parse	Manual	Manual
Logician	cargo add logician	Yes, with clear panics	Built-in	Built-in

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

Solver	Configuration
Z3	program: "z3", args: ["-in"]
CVC5	program: "cvc5", args: ["--lang", "smt2"]
Yices 2	program: "yices-smt2"

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.

Tier	What You Get
$5/month Coffee Hero	My eternal gratitude + sponsor badge
$25/month Developer	Priority support + name in SPONSORS.md
$100/month Corporate	Logo on README + monthly office hours
$500/month Enterprise	Direct support + feature input

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