Unofficial Dub Package Documentation 
1 module satd.solvers.cdcl;
2 import satd.cnf : CNF, Clause, Literal, Set;
3 import satd.dimacs : Preamble, parseResult;
4 import std.container : RedBlackTree, redBlackTree;
5 import std.typecons : Tuple;
6 import std.algorithm : each, any, sort, filter, map, countUntil, min, count, all;
7 import std.range : front, popFront, iota, enumerate, empty, retro;
8 import std.math : abs;
9 import std.string : format;
10 import std.stdio : File, stdin;
11 import std.array : join, split, array;
12 import std.conv : to;
13 import std.variant : Algebraic;
14 
15 import std.stdio;
16 
17 /// LAMBDA は conflict node の意。
18 const Literal LAMBDA = 0;
19 
20 struct ImplicationGraph
21 {
22     /// dlevel とは、decision level のことをさす。
23     alias Node = Tuple!(Literal, "literal", size_t, "dlevel");
24 
25     Set!Node nodes;
26     Set!Node[Node] successors;
27     Set!Node[Node] predecessors;
28     Clause.ID[Node][Node] edges;
29 
30     Literal[] decisionLiterals;
31 
32     void initalize()
33     {
34         nodes = redBlackTree!Node;
35     }
36 
37     /// 与えられた implication graph を deep copy するためのコンストラクタ
38     this(ImplicationGraph graph)
39     {
40         this.nodes = graph.nodes.dup;
41         foreach (key, value; graph.successors)
42             this.successors[key] = value.dup;
43         foreach (key, value; graph.predecessors)
44             this.predecessors[key] = value.dup;
45         foreach (key, value; graph.edges)
46             this.edges[key] = value.dup;
47 
48         this.decisionLiterals = graph.decisionLiterals.dup;
49     }
50 
51     /// 与えられた decision level 以上の頂点やそれに繋がっている辺を削除します。
52     void removeLevel(size_t dlevel)
53     {
54         foreach (node; nodes)
55         {
56             if (node.dlevel >= dlevel)
57                 nodes.removeKey(node);
58         }
59         foreach (key, value; successors)
60         {
61             if (key.dlevel >= dlevel)
62                 successors.remove(key);
63             foreach (node; value)
64             {
65                 if (node.dlevel >= dlevel)
66                     value.removeKey(node);
67             }
68         }
69         foreach (key, value; predecessors)
70         {
71             if (key.dlevel >= dlevel)
72                 successors.remove(key);
73             foreach (node; value)
74             {
75                 if (node.dlevel >= dlevel)
76                     value.removeKey(node);
77             }
78         }
79         foreach (key, value; edges)
80         {
81             if (key.dlevel >= dlevel)
82             {
83                 edges.remove(key);
84                 continue;
85             }
86             foreach (key2, _; value)
87             {
88                 if (key2.dlevel >= dlevel)
89                 {
90                     value.remove(key2);
91                 }
92             }
93         }
94     }
95 
96     /// 与えられたリテラルを持つ頂点を取得します。
97     Node getNode(Literal lit)
98     {
99         auto tmp = nodes.array.filter!(n => n.literal == lit);
100         assert(tmp.count == 1);
101         return tmp.front;
102     }
103 
104     /// 1UIP cut を取得します。
105     Set!Node get1UIPCut()
106     {
107         Set!Node res = redBlackTree!Node;
108 
109         Set!Node visited = redBlackTree!Node;
110 
111         const ulong dlevel = decisionLiterals.length;
112 
113         Node[] queue = [Node(0, dlevel)];
114         bool found1UIP = false;
115         immutable Node decisionNode = Node(decisionLiterals[$ - 1], dlevel);
116         bool is1UIPDecisionNode = false;
117 
118         while (!found1UIP)
119         {
120             Node[] nextQueue;
121             foreach (Node n; queue)
122             {
123                 if (n in predecessors)
124                 {
125                     foreach (pred; predecessors[n])
126                     {
127                         if (pred == decisionNode)
128                             is1UIPDecisionNode = true;
129                         if (visited.insert(pred))
130                         {
131                             if (pred.dlevel != dlevel)
132                                 res.insert(pred);
133                             else
134                                 nextQueue ~= pred;
135                         }
136                     }
137                 }
138             }
139             if (!is1UIPDecisionNode && nextQueue.length == 1)
140             {
141                 found1UIP = true;
142                 res.insert(nextQueue[0]);
143             }
144             else if (nextQueue.length == 0)
145             {
146                 found1UIP = true;
147                 res.insert(decisionNode);
148             }
149             queue = nextQueue;
150             // debug stderr.writefln("nextQueue: %s", nextQueue);
151         }
152 
153         return res;
154     }
155 
156     /++
157      + implication graph を conflict graph の制約を満たすように変形します。
158      + この関数呼出後のグラフは以下の制約のすべてを満たしていることが保証されています。
159      +
160      + 1. Λ とただ一つの conflict variable を含んでいる。
161      + 2. 任意の頂点について、Λ への道が存在する。
162      + 3. Λ を除くすべての頂点 l について、それが decision literal であるか、または
163      +    (l_1 or l_2 or ... or l_k or l) が既知の節として存在して、かつ
164      +    not l_1, not l_2, ..., not l_k が predecessor としてグラフに存在する。
165      +/
166     void transformToConflictGraph(size_t level)
167     {
168         Set!Node conflictGraphNodes = redBlackTree!Node;
169         Node[] queue;
170         queue ~= Node(0, level);
171 
172         while (!queue.empty)
173         {
174             Node n = queue.front;
175             queue.popFront();
176             if (conflictGraphNodes.insert(n))
177             {
178                 if (n in predecessors)
179                     foreach (pred; predecessors[n])
180                         queue ~= pred;
181             }
182         }
183 
184         Set!Node[Node] successors_;
185         Set!Node[Node] predecessors_;
186         Clause.ID[Node][Node] edges_;
187 
188         foreach (n; conflictGraphNodes)
189         {
190             if (n in successors)
191                 foreach (node; successors[n])
192                     if (node in conflictGraphNodes)
193                     {
194                         if (n !in successors_)
195                             successors_[n] = redBlackTree!Node;
196                         successors_[n].insert(node);
197                     }
198             if (n in predecessors)
199                 foreach (node; predecessors[n])
200                     if (node in conflictGraphNodes)
201                     {
202                         if (n !in predecessors_)
203                             predecessors_[n] = redBlackTree!Node;
204                         predecessors_[n].insert(node);
205                     }
206         }
207 
208         foreach (from, tos; successors_)
209             foreach (to; tos)
210                 edges_[from][to] = edges[from][to];
211 
212         nodes = conflictGraphNodes;
213         successors = successors_;
214         predecessors = predecessors_;
215         edges = edges_;
216     }
217 }
218 
219 alias CDCLSolverResult = Algebraic!(Literal[], typeof(null));
220 
221 /// CDCL を実装したソルバー
222 class CDCLSolver
223 {
224     Clause[Clause.ID] clauses;
225     Set!(long) unassignedVariables;
226     /// まだ充足されていない節の ID の集合
227     RedBlackTree!(Clause.ID, "a > b") availClauses;
228     ImplicationGraph implicationGraph;
229     /// implication graph 上の頂点の decision level の最大値
230     size_t currentLevel;
231 
232     RedBlackTree!(Clause.ID, "a > b") unitClauses;
233     Set!(Clause.ID)[Literal] clausesContainingLiteral;
234     /// CNF の単純化が適用されていない形の節
235     Clause[Clause.ID] originalClauses;
236     Literal[] decisionVariables;
237     bool generateGraph = false;
238     bool generateAnotherGraph = false;
239     Preamble preamble;
240 
241     /// ソルバーの状態が各 decision level に対応して保持されている配列
242     CDCLSolver[] history;
243 
244     bool restart = false;
245     long restartThreshold = 100;
246     double restartMult = 1.5;
247     ulong conflictCount;
248 
249     private Clause.ID usedIDNum;
250 
251     Clause.ID nextClauseID()
252     {
253         return ++usedIDNum;
254     }
255 
256     this()
257     {
258         implicationGraph.initalize();
259     }
260 
261     /// 読み込んだ CNF の情報を元にソルバーを初期化します。
262     void initialize(parseResult res)
263     {
264         availClauses = redBlackTree!("a > b", Clause.ID);
265         unitClauses = redBlackTree!("a > b", Clause.ID);
266         foreach (clause; res.clauses)
267         {
268             this.clauses[clause.id] = clause;
269             if (clause.isUnitClause)
270                 unitClauses.insert(clause.id);
271             availClauses.insert(clause.id);
272 
273             foreach (literal; clause.literals.array)
274             {
275                 if (literal !in clausesContainingLiteral)
276                     clausesContainingLiteral[literal] = redBlackTree!(Clause.ID);
277                 clausesContainingLiteral[literal].insert(clause.id);
278             }
279 
280             // debug stderr.writefln("%d: %s", clause.id, clause);
281         }
282         clausesContainingLiteral[0] = redBlackTree!(Clause.ID);
283 
284         foreach (key, value; this.clauses)
285         {
286             this.originalClauses[key] = Clause(value);
287         }
288         usedIDNum = clauses.length;
289         unassignedVariables = redBlackTree!long(iota(1,
290                 res.preamble.variables + 1).array.to!(long[]));
291         this.preamble = res.preamble;
292     }
293 
294     /// for deep copy
295     this(CDCLSolver solver)
296     {
297         foreach (key, value; solver.clauses)
298             this.clauses[key] = Clause(value);
299         this.unassignedVariables = solver.unassignedVariables.dup;
300         this.availClauses = solver.availClauses.dup;
301         this.implicationGraph = ImplicationGraph(solver.implicationGraph);
302         this.availClauses = solver.availClauses.dup;
303         this.decisionVariables = solver.decisionVariables.dup;
304         this.currentLevel = solver.currentLevel;
305     }
306 
307     enum SolverStatus
308     {
309         SAT,
310         CONFLICT,
311         OK
312     }
313 
314     /// 問題を与えて初期化したソルバーで実行すると、その問題を解いて結果を返します。
315     CDCLSolverResult solve()
316     {
317         // debug stderr.writefln("given clauses: %s", this.clauses.values);
318 
319         if (this.clauses.values.any!(c => c.literals.length == 0))
320             return CDCLSolverResult(null);
321         if (this.preamble.variables == 0 && this.preamble.clauses == 0)
322             return CDCLSolverResult(cast(Literal[])[]);
323         while (true)
324         {
325             while (true)
326             {
327                 immutable SolverStatus status = deduce();
328                 // debug stderr.writefln("Deduce done. nodes: %(%s, %)",
329                 // implicationGraph.nodes.array.map!(p => format("(%d, %d)", p[0], p[1])));
330                 if (status == SolverStatus.SAT)
331                     return CDCLSolverResult(implicationGraph.nodes.array.map!(node => node.literal)
332                             .array);
333                 if (status == SolverStatus.CONFLICT)
334                 {
335                     toDOT(true);
336                     auto res = analyzeConflict();
337                     if (res.blevel == -1)
338                         return CDCLSolverResult(null);
339 
340                     backtrack(res.blevel);
341                     addConflictClause(res.conflict);
342                     conflictCount++;
343 
344                     // リスタートが有効であり、conflict の回数が閾値に達していたならば、リスタートを実施します。
345                     if (restart && conflictCount == restartThreshold)
346                     {
347                         writefln("c restart. conflicted %d times", conflictCount);
348                         backtrack(0);
349                         restartThreshold = cast(long)(cast(double) restartThreshold * restartMult);
350                     }
351                 }
352                 else
353                     break;
354             }
355             decideNextBranch();
356         }
357     }
358 
359     /// 真偽値が未割り当ての変数を1つ選んで真を割り当てます。
360     void decideNextBranch()
361     {
362         // 現在のソルバーの状態を保存します。
363         history ~= new CDCLSolver(this);
364 
365         Literal lit = unassignedVariables.front;
366         // debug stderr.writefln("decision literal: %d", lit);
367         currentLevel++;
368         assignLiteral(lit);
369         decisionVariables ~= lit;
370         implicationGraph.decisionLiterals ~= lit;
371     }
372 
373     /++
374      + 単位伝播を繰り返します。
375      + 途中で矛盾が生じたら CONFLICT を返します。
376      + 矛盾なくすべての変数に真偽値を割り当てられたら SAT を返します。
377      + それ以外の場合には OK を返します。
378      +/
379     SolverStatus deduce()
380     {
381         while (!unitClauses.empty)
382         {
383             // debug stderr.writefln("unitClauses: %s", unitClauses);
384 
385             Clause.ID clsID = unitClauses.front;
386             unitClauses.removeKey(clsID);
387             Literal lit = clauses[clsID].unitLiteral;
388             if (iota(0, currentLevel + 1).map!(l => ImplicationGraph.Node(-lit, l))
389                     .any!(n => n in implicationGraph.nodes))
390             {
391                 assignLiteral(LAMBDA, lit);
392                 addEdge(-lit, LAMBDA, 0);
393                 addEdge(lit, LAMBDA, 0);
394 
395                 foreach (pred; this.originalClauses[clsID].literals.array.filter!(
396                         pred => pred != lit))
397                     addEdge(pred, lit, clsID);
398                 implicationGraph.transformToConflictGraph(currentLevel);
399                 return SolverStatus.CONFLICT;
400             }
401             assignLiteral(lit);
402             foreach (oclit; this.originalClauses[clsID].literals.array.filter!(
403                     oclit => oclit != lit))
404                 addEdge(oclit, lit, clsID);
405             toDOT(false);
406         }
407         if (unassignedVariables.empty)
408             return SolverStatus.SAT;
409         else
410             return SolverStatus.OK;
411     }
412 
413     alias analyzeConflictResult = Tuple!(long, "blevel", Clause, "conflict");
414     /++
415      + 矛盾を分析します。
416      + Returns: バックトラック先のレベルと学習節
417      +/
418     analyzeConflictResult analyzeConflict()
419     {
420         while (true)
421         {
422             if (currentLevel == 0)
423                 return analyzeConflictResult(-1, Clause(0, []));
424 
425             auto reasonNodes = implicationGraph.get1UIPCut();
426 
427             long blevel;
428             if (reasonNodes.array.length >= 2)
429                 blevel = reasonNodes.array
430                     .map!(node => node.dlevel)
431                     .array
432                     .sort!("a > b")[1];
433             else
434                 blevel = 0;
435 
436             // debug stderr.writefln("reasonNodes: %(%s %)",
437             // reasonNodes.array.map!(c => format("(%s, %s)", c[0], c[1])));
438 
439             auto learningLiterals = reasonNodes.array.map!(node => -node.literal).array;
440             Clause conflict = newClause(learningLiterals);
441             return analyzeConflictResult(blevel, conflict);
442         }
443     }
444 
445     /++
446      + 与えられたレベルまでバックトラックします。
447      + 具体的には、ソルバーの状態を与えられたレベルのときのソルバーの状態まで復元します。
448      +/
449     void backtrack(size_t dlevel)
450     {
451         dlevel = min(history.length - 1, dlevel);
452         // debug stderr.writefln("backtrack from %d to %d", currentLevel, dlevel);
453         // debug stderr.writefln("history length: %d, currentLevel: %d",
454         // this.history.length, currentLevel);
455         assert(this.history.length == currentLevel);
456         CDCLSolver oldSolver = this.history[dlevel];
457         this.history.length = dlevel;
458 
459         this.clauses = oldSolver.clauses;
460         this.unassignedVariables = oldSolver.unassignedVariables;
461         this.availClauses = oldSolver.availClauses;
462         this.decisionVariables = oldSolver.decisionVariables;
463         this.implicationGraph = oldSolver.implicationGraph;
464         this.currentLevel = oldSolver.currentLevel;
465 
466         this.unitClauses.clear();
467         availClauses.array
468             .filter!(clauseID => clauses[clauseID].isUnitClause)
469             .each!(clauseID => unitClauses.insert(clauseID));
470         // debug stderr.writefln("availClauses: %(%s, %)", availClauses.array.map!(id => clauses[id]));
471     }
472 
473     /++
474      + ソルバーの状態を、真偽値割り当てがなされていない初期状態にリセットします。
475      + 初期化時以外で追加された制約はそのまま追加された状態を維持します。
476      +/
477     void reset()
478     {
479         backtrack(0);
480     }
481 
482     /// 与えられたリテラルを含んだ新しい節を作成します。
483     Clause newClause(T...)(T literals)
484     {
485         return Clause(redBlackTree!Literal(literals));
486     }
487 
488     /// 与えられたリテラルの集合に対応する新しい節を作成します。
489     Clause newClause(T)(Set!T literals) if (isIntegral!T)
490     {
491         return Clause(literals);
492     }
493 
494     /// 与えられた節をソルバーの制約として追加します。
495     void addClause(Clause clause)
496     {
497         usedIDNum++;
498         clause.id = usedIDNum;
499 
500         assert(clause.id !in clauses);
501         originalClauses[clause.id] = Clause(clause);
502         availClauses.insert(clause.id);
503 
504         foreach (dlevel; 0 .. currentLevel)
505         {
506             history[dlevel].clauses[clause.id] = Clause(clause);
507             foreach (node; history[dlevel].implicationGraph.nodes)
508                 history[dlevel].clauses[clause.id].removeLiteral(-node.literal);
509             if (history[dlevel].clauses[clause.id].isUnitClause)
510                 history[dlevel].unitClauses.insert(clause.id);
511             history[dlevel].availClauses.insert(clause.id);
512         }
513         foreach (literal; clause.literals)
514             clausesContainingLiteral[literal].insert(clause.id);
515 
516         foreach (node; implicationGraph.nodes.array.filter!(node => node.literal != 0))
517             clause.removeLiteral(-node.literal);
518 
519         clauses[clause.id] = clause;
520         if (clause.isUnitClause)
521             unitClauses.insert(clause.id);
522     }
523 
524     /// 与えられた節を学習節として追加します。
525     void addConflictClause(Clause conflict)
526     {
527         // debug stderr.writefln("conflict clause: %s", conflict);
528         assert(!originalClauses.values.any!(c => c.literals == conflict.literals));
529         addClause(conflict);
530         // debug stderr.writefln("conflictClauseApplied: %s", conflict);
531     }
532 
533     /// 与えられたリテラルが真になるように変数への真偽値割り当てを行います。
534     void assignLiteral(T...)(T literals)
535     {
536         debug
537         {
538             // debug stderr.writefln("assignLiteral: %s", literals);
539             // debug stderr.writeln(unassignedVariables);
540             if (literals[0] != 0)
541                 assert(literals[0].abs in unassignedVariables);
542         }
543         foreach (lit; literals)
544         {
545             addNode(lit, this.currentLevel);
546             removeClausesContaining(lit);
547             removeLiteralFromClauses(-lit);
548             unassignedVariables.removeKey(abs(lit));
549         }
550     }
551 
552     void addNode(Literal lit, size_t dlevel)
553     {
554         // debug stderr.writefln("new node: %s, at level %s", lit, dlevel);
555         implicationGraph.nodes.insert(ImplicationGraph.Node(lit, dlevel));
556     }
557 
558     void addEdge(Literal from, Literal to, Clause.ID clauseID)
559     {
560         alias Node = ImplicationGraph.Node;
561 
562         // debug stderr.writefln("Add edge from %s to %s", -from, to);
563         Node fromNode = implicationGraph.getNode(-from), toNode = implicationGraph.getNode(to);
564         if (fromNode !in implicationGraph.successors)
565             implicationGraph.successors[fromNode] = redBlackTree!Node;
566         implicationGraph.successors[fromNode].insert(toNode);
567         if (toNode !in implicationGraph.predecessors)
568             implicationGraph.predecessors[toNode] = redBlackTree!Node;
569         implicationGraph.predecessors[toNode].insert(fromNode);
570         implicationGraph.edges[fromNode][toNode] = clauseID;
571 
572     }
573 
574     /// 与えられたリテラルを含む節を削除します。
575     void removeClausesContaining(Literal lit)
576     {
577         if (lit !in clausesContainingLiteral)
578             return;
579         foreach (clauseID; clausesContainingLiteral[lit].array.filter!(cid => cid in availClauses))
580         {
581             availClauses.removeKey(clauseID);
582             unitClauses.removeKey(clauseID);
583         }
584     }
585 
586     /// 与えられたリテラルをそれぞれの節の中から削除します。
587     void removeLiteralFromClauses(Literal lit)
588     {
589         if (lit !in clausesContainingLiteral)
590             return;
591         foreach (clauseID; clausesContainingLiteral[lit].array.filter!(cid => cid in availClauses))
592         {
593             if (!clauses[clauseID].isUnitClause)
594                 clauses[clauseID].removeLiteral(lit);
595             if (clauses[clauseID].isUnitClause)
596                 unitClauses.insert(clauseID);
597             if (clauses[clauseID].isEmptyClause)
598                 unitClauses.removeKey(clauseID);
599         }
600     }
601 
602     private int dotCounter;
603     /++
604      + implication graph の状態を DOT 言語で出力します。
605      + ファイル名は 1.dot, 2.dot, … のように続きます。
606      +/
607     void toDOT(bool conflict)
608     {
609         // if (conflict)
610         // debug stderr.writefln("conflict exported: %d", dotCounter);
611         if (!generateGraph && !generateAnotherGraph)
612             return;
613         if (implicationGraph.edges.length == 0)
614             return;
615 
616         string dotSource;
617         if (generateGraph)
618             dotSource = generateGraph1(conflict);
619         else
620             dotSource = generateGraph2(conflict);
621 
622         import std.file : write;
623 
624         write(format("%d.dot", dotCounter), dotSource);
625         dotCounter++;
626     }
627 
628     /// implication graph の定義に即した形のグラフを表す DOT 言語のソースを返します。
629     string generateGraph1(bool conflict)
630     {
631         string res = "digraph cdcl {\nnode[style=filled, fillcolor=white];\n";
632         res ~= "graph [layout = dot];\n";
633         if (conflict)
634             res ~= "\"0@%d\" [label = \"Λ\"];\n".format(currentLevel);
635         foreach (level, variable; decisionVariables)
636             res ~= format("\"%d@%d\" [shape = record, label = \"%d@%d\"];\n",
637                     variable, level + 1, variable, level + 1);
638 
639         foreach (from, tos; implicationGraph.edges)
640         {
641             foreach (to, clause; tos)
642             {
643                 res ~= format("\"%s@%d\" -> \"%s@%d\" [label = \"%s\"];\n", from.literal, from.dlevel,
644                         to.literal, to.dlevel, clause == 0 ? "" : (clause > preamble.clauses
645                             ? "L:" : "") ~ this.originalClauses[clause].toString);
646             }
647         }
648 
649         res ~= "}\n";
650         return res;
651     }
652 
653     /// implication graph を元に、単位伝播で用いられた節も頂点にしたグラフの DOT 言語のソースを返します。
654     string generateGraph2(bool conflict)
655     {
656         string label(string content, string color)
657         {
658             return "<font color=\"" ~ color ~ "\">" ~ content ~ "</font>";
659         }
660 
661         string generateClauseLabel(Clause.ID cl, Literal implicated)
662         {
663             if (cl == 0)
664                 return "conflict";
665 
666             auto literals = this.originalClauses[cl].literals.array;
667             Literal[] l, r;
668             auto tmp = literals.split(implicated);
669             l = tmp[0], r = tmp[1];
670             string ls = l.empty ? "" : format("%(%d ∨%) ∨ ", l);
671             string rs = r.empty ? "" : format(" ∨ %(%d ∨%)", r);
672             string res = "(%s%s%s)".format(ls, label(implicated.to!string, "black"), rs);
673             if (cl > preamble.clauses)
674                 return "L:" ~ res;
675             else
676                 return res;
677         }
678 
679         string res = "digraph cdcl {\nnode[style=filled, fillcolor=white];\n";
680         res ~= "graph [layout = dot, bgcolor=\"#eaeaea\"];\n";
681         if (conflict)
682             res ~= "\"0@%d\" [label = \"Λ\"];\n".format(currentLevel);
683         foreach (level, variable; decisionVariables)
684             res ~= format("\"%d@%d\" [shape = record, label = \"%d@%d\"];\n",
685                     variable, level + 1, variable, level + 1);
686 
687         alias T = Tuple!(Clause.ID, "clauseID", Literal, "implicated");
688         T[] clausesAndImplicateds;
689 
690         foreach (_, tos; implicationGraph.edges)
691             foreach (to, clause; tos)
692                 clausesAndImplicateds ~= T(clause, to.literal);
693 
694         foreach (p; clausesAndImplicateds)
695             if (p.clauseID != 0)
696                 res ~= format("\"cls%d\" [shape = invtrapezium, fontcolor=gray60, label=<%s>];\n",
697                         p.clauseID, generateClauseLabel(p.clauseID, p.implicated));
698 
699         auto clauseRendered = redBlackTree!(Clause.ID);
700 
701         foreach (from, tos; implicationGraph.edges)
702         {
703             foreach (to, clause; tos)
704             {
705                 if (clause == 0)
706                     res ~= format("\"%s@%d\" -> \"%s@%d\"\n", from.literal,
707                             from.dlevel, to.literal, to.dlevel);
708                 else
709                 {
710                     res ~= format("\"%d@%d\" -> \"cls%d\"\n", from.literal, from.dlevel, clause);
711                     if (clauseRendered.insert(clause))
712                         res ~= format("\"cls%d\" -> \"%d@%d\"\n", clause, to.literal, to.dlevel);
713                 }
714             }
715         }
716 
717         res ~= "}\n";
718         return res;
719     }
720 }

Page generated by adrdox