structure Duper.MClause : Type

• lits : Array Lit

instance Duper.instInhabitedMClause : Inhabited MClause

Equations

• Duper.instInhabitedMClause = { default := Duper.instInhabitedMClause.default }

def Duper.instInhabitedMClause.default : MClause

Equations

• Duper.instInhabitedMClause.default = { lits := default }

def Duper.instBEqMClause.beq : MClause → MClause → Bool

Equations

• Duper.instBEqMClause.beq { lits := a } { lits := b } = (a == b)
• Duper.instBEqMClause.beq x✝¹ x✝ = false

instance Duper.instBEqMClause : BEq MClause

Equations

• Duper.instBEqMClause = { beq := Duper.instBEqMClause.beq }

def Duper.instHashableMClause.hash : MClause → UInt64

Equations

• Duper.instHashableMClause.hash { lits := a } = mixHash 0 (hash a)

instance Duper.instHashableMClause : Hashable MClause

Equations

• Duper.instHashableMClause = { hash := Duper.instHashableMClause.hash }

def Duper.MClause.toExpr (c : MClause) : Lean.Expr

Equations

• c.toExpr = Duper.MClause.toExpr.litsToExpr c.lits.toList

def Duper.MClause.toExpr.litsToExpr : List Lit → Lean.Expr

Equations

• Duper.MClause.toExpr.litsToExpr [] = Lean.mkConst `False
• Duper.MClause.toExpr.litsToExpr [l] = l.toExpr
• Duper.MClause.toExpr.litsToExpr (l :: ls) = Lean.mkApp2 (Lean.mkConst `Or) l.toExpr (Duper.MClause.toExpr.litsToExpr ls)

def Duper.MClause.fromExpr (e : Lean.Expr) : MClause

Equations

• Duper.MClause.fromExpr e = { lits := (Duper.MClause.fromExpr.litsFromExpr e).toArray }

def Duper.MClause.fromExpr.litsFromExpr : Lean.Expr → List Lit

Equations

