Bags

The Lean type denoting an SMT bag: a Std.TreeMap from elements to their multiplicity, so the element type must be ordered. Multiplicities are positive: the functions below drop an element whose multiplicity reaches zero, and subtraction stops there, as SMT's bag difference does.

Converting a bag to a term and back is done by Cvc.Untyped.Theory.Bag and Cvc.Typed.Theory.Bag.

@[reducible, inline]

abbrev Cvc.Bag (α : Type) [Ord α] : Type

An SMT bag (multiset): each element's multiplicity, absent elements standing for zero.

Equations

• Cvc.Bag α = Std.TreeMap α Nat compare

def Cvc.Bag.empty {α : Type} [Ord α] : Bag α

The empty bag.

Equations

• Cvc.Bag.empty = Std.TreeMap.empty

def Cvc.Bag.alter {α : Type} [Ord α] (bag : Bag α) (key : α) (f : Nat → Nat) : Bag α

Applies f to an element's multiplicity, removing the element when the result is zero.

Equations

• bag.alter key f = Std.TreeMap.alter bag key fun (val? : Option Nat) => match f (val?.getD 0) with | 0 => none | n => some n

def Cvc.Bag.increment {α : Type} [Ord α] (bag : Bag α) (key : α) : Bag α

Adds one occurrence of an element.

Equations

• bag.increment key = bag.alter key fun (x : Nat) => x + 1

def Cvc.Bag.decrement {α : Type} [Ord α] (bag : Bag α) (key : α) : Bag α

Removes one occurrence of an element, if any.

Equations

• bag.decrement key = bag.alter key fun (x : Nat) => x - 1

def Cvc.Bag.add {α : Type} [Ord α] (bag : Bag α) (key : α) (n : Nat) : Bag α

Adds n occurrences of an element.

Equations

• bag.add key n = bag.alter key fun (x : Nat) => x + n

def Cvc.Bag.sub {α : Type} [Ord α] (bag : Bag α) (key : α) (n : Nat) : Bag α

Removes n occurrences of an element, or all of them if it has fewer.

Equations

• bag.sub key n = bag.alter key fun (x : Nat) => x - n

def Cvc.Bag.get? {α : Type} [Ord α] (bag : Bag α) (key : α) : Option Nat

An element's multiplicity, none if absent.

Equations

• bag.get? key = Std.TreeMap.get? bag key

def Cvc.Bag.get {α : Type} [Ord α] (bag : Bag α) (key : α) : Nat

An element's multiplicity, zero if absent.

Equations

• bag.get key = (bag.get? key).getD 0

def Cvc.Bag.contains {α : Type} [Ord α] (bag : Bag α) (key : α) : Bool

Whether an element's multiplicity is positive.

Equations

• bag.contains key = decide (0 < bag.get key)

@[reducible, inline]

abbrev Cvc.Bag.mem {α : Type} [Ord α] (bag : Bag α) (key : α) : Prop

Equations

• bag.mem key = (bag.contains key = true)

@[instance_reducible]

instance Cvc.Bag.instMembership {α : Type} [Ord α] : Membership α (Bag α)

Equations

• Cvc.Bag.instMembership = { mem := Cvc.Bag.mem }

theorem Cvc.Bag.mem_def {α : Type} [Ord α] (bag : Bag α) {key : α} : (key ∈ bag) = (bag.contains key = true)

@[instance_reducible]

instance Cvc.Bag.instDecidableMem {α : Type} [Ord α] (bag : Bag α) (key : α) : Decidable (key ∈ bag)

Equations

• bag.instDecidableMem key = ⋯ ▸ if h : bag.contains key = true then isTrue h else isFalse h

def Cvc.Bag.toString {α : Type} [Ord α] [ToString α] (bag : Bag α) : String

Equations

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

@[instance_reducible]

instance Cvc.Bag.instToString {α : Type} [Ord α] [ToString α] : ToString (Bag α)

Equations

• Cvc.Bag.instToString = { toString := Cvc.Bag.toString }

@[instance_reducible]

instance Cvc.Bag.instToTyp {α : Type} [Ord α] [A : ToTyp α] : ToTyp (Bag α)

Equations

• Cvc.Bag.instToTyp = { typ := Cvc.Typ.bag (Cvc.Typ?.typ (Cvc.ToTyp.typ α)) }

def Cvc.Bag.compare {α : Type} [Ord α] (b1 b2 : Bag α) : Ordering

Equations

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

@[instance_reducible]

instance Cvc.Bag.instOrd {α : Type} [Ord α] : Ord (Bag α)

Equations

• Cvc.Bag.instOrd = { compare := Cvc.Bag.compare }