inductive Trestle.Solver.Res : Type

• sat (assn : HashAssn ILit) : Res
• unsat : Res
• error : Res

instance Trestle.Solver.instToStringRes : ToString Res

Equations

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

def Trestle.Solver.Res.isSat : Res → Bool

Equations

• (Trestle.Solver.Res.sat assn).isSat = true
• x✝.isSat = false

def Trestle.Solver.Res.getAssn? : Res → Option (HashAssn ILit)

Equations

• (Trestle.Solver.Res.sat assn).getAssn? = some assn
• x✝.getAssn? = none

class Trestle.Solver (m : Type → Type v) : Type (max 1 v)

• solve [Monad m] : ICnf → m Res

def Trestle.Solver.Solutions (_f : ICnf) (_varsToBlock : List IVar) : Type

Equations

• Trestle.Solver.Solutions _f _varsToBlock = Unit

def Trestle.Solver.solutions (f : ICnf) (vars : List IVar) : Solutions f vars

Equations

• Trestle.Solver.solutions f vars = ()

instance Trestle.Solver.instForInSolutionsHashAssnIVarILit {m : Type → Type u_1} {f : ICnf} {vars : List IVar} [Solver m] : ForIn m (Solutions f vars) (HashAssn ILit)

Equations

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

def Trestle.Solver.allSolutions {m : Type → Type u_1} [Monad m] [Solver m] (f : ICnf) (varsToBlock : List IVar) : m (List (HashAssn ILit))

Equations

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

class Trestle.Solver.IpasirSolver (S : outParam Type) (m : Type → Type v) : Type (max 1 v)

• new : m S
• addClause : IClause → S → m S
• solve {SolveRes : Type} : S → m SolveRes

instance Trestle.Solver.instOfMonadOfIpasirSolver {m : Type → Type u_1} {S : Type} [Monad m] [IpasirSolver S m] : Solver m

Equations

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

class Trestle.Solver.ModelCount (m : Type → Type v) [outParam (Monad m)] : Type v

• modelCount : ICnf → Option (List IVar) → m ℕ

class Trestle.Solver.ModelSample (m : Type → Type v) : Type v

• modelSample : ICnf → Option (List IVar) → ℕ → m (List (HashAssn ILit))