From 93aa18f4239877af6135f6eff6c86ed7f751e7fb Mon Sep 17 00:00:00 2001 From: Mark Liffiton Date: Thu, 12 Oct 2017 22:53:36 -0500 Subject: [PATCH] Add --print-mcses option; release v2.0.1. --- CHANGES_since_1.0 | 4 ++++ README.md | 5 ++++- VERSION | 2 +- marco.py | 11 ++++++++--- 4 files changed, 17 insertions(+), 5 deletions(-) diff --git a/CHANGES_since_1.0 b/CHANGES_since_1.0 index 3a55586..1b51b9e 100644 --- a/CHANGES_since_1.0 +++ b/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") diff --git a/README.md b/README.md index c2ec6ed..3092586 100644 --- a/README.md +++ b/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 diff --git a/VERSION b/VERSION index cd5ac03..38f77a6 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -2.0 +2.0.1 diff --git a/marco.py b/marco.py index 3ef84c1..fc1e47e 100755 --- a/marco.py +++ b/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())