Batch compilation of Boolean formulas

This file defines small finite conjunction and disjunction constructors and a proof-free batch compiler for BoolFormula. Every formula in a batch is compiled against the same incoming wire prefix. The individual formula outputs are then copied into one contiguous block, in list order.

The contiguous block is the key interface for clients that represent a structured value by many Boolean formulas: later fragments can address the result by a base wire and an index without retaining the variable-sized offset of every formula tree.

def Complexity.BoolFormula.literal (wire : ℕ) (value : Bool) : BoolFormula

A Boolean literal testing whether an existing wire has the requested value.

Equations

• Complexity.BoolFormula.literal wire value = if value = true then Complexity.BoolFormula.var wire else (Complexity.BoolFormula.var wire).neg

def Complexity.BoolFormula.conjs : List BoolFormula → BoolFormula

Conjoin a finite list of formulas. The empty conjunction is true.

Equations

• Complexity.BoolFormula.conjs [] = Complexity.BoolFormula.tru
• Complexity.BoolFormula.conjs (formula :: formulas) = formula.conj (Complexity.BoolFormula.conjs formulas)

def Complexity.BoolFormula.disjs : List BoolFormula → BoolFormula

Disjoin a finite list of formulas. The empty disjunction is false.

Equations

• Complexity.BoolFormula.disjs [] = Complexity.BoolFormula.fls
• Complexity.BoolFormula.disjs (formula :: formulas) = formula.disj (Complexity.BoolFormula.disjs formulas)

structure Complexity.BoolFormula.RawBatchBuild : Type

Raw formulas compiled in sequence, together with their absolute output wires.

• circuit : CircuitCode.RawCircuit

  The concatenated formula fragments, before output packing.

• outputs : List ℕ

  One absolute output wire per source formula, in source order.

def Complexity.BoolFormula.compileRawOutputs (available : ℕ) : List BoolFormula → RawBatchBuild

Compile formulas successively, recording each variable-sized output wire.

Every formula may refer only to wires in the prefix present at the start of the whole batch. The increasing available parameter is used solely to place the emitted fragments after one another.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BoolFormula.compileRawOutputs available [] = { circuit := [], outputs := [] }

def Complexity.BoolFormula.rawBatchOutputBase (available : ℕ) (formulas : List BoolFormula) : ℕ

First wire of the packed output block of a formula batch.

Equations

• Complexity.BoolFormula.rawBatchOutputBase available formulas = available + (List.map Complexity.BoolFormula.size formulas).sum

def Complexity.BoolFormula.compileRawBatch (available : ℕ) (formulas : List BoolFormula) : CircuitCode.RawCircuit

Compile formulas successively and copy their results into a contiguous block.

Equations

• One or more equations did not get rendered due to their size.