# Design contract

## Input model

- A function has one output and 1–8 input bits.
- Row numbers are unsigned binary indices. The first input is the most significant bit.
- The on-set and don't-care set are unique, disjoint, and within the truth-table range.
- Rows omitted from both sets are required zeroes.
- `TruthSpec::new` copies both row arrays after validation. The stored arrays stay private; public accessors return copies so later caller mutations cannot invalidate the specification.

## ROBDD manager

- `BddManager` fixes a variable order at construction and supports 1–32 variables. Variable index 0 is the first decision level.
- Node IDs 0 and 1 are the false and true terminals. Non-terminal IDs are local to one manager and must not be mixed with IDs from another manager.
- `make_node` applies the reduction rule `low == high => low` and linearly searches the unique table for an existing `(variable, low, high)` triple.
- AND, OR, and XOR use Shannon expansion in the fixed variable order. The apply cache memoizes canonicalized operand pairs, and complement results are memoized by node; all exposed operations check IDs before using them.
- Equivalent functions built in the same manager reduce to the same node ID. `reachable_node_count` reports the final graph size; `node_count` reports all non-terminal nodes allocated during the manager lifetime, including intermediate nodes.
- ROBDDs can be exponential in the worst case and the current unique/apply tables use linear lookup. This is a foundational symbolic Boolean package, not a SAT, BDD-optimized, or SMT solver, and no arbitrary-formula performance guarantee is made.
- `verify_sop_with_bdd` builds a truth-table reference and a selected-cover graph, masks don't-care rows, and checks that their difference is false over every cared row. Circuit examples run this check alongside their explicit expected-output vectors.

## CNF and DPLL SAT package

- The independent `sat/` package accepts variables numbered from 1 through 4,096. Formula construction rejects zero/out-of-range literals, copies caller data, sorts and deduplicates literals, removes tautologies and duplicate clauses, and preserves empty clauses as contradictions. Its DIMACS parser validates the `p cnf` header, integer bounds, zero-terminated clauses, declared clause count, and comments before returning a formula.
- `BoolExpr` represents constants, variables, negation, AND, OR, and XOR. The Tseitin encoder allocates a fresh variable for each distinct compound operation, emits equivalence clauses for it, and adds a unit clause requiring the root expression to be true. It caps source variables at 256, encoded variables at 4,096, and distinct expression nodes at 100,000.
- Structurally identical Boolean subexpressions reuse the same Tseitin literal. A regression test nests the same expression 24 times and verifies the encoding remains linear in the number of distinct nodes.
- The solver uses deterministic DPLL with two watched literals per non-unit clause; unit clauses use one watcher. Assignments enter a propagation trail; only clauses watching a newly falsified literal are revisited, and each watcher moves to a non-false replacement when one exists. It branches on the first literal in the first unresolved clause and explores both values chronologically.
- It returns a complete model, a proof of unsatisfiability, or `Unknown` when its caller-supplied search-node budget is exhausted. This baseline does not implement conflict analysis, learned clauses, non-chronological backtracking, activity heuristics, or SMT theories. Worst-case runtime remains exponential; no industrial-scale performance claim is made.
- Exhaustive tests compare all 256 CNFs over two variables to a truth-assignment oracle. Another 1,024 deterministic three-variable formulas are checked by full assignment enumeration. DIMACS parsing, malformed-input paths, and Tseitin encodings are covered; the two-variable CNFs are also cross-checked against ROBDD canonical roots. Circuit-level SAT verification queries for counterexamples and does not treat `Unknown` as proof.
- `verify_sop_with_sat` compiles `(expected XOR selected_cover) AND care` to CNF. SAT returns the input portion of a counterexample model; UNSAT proves equivalence over cared rows; budget exhaustion and malformed covers remain distinct outcomes.

## Bounded QF_BV front end

- The `smt/` package models unsigned bit-vectors with widths from 1 through 8. Variable bits use consecutive source-variable IDs in least-significant-bit-first order; callers provide the total source-variable count when creating a problem.
- Supported terms are constants, variables, bitwise NOT/AND/OR/XOR, add/subtract modulo `2^width`, low-product multiplication modulo `2^width`, equality, and signed/unsigned less-than. Binary operations reject mismatched widths. Results are lowered to the existing Boolean-expression AST and Tseitin CNF encoder; the DPLL backend returns source-variable values without its auxiliary variables. `BitVec::evaluate` converts a term under a source model back to an unsigned value and returns `None` for missing source assignments.
- This is a bounded bit-blasting front end for a QF_BV fragment, not a native theory solver, SMT-LIB parser, or general-purpose SMT implementation. Signed division, unsigned division/remainder, shifts, concatenation, arrays, uninterpreted functions, and quantifiers are unsupported; signed ordering is supported. The underlying DPLL search remains exponential and can return `Unknown` at its configured budget.
- Tests check constructors and width mismatches, SAT/UNSAT/Unknown/invalid outcomes, a unique four-bit wraparound model, and every pair of two-bit operands for addition, subtraction, multiplication, bitwise operations, equality, and signed/unsigned comparison against concrete arithmetic results. The pinned-Z3 corpus covers widths 1–8 for each result-producing operator and each truth value of signed comparison.

## Refinement invariant

A cube stores a value mask and a wildcard mask. Two cubes merge only when their wildcard masks match and exactly one specified bit differs. Each merge round keeps one copy of each resulting shape. A cube is reported as prime after a round in which it cannot merge further; don't-care-only cubes are excluded from the reported prime list.

`refine` returns prime implicants for the cover selector described below.
Refinement alone does not select a cover. Exact cover selection minimizes the
two-level term/literal objective, not an arbitrary gate network, propagation
delay, or loading.