• Duper.MClause.fromExpr.litsFromExpr (((Lean.Expr.const `Or us).app litexpr).app other) = Duper.Lit.fromExpr litexpr :: Duper.MClause.fromExpr.litsFromExpr other
• Duper.MClause.fromExpr.litsFromExpr (Lean.Expr.const `False us) = []
• Duper.MClause.fromExpr.litsFromExpr x✝ = [Duper.Lit.fromExpr x✝]

def Duper.MClause.appendLits (c : MClause) (lits : Array Lit) : MClause

Equations

• c.appendLits lits = { lits := c.lits.append lits }

def Duper.MClause.eraseLit (c : MClause) (idx : Nat) : MClause

Equations

• c.eraseLit idx = { lits := c.lits.eraseIdxIfInBounds idx }

def Duper.MClause.replaceLit? (c : MClause) (idx : Nat) (l : Lit) : Option MClause

Equations

• c.replaceLit? idx l = if idx ≥ c.lits.size then none else some { lits := c.lits.set! idx l }

def Duper.MClause.replaceLit! (c : MClause) (idx : Nat) (l : Lit) : MClause

Equations

• c.replaceLit! idx l = { lits := c.lits.set! idx l }

def Duper.MClause.map (f : Lean.Expr → Lean.Expr) (c : MClause) : MClause

Equations

• Duper.MClause.map f c = { lits := Array.map (fun (l : Duper.Lit) => Duper.Lit.map f l) c.lits }

def Duper.MClause.mapWithPos (f : Lean.Expr → Lean.Expr × Array ExprPos) (c : MClause) : MClause × Array ClausePos

Equations

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

def Duper.MClause.mapMWithPos {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (f : Lean.Expr → m (Lean.Expr × Array ExprPos)) (c : MClause) : m (MClause × Array ClausePos)

Equations

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

def Duper.MClause.mapM {m : Type → Type w} [Monad m] (f : Lean.Expr → m Lean.Expr) (c : MClause) : m MClause

Equations

• Duper.MClause.mapM f c = do let __do_lift ← Array.mapM (fun (l : Duper.Lit) => Duper.Lit.mapM f l) c.lits pure { lits := __do_lift }

def Duper.MClause.fold {β : Type v} (f : β → Lean.Expr → β) (init : β) (c : MClause) : β

Equations

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

def Duper.MClause.foldM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Lean.Expr → ClausePos → m β) (init : β) (c : MClause) : m β

Equations

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

def Duper.MClause.foldGreenM {m : Type → Type u_1} {β : Type} [Monad m] [MonadLiftT Lean.MetaM m] (f : β → Lean.Expr → ClausePos → m β) (init : β) (c : MClause) : m β

Equations

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

def Duper.MClause.getAtPos! {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (c : MClause) (pos : ClausePos) : m Lean.Expr

Equations

• c.getAtPos! pos = c.lits[pos.lit]!.getAtPos! { side := pos.side, pos := pos.pos }

def Duper.MClause.replaceAtPos? {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (c : MClause) (pos : ClausePos) (replacement : Lean.Expr) : m (Option MClause)

Equations

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

def Duper.MClause.replaceAtPos! {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [Lean.MonadError m] (c : MClause) (pos : ClausePos) (replacement : Lean.Expr) : m MClause

Equations

• c.replaceAtPos! pos replacement = do let replacedLit ← c.lits[pos.lit]!.replaceAtPos! pos.toLitPos replacement pure { lits := c.lits.set! pos.lit replacedLit }

def Duper.MClause.replaceAtPosUpdateType? (c : MClause) (pos : ClausePos) (replacement : Lean.Expr) : Lean.MetaM (Option MClause)

Equations

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

def Duper.MClause.abstractAtPos! (c : MClause) (pos : ClausePos) : Lean.MetaM MClause

This function acts as Meta.kabstract except that it takes a ClausePos rather than Occurrences and expects the given expression to consist only of applications up to the given ExprPos. Additionally, since the exact position is given, we don't need to pass in Meta.kabstract's second argument p

Equations

• c.abstractAtPos! pos = do let __do_lift ← c.lits[pos.lit]!.abstractAtPos! pos.toLitPos pure { lits := c.lits.set! pos.lit __do_lift }

def Duper.MClause.append (c d : MClause) : MClause

Equations

• c.append d = { lits := c.lits.append d.lits }

def Duper.MClause.eraseIdx (i : Nat) (c : MClause) : MClause

Equations

• Duper.MClause.eraseIdx i c = { lits := c.lits.eraseIdxIfInBounds i }

def Duper.MClause.isTrivial (c : MClause) : Bool

Equations

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

def Duper.MClause.getMinimalLits (ord : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (filter_fn : Lit → Bool) : Lean.MetaM (Array Nat)

Returns the list of minimal literal indices that satisfy the provided filter_fn

Equations

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

def Duper.MClause.getMaximalLits (ord : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (filter_fn : Lit → Bool) : Lean.MetaM (Array Nat)

Returns the list of maximal literal indices that satisfy the provided filter_fn

Equations

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

def Duper.MClause.getMaxDiffLits (getNetWeight : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Order.Weight) (alreadyReduced : Bool) (c : MClause) (filter_fn : Lit → Nat → Bool) : Lean.MetaM (Array Nat)

Returns the list of literals (that satisfy the provided filter_fn) for which the size difference between the lhs and rhs is maximal. Note: For getMaxDiffLits, the filter_fn takes in both the lit and its index because filtering by index is more convenient for some selection functions.

Equations

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

def Duper.MClause.isMaximalLit (ord : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (idx : Nat) (strict : Bool := false) : Lean.MetaM Bool

Determines whether c.lits[idx]! is maximal in c. If strict is set to true, then there can be no idx' such that c.lits[idx]! and c.lits[idx']! are evaluated as equal by the comparison function

Equations

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

def Duper.MClause.canNeverBeMaximal (ord : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (idx : Nat) : Lean.MetaM Bool

Returns true if there may be some assignment in which the given idx is maximal, and false if there is some idx' that is strictly greater than idx (in this case, since idx < idx', for any subsitution σ, idx σ < idx' σ so idx can never be maximal)

Note that for this function, strictness does not actually matter, because regardless of whether we are considering potential strict maximality or potential nonstrict maximality, we can only determine that idx can never be maximal if we find an idx' that is strictly gerater than it

Equations

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