Axeyum SMT Solver

Implementation

Axeyum implements its SMT solver in Rust, from typed terms and SMT-LIB parsing through rewriting, theory-specific decisions, bit-blasting, and SAT search. A sat result is replayed against the original terms before it is reported.

Z3, cvc5, and Bitwuzla are comparison systems and optional test oracles. They do not run in Axeyum's default reasoning path.

• Typed terms and SMT-LIB parsing
• Query planning and rewriting
• Bit-vector, floating-point, string, and arithmetic routes
• Model replay and route-specific unsat evidence

Rust crates

These crates implement the component or connect its results to another Axeyum checker. Each link opens the crate's source directory.

• axeyum-ir Typed terms and exact semantics
• axeyum-query Query planning
• axeyum-rewrite Term rewriting
• axeyum-bv Bit-vector operations and lowering
• axeyum-fp Floating-point operations
• axeyum-strings String operations
• axeyum-smtlib SMT-LIB parsing and commands
• axeyum-solver SAT search and certificates

Reference systems and results

The result report compares selected SMT-LIB divisions with Z3, cvc5, and Bitwuzla.

Problems studied with this component

• A BCNF decomposition counterexample Database theory
• The cause of an infeasible ICU roster Operations research
• The cause of an impossible project deadline Operations research

Current limit