class Duper.MStream (m : Type (max u_1 u_2) → Type u_3) [Monad m] (stream : Type u_1) (value : outParam (Type u_2)) : Type (max u_1 u_3)

• next? : stream → m (Option (value × stream))

@[reducible, inline]

abbrev Duper.OptionMStream (m : Type (max u_1 u_2) → Type u_3) [Monad m] (stream : Type u_2) (value : Type u_1) : Type (max u_2 u_3)

Equations

• Duper.OptionMStream m stream value = Duper.MStream m stream (Option value)

structure Duper.IdStrategyHeap (σ : Type w) {β : Type v} : Type (max v w)

• map : Std.HashMap Nat (Array Nat × σ)
• heaps : Array (Batteries.BinomialHeap (Nat × Nat) fun (c d : Nat × Nat) => decide (c.fst ≤ d.fst))
• nextId : Nat
• status : β

instance Duper.instInhabitedIdStrategyHeap {a✝ : Type u_1} {a✝¹ : Type u_2} [Inhabited a✝¹] : Inhabited (IdStrategyHeap a✝)

Equations

• Duper.instInhabitedIdStrategyHeap = { default := { map := default, heaps := default, nextId := default, status := default } }

def Duper.IdStrategyHeap.isEmpty {σ : Type u_1} {β : Type u_2} (oh : IdStrategyHeap σ) : Bool

Equations

• oh.isEmpty = oh.map.isEmpty

def Duper.IdStrategyHeap.size {σ : Type u_1} {β : Type u_2} (oh : IdStrategyHeap σ) : Nat

Equations

• oh.size = oh.map.size

def Duper.IdStrategyHeap.contains {σ : Type u_1} {β : Type u_2} (oh : IdStrategyHeap σ) (id : Nat) : Bool

Equations

• oh.contains id = oh.map.contains id

structure Duper.ClauseStreamHeapStatus : Type

• nProbed : Std.HashMap Nat Nat
• fairnessCounter : Nat

def Duper.ClauseStreamHeapStatus.insertNProbed (cshs : ClauseStreamHeapStatus) (id nProbed : Nat) : ClauseStreamHeapStatus

Equations

• cshs.insertNProbed id nProbed = { nProbed := cshs.nProbed.insert id nProbed, fairnessCounter := cshs.fairnessCounter }

def Duper.ClauseStreamHeapStatus.eraseNProbed (cshs : ClauseStreamHeapStatus) (id : Nat) : ClauseStreamHeapStatus

Equations

• cshs.eraseNProbed id = { nProbed := cshs.nProbed.erase id, fairnessCounter := cshs.fairnessCounter }

@[reducible, inline]

abbrev Duper.ClauseStreamHeap (σ : Type u_1) : Type u_1

Equations

• Duper.ClauseStreamHeap σ = Duper.IdStrategyHeap σ

@[inline]

def Duper.ClauseStreamHeap.increaseFairnessCounter {σ : Type u_1} (Q : ClauseStreamHeap σ) : IdStrategyHeap σ

Equations

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

@[reducible, inline]

abbrev Duper.ClauseStreamHeap.empty (σ : Type u_1) : ClauseStreamHeap σ

Equations

• Duper.ClauseStreamHeap.empty σ = { heaps := #[Batteries.BinomialHeap.empty, Batteries.BinomialHeap.empty], nextId := 0, status := { } }

@[inline]

def Duper.ClauseStreamHeap.insertWithNProbed {σ : Type u_1} (csh : ClauseStreamHeap σ) (x : σ) (ns : Array Nat) (nProbed : Nat) : ClauseStreamHeap σ

Equations

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

@[inline]

def Duper.ClauseStreamHeap.eraseWithNProbed {σ : Type u_1} (csh : ClauseStreamHeap σ) (id : Nat) : IdStrategyHeap σ

Equations

• csh.eraseWithNProbed id = { map := csh.map.erase id, heaps := csh.heaps, nextId := csh.nextId, status := csh.status.eraseNProbed id }

@[inline]

def Duper.ClauseStreamHeap.deleteMinWithNProbed {σ : Type} (oh : ClauseStreamHeap σ) (n : Nat) : Option ((Nat × Array Nat × σ) × ClauseStreamHeap σ)

Equations

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