GitHub - skorotkiewicz/algebruh · GitHub
/" data-turbo-transient="true" />
Skip to content
Type / to search
Sign in<br>Sign upAppearance settings
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
skorotkiewicz
algebruh
Public
Notifications<br>You must be signed in to change notification settings
Fork
Star
dev
BranchesTags
Go to file
CodeOpen more actions menu
Folders and files<br>NameNameLast commit message<br>Last commit date<br>Latest commit
History<br>52 Commits<br>52 Commits
assets
assets
docs
docs
fuzz
fuzz
src
src
.gitignore
.gitignore
Cargo.lock
Cargo.lock
Cargo.toml
Cargo.toml
README.md
README.md
justfile
justfile
shell.nix
shell.nix
View all files
Repository files navigation
Algebruh
Algebruh classifies arithmetic equality and disequality claims. It reports proofs, models, countermodels, and disagreements between independent checkers.
Build
Algebruh requires Rust 1.85 or later, Cargo, and the Z3 development library through pkg-config.
cargo build --release<br>cp target/release/algebruh .
For all optional proof tools and checkers, enter the included Nix shell before building:
nix-shell
Use
./algebruh [--all] [--json] [--interpret LIST] [--assume EXPR]... [--injective NAME]... [--ai-command CMD] [--emit PREFIX] CLAIM<br>./algebruh doctor [--json]
Examples:
./algebruh "2 = 3"<br>./algebruh --assume "a = c" --assume "c = b" "a = b"<br>./algebruh --interpret int,real,bv8,mod:1 "2 = 3"<br>./algebruh --injective f --assume "f(a) = f(b)" "a = b"<br>./algebruh --interpret f32 "16777216 + 1 = 16777216"<br>./algebruh --all --json "a = b"
--all runs additional checkers, tries extra solver seeds, searches for sufficient premises, and prints every attempt. --json prints the complete report as JSON.
--ai-command CMD sends the problem as JSON to CMD. Its output must be a Lean tactic, which Algebruh accepts only after Lean kernel verification.
Expressions
Expressions support integers, variable names, unary function applications such as f(x), parentheses, unary minus, +, -, *, /, %, =, ==, and !=.
Use repeatable --injective NAME options to declare unary functions as injective. Function applications without this option remain uninterpreted.
Multiplication, division, and modulo have higher precedence than addition and subtraction. Operator semantics follow the selected interpretation.
Each claim or assumption must contain one equality or disequality. Comparisons such as and >= are not supported.
Interpretations
--interpret accepts a comma-separated list:
Value<br>Meaning
int<br>Z3 integers. This is the default.
real<br>Exact real arithmetic. The % operator is not supported.
bvN, sbvN<br>A signed N-bit vector, where N is from 1 through 256.
ubvN<br>An unsigned N-bit vector.
mod:N<br>Integer expressions compared modulo a positive N.
quot:N<br>The quotient ring ℤ/Nℤ.
equiv:N<br>User-defined equality x ~ y when x and y have the same residue modulo N.
f32, f64<br>IEEE-754 arithmetic; integer literals are cast with round-to-nearest, ties-to-even.
singleton<br>A domain where all values are equal.
Algebruh always evaluates the integer interpretation as a baseline. It reports REINTERPRETED when a selected alternative proves a claim that integers do not. Signed and unsigned bit-vector runs are paired automatically; differences from integers or from each other are printed as semantic warnings.
Results
Result<br>Meaning<br>Exit code
PROVED<br>The assumptions prove the claim.
REFUTED<br>The assumptions prove the negation of the claim.
CONTINGENT<br>The claim and its negation both have models.
CONDITIONAL<br>Additional premises found by --all prove the claim.
VACUOUS<br>The assumptions are inconsistent.
REINTERPRETED<br>A selected alternative interpretation proves the claim.
UNKNOWN<br>No candidate result passed independent verification.
UNSAFE_AXIOM<br>A Lean candidate uses or depends on an unsafe axiom.
CHECKER_BUG_CANDIDATE<br>Solvers or proof checkers disagree.
Input, artifact, sandbox, and solver errors use exit code 2.
Checkers
The default run combines the linked Z3 library with exact evaluation, equality saturation, bounded model search, and built-in LRAT replay for direct propositional contradictions. --all can also use cvc5, Carcara, Lean with Mathlib, Vampire, and E.
For proved or refuted integer claims, --all records one differential result across Z3, cvc5, Carcara, and the Lean kernel. A disagreement is labeled CHECKER_BUG_CANDIDATE; Algebruh removes unnecessary assumptions and shrinks expressions while the disagreement still reproduces.
External tools run through Bubblewrap and prlimit. Algebruh finds them on PATH.
Check tool availability with:
./algebruh doctor
The command exits with code 1 if any listed tool is unavailable.
Proof artifacts
Use --emit PREFIX to save the selected SMT-LIB script and Z3 proof:
./algebruh --emit...