#Fusekite

#Install from Mooncakes

moon add Lyhdsba/fusekite

#Start with your own logic table

1. Fix the input order (first input is the most significant row bit), then pass 1–8 inputs, required 1 rows, and don't-care rows to TruthSpec::new. All other rows require 0; invalid specs return None.
2. Call minimize_sop and/or minimize_pos; read deterministic patterns and term/clause and literal counts. Check against your application rule and use the BDD/SAT verifiers. SAT Unknown is inconclusive.
3. Call estimate_sop_gate_cost or estimate_pos_gate_cost, then the matching @parts.estimate_74hc_packages or @parts.estimate_74hc_pos_packages. These are direct structural estimates, without timing, pin wiring, or electrical qualification.

moon -C examples/status-indicator run .

#Example

let spec = TruthSpec::new(3, [1, 3, 5, 7], [])
let solution = minimize_sop(spec.unwrap())
println(solution.patterns()) // ["--1"]

let spec = TruthSpec::new(2, [0, 2, 3], []).unwrap()
let solution = minimize_pos(spec)
println(solution.patterns()) // ["01"]: (A OR NOT B)
solution.evaluate(1) // Some(false)
solution.evaluate(3) // Some(true)
solution.evaluate(4) // None: out of range

moon run cmd/main

#Three complete usage scenarios

#Choosing SOP or POS and respecting the limits

#Supporting reasoning modules

#Standalone API examples

let manager = BddManager::new(2).unwrap()
let a = manager.variable(0).unwrap()
let b = manager.variable(1).unwrap()
let both = manager.apply(BddOp::And, a, b).unwrap()
manager.evaluate(both, [true, false]) // Some(false)

let expr = @sat.BoolExpr::Xor(
  @sat.BoolExpr::Variable(1),
  @sat.BoolExpr::Variable(2),
)
let formula = @sat.CnfFormula::from_expression(2, expr).unwrap()
let report = formula.solve(@sat.SolverConfig::new(10_000).unwrap())

#Relationship to MoonBDD

#Implemented milestones

1. Symbolic Boolean foundation — canonical ROBDD operations and Tseitin CNF encoding with bounded DPLL SAT solving.
2. Truth-table refinement and SOP cover — explicit validation, coverage chart, essential implicants, deterministic exact selection, and BDD/SAT equivalence checks.
3. Bench planning — two-level gate estimates, a TI-sourced 74HC catalog, and three circuit examples with independent truth-table, BDD, and SAT checks.
4. Bounded bit-vector reasoning — a small QF_BV bit-blasting front end for vectors up to 8 bits, with add/subtract/multiply and signed/unsigned comparison, checked against exhaustive two-bit cases and a Z3 corpus.
5. Exact POS minimization — complement-cover reuse with separate clause/result types, zero-pattern presentation, checked row evaluation, constants and don't-cares, an independent cost oracle over all 6,561 three-input ternary specs, and direct BDD/SAT verification with replayed counterexamples.
6. POS circuit planning — direct OR-AND gate counts and sourced 74HC package estimates, checked against the interlock, BCD, and majority examples.

#Planned work

1. Evaluate NAND/NOR mapping with explicit device models and independent checks.
2. Add conflict learning and measured branching heuristics only alongside independent regression oracles and a published formula set.
3. Extend the deterministic Z3 differential corpus beyond the current bounded operator and width matrix before adding more QF_BV constructs.
4. Consider division, shifts, and concatenation only with width-boundary and independent semantic tests; the current front end does not implement full SMT.
5. Add pin-level wiring guidance only for exact device variants after datasheet review; physical qualification remains out of scope until actually performed.

#Project shape

#Build and test

moon fmt --check
moon check --deny-warn
moon test
moon build
moon run cmd/main
moon -C examples/status-indicator fmt --check
moon -C examples/status-indicator check --deny-warn
moon -C examples/status-indicator run .
moon doc
moon package --list

python -m pip install -r tests/requirements.txt
python -B -m unittest discover -s tests -p 'test_*.py' -v
python -B tests/qfbv_z3_oracle.py

#Mooncakes metadata

moon publish

#License