Simplifications for 0.9 release.

MarcoPolo.py

@@ -38,16 +38,8 @@ def enumerate(self):
                 # subset check may improve upon seed w/ unsat_core or sat_subset
                 seed_is_sat, seed = self.subs.check_subset(seed, improve_seed=True)
 
-            if self.config['half_max'] and not known_max and (seed_is_sat == self.bias_high):
-                assert not self.config['maxseed']
-                with self.timer.measure('half_max'):
-                    # Maximize within Map and re-check satisfiability
-                    seed = self.map.maximize_seed(seed, direction=self.bias_high)
-                    seed_is_sat, seed = self.subs.check_subset(seed, improve_seed=True)
-                    known_max = True
-
             if seed_is_sat:
-                if self.bias_high and (self.config['nogrow'] or known_max):
+                if self.bias_high and known_max:
                     MSS = seed
                 else:
                     with self.timer.measure('grow'):
@@ -56,15 +48,6 @@ def enumerate(self):
                 yield ("S", MSS)
                 self.map.block_down(MSS)
 
-                if self.config['mssguided']:
-                    with self.timer.measure('mssguided'):
-                        # don't check parents if parent is top and we've already seen it (common)
-                        if len(MSS) < self.n-1 or not self.got_top:
-                            # add any unexplored superset to the queue
-                            newseed = self.map.find_above(MSS)
-                            if newseed:
-                                self.seeds.add_seed(newseed, False)
-
             else:
                 self.got_top = True  # any unsat set covers the top of the lattice
                 if known_max and not self.bias_high:
@@ -75,9 +58,6 @@ def enumerate(self):
 
                 yield ("U", MUS)
                 self.map.block_up(MUS)
-                if self.config['smus']:
-                    self.map.block_down(MUS)
-                    self.map.block_above_size(len(MUS)-1)
 
 
 class SeedManager:

VERSION

@@ -1 +1 @@
-0.8.9
+0.9

marco.py

@@ -26,14 +26,6 @@ def parse_args():
                         help="always find a maximal/minimal seed (local optimum), controlled by bias setting (high=maximal, low=minimal)")
     max_group.add_argument('-M', '--maximum-seed', action='store_true',
                         help="always find a maximum/minimum seed (largest/smallest cardinality), controlled by bias setting (high=maximum, low=minimum) (uses MiniCard as Map solver)")
-    parser.add_argument('--smus', action='store_true',
-                        help="calculate an SMUS (smallest MUS)")
-    parser.add_argument('--mssguided', action='store_true',
-                        help="check for unexplored subsets in immediate supersets of any MSS found")
-    parser.add_argument('--nogrow', action='store_true',
-                        help="do not grow any satisfiable subsets found, just block as-is")
-    parser.add_argument('--half-max', action='store_true',
-                        help="only compute a maximal model if the initial seed is SAT / bias is high or seed is UNSAT /bias is low")
     type_group = parser.add_mutually_exclusive_group()
     type_group.add_argument('--cnf', action='store_true',
                         help="assume input is in DIMACS CNF format (autodetected if filename is *.cnf or *.cnf.gz).")
@@ -120,7 +112,7 @@ def setup_solvers(args):
 
     # create appropriate map solver
     varbias = (args.bias == 'high')
-    if args.maximum_seed or args.smus:
+    if args.maximum_seed:
         from mapsolvers import MinicardMapSolver
         msolver  = MinicardMapSolver(n=csolver.n, bias=varbias)
     else:
@@ -140,12 +132,8 @@ def main():
         (csolver, msolver) = setup_solvers(args)
 
         config = {}
-        config['smus'] = args.smus
         config['bias'] = args.bias
         config['maxseed'] = args.max_seed or args.maximum_seed
-        config['mssguided'] = args.mssguided
-        config['nogrow'] = args.nogrow
-        config['half_max'] = args.half_max
 
         mp = MarcoPolo(csolver, msolver, timer, config)
 

mkdist.sh

@@ -2,7 +2,7 @@
 
 # gather "whitelist" of files to include
 marco_files="*.py muser2-static README VERSION"
-test_files="tests/*.cnf tests/*.smt2 tests/*.gz tests/*.py tests/out/*"
+test_files="tests/*.cnf tests/*.smt2 tests/*.gz tests/*.py tests/out/*/*"
 minisolvers_files=`find pyminisolvers/ \( -name "*.cc" -or -name "*.cpp" -or -name "*.h" -or -name "Makefile" -or -name "makefile" -or -name "*.py" -or -name "*.pyx" \) -print`
 
 if [ "$1" = "list" ] ; then

tests/testconfig.py

@@ -16,20 +16,13 @@
     {
       'name':    'marco_py', 
       'cmd':     '../marco.py',
-      'flags':   ['', '-m', '-M', '--mssguided', '--nogrow', '--half-max'],
+      'flags':   ['', '-m', '-M'],
       'flags_all': common_flags,
     },
     {
       'name':    'marco_py', 
       'cmd':     '../marco.py',
-      'flags':   ['-b low', '-m -b low', '-M -b low', '-b low --mssguided', '-b low -m --mssguided', '-b low --half-max'],
-      'flags_all': common_flags,
-      'exclude': ['dlx2_aa.cnf'],
-    },
-    {
-      'name':    'marco_py_smus', 
-      'cmd':     '../marco.py',
-      'flags':   ['--smus'],
+      'flags':   ['-b low', '-m -b low', '-M -b low'],
       'flags_all': common_flags,
       'exclude': ['dlx2_aa.cnf'],
     },