forked from tammet/logictools
-
Notifications
You must be signed in to change notification settings - Fork 0
/
proplog_parse.js
304 lines (251 loc) · 8.09 KB
/
proplog_parse.js
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
/*
Propositional logic formula and clause set (dimacs) syntax parsers.
Use like this:
proplog_parse.parse("-1 2\n 1 \n -2") parses both dimacs and formulas
proplog_parse.parse_tree("-1 2\n 1 \n -2") returns parse result as a string
proplog_parse.parse_dimacs("-1 2\n 1 \n -2")
proplog_parse.parse_formula("x=>y & x & -y")
Fully self-contained, no dependencies.
Exports functions
parse
parse_tree
parse_dimacs
parse_formula
See http://logictools.org and http://github.com/tammet/logictools
for UI and other tools.
Recommended to use with the accompanying proplog.html file providing
a basic user interface and other tools for propositional logic.
This software is covered by the MIT licence, see http://opensource.org/licenses/MIT
or http://en.wikipedia.org/wiki/MIT_License
Copyright (c) 2015 Tanel Tammet (tanel.tammet at gmail.com)
*/
(function(exports) {
"use strict";
// ====== module start =========
// ====== universal parser ==========
/* parse tries to first interpret input as dimacs text,
if this fails, it tries to parse input as a formula.
Input:
- txt: plain text in dimacs or formula syntax
Returns one of:
- parsed dimacs as [2,[-1,2],[1],[-2]] (first el is nr of vars)
- parsed formula as ["&",["->","a","b"],"b"]]
- formula parsing error as ["error",some_err_string]
*/
exports.parse = function(txt) {
var tmp;
tmp=exports.parse_dimacs(txt);
if (tmp[0]!==0 && tmp.length>1) {
// possibly dimacs
if (tmp[1].length>0) return tmp;
}
// here we assume non-dimacs, parse as formula
tmp=exports.parse_formula(txt);
return tmp;
}
/* parse_tree returns a human-readable parse result string
built by stringifying the result of parse_formula.
& and V operators are added to dimacs parse results.
*/
exports.parse_tree = function(txt) {
var tmp,i,res;
tmp=exports.parse(txt);
if (err_data(tmp))
return ("syntax error: "+tmp[1]);
else if (typeof tmp[0]=="number") {
// dimacs: add & and V operators
res=["&"];
for(i=1;i<tmp.length;i++) {
if (tmp[i].length>1) res.push(["V"].concat(tmp[i]));
else if (tmp[i].length===1) res.push(tmp[i][0]);
}
return JSON.stringify(res);
} else {
// formula
return JSON.stringify(tmp);
}
}
/* ============
Parse dimacs format string and return a list where
- first el is the maximal variable nr (always positive)
- from the second el start clauses like [[1,-2],[-2,1]]
for example: [2,[1,-2],[-2,1]]
We parse a superset of dimacs, where
- c and p lines may be missing altogether
- textual variable names like var7 may be used in addition to numeric variable names
- 0 at end may be missing
Standard dimacs formula example:
c start with comments
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0
We allow also the following form of the previous example:
x -5 4
-x 5 y 4
-y -4
===============
*/
exports.parse_dimacs = function(txt) {
var clauses,clause,lines,line,spl,i,j,sv,nv,anv,maxv;
clauses=[];
maxv=0;
lines=txt.split("\n");
for(i=0;i<lines.length;i++) {
line=lines[i].trim();
if (!line || line.lastIndexOf("c",0)===0 || line.lastIndexOf("p",0)===0) continue;
clause=[];
spl=line.split(" ");
for(j=0;j<spl.length;j++) {
sv=spl[j];
if (!sv) continue;
nv=parseInt(sv);
if (isNaN(nv)) continue;
if (nv===0) break;
anv=nv;
if (anv<0) anv=anv * -1;
if (anv>maxv) maxv=anv;
clause.push(nv);
}
if (clause) clauses.push(clause);
}
clauses.unshift(maxv); // prepend to clause list
return clauses;
}
/* =========================
Parse a non-clausal formula in the traditional infix notation like
(a & -b) -> c
where
negation symbols are -, ~ : - is used in the constructed term
conjunction symbols are &,and: & is used in the constructed term
disjunction symbols are |,v,V,or : V is used in the constructed term
xor symbols are +,xor : + is used in the constructed term
implication symbols are ->,=> : -> is used in the constructed term
equivalence symbols are <->,<=> : <-> is used in the constructed term
There is no operator precedence: all operators are bound from left:
a & b v c & d v e
is parsed as
[V,[&,[V,[&,a,b],c],d],e]
=========================
*/
/* parse_formula returns a parse tree as a nested list like
["&",["-","a"],"b"]
In the error case it returns
["error", concrete_error_message_string]
*/
exports.parse_formula = function(txt) {
var tmp,exp,pos;
tmp=parse_expression_tree(txt,0);
if (err_data(tmp)) return tmp;
exp=tmp[0];
pos=tmp[1];
tmp=parse_skip(txt,pos);
if (tmp<txt.length)
return (parse_error("remaining text at "+txt.substring(pos)));
else
return exp;
}
function parse_expression_tree(txt,pos) {
var isneg,exp,op,node,tmp;
pos=parse_skip(txt,pos);
isneg=false;
if (parse_isatpos(txt,pos,"-")) { isneg=true; pos++;}
else if (parse_isatpos(txt,pos,"~")) { isneg=true; pos++;}
tmp=parse_term_tree(txt,pos);
if (err_data(tmp)) return tmp;
exp=tmp[0];
pos=tmp[1];
if (isneg) exp=["-",exp];
pos=parse_skip(txt,pos);
while(true) {
op=null;
if (parse_isatpos(txt,pos,"&")===true) { op="&"; pos++; }
else if (parse_isatpos(txt,pos,"and")===true) { op="&"; pos+=3; }
else if (parse_isatpos(txt,pos,"+")===true) { op="+"; pos++; }
else if (parse_isatpos(txt,pos,"xor")===true) { op="+"; pos+=3; }
else if (parse_isatpos(txt,pos,"|")===true) { op="V"; pos++; }
else if (parse_isatpos(txt,pos,"v")===true) { op="V"; pos++; }
else if (parse_isatpos(txt,pos,"V")===true) { op="V"; pos++; }
else if (parse_isatpos(txt,pos,"or")===true) { op="V"; pos+=3; }
else if (parse_isatpos(txt,pos,"->")===true) { op="->"; pos+=2; }
else if (parse_isatpos(txt,pos,"=>")===true) { op="->"; pos+=2; }
else if (parse_isatpos(txt,pos,"<->")===true) { op="<->"; pos+=3; }
else if (parse_isatpos(txt,pos,"<=>")===true) { op="<->"; pos+=3; }
if (op===null) break;
tmp=parse_term_tree(txt,pos);
if (err_data(tmp)) return tmp;
exp=[op,exp,tmp[0]];
pos=tmp[1];
pos=parse_skip(txt,pos);
if (pos>=txt.length) break;
}
return [exp,pos];
}
function parse_term_tree(txt,pos) {
var c,n,j,v,tmp,exp,found,isneg;
pos=parse_skip(txt,pos);
isneg=false;
if (parse_isatpos(txt,pos,"-")) { isneg=true; pos++; pos=parse_skip(txt,pos); }
else if (parse_isatpos(txt,pos,"~")) { isneg=true; pos++; pos=parse_skip(txt,pos); }
j=pos;
found=false;
v=null;
while(true) {
c=txt.charAt(j);
n=txt.charCodeAt(j);
// numbers and letters
if (j<txt.length && ((n>=48 && n<=57) || (n>=65 && n<=122))) { j++; continue; }
// not a number or a letter or at the end of text
if (j>pos) {
// a var was found
v=txt.substring(pos,j);
if (isneg) return [["-",v],j];
return [v,j];
}
break;
}
if (c==="(") {
pos++;
tmp=parse_expression_tree(txt,pos);
if (err_data(tmp)) return tmp;
exp=tmp[0];
pos=tmp[1];
pos=parse_skip(txt,pos);
if (txt.charAt(pos)!==")")
return(parse_error("right parenthesis missing"));
pos++;
if (isneg) return [["-",exp],pos];
return[exp,pos];
} else if (c===")") {
return(parse_error("extra right parenthesis at "+txt.substring(pos)));
} else {
return(parse_error("unexpected text "+c+" encountered at "+txt.substring(pos)));
}
}
function parse_isatpos(txt,pos,str) {
if(str.length===1) {
if(txt.charAt(pos)===str) return true;
else return false;
} else {
if(txt.substr(pos,str.length)===str) return true;
else return false;
}
}
function parse_skip(txt,pos) {
var c;
while(pos<txt.length) {
c=txt.charAt(pos);
if (c===" " || c==="\t" || c==="\n" || c==="\r") pos++;
else break;
}
return pos;
}
function parse_error(txt) {
return ["error",txt];
}
function err_data(data) {
if (typeof data!== "string" && data[0]==="error") return true;
else return false;
}
// ====== module end ==========
})(this.proplog_parse = {});