Skip to content

Commit

Permalink
try to fix header in source encoding
Browse files Browse the repository at this point in the history
  • Loading branch information
alpavlenko committed May 23, 2023
1 parent 9e4f125 commit f0cb463
Showing 1 changed file with 14 additions and 3 deletions.
17 changes: 14 additions & 3 deletions instance/module/encoding/impl/source.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,29 @@

class SourceData(EncodingData):
def __init__(self, lines: str = None):
self._lines = lines
line, tail = lines.split('\n', maxsplit=1)
if line.startswith('p'):
parts = line.split()
self._lines = tail
self.max_lit = int(parts[2])
self.clauses = int(parts[3])
else:
self._lines = lines
self.max_lit = 0
self.clauses = 0

def source(self, supplements: Supplements = ((), ())) -> str:
assumptions, constraints = supplements
clauses = self.clauses + len(constraints) + len(assumptions)
header = f'p cnf {self.max_lit} {clauses}\n' if self.clauses else ''
return ''.join([
self._lines, *(f'{x} 0\n' for x in assumptions),
header, self._lines, *(f'{x} 0\n' for x in assumptions),
*(' '.join(map(str, c)) + ' 0\n' for c in constraints),
])

@property
def max_literal(self) -> int:
return 0
return self.max_lit


class Source(Encoding):
Expand Down

0 comments on commit f0cb463

Please sign in to comment.