Crate logician 

Logician

A type-safe SMT solver driver for Rust.

Logician provides a fluent API for building logical formulas and communicating with SMT (Satisfiability Modulo Theories) solvers like Z3 and CVC5. Unlike string-based libraries, Logician enforces sort constraints at runtime through invariant checking, preventing malformed queries before they reach the solver.

Quick Example

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

let config = Config {
    program: "z3".into(),
    args: vec!["-in".into()],
    timeout: Duration::from_secs(30),
    trace: false,
};

let mut solver = Solver::new(config).unwrap();
solver.declare("x", &Sort::Bool).unwrap();

let x = Term::Var("x".into(), Sort::Bool);
solver.assert(&x).unwrap();

match solver.check().unwrap() {
    Response::Sat => println!("Satisfiable!"),
    Response::Unsat => println!("Unsatisfiable!"),
    _ => {}
}

Modules

• term - Type-safe Term AST with sort inference and fluent builders
• solver - Stateful SMT solver session management
• parser - S-expression parser for solver output
• driver - Process management with watchdog timeout
• multisolver - Multi-solver fallback orchestration
• invariant - Runtime assertion tracking system

Features

• tokio - Enable async API (default: synchronous std::io)

Modules

driver

SMT Solver Process Driver

invariant

Invariant Assertion and Tag Tracking System

multisolver

Multi-Solver with Automatic Fallback

parser

SMT Solver Output Parser

solver

Stateful SMT Solver Session

term

Type-Safe Term AST with Sort Inference

Macros

assert_invariant

Assert an invariant condition, recording the tag and panicking on failure.