2828# https://www.gnu.org/licenses/
2929##############################################################################
3030
31- import os
31+ from pathlib import Path
3232import sys
3333import subprocess
3434import shlex
35+ from time import sleep
3536
3637from sage .sat .solvers .satsolver import SatSolver
3738from sage .misc .temporary_file import tmp_filename
38- from time import sleep
3939
4040
4141class DIMACS (SatSolver ):
@@ -44,7 +44,7 @@ class DIMACS(SatSolver):
4444
4545 .. NOTE::
4646
47- Usually, users won't have to use this class directly but some
47+ Usually, users will not have to use this class directly but some
4848 class which inherits from this class.
4949
5050 .. automethod:: __init__
@@ -136,10 +136,9 @@ def __del__(self):
136136 """
137137 if not self ._tail .closed :
138138 self ._tail .close ()
139- if os .path .exists (self ._tail .name ):
140- os .unlink (self ._tail .name )
141- if self ._headname_file_created_during_init and os .path .exists (self ._headname ):
142- os .unlink (self ._headname )
139+ Path (self ._tail .name ).unlink (missing_ok = True )
140+ if self ._headname_file_created_during_init :
141+ Path (self ._headname ).unlink (missing_ok = True )
143142
144143 def var (self , decision = None ):
145144 """
@@ -209,7 +208,7 @@ def add_clause(self, lits):
209208 self .var ()
210209 l .append (str (lit ))
211210 l .append ("0\n " )
212- self ._tail .write (" " .join (l ) )
211+ self ._tail .write (" " .join (l ))
213212 self ._lit += 1
214213
215214 def write (self , filename = None ):
@@ -246,19 +245,19 @@ def write(self, filename=None):
246245 headname = self ._headname if filename is None else filename
247246 head = open (headname , "w" )
248247 head .truncate (0 )
249- head .write ("p cnf %d %d\n " % (self ._var ,self ._lit ))
248+ head .write ("p cnf %d %d\n " % (self ._var , self ._lit ))
250249 head .close ()
251250
252251 tail = self ._tail
253252 tail .close ()
254253
255- head = open (headname ,"a" )
254+ head = open (headname , "a" )
256255 tail = open (self ._tail .name )
257256 head .write (tail .read ())
258257 tail .close ()
259258 head .close ()
260259
261- self ._tail = open (self ._tail .name ,"a" )
260+ self ._tail = open (self ._tail .name , "a" )
262261 return headname
263262
264263 def clauses (self , filename = None ):
@@ -313,7 +312,7 @@ def clauses(self, filename=None):
313312 if lit == 0 :
314313 break
315314 clause .append (lit )
316- clauses .append ( ( tuple (clause ), False , None ) )
315+ clauses .append (( tuple (clause ), False , None ) )
317316 tail .close ()
318317 self ._tail = open (self ._tail .name , "a" )
319318 return clauses
@@ -362,20 +361,19 @@ def render_dimacs(clauses, filename, nlits):
362361 1 2 -3 0
363362 <BLANKLINE>
364363 """
365- fh = open (filename , "w" )
366- fh .write ("p cnf %d %d\n " % (nlits ,len (clauses )))
367- for clause in clauses :
368- if len (clause ) == 3 and clause [1 ] in (True , False ) and clause [2 ] in (True ,False ,None ):
369- lits , is_xor , rhs = clause
370- else :
371- lits , is_xor , rhs = clause , False , None
372-
373- if is_xor :
374- closing = lits [- 1 ] if rhs else - lits [- 1 ]
375- fh .write ("x" + " " .join (map (str , lits [:- 1 ])) + " %d 0\n " % closing )
376- else :
377- fh .write (" " .join (map (str , lits )) + " 0\n " )
378- fh .close ()
364+ with open (filename , "w" ) as fh :
365+ fh .write ("p cnf %d %d\n " % (nlits , len (clauses )))
366+ for clause in clauses :
367+ if len (clause ) == 3 and clause [1 ] in (True , False ) and clause [2 ] in (True , False , None ):
368+ lits , is_xor , rhs = clause
369+ else :
370+ lits , is_xor , rhs = clause , False , None
371+
372+ if is_xor :
373+ closing = lits [- 1 ] if rhs else - lits [- 1 ]
374+ fh .write ("x" + " " .join (map (str , lits [:- 1 ])) + " %d 0\n " % closing )
375+ else :
376+ fh .write (" " .join (map (str , lits )) + " 0\n " )
379377
380378 def _run (self ):
381379 r"""
0 commit comments