<file_sep>#!/usr/bin/env python3

"""
    run.py
    ======

    Script for executable module.

    Compute a hash value for the given DIMACS file.

    * Ignores comments 'c' and '%' lines
    * Order of clauses matters
    * Order of literals matters

    A more formal specification is provided at
    `cnfhash project homepage <http://lukas-prokop.at/proj/cnfhash/>`_.

    (C) <NAME>, 2016, Public Domain
"""

import gzip
import os.path
import argparse
import datetime
import multiprocessing

from . import hashing


def read_chunks(fd, chunk_size=None):
    """Read chunks from a file descriptor"""
    if chunk_size is None:
        import resource
        chunk_size = resource.getpagesize()
    while True:
        data = fd.read(chunk_size)
        if not data:
            break
        yield data


def run(arg):
    args, dimacsfile = arg
    if dimacsfile.endswith('.gz'):
        opener = gzip.open
    else:
        opener = open

    with opener(dimacsfile, 'rb') as fd:
        ignore_lines = b'c'
        for prefix in (args.ignore or []):
            ignore_lines += prefix.encode('ascii')
        try:
            gen = read_chunks(fd)
            hashvalue = hashing.hash_dimacs(gen, ignore_lines=ignore_lines)
        except hashing.DimacsSyntaxError as e:
            raise hashing.DimacsSyntaxError("Error while processing {}".format(dimacsfile))

    filename = os.path.basename(dimacsfile)
    print('{:<45}  {}'.format(hashvalue, dimacsfile if args.fullpath else filename))


def main():
    parser = argparse.ArgumentParser(description='CNF hashing')
    parser.add_argument('dimacsfiles', metavar='dimacsfiles', nargs='+',
                        help='filepath of DIMACS file')
    parser.add_argument('--ignore', action='append',
                        help='a prefix for lines that shall be ignored (like "c")')
    parser.add_argument('-f', '--fullpath', action='store_true',
                        help='the hash value will be followed by the filepath, not filename')

    args = parser.parse_args()
    print('cnf-hash-py 2.1.2 {} {}'.format(datetime.datetime.utcnow().isoformat(), os.getcwd()))
    with multiprocessing.Pool(multiprocessing.cpu_count()) as pool:
        pool.map(run, zip([args] * len(args.dimacsfiles), args.dimacsfiles))

if __name__ == '__main__':
    main()
<file_sep>#!/usr/bin/env python3

"""
    cnfhash.hashing
    ---------------

    Integer hashing library for cnfhash.

    (C) <NAME>, 2015, Public Domain
"""

import os
import string
import hashlib
import functools

LITERAL_DELIM = b' '
CLAUSE_DELIM = b'0\n'
ENCODING = 'ascii'


def hash_cnf(ints: [int], check_header=True):
    """Hash a given CNF defined as sequence of integers.

    `ints` is a sequence of integers:
    (1) the first 2 integers are expected to be nbvars and nbclauses
    (2) the following integers are considered literals
        where 0 terminates a clause

    Hence, the following file::

        p cnf 3 2
        1 -3 0
        -1 2 0

    will be hashed correctly by calling::

        hash_cnf([3, 2, 1, -3, 0, -1, 2, 0])

    If `check_header` is False, all checks related to nbvars and nbclauses
    will be skipped.
    """
    sha1 = hashlib.sha1()
    clause_ended = False
    nbclauses = None
    clauses = 0

    for i, lit in enumerate(ints):
        if i == 0:
            nbvars = lit
            clause_ended = False
            if nbvars <= 0:
                tmpl = "nbvars must be non-negative, is {}".format(lit)
                raise ValueError(tmpl)
        elif i == 1:
            nbclauses = lit
            clause_ended = False
            if nbclauses <= 0:
                tmpl = "nbclauses must be non-negative, is {}".format(lit)
                raise ValueError(tmpl)
        elif lit == 0:
            if clause_ended:
                continue  # multiple zeros truncated to a single one
            clauses += 1
            sha1.update(CLAUSE_DELIM)
            clause_ended = True
        else:
            clause_ended = False
            if check_header and not (-nbvars <= lit <= nbvars):
                tmpl = "Variable {} outside range ({})--({})".format(lit, -nbvars, nbvars)
                raise ValueError(tmpl)
            sha1.update(str(lit).encode(ENCODING))
            sha1.update(LITERAL_DELIM)

    if not clause_ended:
        sha1.update(CLAUSE_DELIM)
        clauses += 1
    if nbclauses is None:
        errmsg = "Premature end, CNF must at least contain header values"
        raise ValueError(errmsg)
    if not clause_ended:
        raise ValueError("CNF must be terminated by zero")
    if check_header and nbclauses != clauses:
        tmpl = "Invalid number of clauses, expected {}, got {} clauses"
        raise ValueError(tmpl.format(nbclauses, clauses))

    return 'cnf2$' + sha1.hexdigest()


def hash_decorator(f):
    """Decorator wrapping `hash_cnf`"""
    @functools.wraps(f)
    def inner(*args, **kwargs):
        return hash_cnf(f(*args, **kwargs))
    return inner


