This module implements parsers and serializers for both the binary and non-binary LRAT format.

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.skipNewline : Internal.Parsec.ByteArray.Parser Unit

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.skipNewline = (Std.Internal.Parsec.ByteArray.skipByteChar '\n' <|> Std.Internal.Parsec.ByteArray.skipString "\x0d\n")

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parsePos : Internal.Parsec.ByteArray.Parser Nat

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.parsePos = do let ident ← Std.Internal.Parsec.ByteArray.digits if (ident == 0) = true then Std.Internal.Parsec.fail "id was 0" else pure ident

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseNeg : Internal.Parsec.ByteArray.Parser Int

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.parseNeg = do Std.Internal.Parsec.ByteArray.skipByteChar '-' let nat ← Std.Tactic.BVDecide.LRAT.Parser.Text.parsePos pure (-↑nat)

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseId : Internal.Parsec.ByteArray.Parser Nat

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.parseId = Std.Tactic.BVDecide.LRAT.Parser.Text.parsePos

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseZero : Internal.Parsec.ByteArray.Parser Unit

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.parseZero = Std.Internal.Parsec.ByteArray.skipByteChar '0'

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseIdList : Internal.Parsec.ByteArray.Parser (Array Nat)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.parseIdList = Std.Internal.Parsec.many Std.Tactic.BVDecide.LRAT.Parser.Text.parseIdList.idWs✝

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseDelete : Internal.Parsec.ByteArray.Parser IntAction

Equations

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseLit : Internal.Parsec.ByteArray.Parser Int

Equations

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

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseClause : Internal.Parsec.ByteArray.Parser (Array Int)

Equations

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

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseRes : Internal.Parsec.ByteArray.Parser (Nat × Array Nat)

Equations

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

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseRat (ident : Nat) : Internal.Parsec.ByteArray.Parser IntAction

Equations

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

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseAction : Internal.Parsec.ByteArray.Parser IntAction

Equations

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

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseActions : Internal.Parsec.ByteArray.Parser (Array IntAction)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.parseActions = Std.Tactic.BVDecide.LRAT.Parser.Text.parseActions.go✝ #[]

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseZero : Internal.Parsec.ByteArray.Parser Unit

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseZero = Std.Internal.Parsec.ByteArray.skipByte 0

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit : Internal.Parsec.ByteArray.Parser Int

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit = Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit.go✝ 0 0

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseNeg : Internal.Parsec.ByteArray.Parser Nat

Equations

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parsePos : Internal.Parsec.ByteArray.Parser Nat

Equations

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseId : Internal.Parsec.ByteArray.Parser Nat

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseId = Std.Tactic.BVDecide.LRAT.Parser.Binary.parsePos

@[specialize #[]]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillZero {α : Type} (parser : Internal.Parsec.ByteArray.Parser α) : Internal.Parsec.ByteArray.Parser (Array α)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillZero parser = Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillZero.go✝ parser #[]

@[specialize #[]]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillNegOrZero {α : Type} (parser : Internal.Parsec.ByteArray.Parser α) : Internal.Parsec.ByteArray.Parser (Array α)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillNegOrZero parser = Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillNegOrZero.go✝ parser #[]

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseIdList : Internal.Parsec.ByteArray.Parser (Array Nat)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseIdList = Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillNegOrZero Std.Tactic.BVDecide.LRAT.Parser.Binary.parseId

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseClause : Internal.Parsec.ByteArray.Parser (Array Int)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseClause = Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillZero Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRes : Internal.Parsec.ByteArray.Parser (Nat × Array Nat)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRes = do let lhs ← Std.Tactic.BVDecide.LRAT.Parser.Binary.parseNeg let idents ← Std.Tactic.BVDecide.LRAT.Parser.Binary.parseIdList pure (lhs, idents)

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRatHints : Internal.Parsec.ByteArray.Parser (Array (Nat × Array Nat))

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRatHints = Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillZero Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRes

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction : Internal.Parsec.ByteArray.Parser IntAction

Equations

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

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseActions : Internal.Parsec.ByteArray.Parser (Array IntAction)

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Binary.parseActions = do let actions ← Std.Internal.Parsec.many Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction Std.Internal.Parsec.eof pure actions

def Std.Tactic.BVDecide.LRAT.Parser.parseActions : Internal.Parsec.ByteArray.Parser (Array IntAction)

Based on the first byte parses the input either as a binary or non-binary LRAT.

Equations

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

def Std.Tactic.BVDecide.LRAT.loadLRATProof (path : System.FilePath) : IO (Array IntAction)

Read and parse an LRAT proof from path. path may contain either the binary or the non-binary LRAT format.

Equations

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

def Std.Tactic.BVDecide.LRAT.parseLRATProof (proof : ByteArray) : Except String (Array IntAction)

Parse proof as an LRAT proof. proof may contain either the binary or the non-binary LRAT format.

Equations

• Std.Tactic.BVDecide.LRAT.parseLRATProof proof = Std.Tactic.BVDecide.LRAT.Parser.parseActions.run proof

def Std.Tactic.BVDecide.LRAT.lratProofToString (proof : Array IntAction) : String

Serialize proof into the non-binary LRAT format as a String.

Equations

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

def Std.Tactic.BVDecide.LRAT.lratProofToBinary (proof : Array IntAction) : ByteArray

Serialize proof into the binary LRAT format as a ByteArray.

Equations

• Std.Tactic.BVDecide.LRAT.lratProofToBinary proof = Std.Tactic.BVDecide.LRAT.lratProofToBinary.go✝ proof 0 (ByteArray.emptyWithCapacity (4 * proof.size))

def Std.Tactic.BVDecide.LRAT.dumpLRATProof (path : System.FilePath) (proof : Array IntAction) (binaryProofs : Bool) : IO Unit

Dump proof into path, either in the binary or non-binary LRAT format, depending on binaryProofs.

Equations

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