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 :

Std.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")

Instances For

source

@[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

Instances For

source

@[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)

Instances For

source

@[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

Instances For

source

@[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'

Instances For

source

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

Instances For

source

@[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.

Instances For

source

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.

Instances For

source

@[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.

Instances For

source

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.

Instances For

source

@[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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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 #[]

Instances For

source

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)

source

@[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

Instances For

source

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

Instances For

source

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

Std.Internal.Parsec.ByteArray.Parser Int

source

@[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.

Instances For

source

@[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.

Instances For

source

@[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

Instances For

source

@[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 #[]

Instances For

source

@[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 α)

source

@[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 #[]

Instances For

source

@[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 α)

source

@[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

Instances For

source

@[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

Instances For

source

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)

Instances For

source

@[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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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

Instances For

source

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.

Instances For

source

def Std.Tactic.BVDecide.LRAT.loadLRATProof (path : System.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.

Instances For

source

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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

Instances For

source

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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))

Instances For

source

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

ByteArray

source

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.

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

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

Instances For

source

@[inline]

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

ByteArray

Equations

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

Instances For

source

@[inline]

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

ByteArray

Equations

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

Instances For

source

@[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

Instances For

source

def Std.Tactic.BVDecide.LRAT.dumpLRATProof (path : System.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.

Instances For