def Trestle.HashAssn {ν : Type u_1} (L : Type u) [LitVar L ν] [BEq ν] [Hashable ν] : Type u_1

Partial assignment implementation backed by Std.HashMap.

Good for sparse partial assignments.

Equations

• Trestle.HashAssn L = Std.HashMap ν Bool

def Trestle.HashAssn.empty {L : Type u} {ν : Type v} [LitVar L ν] [BEq ν] [Hashable ν] : HashAssn L

Equations

• Trestle.HashAssn.empty = Std.HashMap.emptyWithCapacity

def Trestle.HashAssn.set {L : Type u} {ν : Type v} [LitVar L ν] [BEq ν] [Hashable ν] (self : HashAssn L) (l : L) : HashAssn L

Equations

• self.set l = Std.HashMap.insert self (Trestle.LitVar.toVar l) (Trestle.LitVar.polarity l)

def Trestle.HashAssn.toLitArray {L : Type u} {ν : Type v} [LitVar L ν] [BEq ν] [Hashable ν] (self : HashAssn L) : Array L

Equations

• self.toLitArray = Array.map (fun (x : ν × Bool) => match x with | (a, b) => Trestle.LitVar.mkLit L a b) (Std.HashMap.toArray self)

instance Trestle.HashAssn.instToString {L : Type u} {ν : Type v} [LitVar L ν] [BEq ν] [Hashable ν] [ToString L] : ToString (HashAssn L)

Equations

• Trestle.HashAssn.instToString = { toString := fun (a : Trestle.HashAssn L) => Std.HashMap.fold (fun (s : String) (v : ν) (b : Bool) => s ++ toString (Trestle.LitVar.mkLit L v b)) "" a }