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

@[inline]

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

Equations

• Std.Tactic.BVDecide.LRAT.Parser.Text.skipNewline = HOrElse.hOrElse (Std.Internal.Parsec.ByteArray.skipByteChar '\n') fun (x : Unit) => Std.Internal.Parsec.ByteArray.skipString "\x0d\n"

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parsePos : Std.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 : Std.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 : Std.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 : Std.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 : Std.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

@[inline]

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

Equations

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

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

Equations

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseLit : Std.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 : Std.Internal.Parsec.ByteArray.Parser (Array Int)

Equations

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseClause.litWs : Std.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.parseRes : Std.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) : Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction

Equations

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

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

Equations

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

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

Equations

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

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseZero : Std.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 : Std.Internal.Parsec.ByteArray.Parser Int

Equations

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

partial def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit.go (uidx : UInt64) (shift : UInt64) : Std.Internal.Parsec.ByteArray.Parser Int

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseNeg : Std.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 : Std.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 : Std.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 : Std.Internal.Parsec.ByteArray.Parser α) : Std.Internal.Parsec.ByteArray.Parser (Array α)

Equations

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

@[specialize #[]]

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

@[specialize #[]]

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

Equations

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

@[specialize #[]]

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseIdList : Std.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 : Std.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 : Std.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 : Std.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 : Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction

Equations

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

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

Equations

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

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

Equations

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

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseActions : Std.Internal.Parsec.ByteArray.Parser (Array Std.Tactic.BVDecide.LRAT.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 : Std.Internal.Parsec.ByteArray.Parser (Array Std.Tactic.BVDecide.LRAT.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 : Lake.FilePath) : IO (Array Std.Tactic.BVDecide.LRAT.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 Std.Tactic.BVDecide.LRAT.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 Std.Tactic.BVDecide.LRAT.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.lratProofToString.serialize (a : Std.Tactic.BVDecide.LRAT.IntAction) : String

Equations

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

def Std.Tactic.BVDecide.LRAT.lratProofToString.serializeIdList (ids : Array Nat) : String

Equations

• Std.Tactic.BVDecide.LRAT.lratProofToString.serializeIdList ids = Array.foldl (fun (x1 : String) (x2 : Nat) => x1 ++ (toString "" ++ toString x2 ++ toString " ")) "" ids

def Std.Tactic.BVDecide.LRAT.lratProofToString.serializeClause (clause : Array Int) : String

Equations

• Std.Tactic.BVDecide.LRAT.lratProofToString.serializeClause clause = Array.foldl (fun (x1 : String) (x2 : Int) => x1 ++ (toString "" ++ toString x2 ++ toString " ")) "" clause

def Std.Tactic.BVDecide.LRAT.lratProofToString.serializeRatHint (hint : Nat × Array Nat) : String

Equations

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

def Std.Tactic.BVDecide.LRAT.lratProofToString.serializeRatHints (hints : Array (Nat × Array Nat)) : String

Equations

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

def Std.Tactic.BVDecide.LRAT.lratProofToBinary (proof : Array Std.Tactic.BVDecide.LRAT.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.mkEmpty (4 * proof.size))

partial def Std.Tactic.BVDecide.LRAT.lratProofToBinary.go (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) (idx : Nat) (acc : ByteArray) : ByteArray

def Std.Tactic.BVDecide.LRAT.lratProofToBinary.addInt (acc : ByteArray) (lit : Int) : ByteArray

Equations

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

partial def Std.Tactic.BVDecide.LRAT.lratProofToBinary.variableLengthEncode (acc : ByteArray) (lit : UInt64) : ByteArray

@[inline]

def Std.Tactic.BVDecide.LRAT.lratProofToBinary.startAdd (acc : ByteArray) : ByteArray

Equations

• Std.Tactic.BVDecide.LRAT.lratProofToBinary.startAdd acc = acc.push 'a'.toUInt8

@[inline]

def Std.Tactic.BVDecide.LRAT.lratProofToBinary.startDelete (acc : ByteArray) : ByteArray

Equations

• Std.Tactic.BVDecide.LRAT.lratProofToBinary.startDelete acc = acc.push 'd'.toUInt8

@[inline]

def Std.Tactic.BVDecide.LRAT.lratProofToBinary.zeroByte (acc : ByteArray) : ByteArray

Equations

• Std.Tactic.BVDecide.LRAT.lratProofToBinary.zeroByte acc = acc.push 0

@[inline]

def Std.Tactic.BVDecide.LRAT.lratProofToBinary.addNat (acc : ByteArray) (n : Nat) : ByteArray

Equations

• Std.Tactic.BVDecide.LRAT.lratProofToBinary.addNat acc n = Std.Tactic.BVDecide.LRAT.lratProofToBinary.addInt acc ↑n

def Std.Tactic.BVDecide.LRAT.dumpLRATProof (path : Lake.FilePath) (proof : Array Std.Tactic.BVDecide.LRAT.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.