1 % (c) 2026-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(dimacs_parser, [read_dimacs_cnf_file/2, convert_dimacs_cnf2b/2]).
6
7 :- use_module('../../src/module_information.pl').
8 :- module_info(group,satsolver).
9 :- module_info(description,'This is a parser for reading Dimacs .cnf files and converting them to B').
10
11 :- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2, add_warning/3]).
12 :- use_module(probsrc(tools), [ajoin/2]).
13 :- use_module(library(lists), [nth1/3]).
14
15 blank_char(0' ).
16 blank_char(0'\t).
17 blank_char(0'\n).
18 blank_char(0'\r).
19
20 blank --> [C], { blank_char(C) }.
21
22 blanks --> blank, !, blanks.
23 blanks --> [].
24
25 blanks1 --> blank, blanks.
26
27 digit_code(C) --> [C], { C >= 0'0, C =< 0'9 }.
28
29 digits([C|Cs]) --> digit_code(C), !, digits(Cs).
30 digits([]) --> [].
31
32 digits1([C|Cs]) --> digit_code(C), digits(Cs).
33
34 signed_int(N) --> "-", !, digits1(Ds), { number_codes(N0, Ds), N is -N0 }.
35 signed_int(N) --> digits1(Ds), { number_codes(N, Ds) }.
36
37 % comment lines: "c" followed by anything up to end of line
38
39 comment_line --> "c", line_rest, opt_newline.
40
41 line_rest --> [C], { C \== 0'\n }, !, line_rest.
42 line_rest --> [].
43
44 opt_newline --> "\n".
45 opt_newline --> [].
46
47 % problem line: p cnf <vars> <clauses>
48
49 problem_line(NumVars, NumClauses) -->
50 "p", blanks1, "cnf", blanks1,
51 signed_int(NumVars), blanks1, signed_int(NumClauses).
52
53 % clauses: sequence of nonzero ints terminated by 0
54
55 cnf_clause(Lits) --> blanks, clause_literals(Lits).
56
57 clause_literals(Lits) -->
58 signed_int(N),
59 ( { N =:= 0 }
60 -> { Lits = [] }
61 ; { Lits = [N|Ls] }, blanks, clause_literals(Ls)
62 ).
63
64 % top-level sequence of clauses interleaved with comments
65
66 clause_section(Clauses) --> blanks, clause_section_(Clauses).
67
68 clause_section_(Clauses) --> comment_line, !, clause_section(Clauses).
69 clause_section_([Lits|Rest]) --> cnf_clause(Lits), !, clause_section(Rest).
70 clause_section_([]) --> [].
71
72 skip_comments --> blanks, comment_line, !, skip_comments.
73 skip_comments --> blanks.
74
75 % whole file
76
77 dimacs_cnf(cnf_encoding(NumVars, NumClauses, Clauses)) -->
78 skip_comments,
79 problem_line(NumVars, NumClauses),
80 clause_section(Clauses).
81
82 % I/O helpers
83
84 read_all_codes(Stream, Codes) :-
85 get_code(Stream, C),
86 ( C = -1
87 -> Codes = []
88 ; Codes = [C|Cs], read_all_codes(Stream, Cs)
89 ).
90
91 parse_dimacs_cnf(Codes, Term) :-
92 phrase(dimacs_cnf(Term), Codes),
93 validate_dimacs_cnf(Term).
94
95 :- use_module(probsrc(tools_io),[safe_intelligent_open_file/4]).
96 read_dimacs_cnf_file(FileName, Term) :-
97 safe_intelligent_open_file(FileName, read, Stream,[encoding(utf8)]),
98 call_cleanup(
99 ( read_all_codes(Stream, Codes),
100 parse_dimacs_cnf(Codes, Term)
101 ),
102 close(Stream)
103 ).
104
105 %
106 % check if number of propositional variables and number of clauses are correct
107 validate_dimacs_cnf(cnf_encoding(NumVars, NumClauses, Clauses)) :-
108 format('Read in CNF with ~w propositional variables and ~w clauses~n',[NumVars, NumClauses]),
109 length(Clauses, ActualClauses),
110 ( ActualClauses = NumClauses -> true
111 ; ajoin(['CNF header declares ',NumClauses,' but found: '],Msg),
112 add_warning(dimacs_parser,Msg,ActualClauses)
113 ),
114 ( nth1(ClauseNr,Clauses,Clause),
115 nth1(LitNr,Clause,Lit),
116 abs(Lit) > NumVars,
117 ajoin(['CNF literal ',LitNr,' in clause nr ',ClauseNr,' exceeds ',NumVars,':'],Msg),
118 add_warning(dimacs_parser,Msg,Lit),
119 fail
120 ; true
121 ).
122
123
124 :- use_module(probsrc(tools),[get_tail_filename/2,split_filename/3]).
125
126 % convert a .cnf file to a .mch file with the same root filename
127 convert_dimacs_cnf2b(FileName,BMachineFileName) :-
128 read_dimacs_cnf_file(FileName,Term),
129 get_tail_filename(FileName,Tail),
130 split_filename(Tail,MachName,_Ext),
131 split_filename(FileName,Base,_Extension),
132 atom_concat(Base,'.mch',BMachineFileName),
133 % TODO: check that file does not already exist or is @generated
134 safe_intelligent_open_file(BMachineFileName, write, Stream, [encoding(utf8)]),
135 call_cleanup(portray_cnf_as_b(Stream,MachName,Term),
136 close(Stream)).
137
138
139 :- use_module(library(system),[ datime/1]).
140 :- use_module(probsrc(version),[version_str/1]).
141 :- use_module(probsrc(tools_strings),[number_codes_min_length/3]).
142 :- use_module(probsrc(tools_strings),[is_simple_classical_b_identifier/1]).
143 portray_cnf_as_b(Stream,Name,cnf_encoding(NumVars,NumClauses,Clauses)) :-
144 format(Stream,' /*@generated */~n',[]),
145 (is_simple_classical_b_identifier(Name) % TODO: check id_requires_escaping
146 -> format(Stream,'MACHINE ~w~n',[Name])
147 ; format(Stream,'MACHINE `~w`~n',[Name])
148 ),
149 version_str(Str),datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
150 number_codes_min_length(Min,2,MC),
151 format(Stream,' /* Generated on ~w/~w/~w at ~w:~s using ProB version ~w */~n',[Day,Mon,Yr,Hr,MC,Str]),
152 format(Stream,'CONSTANTS~n',[]),
153 output_all_constants(Stream,1,NumVars), nl(Stream),
154 format(Stream,'DEFINITIONS~n',[]),
155 format(Stream,' SET_PREF_SOLVER_FOR_PROPERTIES == "sat";~n',[]),
156 (convert_as_array ->
157 % CUSTOM_GRAPH Encoding of Variable Incidence Graph
158 (NumClauses+NumVars > 600 -> ENG = sfdp ; ENG= fdp), % sfdp is faster, but fdp more useful
159 format(Stream,' SET_PREF_DOT_ENGINE == "~w";~n',[ENG]),
160 format(Stream,' CUSTOM_GRAPH_NODES1 == {(i).i:1..~w|rec(`id`:i, label:```x${i}```,color:IF x(i)=TRUE THEN "olivedrab2" ELSE "tomato" END,shape:"box",style:"rounded",penwidth:2)};~n',[NumVars]),
161 format(Stream,' CUSTOM_GRAPH_NODES2 == {(c).c:1..~w|rec(`id`:c+~w, label:```Clause ${c}```,color:"blue",shape:"box")};~n',[NumClauses,NumVars]),
162 format(Stream,' CUSTOM_GRAPH_EDGES1 == {(ci,c,i).ci|->c:CLAUSES & i:ran(c) & i>0 |rec(color:"black", style:IF x(i)=TRUE THEN "solid" ELSE "dotted" END, label:"+", dir:"none", penwidth:2,from:i,to:ci+~w)};~n',[NumVars]),
163 format(Stream,' CUSTOM_GRAPH_EDGES2 == {(ci,c,i).ci|->c:CLAUSES & i:ran(c) & i<0 |rec(color:"purple", style:IF x(-i)=FALSE THEN "solid" ELSE "dotted" END, label:"-", dir:"none", penwidth:2,from:-i,to:ci+~w)};~n',[NumVars]),
164
165 % VisB Encoding of clauses and literals
166 % does not work well with large number of small clauses
167 format(Stream,' WIDTH==6; HEIGHT==4;WIDTH1==WIDTH+1;HEIGHT1==HEIGHT+1;~n',[]),
168 format(Stream,' MAXCLAUSESIZE == max({(i).i:dom(CLAUSES)|size(CLAUSES(i))});~n',[]),
169 format(Stream,' VISB_SVG_BOX == rec(width:WIDTH1*MAXCLAUSESIZE,height:1+HEIGHT1*size(CLAUSES));~n',[]),
170 format(Stream,' VISB_SVG_OBJECTS == {(i,j) . i:dom(CLAUSES) & j:dom(CLAUSES(i)) | VISB_LITERAL(i,j,CLAUSES(i)(j))};~n',[]),
171 format(Stream,' VISB_LITERAL(i,j,lit) == (rec(svg_class:"rect",rx:1,width:WIDTH,height:HEIGHT,~n',[]),
172 format(Stream,' fill:IF lit<0 & x(-lit)=FALSE THEN "lightgreen" ELSIF lit>0 & x(lit)=TRUE THEN "palegreen" ELSE "burlywood" END,~n',[]),
173 format(Stream,' stroke:"gray", hovers:rec(stroke:"black"), `stroke-width`:0.2,~n',[]),
174 format(Stream,' x:(j-1)*WIDTH1, y:1+(i-1)*HEIGHT1,title:```Literal ${j} in clause ${i}```),~n',[]),
175 format(Stream,' rec(svg_class:"text",x:(j-1)*WIDTH1+WIDTH/2,y:1+(i-1)*HEIGHT1+HEIGHT/2,~n',[]),
176 format(Stream,' `font-size`:2.0,`alignment-baseline`:"middle",`text-anchor`:"middle",~n',[]),
177 format(Stream,' text:IF lit<0 THEN ```\xAC\x${-lit}``` ELSE ```x${lit}```END));~n',[])
178 % see unicode_translation(negation,'\xAC\').
179 ; true),
180 % Clause representation as a DEFINITION:
181 format(Stream,' CLAUSES ==~n',[]),
182 output_clauses_as_b_list(Clauses,Stream), % output clauses for visualisations
183 format(Stream,'PROPERTIES~n',[]),
184 output_typing(Stream,1,NumVars),
185 output_clauses_as_b_pred(Clauses,Stream),
186 format(Stream,'END~n',[]).
187
188 output_clauses_as_b_list([],Stream) :- format(Stream,' []~n',[]).
189 output_clauses_as_b_list(Clauses,Stream) :-
190 format(Stream,' [~n',[]),
191 output_clauses_as_b_list2(Clauses,Stream),
192 format(Stream,' ]~n',[]).
193
194 output_clauses_as_b_list2([Clause|TC],Stream) :-
195 format(Stream,' ',[]),
196 format(Stream,'~w',[Clause]), % Prolog list is also valid B list
197 (TC=[] -> format(Stream,'~n',[])
198 ; format(Stream,',~n',[]),
199 output_clauses_as_b_list2(TC,Stream)
200 ).
201
202 output_clauses_as_b_pred([],_Stream).
203 output_clauses_as_b_pred([Clause|TC],Stream) :-
204 format(Stream,' (',[]),
205 output_clause(Clause,Stream),
206 (TC=[] -> format(Stream,')~n',[])
207 ; format(Stream,') &~n',[]),
208 output_clauses_as_b_pred(TC,Stream)
209 ).
210
211 output_clause([],Stream) :- nl(Stream).
212 output_clause([Lit|TC],Stream) :-
213 output_lit(Lit,Stream),
214 (TC=[] -> true
215 ; format(Stream,' or ',[]),
216 output_clause(TC,Stream)
217 ).
218
219 output_lit(Lit,Stream) :- Lit<0, !, L is -Lit,
220 format_id(Stream,L),format(Stream,' = FALSE',[]).
221 output_lit(Lit,Stream) :-
222 format_id(Stream,Lit),format(Stream,' = TRUE ',[]).
223
224 :- dynamic convert_as_array/0.
225 convert_as_array. % takes longer to convert to CNF later by ProB, but easier to manipulate, e.g., x~[{TRUE}]
226
227 format_id(Stream,Nr) :- convert_as_array,!,format(Stream,'x(~w)',[Nr]).
228 format_id(Stream,Nr) :- format(Stream,'x~w',[Nr]).
229
230 output_typing(Stream,From,To) :- convert_as_array,!,
231 format(Stream,' x:~w..~w --> BOOL &~n',[From,To]).
232 output_typing(Stream,From,_To) :-
233 format(Stream,' x~w : BOOL &~n',[From]). % TODO: add other if necessary
234
235 output_all_constants(Stream,_From,_To) :- convert_as_array,!,
236 format(Stream,' x',[]).
237 output_all_constants(Stream,From,To) :-
238 output_ids(Stream,From,To).
239 output_ids(Stream,From,To) :-
240 format(Stream,' ',[]), format_id(Stream,From),
241 F1 is From+1,
242 (F1>To -> true
243 ; format(Stream,',~n',[]),output_ids(Stream,F1,To)).