class DimacsSyntaxError(Exception):
    """An exception representing a syntax error in DIMACS"""
    pass


@hash_decorator
def hash_dimacs(dimacs_bytes, ignore_lines=b'c%'):
    """Given a DIMACS file as sequence of bytes,
    return the corresponding cnfhash.

    `dimacs_bytes`
      A sequence of byte specifying content in DIMACS format.
    `ignore_lines`
      A sequence of characters. If a line starts with this
      character, the line is ignored. Example::

          ignore_lines=b'c'

      will ignore all lines like::

          c this is a comment
    """
    # '%' is included because ... there are strange CNF files out there
    skip_line = False
    got_newline = False
    got_line_whitespace = False
    start, end = 0, 0
    mode = 0
    lineno = 1
    intcache = ""

    WS = set(string.whitespace.encode(ENCODING))
    LINE_WS = set(string.whitespace.replace('\n', '').encode(ENCODING))
    DIGIT = set(string.digits.encode(ENCODING))
    HYPHEN = ord('-')
    NEWLINE = ord('\n')
    KEYWORD = b'pcnf'

    def unexp_byte(given, expected):
        errmsg = "Unexpected byte {} found at line {}, expected {}"
        return DimacsSyntaxError(errmsg.format(bytes([given]), lineno, expected))

    # I know this is a rdiciulously long state machine.
    # However, a consume-parser design was terribly slow
    while True:
        try:
            block = next(dimacs_bytes)
        except StopIteration:
            break

        for i in range(len(block)):
            if block[i] == NEWLINE:
                lineno += 1
            if skip_line:
                if block[i] == NEWLINE:
                    skip_line = False
                    got_newline = True
                continue

            if block[i] in LINE_WS:
                got_line_whitespace = True
            elif block[i] == NEWLINE:
                got_newline = True
            else:
                char = block[i]
                if mode == 0:
                    if char == ord(b'p'):
                        mode = 1
                    elif char in set(ignore_lines):
                        skip_line = True
                    else:
                        raise unexp_byte(char, "keyword 'p'")
                elif mode == 1:
                    if not got_line_whitespace:
                        raise unexp_byte(char, "whitespace")
                    elif char == ord(b'c'):
                        mode = 2
                    else:
                        raise unexp_byte(char, "keyword 'cnf'")
                elif mode == 2:
                    if not got_line_whitespace and char == ord(b'n'):
                        mode = 3
                    else:
                        raise unexp_byte(char, "keyword 'cnf'")
                elif mode == 3:
                    if not got_line_whitespace and char == ord(b'f'):
                        mode = 4
                    else:
                        raise unexp_byte(char, "keyword 'cnf'")
                elif mode == 4:
                    if got_line_whitespace and char in DIGIT:
                        intcache += chr(char)
                        mode = 5
                    else:
                        raise unexp_byte(char, "non-negative integer")
                elif mode == 5:
                    if not got_line_whitespace and char in DIGIT:
                        intcache += chr(char)
                    elif got_line_whitespace and char in DIGIT:
                        yield int(intcache)
                        intcache = chr(char)
                        mode = 6
                    else:
                        raise unexp_byte(char, "non-negative integer")
                elif mode == 6:
                    if got_line_whitespace or got_newline:
                        yield int(intcache)
                        if char in DIGIT or char == HYPHEN:
                            intcache = chr(char)
                        else:
                            intcache = ''
                            if got_newline and char in set(ignore_lines):
                                skip_line = True
                        mode = 7
                    elif not got_line_whitespace and char in DIGIT:
                        intcache += chr(char)
                    else:
                        raise unexp_byte(char, "non-negative integer")
                elif mode == 7:
                    if (got_line_whitespace or got_newline) and intcache:
                        yield int(intcache)
                        intcache = ''
                    if got_newline and char in set(ignore_lines):
                        skip_line = True
                    elif char in DIGIT or char == HYPHEN:
                        intcache += chr(char)
                    else:
                        raise unexp_byte(char, "digit or hyphen")

                got_line_whitespace = False
                got_newline = False

    if intcache:
        yield int(intcache)
<file_sep>from .run import main
main()
<file_sep>#!/usr/bin/env python3

"""
    cnf-hash
    --------

    A library to hash CNF/DIMACS files.

    (C) <NAME>, 2016, Public Domain
"""

from . import hashing

hash_cnf = hashing.hash_cnf
hash_dimacs = hashing.hash_dimacs

__author__ = '<NAME>'
__version_info__ = ('1', '0', '0')
__version__ = '.'.join(__version_info__)
__license__ = 'Public Domain'
__docformat__ = 'reStructuredText en'
<file_sep>#!/usr/bin/env python3

"""
    cnfhash.test
    ------------

    Testsuite for the python3 implementation of CNF hashing.

    Provide the folder to the testsuite either as environment
    variable TESTSUITE, as second command line parameter or
    'testsuite' is taken.

    'testsuite' is a folder with CNF files with their hash value
    in their name like `cnf-hash-test <https://github.com/prokls/cnf-hash-tests>`_.

    (C) <NAME>, 2016, Public Domain
"""

