Merge branch 'dev' into master.

Brings in all work on parallelization and a few other improvements.

CNFsolvers.py

@@ -1,4 +1,3 @@
-import array
 import atexit
 import bisect
 import collections
@@ -7,17 +6,28 @@
 import re
 import subprocess
 import tempfile
+import utils
 from pyminisolvers import minisolvers
 
 
-class MinisatSubsetSolver:
-    def __init__(self, infile, store_dimacs=False):
+class MinisatSubsetSolver(object):
+    def __init__(self, infile, rand_seed=None, store_dimacs=False):
         self.s = minisolvers.MinisatSubsetSolver()
+
+        # Initialize random seed and randomize variable activity if seed is given
+        if rand_seed is not None:
+            self.s.set_rnd_seed(rand_seed)
+            self.s.set_rnd_init_act(True)
+
         self.store_dimacs = store_dimacs
         if self.store_dimacs:
             self.dimacs = []
             self.groups = collections.defaultdict(list)
         self.read_dimacs(infile)
+        self._msolver = None
+
+    def set_msolver(self, msolver):
+        self._msolver = msolver
 
     def parse_dimacs(self, f):
         i = 0
@@ -49,6 +59,10 @@ def parse_dimacs(self, f):
             if line.startswith(b'c'):
                 continue
 
+            line = line.strip()
+            if line == b'':
+                continue
+
             # anything else is a clause
             assert self.n > 0
             vals = line.split()
@@ -74,7 +88,7 @@ def parse_dimacs(self, f):
                     self.dimacs.append(b" ".join(str(x).encode() for x in clause) + b" 0\n")
                     self.groups[groupid].append(i)
                 else:
-                    self.dimacs.append(line)
+                    self.dimacs.append(line + b"\n")
                     self.groups[groupid] = [i]
 
             i += 1
@@ -85,27 +99,31 @@ def read_dimacs(self, infile):
         if infile.name.endswith('.gz'):
             # use gzip to decompress
             infile.close()
-            with gzip.open(infile.name) as gz_f:
+            with gzip.open(infile.name, 'rb') as gz_f:
                 self.parse_dimacs(gz_f)
         else:
+            # XXX TODO: using open() here to avoid dupe infile object for parallel branch,
+            #           but this breaks reading from stdin.
             # assume plain .cnf and pass through the file object
-            self.parse_dimacs(infile)
+            with open(infile.name, 'rb') as f:
+                self.parse_dimacs(f)
 
     def check_subset(self, seed, improve_seed=False):
-        is_sat = self.s.solve_subset(seed)
+        is_sat = self.s.solve_subset([i-1 for i in seed])
         if improve_seed:
             if is_sat:
-                seed = self.s.sat_subset()
+                seed = self.s.sat_subset(offset=1)
             else:
-                seed = self.s.unsat_core()
+                seed = self.s.unsat_core(offset=1)
             return is_sat, seed
         else:
             return is_sat
 
     def complement(self, aset):
-        return set(range(self.n)).difference(aset)
+        return set(range(1, self.n+1)).difference(aset)
 
-    def shrink(self, seed, hard=[]):
+    def shrink(self, seed):
+        hard = self._msolver.implies()
         current = set(seed)
         for i in seed:
             if i not in current or i in hard:
@@ -114,7 +132,7 @@ def shrink(self, seed, hard=[]):
             current.remove(i)
             if not self.check_subset(current):
                 # Remove any also-removed constraints
-                current = set(self.s.unsat_core())  # helps a bit
+                current = set(self.s.unsat_core(offset=1))  # helps a bit
             else:
                 current.add(i)
         return current
@@ -132,11 +150,8 @@ def check_above(self, seed):
         self.s.add_clause([-x])  # remove the temporary clause
         return ret
 
-    def grow(self, seed, inplace):
-        if inplace:
-            current = seed
-        else:
-            current = seed[:]
+    def grow(self, seed):
+        current = seed
 
         #while self.check_above(current):
         #    current = self.s.sat_subset()
@@ -153,31 +168,23 @@ def grow(self, seed, inplace):
             current.append(x)
             if self.check_subset(current):
                 # Add any also-satisfied constraint
-                current = self.s.sat_subset()
+                current = self.s.sat_subset(offset=1)
             else:
                 current.pop()
 
         return current
 
 
-class MUSerException(Exception):
-    pass
-
-
 class MUSerSubsetSolver(MinisatSubsetSolver):
-    def __init__(self, filename):
-        MinisatSubsetSolver.__init__(self, filename, store_dimacs=True)
+    def __init__(self, filename, rand_seed=None, numthreads=1):
+        MinisatSubsetSolver.__init__(self, filename, rand_seed, store_dimacs=True)
         self.core_pattern = re.compile(r'^v [\d ]+$', re.MULTILINE)
