Std.Tactic.BVDecide.LRAT.Parser

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

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.skipNewline :

Internal.Parsec.ByteArray.Parser Unit

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parsePos :

Internal.Parsec.ByteArray.Parser Nat

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseNeg :

Internal.Parsec.ByteArray.Parser Int

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseId :

Internal.Parsec.ByteArray.Parser Nat

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseZero :

Internal.Parsec.ByteArray.Parser Unit

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseIdList :

Internal.Parsec.ByteArray.Parser (Array Nat)

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseIdList.idWs :

Internal.Parsec.ByteArray.Parser Nat

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseDelete :

Internal.Parsec.ByteArray.Parser IntAction

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseLit :

Internal.Parsec.ByteArray.Parser Int

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseClause :

Internal.Parsec.ByteArray.Parser (Array Int)

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseClause.litWs :

Internal.Parsec.ByteArray.Parser Int

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseRes :

Internal.Parsec.ByteArray.Parser (Nat × Array Nat)

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseRat (ident : Nat) :

Internal.Parsec.ByteArray.Parser IntAction

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseAction :

Internal.Parsec.ByteArray.Parser IntAction

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Text.parseActions :

Internal.Parsec.ByteArray.Parser (Array IntAction)

Equations

Instances For

source

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

Internal.Parsec.ByteArray.Parser (Array IntAction)

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseZero :

Internal.Parsec.ByteArray.Parser Unit

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit :

Internal.Parsec.ByteArray.Parser Int

Equations

Instances For

source

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

Internal.Parsec.ByteArray.Parser Int

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseNeg :

Internal.Parsec.ByteArray.Parser Nat

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parsePos :

Internal.Parsec.ByteArray.Parser Nat

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseId :

Internal.Parsec.ByteArray.Parser Nat

Equations

Instances For

source

@[specialize #[]]

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

Internal.Parsec.ByteArray.Parser (Array α)

Equations

Instances For

source

@[specialize #[]]

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

Internal.Parsec.ByteArray.Parser (Array α)

source

@[specialize #[]]

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

Internal.Parsec.ByteArray.Parser (Array α)

Equations

Instances For

source

@[specialize #[]]

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

Internal.Parsec.ByteArray.Parser (Array α)

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseIdList :

Internal.Parsec.ByteArray.Parser (Array Nat)

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseClause :

Internal.Parsec.ByteArray.Parser (Array Int)

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRes :

Internal.Parsec.ByteArray.Parser (Nat × Array Nat)

Equations

Instances For

source

@[inline]

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRatHints :

Internal.Parsec.ByteArray.Parser (Array (Nat × Array Nat))

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction :

Internal.Parsec.ByteArray.Parser IntAction

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction.parseAdd :

Internal.Parsec.ByteArray.Parser IntAction

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction.parseDelete :

Internal.Parsec.ByteArray.Parser IntAction

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.Parser.Binary.parseActions :

Internal.Parsec.ByteArray.Parser (Array IntAction)

Equations

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

String

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

Equations

Instances For

source

def Std.Tactic.BVDecide.LRAT.lratProofToString.serialize (a : IntAction) :

String

Equations

Instances For

source

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

String

Equations

Instances For

source

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

String

Equations

Instances For

source

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

String

Equations

Instances For

source

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

String

Equations

Instances For

source

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

ByteArray

Serialize proof into the binary LRAT format as a ByteArray.

Equations

Instances For

source

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

ByteArray

source

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

ByteArray

Equations

Instances For

source

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

ByteArray

source

@[inline]

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

ByteArray

Equations

Instances For

source

@[inline]

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

ByteArray

Equations

Instances For

source

@[inline]

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

ByteArray

Equations

Instances For

source

@[inline]

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

ByteArray

Equations

Instances For

source

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

Instances For