Add --print-mcses option; release v2.0.1.

CHANGES_since_1.0

@@ -1,3 +1,7 @@
+2.0.1 - 2017-10-12
+------------------
+ * Add --print-mcses option to print MCS constraints instead of MSS constraints
+
 2.0   - 2016-10-29
 ------------------
  * Add mode for parallel execution ("MARCOs")

README.md

@@ -89,7 +89,10 @@ The output lists MUSes ("U") and MSSes ("S"), one per line.  In 'verbose' mode
 (-v), each line also lists the indexes of the constraints included in each set
 (with 1-based counting).  MCSes are the complements of the MSSes w.r.t. the
 original set of input constraints (e.g., if MARCO reports an MSS "1 3 4" for a
-5-constraint input, the corresponding MCS is constraints 2 and 5).
+5-constraint input, the corresponding MCS is constraints 2 and 5).  If you want
+the MCSes printed directly, use the '--print-mcses' command line option; MCSes
+will be printed on lines starting with "C" (in place of the "S" lines for their
+MSSes).
 
 
 ## Authors

VERSION

@@ -1 +1 @@
-2.0
+2.0.1

marco.py

@@ -41,6 +41,8 @@ def parse_args():
                             help="assume input is in SMT2 format (autodetected if filename is *.smt2).")
     parser.add_argument('-b', '--bias', type=str, choices=['MUSes', 'MCSes'], default='MUSes',
                         help="bias the search toward MUSes or MCSes early in the execution [default: MUSes] -- all will be enumerated eventually; this just uses heuristics to find more of one or the other early in the enumeration.")
+    parser.add_argument('--print-mcses', action='store_true',
+                        help="for every satisfiable subset found, print the constraints in its complementary MCS instead of the MSS.")
     parser.add_argument('--check-muser', action='store_true',
                         help="just run a check of the MUSer2 helper application and exit (used to configure tests).")
 
@@ -267,7 +269,7 @@ def enumerate():
             if pipe:
                 pipe.send(result)
             else:
-                print_result(result, args, stats)
+                print_result(result, args, stats, csolver.n)
                 if remaining:
                     remaining -= 1
                     if remaining == 0:
@@ -369,7 +371,7 @@ def run_master(stats, args, pipes):
 
                         #results.add(res_set)
 
-                        print_result(result, args, stats)
+                        print_result(result, args, stats, csolver.n)
 
                         if remaining:
                             remaining -= 1
@@ -388,7 +390,10 @@ def run_master(stats, args, pipes):
                                     other.send(result)
 
 
-def print_result(result, args, stats):
+def print_result(result, args, stats, num_constraints):
+    if result[0] == 'S' and args.print_mcses:
+        # MCS = the complement of the MSS relative to the full set of constraints
+        result = ('C', set(range(1, num_constraints+1)).difference(result[1]))
     output = result[0]
     if args.alltimes:
         output = "%s %0.3f" % (output, stats.total_time())