## Cover selection

The chart contains only required one-rows; don't-care rows may expand a prime but do not need coverage. A required row with one chart entry makes that prime essential. The exact selector starts with all primes as a valid upper bound, seeds the search with essential primes, then branches on the uncovered row with the fewest remaining coverers. It memoizes sorted selected-index states and uses a maximum-new-coverage lower bound to prune branches.

Covers are ranked by fewest product terms, then fewest total literals, then the lexicographically smallest sorted pattern list, with `- < 0 < 1`. The chart sorts patterns in that same order, so the final tie-break is stable.

## Product-of-sums selection

`minimize_pos(TruthSpec)` returns a separate `PosSolution`; `CoverSolution`,
`minimize_sop`, SOP verification, and SOP gate estimates retain their contracts.
The required zero rows become the complement's on-set, and the same don't-care
rows remain unconstrained. The existing exact SOP selector solves that
complement. De Morgan's law maps each selected product to one sum clause with
the same literal count, so minimizing complement products exactly minimizes
POS clause count and then total literals. This is a two-level objective, not
an arbitrary gate-network or package-count optimum. The same exponential
search limits apply; the 1–8 input bound is not a runtime guarantee.

`PosClause` stores its falsifying cube privately. Its pattern uses `0` for a
positive literal, `1` for a complemented literal, and `-` for an omitted input;
`01-` thus means `(A OR NOT B)`. These are **zero patterns**, unlike SOP product
patterns. Results use the lexicographically smallest sorted zero-pattern list
(`- < 0 < 1`) as the final tie-break. Essential clauses correspond to complement
prime-chart entries uniquely needed by a required zero row. `explored_states`
counts the complement selector's visited search states.

The product is an AND of OR clauses. An empty clause is false, and an empty
clause list is true. An all-zero function selects one all-dash empty clause;
an all-one function selects no clauses. With no required zero rows the result
is also true, including the fully unconstrained table. With required zeroes
but no required ones it selects constant false. Don't-care-only cubes add no
clauses, and different SOP/POS results may choose different don't-care values.
`evaluate(row)` returns the selected completion on don't-care rows and `None`
outside `0 <= row < 2^input_count`. Clause/essential accessors return copies so
caller mutation cannot invalidate the result or its counts.

POS black-box tests enumerate all 256 three-input Boolean functions, all
81 two-input and all 6,561 three-input ternary specifications (0, 1, don't-care). A separate oracle
enumerates all literal choices for valid sum clauses and uses subset dynamic
programming to find the minimum clause/literal cost without using refinement,
SOP selection, cube matching, or POS evaluation. Exported patterns are also
evaluated independently as literal ORs followed by AND. Targeted tests cover
tie-breaks, array copies, constants at every width 1–8, and eight-input endpoint
and most-significant-bit cases.

`verify_pos_with_bdd` and `verify_pos_with_sat` independently construct an AND
of literal OR clauses from the exported zero patterns, rather than checking
the complement SOP or calling the POS row evaluator. They compare it with the
required on-set while masking don't-care rows. The BDD check tests that the
masked XOR is false; the SAT check solves that mismatch with the existing
Tseitin/DPLL backend. Only UNSAT becomes `Equivalent`; SAT returns an MSB-first
input assignment, and exhausted search returns `Unknown(stats)`. A mismatched
input width is rejected as false / `InvalidInput`, including empty products.

All 256 three-input functions and all 6,561 three-input ternary specs pass
both symbolic checks. Every one of the 16 two-input Boolean completions is
also checked against each of the 81 ternary specs (1,296 comparisons); a
separate cared-row enumeration decides equivalence, and every returned SAT
witness is replayed through literal semantics and checked to be a cared row.
Symbolic boundary checks cover constants and fully unconstrained specs at
widths 1–8, eight-input witnesses, width rejection, and budget exhaustion.
These finite automated checks do not establish correctness for arbitrary
unbounded formulas or hardware behavior. POS gate estimates are not implemented.

## Application scope

- The [worked examples](circuits/WORKED.md) compare SOP and POS for three combinational circuits with explicit truth tables and BDD/SAT checks.
- SAT search uses deterministic chronological DPLL; conflict learning, non-chronological backtracking, and activity-based branching heuristics are not implemented.
- Gate/package estimation accepts SOP results and uses the direct AND/OR/NOT model below. POS estimates and NAND/NOR technology mapping are not implemented.
- The catalog supplies channel counts for package estimates. Pin-level wiring guidance and physical device qualification are outside the implemented scope.

## Two-level gate-count estimate

`estimate_sop_gate_cost` maps each selected product to a two-input AND tree and
joins multiple products with a two-input OR tree. An input complement is
counted once per variable and shared by every product that needs it. A single
literal or a one-product sum needs no AND or OR gate in this structural model.
`GateCost::packages_for` rounds a nonnegative channel count up to whole
packages; it does not choose a part.

The public `GateCost::new` rejects negative counts and totals that exceed the
signed 32-bit `Int32` range. Package rounding uses quotient and remainder so the
ceiling calculation does not overflow when the requested gate count is near
`Int32`'s maximum. Regression tests cover that numeric boundary and sparse
eight-input truth tables, including row 255 where the most significant bit is
set.

This estimate is intentionally limited to gate counts for a direct SOP
implementation. It does not perform technology mapping, exploit NAND/NOR
forms, share internal product subexpressions, estimate delay or power, check
fan-out, or account for board wiring and unused package inputs. The part
catalog records channel counts from manufacturer documentation, while a real
build still needs a selected package variant and datasheet-level electrical
checks.