def Trestle.Solver.Dimacs.formatVar : IVar → String

Equations

• Trestle.Solver.Dimacs.formatVar x✝ = toString "" ++ toString x✝ ++ toString ""

def Trestle.Solver.Dimacs.formatLit (l : ILit) : String

Equations

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

def Trestle.Solver.Dimacs.formatClause : IClause → String

Equations

• Trestle.Solver.Dimacs.formatClause { toList := lits } = " ".intercalate (List.map (fun (x : Trestle.ILit) => Trestle.Solver.Dimacs.formatLit x) lits ++ ["0"])

def Trestle.Solver.Dimacs.formatComment (s : String) : String

Equations

• Trestle.Solver.Dimacs.formatComment s = "\n".intercalate (List.map (fun (x : String) => "c " ++ x) (s.splitOn "\n"))

def Trestle.Solver.Dimacs.formatFormula (f : ICnf) : String

Equations

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

def Trestle.Solver.Dimacs.printICnf {m : Type → Type u_1} [Monad m] (print : String → m Unit) (f : ICnf) (vars : ℕ := f.maxVar) : m Unit

Equations

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

def Trestle.Solver.Dimacs.printRichCnf {m : Type → Type u_1} [Monad m] (print : String → m Unit) (f : RichCnf) (vars : ℕ := f.maxVar) : m Unit

Equations

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

def Trestle.Solver.Dimacs.toFile (file : System.FilePath) (cnf : ICnf) : IO Unit

Equations

• Trestle.Solver.Dimacs.toFile file cnf = IO.FS.withFile file IO.FS.Mode.write fun (handle : IO.FS.Handle) => Trestle.Solver.Dimacs.printICnf handle.putStr cnf

def Trestle.Solver.Dimacs.toFileRich (file : System.FilePath) (cnf : RichCnf) : IO Unit

Equations

• Trestle.Solver.Dimacs.toFileRich file cnf = IO.FS.withFile file IO.FS.Mode.write fun (handle : IO.FS.Handle) => Trestle.Solver.Dimacs.printRichCnf handle.putStr cnf

def Trestle.Solver.Dimacs.formatAssn (a : HashAssn ILit) : String

Equations

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

def Trestle.Solver.Dimacs.printRes {m : Type → Type u_1} {ε : Type u_2} [Monad m] [MonadExcept ε m] [Inhabited ε] (print : String → m Unit) : Res → m Unit

Equations

• Trestle.Solver.Dimacs.printRes print (Trestle.Solver.Res.sat assn) = do print "s SATISFIABLE" print (Trestle.Solver.Dimacs.formatAssn assn)
• Trestle.Solver.Dimacs.printRes print Trestle.Solver.Res.unsat = print "s UNSATISFIABLE"
• Trestle.Solver.Dimacs.printRes print Trestle.Solver.Res.error = throw default

structure Trestle.Solver.Dimacs.DimacsParseRes : Type

• vars : ℕ
• clauses : RichCnf

def Trestle.Solver.Dimacs.parseVar (maxVar : ℕ) (s : String) : Except String IVar

Equations

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

def Trestle.Solver.Dimacs.parseLit (maxVar : ℕ) (s : String) : Except String ILit

Equations

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

def Trestle.Solver.Dimacs.parseClause (maxVar : ℕ) (s : String) : Except String IClause

Equations

• Trestle.Solver.Dimacs.parseClause maxVar s = Trestle.Solver.Dimacs.parseClause.aux maxVar s (List.filter (fun (x : String) => !x.isEmpty) s.splitOn) #[]

def Trestle.Solver.Dimacs.parseClause.aux (maxVar : ℕ) (s : String) (L : List String) (acc : Array ILit) : Except String IClause

Equations

• Trestle.Solver.Dimacs.parseClause.aux maxVar s [] acc = throw (toString "Line was empty? `" ++ toString s ++ toString "`")
• Trestle.Solver.Dimacs.parseClause.aux maxVar s [last] acc = if last = "0" then pure acc else throw (toString "Expected last entry of line to be zero; got: `" ++ toString s ++ toString "`")
• Trestle.Solver.Dimacs.parseClause.aux maxVar s (lit :: rest) acc = do let lit ← Trestle.Solver.Dimacs.parseLit maxVar lit Trestle.Solver.Dimacs.parseClause.aux maxVar s rest (acc.push lit)

def Trestle.Solver.Dimacs.parseHeader (s : String) : Except String (ℕ × ℕ)

Equations

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

def Trestle.Solver.Dimacs.parseFormula (s : String) : Except String DimacsParseRes

Equations

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

def Trestle.Solver.Dimacs.parseVLines (maxVar : ℕ) (assn : HashAssn ILit) (s : String) : Except String (HashAssn ILit)

Equations

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

def Trestle.Solver.Dimacs.parseResult (maxVar : ℕ) (s : String) : Except String Res

Equations

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

def Trestle.Solver.Dimacs.fromFileEnc (cnfFile : String) : IO (Encode.EncCNF.State IVar)

auxiliary for getting an EncCNF.State from a DIMACS cnf file

Equations

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

def Trestle.Solver.Dimacs.parseAssnLine (maxVar : ℕ) (s : String) : Except String (HashAssn ILit)

Equations

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

def Trestle.Solver.Dimacs.parseAssnLines (maxVar : ℕ) (s : String) : Except String (List (HashAssn ILit))

Equations

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