Expand description
§miniKanren as 1-Bit Matrix Operations ☧
Hardware-accelerated logic programming through bit-parallel constraint propagation.
Core insight: miniKanren search = sparse Boolean tensor network contraction
§Quick Example
use minikanren_1bit_chirho::*;
// Create term store and define variables
let mut store_chirho = TermStoreChirho::new();
let (_, x_chirho) = store_chirho.fresh_var_chirho();
let one_chirho = store_chirho.int_chirho(1);
let two_chirho = store_chirho.int_chirho(2);
// Goal: x ∈ {1, 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 results_chirho = run_chirho(10, x_chirho, goal_chirho, &store_chirho);
assert_eq!(results_chirho.len(), 2);§Solvers
Ready-to-use constraint solvers:
use minikanren_1bit_chirho::solvers_chirho::{SudokuSolverChirho, NQueensSolverChirho};
// Sudoku: 9-bit domains per cell
let mut sudoku_chirho = SudokuSolverChirho::new_chirho();
sudoku_chirho.load_puzzle_chirho("530070000600195000098000060800060003400803001700020006060000280000419005000080079");
sudoku_chirho.solve_adaptive_chirho();
// N-Queens: 64-bit domains
let mut queens_chirho = NQueensSolverChirho::new_chirho(8);
let count_chirho = queens_chirho.count_solutions_chirho(); // 92 solutions§Performance
| Operation | Time | Notes |
|---|---|---|
| Unify (64-bit AND) | 2ns | Single SIMD instruction |
| Domain intersection | 8ns | 8 domains parallel (AVX2) |
| Sudoku (hard) | 10μs | 17-clue puzzles |
| N-Queens 8 (count 92) | 4μs | Bit-parallel |
§Features
egraph_native_chirho(default): Native hardware-optimized e-graphegg_chirho: External egg crate integrationwasm_chirho: WebAssembly bindingsgoal_ast_chirho: Goals as AST for introspection
§Module Organization
Core (core_chirho):
- [
core_chirho::terms_chirho]: Hash-consed term storage - [
core_chirho::union_find_chirho]: O(α(n)) variable equivalence classes - [
core_chirho::unify_chirho]: Unification with occurs check core_chirho::goals_chirho: Goal combinators (==, conde, conj, disj, not, conda, condu, =/=)- [
core_chirho::stream_chirho]: Lazy streams with interleaving
Hardware (hardware_chirho):
hardware_chirho::hardware_chirho: FPGA primitives (BitVec64, CAM)hardware_chirho::simd_chirho: AVX2 bulk operationshardware_chirho::optics_hw_chirho: Hardware optics (3000× faster than heap)hardware_chirho::bitmatrix_chirho: Sparse Boolean tensors (COO format)
Solvers (solvers_chirho):
solvers_chirho::sudoku_chirho: Sudoku solver (9-bit domains)solvers_chirho::nqueens_chirho: N-Queens solver (64-bit domains)
Semirings (semiring_chirho):
semiring_chirho::semiring_chirho: Semiring abstraction (Bool, Prob, Tropical, Count)semiring_chirho::diff_semiring_chirho: Differentiable relaxation with gradients
Experimental (experimental_chirho):
- E-graphs, SMT, neural heuristics, category-theoretic abstractions
Re-exports§
pub use backend_chirho::create_backend_chirho;pub use backend_chirho::create_cpu_backend_chirho;pub use backend_chirho::BackendConfigChirho;pub use backend_chirho::BackendInfoChirho;pub use backend_chirho::ConstraintChirho;pub use backend_chirho::CpuBackendChirho;pub use backend_chirho::DomainVecChirho;pub use backend_chirho::SolutionChirho;pub use backend_chirho::SolverBackendChirho;pub use reference_chirho::terms_chirho::TermChirho;pub use reference_chirho::terms_chirho::TermIdChirho;pub use reference_chirho::terms_chirho::TermStoreChirho;pub use reference_chirho::union_find_chirho::UnionFindChirho;pub use reference_chirho::union_find_chirho::UnionFindHwChirho;pub use reference_chirho::unify_chirho::ground_eq_chirho;pub use reference_chirho::unify_chirho::unify_chirho;pub use reference_chirho::unify_chirho::SubstChirho;pub use reference_chirho::unify_chirho::UnifyResultChirho;pub use reference_chirho::goals_chirho::conda_chirho;pub use reference_chirho::goals_chirho::conde_chirho;pub use reference_chirho::goals_chirho::conj_all_chirho;pub use reference_chirho::goals_chirho::conj_chirho;pub use reference_chirho::goals_chirho::condu_chirho;pub use reference_chirho::goals_chirho::diseq_chirho;pub use reference_chirho::goals_chirho::disj_all_chirho;pub use reference_chirho::goals_chirho::disj_chirho;pub use reference_chirho::goals_chirho::eq_chirho;pub use reference_chirho::goals_chirho::fail_chirho;pub use reference_chirho::goals_chirho::not_chirho;pub use reference_chirho::goals_chirho::project_chirho;pub use reference_chirho::goals_chirho::run_all_chirho;pub use reference_chirho::goals_chirho::run_chirho;pub use reference_chirho::goals_chirho::succeed_chirho;pub use reference_chirho::goals_chirho::GoalFnChirho;pub use reference_chirho::constraint_chirho::BinaryConstraintChirho;pub use reference_chirho::constraint_chirho::ConstraintStoreChirho;pub use reference_chirho::constraint_chirho::DomainChirho;pub use reference_chirho::tabling_chirho::CallPatternChirho;pub use reference_chirho::tabling_chirho::LookupResultChirho;pub use reference_chirho::tabling_chirho::TableStoreChirho;pub use reference_chirho::types_chirho::EClassIdChirhoSafe;pub use reference_chirho::types_chirho::ENodeIdChirhoSafe;pub use reference_chirho::types_chirho::GoalIdChirho;pub use reference_chirho::types_chirho::SymIdChirho;pub use reference_chirho::types_chirho::TensorIdChirho;pub use reference_chirho::types_chirho::TermIdChirhoSafe;pub use reference_chirho::types_chirho::TypedIndexChirho;pub use reference_chirho::types_chirho::TypedVecChirho;pub use reference_chirho::types_chirho::VarIdChirho;pub use hardware_chirho::bitmatrix_chirho::BitMatrixChirho;pub use hardware_chirho::bitmatrix_chirho::BitTensor3Chirho;pub use hardware_chirho::bitmatrix_packed_chirho::BitMatrix64Chirho;pub use hardware_chirho::bitmatrix_packed_chirho::BitMatrixPackedChirho;pub use hardware_chirho::bitmatrix_packed_chirho::Word64Chirho;pub use hardware_chirho::hardware_chirho::BitVec256Chirho;pub use hardware_chirho::hardware_chirho::BitVec64Chirho;pub use hardware_chirho::hardware_chirho::CamHwChirho;pub use hardware_chirho::hardware_chirho::SearchState256HwChirho;pub use hardware_chirho::hardware_chirho::SearchStateHwChirho;pub use hardware_chirho::hardware_chirho::UnifyUnitHwChirho;pub use hardware_chirho::optics_hw_chirho::collect_nonempty_chirho;pub use hardware_chirho::optics_hw_chirho::traverse_all_chirho;pub use hardware_chirho::optics_hw_chirho::DomainHwChirho;pub use hardware_chirho::optics_hw_chirho::LensHwChirho;pub use hardware_chirho::optics_hw_chirho::PartitionedDomainChirho;pub use hardware_chirho::optics_hw_chirho::PrismHwChirho;pub use hardware_chirho::optics_hw_chirho::StateHwChirho;pub use hardware_chirho::simd_chirho::bulk_and_chirho;pub use hardware_chirho::simd_chirho::bulk_not_chirho;pub use hardware_chirho::simd_chirho::bulk_or_chirho;pub use hardware_chirho::simd_chirho::bulk_popcount_chirho;pub use hardware_chirho::simd_chirho::bulk_xor_chirho;pub use hardware_chirho::simd_chirho::AlignedBitMatrixChirho;pub use solvers_chirho::nqueens_chirho::NQueensSolverChirho;pub use solvers_chirho::nqueens_chirho::KNOWN_SOLUTIONS_CHIRHO;pub use solvers_chirho::sudoku_chirho::puzzles_chirho;pub use solvers_chirho::sudoku_chirho::SudokuSolverChirho;pub use semiring_chirho::contraction_semiring_chirho::BoolTensorChirho;pub use semiring_chirho::contraction_semiring_chirho::CountTensorChirho;pub use semiring_chirho::contraction_semiring_chirho::ProbTensorChirho;pub use semiring_chirho::contraction_semiring_chirho::SemiringNetworkChirho;pub use semiring_chirho::contraction_semiring_chirho::SemiringTensorChirho;pub use semiring_chirho::contraction_semiring_chirho::TropicalTensorChirho;pub use semiring_chirho::diff_semiring_chirho::annealed_temp_chirho;pub use semiring_chirho::diff_semiring_chirho::log_sum_exp_chirho;pub use semiring_chirho::diff_semiring_chirho::soft_eq_chirho;pub use semiring_chirho::diff_semiring_chirho::soft_eq_with_grad_chirho;pub use semiring_chirho::diff_semiring_chirho::DiffProbChirho;pub use semiring_chirho::diff_semiring_chirho::GumbelSoftmaxChirho;pub use semiring_chirho::diff_semiring_chirho::LearnableRelationChirho;pub use semiring_chirho::diff_semiring_chirho::StraightThroughChirho;pub use semiring_chirho::diff_semiring_chirho::WeightedTupleChirho;pub use semiring_chirho::semiring_chirho::BoolSemiringChirho;pub use semiring_chirho::semiring_chirho::CountSemiringChirho;pub use semiring_chirho::semiring_chirho::LogSemiringChirho;pub use semiring_chirho::semiring_chirho::ProbSemiringChirho;pub use semiring_chirho::semiring_chirho::SemiringChirho;pub use semiring_chirho::semiring_chirho::TropicalSemiringChirho;pub use semiring_chirho::semiring_chirho::WeightedMatrixChirho;pub use experimental_chirho::contraction_learn_chirho::EdgeFeaturesChirho;pub use experimental_chirho::contraction_learn_chirho::LearnedContractionChirho;pub use experimental_chirho::contraction_learn_chirho::LinearEdgeScorerChirho;pub use experimental_chirho::contraction_learn_chirho::TensorNetworkChirho;pub use experimental_chirho::jsonschema_chirho::validate_chirho;pub use experimental_chirho::jsonschema_chirho::JsonValueChirho;pub use experimental_chirho::jsonschema_chirho::SchemaChirho;pub use experimental_chirho::jsonschema_chirho::ValidationErrorChirho;pub use experimental_chirho::jsonschema_chirho::ValidatorChirho;pub use experimental_chirho::nested_pattern_chirho::NestedPatternChirho;pub use experimental_chirho::nested_pattern_chirho::NodeConstraintChirho;pub use experimental_chirho::nested_pattern_chirho::NodeTypeChirho;pub use experimental_chirho::nested_pattern_chirho::PathStepChirho;pub use experimental_chirho::nested_pattern_chirho::TreePathChirho;pub use experimental_chirho::neural_chirho::beam_search_chirho;pub use experimental_chirho::neural_chirho::NeuralHeuristicChirho;pub use experimental_chirho::neural_chirho::NeuralStateChirho;pub use experimental_chirho::neural_chirho::SoftDomainChirho;pub use experimental_chirho::recursion_chirho::cata_indexed_chirho;pub use experimental_chirho::recursion_chirho::depth_algebra_chirho;pub use experimental_chirho::recursion_chirho::is_ground_algebra_chirho;pub use experimental_chirho::recursion_chirho::para_indexed_chirho;pub use experimental_chirho::recursion_chirho::size_algebra_chirho;pub use experimental_chirho::recursion_chirho::vars_algebra_chirho;pub use experimental_chirho::recursion_chirho::OccursCheckAlgebraChirho;pub use experimental_chirho::recursion_chirho::TermFChirho;pub use experimental_chirho::recursion_chirho::TermStoreIndexedChirho;pub use experimental_chirho::slg_complete_chirho::EvenOddTensorChirho;pub use experimental_chirho::slg_complete_chirho::GoalStatusChirho;pub use experimental_chirho::slg_complete_chirho::SlgGoalChirho;pub use experimental_chirho::slg_complete_chirho::SlgTableChirho;pub use experimental_chirho::smt_chirho::domain_to_smt_chirho;pub use experimental_chirho::smt_chirho::SmtExprChirho;pub use experimental_chirho::smt_chirho::SmtProblemChirho;pub use experimental_chirho::smt_chirho::SmtSortChirho;pub use hardware_chirho::unify_matrix_chirho::unify_matrix_chirho;pub use hardware_chirho::unify_matrix_chirho::SubstMatrixChirho;pub use hardware_chirho::egraph_native_chirho::EClassDataChirho;pub use hardware_chirho::egraph_native_chirho::EClassIdChirho;pub use hardware_chirho::egraph_native_chirho::EGraphNativeChirho;pub use hardware_chirho::egraph_native_chirho::ENodeChirho;pub use hardware_chirho::egraph_native_chirho::ENodeIdChirho;pub use reference_chirho::constraint_chirho;pub use reference_chirho::goals_chirho;pub use reference_chirho::stream_chirho;pub use reference_chirho::tabling_chirho;pub use reference_chirho::terms_chirho;pub use reference_chirho::types_chirho;pub use reference_chirho::unify_chirho as unify_mod_chirho;pub use reference_chirho::unify_chirho as unify_mod_chirho;pub use reference_chirho::union_find_chirho;pub use hardware_chirho::bitmatrix_chirho;pub use hardware_chirho::bitmatrix_packed_chirho;pub use hardware_chirho::hardware_chirho as hardware_mod_chirho;pub use hardware_chirho::optics_hw_chirho;pub use hardware_chirho::simd_chirho;pub use solvers_chirho::nqueens_chirho;pub use solvers_chirho::sudoku_chirho;pub use semiring_chirho::contraction_semiring_chirho;pub use semiring_chirho::diff_semiring_chirho;pub use semiring_chirho::semiring_chirho as semiring_mod_chirho;pub use experimental_chirho::contraction_chirho;pub use experimental_chirho::contraction_learn_chirho;pub use experimental_chirho::jsonschema_chirho;pub use experimental_chirho::nested_pattern_chirho;pub use experimental_chirho::neural_chirho;pub use experimental_chirho::recursion_chirho;pub use hardware_chirho::relation_chirho;pub use experimental_chirho::relations_chirho;pub use experimental_chirho::slg_complete_chirho;pub use experimental_chirho::smt_chirho;pub use hardware_chirho::unify_matrix_chirho as unify_matrix_mod_chirho;pub use hardware_chirho::unify_matrix_chirho as unify_matrix_mod_chirho;pub use hardware_chirho::egraph_native_chirho;
Modules§
- approaches_
chirho - Domain approaches for infinite/hybrid miniKanren
- backend_
chirho - Pluggable solver backends (CPU/FPGA) Pluggable Solver Backends
- core_
chirho - Core API: facade that selects reference or hardware backend Core miniKanren API ☧
- experimental_
chirho - Experimental and research modules Experimental modules ☧
- gpu_
fused_ chirho - Fused GPU/FPGA kernel design (eliminates PCIe bottleneck) Fused GPU Kernel Design ☧
- hardware_
chirho - Hardware-accelerated primitives (FPGA-friendly, SIMD) Hardware-accelerated primitives ☧
- learn_
chirho - Differentiable learning for miniKanren Differentiable Learning for miniKanren ☧
- parallel_
chirho - Parallel search state processing (multi-core with Rayon) Parallel Search State Processing ☧
- profile_
chirho - Profiling infrastructure for wall-clock breakdown Profiling Infrastructure for Wall-Clock Breakdown ☧
- reference_
chirho - Reference implementation: traditional stream-based miniKanren Reference miniKanren implementation ☧
- semiring_
chirho - Semiring abstractions for generalized provenance Semiring abstractions ☧
- solvers_
chirho - Ready-to-use constraint solvers Ready-to-use constraint solvers ☧
- synthesis_
chirho - Program synthesis via domain-pruned enumeration Program Synthesis via Domain-Pruned Enumeration ☧
- verify_
hw_ chirho - Hardware verification bridge: Rust ↔ Verilator co-simulation Part of P5-00: Bridge of Truth Verilator Verification Bridge ☧