Skip to content

Commit

Permalink
Add note on GCNF support to README, include .gcnf tests in dist.
Browse files Browse the repository at this point in the history
  • Loading branch information
liffiton committed Nov 11, 2014
1 parent 129fe64 commit eb5408b
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 5 deletions.
12 changes: 8 additions & 4 deletions README
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@
MARCO: an efficient MUS and MCS enumeration tool

This is a Python implementation of the MARCO algorithm [1] for enumerating
MUSes and MCSes of infeasible constraint systems (currently: SAT and SMT).
This implementation makes use of MUSer2 [2] for MUS extraction and MiniSAT 2.2
[3] for satisfiability testing and the generation of SAT models.
MUSes and MCSes of infeasible constraint systems (currently: CNF, GCNF, and
SMT). This implementation makes use of MUSer2 [2] for MUS extraction and
MiniSAT 2.2 [3] for satisfiability testing and the generation of SAT models.

Web: http://www.iwu.edu/~mliffito/marco/

Expand Down Expand Up @@ -68,7 +68,11 @@ Example: ./marco.py tests/test1.cnf

Run ./marco.py --help for a list of available options.

Input files may be gzipped.
Input files may be in CNF, GCNF (group oriented CNF), or SMT2 format. Input
files may be gzipped.

The supported GCNF format is the one specified in:
http://www.satcompetition.org/2011/rules.pdf

The output lists MUSes ("U") and MCSes ("S"), one per line. In 'verbose' mode
(-v), each line also lists the indexes of the constraints included in each set
Expand Down
2 changes: 1 addition & 1 deletion mkdist.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
# gather "whitelist" of files to include
marco_files="*.py muser2-static README VERSION"
if [ $# -lt 2 -o "$2" != "notest" ] ; then
test_files="tests/*.cnf tests/*.smt2 tests/*.gz tests/*.py tests/out/*/*"
test_files="tests/*.cnf tests/*.gcnf tests/*.smt2 tests/*.gz tests/*.py tests/out/*/*"
fi
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`

Expand Down

0 comments on commit eb5408b

Please sign in to comment.