satd.dimacs source code

1 module satd.dimacs;
2 import satd.cnf;
3 import satd.solvers.dpll : SolverResult, Null;
4 import std.stdio : readln, stdin, writeln;
5 import std.array : array, join;
6 import std.string : split;
7 import std.conv : to;
8 import std.math : abs;
9 import std.range : empty;
10 import std.stdio : stdin, File;
11 import std.typecons : Tuple;
12 
13 public:
14 
15 /*
16  * "p FORMAT VARIABLES CLAUSES"
17  * FORMAT must be "cnf"
18  * VARIABLES and CLAUSES must be positive integers
19 */
20 Preamble parsePreamble(File f = stdin)
21 {
22     string[] inp;
23 
24     // comments appear in the input is ignored
25     do
26     {
27         inp = f.readln.split;
28     }
29     while (inp.length < 1 || inp[0] == "c");
30 
31     if (inp[0] != "p")
32     {
33         error("Unknown command: %s", inp[0]);
34         assert(0);
35     }
36 
37     else
38     {
39         if (inp.length != 4)
40             error("Not enough arguments");
41 
42         if (inp[1] != "cnf")
43             error("Given format \"%s\" not supported", inp[1]);
44 
45         size_t variables, clauses;
46         try
47         {
48             variables = inp[2].to!size_t, clauses = inp[3].to!size_t;
49         }
50         catch (Exception e)
51         {
52             error("Numbers in preamble couldn't be parsed");
53         }
54         return Preamble(variables, clauses);
55     }
56 }
57 
58 struct Preamble
59 {
60     size_t variables;
61     size_t clauses;
62 }
63 
64 alias parseResult = Tuple!(Clause[], "clauses", Preamble, "preamble");
65 parseResult parseClauses(File f = stdin)
66 {
67     Preamble preamble = parsePreamble(f);
68     Clause[] clauses;
69     Literal[] literals;
70     Clause.ID id = 1;
71 
72     // read until EOF then ...
73     long[] tokens;
74     try
75     {
76         tokens = f.byLineCopy.array.join(' ').split.to!(long[]);
77     }
78     catch (Exception e)
79     {
80         error("Malformed input");
81     }
82 
83     foreach (token; tokens)
84     {
85         if (token == 0)
86         {
87             if (clauses.length >= preamble.clauses)
88                 error("Too many clauses");
89 
90             Clause clause = Clause(id, literals);
91             clauses ~= clause;
92             literals = null;
93             id++;
94             continue;
95         }
96         if (abs(token) > preamble.variables)
97             error("Given %d but variable bound is %d", abs(token), preamble.variables);
98 
99         Literal literal = token;
100         literals ~= literal;
101     }
102     if (!literals.empty)
103         error("Unexpected End of File");
104 
105     return parseResult(clauses, preamble);
106 
107 }
108 
109 string solverResultToString(SolverResult sr)
110 {
111     if (sr.peek!Null)
112         return "s UNSATISFIABLE";
113     return format("s SATISFIABLE\n%s", sr.get!0.toDIMACSFormat());
114 }
115 
116 private:
117 
118 import std.string : format;
119 
120 void error(A...)(string msg, A args)
121 {
122     class DIMACSReadException : Exception
123     {
124         this(string msg)
125         {
126             super(msg);
127         }
128     }
129 
130     throw new DIMACSReadException(format(msg, args));
131 }