Documentation

Complexitylib.Models.RandomAccessMachine.Structured.ThreeSATSyntax.Defs

Structured RAM exact-3-CNF syntax scanner — definitions #

This is the larger typed-scanner benchmark: the existing 27-state bit-level 3-CNF syntax automaton is compiled without a handwritten numeric transition table or benchmark-specific execution invariant.

source
@[implicit_reducible]
instance Complexity.RAM.Structured.ThreeSATSyntax.instFinEnumTokenState :
FinEnum SAT.ThreeSAT.Syntax.TokenState
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
instance Complexity.RAM.Structured.ThreeSATSyntax.instFinEnumBitState :
FinEnum SAT.ThreeSAT.Syntax.BitState
Equations
  • One or more equations did not get rendered due to their size.
source
def Complexity.RAM.Structured.ThreeSATSyntax.spec :
Scanner.TypedSpec SAT.ThreeSAT.Syntax.BitState

The existing exact-3-CNF syntax automaton as a typed scanner specification.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.RAM.Structured.ThreeSATSyntax.verdictReg :
    ℕ

    Final verdict register inherited from the scanner layout.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Complexity.RAM.Structured.ThreeSATSyntax.inputStore :
      List Bool → Store

      Reserved-prefix input store for the syntax scanner.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Complexity.RAM.Structured.ThreeSATSyntax.program :
        Cmd

        Structured RAM exact-3-CNF syntax program.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Complexity.RAM.Structured.ThreeSATSyntax.compiled :
          Program

          Concrete compiled RAM exact-3-CNF syntax program.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Complexity.RAM.Structured.ThreeSATSyntax.stepCount :
            ℕ → ℕ

            Exact compiled transition count.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Complexity.RAM.Structured.ThreeSATSyntax.timeBound :
              ℕ → ℕ

              Explicit logarithmic-time budget.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Complexity.RAM.Structured.ThreeSATSyntax.spaceBound :
                ℕ → ℕ

                Explicit peak-space budget.

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Complexity.RAM.Structured.ThreeSATSyntax.quasilinearBound :
                  ℕ → ℕ

                  Shifted quasilinear comparison function.

                  Equations
                  Instances For