minikanren_1bit_chirho

Crates.iominikanren_1bit_chirho
lib.rsminikanren_1bit_chirho
version0.2.0
created_at2026-01-24 10:05:30.008505+00
updated_at2026-01-24 15:39:42.446558+00
descriptionminiKanren as 1-bit matrix operations - hardware-accelerated logic programming with SIMD, GPU, and FPGA support. Includes Sudoku solver (14μs), N-Queens, constraint propagation.
homepage
repositoryhttps://github.com/loveJesus/minikanren_1bit_chirho
max_upload_size
id2066494
size577,613
Love JESUS (loveJesus)

documentation

https://docs.rs/minikanren_1bit_chirho

README

minikanren_1bit_chirho

miniKanren as 1-bit matrix operations - hardware-accelerated logic programming.

Core Insight

miniKanren search = sparse Boolean tensor network contraction
miniKanren Tensor Representation
Variable domain Bitmask (1 = value possible)
(== x y) Bitwise AND of domains
conde (or) Row duplication / tensor stack
Relation Sparse N-D Boolean tensor
Composition Tensor contraction

Performance

Operation Time Notes
Unify (64-bit AND) 2ns Single SIMD instruction
Domain intersection (AVX2) 8ns 8 domains parallel
Hardware optics (BitVec64) 420ps Single CPU cycle

vs Heap-based alternatives: 3000-4000x faster

Usage

use minikanren_1bit_chirho::*;

fn main() {
    let mut store_chirho = TermStoreChirho::new();

    // Create terms
    let (_, x_chirho) = store_chirho.fresh_var_chirho();
    let one_chirho = store_chirho.int_chirho(1);
    let two_chirho = store_chirho.int_chirho(2);

    // Build goal: x == 1 OR x == 2
    let goal_chirho = conde_chirho(vec![
        vec![eq_chirho(x_chirho, one_chirho)],
        vec![eq_chirho(x_chirho, two_chirho)],
    ]);

    // Run and collect solutions
    let solutions_chirho = run_chirho(10, x_chirho, goal_chirho, &store_chirho);
    println!("x_chirho can be: {:?}", solutions_chirho); // [1, 2]
}

Features

  • Full miniKanren semantics: ==, conde, fresh, not, conda, condu, =/=, project
  • SIMD acceleration: AVX2/AVX-512 bulk operations
  • Differentiable relaxation: Gradients flow through logic (neural-symbolic)
  • Hardware-ready: Calyx IR and Clash for FPGA synthesis
  • Multiple semirings: Boolean, Probability, Tropical, Counting

Feature Flags

[dependencies]
minikanren_1bit_chirho = { version = "0.1", features = ["kmett_chirho"] }
Feature Description
egraph_native_chirho (default) Native hardware-optimized e-graph
egg_chirho External egg crate for more features
goal_ast_chirho Goals as AST for introspection
gpu_chirho WebGPU backend
optics_chirho Kmett-style Prisms, Lenses, Traversals
free_goal_chirho Free Monad for Bool/Prob/SMT interpreters
comonad_chirho Search zipper with extend
linear_chirho Tensor/Par linear logic connectives
kmett_chirho All category-theoretic extensions

Examples

cargo run --example appendo_chirho   # List append relation
cargo run --example type_infer_chirho # Type inference demo

Naming Convention

All identifiers end with _chirho (the Chi-Rho Christogram).

License

MIT

Soli Deo Gloria

Commit count: 131

cargo fmt