import sys
import os.path
import unittest

import cnfhash


class CnfHashingTestsuite(unittest.TestCase):
    def test_testsuite(self):
        testsuite = sys.argv[1] if len(sys.argv) > 1 else 'testsuite'
        testsuite = dict(os.environ).get('TESTSUITE', testsuite)

        for filename in os.listdir(testsuite):
            if not filename.endswith('.cnf'):
                continue
            if os.path.isdir(os.path.join(testsuite, filename)):
                continue

            filepath = os.path.join(testsuite, filename)
            hashvalue = filename.split('_')[0]

            with open(filepath, 'rb') as fd:
                try:
                    comp_hashvalue = cnfhash.hash_dimacs(fd)
                    assert comp_hashvalue[0:5] == 'cnf2$'
                except Exception as e:
                    print('Failure while processing testcase {}'.format(filepath), file=sys.stderr)
                    raise e

            self.assertEqual(hashvalue, comp_hashvalue[5:], filename[len(hashvalue) + 1:])


if __name__ == '__main__':
    unittest.main()
<file_sep>cnf-hash-py
===========

:author:        <NAME>
:date:          August 2015, May 2016
:version:       2.1.2
:license:       CC-0

A python3 implementation to hash DIMACS CNF files.
See `the technical report <http://lukas-prokop.at/proj/megosat/downloads/cnf-hash.pdf>`_ for more details.
This implementation was pushed to `Python Package Index PyPI <https://pypi.python.org/pypi/cnfhash>`_.

How to use
----------

To install use pip3::

    pip3 install cnfhash

Then you can use the following API in python3::

    import cnfhash

    # reading blockwise from a DIMACS file

    def read_blockwise(filepath):
        with open(filepath) as fd:
            while True:
                buf = fd.read(4096)
                if len(buf) == 0:
                    break
                yield buf

    reader = read_blockwise('test.cnf')
    print(cnfhash.hash_dimacs(reader))

    # or use integers directly

    print(cnfhash.hash_cnf([3, 2, 1, -3, 0, -1, 2, 0]))

Testing the software
--------------------

Download `the testsuite <http://github.com/prokls/cnf-hash-tests1/>`_.
Provide the folder location as environment variable::

    export TESTSUITE="/home/prokls/Downloads/cnf-hash/tests1/"

Then run all files in the ``tests`` directory::

    python3 tests/test_testsuite.py

The testsuite has been run successfully, if the exit code has always been 0.

DIMACS file assumptions
-----------------------

A DIMACS file is valid iff

1. Any line starting with "c" or consisting only of whitespace is considered as *comment line* and content is not interpreted until the next newline character occurs.
2. The remaining file is a sequence of whitespace separated values.

   1. The first value is required to be "p"
   2. The second value is required to be "cnf"
   3. The third value is required to be a non-negative integer and called *nbvars*.
   4. The fourth value is required to be a non-negative integer and called *nbclauses*.
   5. The remaining non-zero integers are called *lits*.
   6. The remaining zero integers are called *clause terminators*.

3. A DIMACS file must be terminated by a clause terminator.
4. Every lit must satisfy ``-nbvars ≤ lit ≤ nbvars``.
5. The number of clause terminators must equate nbclauses.

============== =========================================
**term**       **ASCII mapping**
-------------- -----------------------------------------
"c"            U+0063
"p"            U+0070
"cnf"          U+0063 U+006E U+0066 U+0020
sign           U+002D
nonzero digit  U+0031 – U+0039
digits         U+0030 – U+0039
whitespace     U+0020, U+000D, U+000A, U+0009
zero           U+0030
============== =========================================

Formal specification
--------------------

A valid DIMACS file is read in and a SHA1 instance is fed with bytes:

1. The first four values are dropped.
2. Lits are treated as integers without leading zeros. Integers are submitted as base 10 ASCII digits with an optional leading sign to the SHA1 instance.
3. Clause terminators are submitted as zero character followed by a newline character to the SHA1 instance.

Performance and memory
----------------------

The DIMACS parser uses OS' page size as default block size.
A few constant values and the python runtime is also stored in memory.
So for a python program, this implementation is very memory-friendly.

The technical report shows that 45 DIMACS files summing up to 1 GB memory
can be read in 2989 seconds. In terms of performance, the equivalent `Go
implementation <http://github.com/prokls/cnf-hash-go/>`_ is recommended.

Example
-------

::

    % cat test.cnf
    p cnf 5 6
    1 2 3 0
    2 3 -4 0
    1 -2 0
    -1 2 0
    1 3 5 0
    1 -4 -5 0
    % cnf-hash-py test.cnf
    cnf-hash-py 2.1.2 2016-05-29T12:27:13.991260 /root
    cnf2$776d81a0c805104e265667917b22ffefe9f39433  test.cnf
    %

Cheers!
