@@ -55,7 +55,7 @@ Function: cnft::gate_and
5555
5656 Outputs:
5757
58- Purpose:
58+ Purpose: Tseitin encoding of conjunction of two literals
5959
6060\*******************************************************************/
6161
@@ -88,7 +88,7 @@ Function: cnft::gate_or
8888
8989 Outputs:
9090
91- Purpose:
91+ Purpose: Tseitin encoding of disjunction of two literals
9292
9393\*******************************************************************/
9494
@@ -120,7 +120,7 @@ Function: cnft::gate_xor
120120
121121 Outputs:
122122
123- Purpose:
123+ Purpose: Tseitin encoding of XOR of two literals
124124
125125\*******************************************************************/
126126
@@ -161,7 +161,7 @@ Function: cnft::gate_nand
161161
162162 Outputs:
163163
164- Purpose:
164+ Purpose: Tseitin encoding of NAND of two literals
165165
166166\*******************************************************************/
167167
@@ -193,7 +193,7 @@ Function: cnft::gate_nor
193193
194194 Outputs:
195195
196- Purpose:
196+ Purpose: Tseitin encoding of NOR of two literals
197197
198198\*******************************************************************/
199199
@@ -225,7 +225,7 @@ Function: cnft::gate_equal
225225
226226 Outputs:
227227
228- Purpose:
228+ Purpose: Tseitin encoding of equality between two literals
229229
230230\*******************************************************************/
231231
@@ -242,7 +242,7 @@ Function: cnft::gate_implies
242242
243243 Outputs:
244244
245- Purpose:
245+ Purpose: Tseitin encoding of implication between two literals
246246
247247\*******************************************************************/
248248
@@ -259,7 +259,7 @@ Function: cnft::land
259259
260260 Outputs:
261261
262- Purpose:
262+ Purpose: Tseitin encoding of conjunction between multiple literals
263263
264264\*******************************************************************/
265265
@@ -310,7 +310,7 @@ Function: cnft::lor
310310
311311 Outputs:
312312
313- Purpose:
313+ Purpose: Tseitin encoding of disjunction between multiple literals
314314
315315\*******************************************************************/
316316
@@ -361,7 +361,7 @@ Function: cnft::lxor
361361
362362 Outputs:
363363
364- Purpose:
364+ Purpose: Tseitin encoding of XOR between multiple literals
365365
366366\*******************************************************************/
367367
@@ -387,7 +387,7 @@ Function: cnft::land
387387
388388 Outputs:
389389
390- Purpose:
390+ Purpose:
391391
392392\*******************************************************************/
393393
@@ -583,7 +583,7 @@ Function: cnft::new_variable
583583
584584 Outputs:
585585
586- Purpose:
586+ Purpose: Generate a new variable and return it as a literal
587587
588588\*******************************************************************/
589589
@@ -605,7 +605,7 @@ Function: cnft::eliminate_duplicates
605605
606606 Outputs:
607607
608- Purpose:
608+ Purpose: eliminate duplicates from given vector of literals
609609
610610\*******************************************************************/
611611
@@ -628,7 +628,8 @@ Function: cnft::process_clause
628628
629629 Outputs:
630630
631- Purpose:
631+ Purpose: filter 'true' from clause, eliminate duplicates,
632+ recognise trivially satisfied clauses
632633
633634\*******************************************************************/
634635
0 commit comments