Documentation

Complexitylib.Circuits.FormulaEncoding.Defs

Machine-facing encoding of Boolean formulas #

This file defines a canonical postfix encoding of BoolFormula. Six three-bit tags represent variables, constants, and connectives. A variable tag is followed by the existing terminated-unary natural code. The complete stream starts with its terminated-unary token count.

Postfix order makes decoding iterative: the parser first reads a flat token stream, then a stack machine reconstructs the formula. This avoids a recursive on-tape tree parser and gives the later Barrington generator a simple, self-delimiting input language.

source
inductive Complexity.FormulaCode.Token :
Type

Proof-free postfix tokens for Boolean formulas.

  • var (index : ℕ) : Token

    A variable with its natural-number index.

  • tru : Token

    The constant true.

  • fls : Token

    The constant false.

  • neg : Token

    Unary negation.

  • conj : Token

    Binary conjunction.

  • disj : Token

    Binary disjunction.

Instances For
    source
    @[implicit_reducible]
    instance Complexity.FormulaCode.instDecidableEqToken :
    DecidableEq Token
    Equations
    source
    def Complexity.FormulaCode.instDecidableEqToken.decEq (x✝ x✝¹ : Token) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      def Complexity.FormulaCode.instReprToken.repr :
      Token → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[implicit_reducible]
        instance Complexity.FormulaCode.instReprToken :
        Repr Token
        Equations
        source
        def Complexity.FormulaCode.Token.encode :
        Token → List Bool

        Serialize one postfix token. Tags 110 and 111 are reserved.

        Equations
        Instances For
          source
          def Complexity.FormulaCode.Token.decodePrefix? :
          List Bool → Option (Token × List Bool)

          Parse one token prefix and return the unused suffix.

          Equations
          Instances For
            source
            def Complexity.FormulaCode.Token.codeLength :
            Token → ℕ

            The exact number of bits in a token encoding.

            Equations
            Instances For
              source
              def Complexity.FormulaCode.Token.apply? :
              Token → List BoolFormula → Option (List BoolFormula)

              Apply one postfix token to a formula stack.

              Equations
              Instances For
                source
                def Complexity.FormulaCode.tokens :
                BoolFormula → List Token

                Canonical postfix tokens of a formula.

                Equations
                Instances For
                  source
                  def Complexity.FormulaCode.run? :
                  List Token → List BoolFormula → Option (List BoolFormula)

                  Execute a postfix token stream from an initial formula stack.

                  Equations
                  Instances For
                    source
                    def Complexity.FormulaCode.build? (stream : List Token) :
                    Option BoolFormula

                    Reconstruct exactly one formula from a postfix token stream.

                    Equations
                    Instances For
                      source
                      def Complexity.FormulaCode.decodeTokens? :
                      ℕ → List Bool → Option (List Token × List Bool)

                      Decode exactly count token prefixes and return the unused bit suffix.

                      Equations
                      Instances For
                        source
                        def Complexity.FormulaCode.encode (formula : BoolFormula) :
                        List Bool

                        Canonically encode a Boolean formula.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Complexity.FormulaCode.decodePrefix? (bits : List Bool) :
                          Option (BoolFormula × List Bool)

                          Decode one complete formula prefix and return the unused suffix.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Complexity.FormulaCode.decode? (bits : List Bool) :
                            Option BoolFormula

                            Decode exactly one formula. Trailing bits are rejected.

                            Equations
                            Instances For