-        self.muser_path = os.path.join(os.path.dirname(os.path.realpath(__file__)), 'muser2-static')
-        if not os.path.isfile(self.muser_path):
-            raise MUSerException("MUSer2 binary not found at %s" % self.muser_path)
-        try:
-            # a bit of a hack to check whether we can really run it
-            DEVNULL = open(os.devnull, 'wb')
-            subprocess.Popen([self.muser_path], stdout=DEVNULL, stderr=DEVNULL)
-        except:
-            raise MUSerException("MUSer2 binary %s is not executable.\n"
-                                 "It may be compiled for a different platform." % self.muser_path)
+        self.numthreads = numthreads
+        self.parallel = (numthreads > 1)
+
+        binary = 'muser2-para'
+        self.muser_path = os.path.join(os.path.dirname(os.path.realpath(__file__)), binary)
+        utils.check_executable("MUSer2", self.muser_path)
 
         self._proc = None  # track the MUSer process
         atexit.register(self.cleanup)
@@ -201,39 +208,121 @@ def write_CNF(self, cnffile, seed, hard):
             cnffile.write(self.dimacs[j])
         # also include hard clauses in "Don't care" group
         for i in hard:
-            for j in self.groups[i+1]:
+            for j in self.groups[i]:
                 cnffile.write(b"{0} ")
                 cnffile.write(self.dimacs[j])
 
         for g, i in enumerate(seed):
             if i in hard:
                 # skip hard clauses
                 continue
-            for j in self.groups[i+1]:
+            for j in self.groups[i]:
                 cnffile.write(("{%d} " % (g+1)).encode())
                 cnffile.write(self.dimacs[j])
 
         cnffile.flush()
 
     # override shrink method to use MUSer2
     # NOTE: seed must be indexed (i.e., not a set)
-    def shrink(self, seed, hard=[]):
+    def shrink(self, seed):
+        hard = [x for x in self._msolver.implies() if x > 0]
+        # In parallel mode, this seed may be explored by the time
+        # we get here.  If it is, the hard constraints may include
+        # constraints *outside* of the current seed, which would invalidate
+        # the returned MUS.  If the seed is explored, give up on this seed.
+        if not self._msolver.check_seed(seed):
+            return None
+
+        # Parallel MUSer doesn't like a formula with only hard constraints,
+        # and it's a waste of time to call MUSer at all on it anyway.
+        if len(seed) == len(hard):
+            return seed
+
         # Open tmpfile
         with tempfile.NamedTemporaryFile('wb') as cnf:
             self.write_CNF(cnf, seed, hard)
+            args = [self.muser_path, '-comp', '-grp', '-v', '-1']
+            if self.parallel:
+                args += ['-threads', str(self.numthreads), '-tmp']
+            args += [cnf.name]
 
             # Run MUSer
-            self._proc = subprocess.Popen([self.muser_path, '-comp', '-grp', '-v', '-1', cnf.name],
-                                          stdout=subprocess.PIPE, stderr=subprocess.PIPE)
+            self._proc = subprocess.Popen(args, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
             out, err = self._proc.communicate()
             self._proc = None  # clear it when we're done (so cleanup won't try to kill it)
+
             out = out.decode()
 
         # Parse result, return the core
         matchline = re.search(self.core_pattern, out).group(0)
-        ret = array.array('i', (seed[int(x)-1] for x in matchline.split()[1:-1]) )
+        # pMUSer outputs 0 groups as part of MUSes, so we'll just filter it out to prevent the
+        # duplicate clauses in MUSes
+        ret = [seed[int(x)-1] for x in matchline.split()[1:-1] if int(x) > 0]
 
         # Add back in hard clauses
         ret.extend(hard)
 
+        assert len(ret) <= len(seed)
+
         return ret
+
+
+class ImprovedImpliesSubsetSolver(MinisatSubsetSolver):
+    def __init__(self, infile, rand_seed=None, store_dimacs=False):
+        MinisatSubsetSolver.__init__(self, infile, rand_seed, store_dimacs)
+        self._known_MSS = 0
+        self._known_MUS = 0
+
+    def increment_MSS(self):
+        self._known_MSS += 1
+
+    def increment_MUS(self):
+        self._known_MUS += 1
+
+    def shrink(self, seed):
+        current = set(seed)
+
+        if self._known_MSS > 0:
+            implications = self._msolver.implies(-x for x in self.complement(current))
+            hard = set(x for x in implications if x > 0)
+        else:
+            hard = set()
+
+        for i in seed:
+            if i not in current or i in hard:
+                continue
+            current.remove(i)
+
+            if self.check_subset(current):
+                current.add(i)
+            else:
+                current = set(self.s.unsat_core(offset=1))
+                if self._known_MSS > 0:
+                    implications = self._msolver.implies(-x for x in self.complement(current))
+                    hard = set(x for x in implications if x > 0)
+
+        return current
+
+    def grow(self, seed):
+        current = set(seed)
+
+        if self._known_MUS > 0:
+            implications = self._msolver.implies(current)
+            dont_add = set(x for x in implications if x < 0)
+        else:
+            dont_add = set()
+
+        for i in self.complement(current):
+            if i in current or i in dont_add:
+                continue
+            current.add(i)
+
+            if not self.check_subset(current):
+                current.remove(i)
+            else:
+                current = set(self.s.sat_subset(offset=1))
+                if self._known_MUS > 0:
+                    implications = self._msolver.implies(current)
+                    dont_add = set(x for x in implications if x < 0)
+
+        return current