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

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Nat

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Int

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Nat

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Unit

Instances For

source

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

Internal.Parsec.ByteArray.Parser (Array Nat)

Instances For

source

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

Internal.Parsec.ByteArray.Parser IntAction

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Int

Instances For

source

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

Internal.Parsec.ByteArray.Parser (Array Int)

Instances For

source

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

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

Instances For

source

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

Internal.Parsec.ByteArray.Parser IntAction

Instances For

source

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

Internal.Parsec.ByteArray.Parser IntAction

Instances For

source

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

Internal.Parsec.ByteArray.Parser (Array IntAction)

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Unit

Instances For

source

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

Internal.Parsec.ByteArray.Parser Int

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Nat

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Nat

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser Nat

Instances For

source

@[specialize #[]]

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

Internal.Parsec.ByteArray.Parser (Array α)

Instances For

source

@[specialize #[]]

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

Internal.Parsec.ByteArray.Parser (Array α)

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser (Array Nat)

Instances For

source

@[inline]

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

Internal.Parsec.ByteArray.Parser (Array Int)

Instances For

source

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

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

Instances For

source

@[inline]

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

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

Instances For

source

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

Internal.Parsec.ByteArray.Parser IntAction

Instances For

source

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

Internal.Parsec.ByteArray.Parser (Array IntAction)

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.

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.

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.

Instances For

source

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

String

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

Instances For

source

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

ByteArray

Serialize proof into the binary LRAT format as a ByteArray.

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.

Instances For