def Std.Sat.Literal.dimacs (lit : Literal Nat) : String

Equations

• Std.Sat.Literal.dimacs (id, pol) = if pol = true then toString "" ++ toString (id + 1) ++ toString "" else toString "-" ++ toString (id + 1) ++ toString ""

def Std.Sat.CNF.Clause.dimacs (clause : Clause Nat) : String

Equations

• clause.dimacs = List.foldl (fun (x1 : String) (x2 : Std.Sat.Literal Nat) => x1 ++ x2.dimacs ++ " ") "" clause ++ "0"

def Std.Sat.CNF.dimacs (cnf : CNF Nat) : String

This function turns cnf into a DIMACS String.

Note: This function will add 1 to all literal identifiers by default. This is because 0 is an illegal identifier in the DIMACS format and we can avoid producing invalid DIMACs like this.

Equations

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