diff --git a/tests/test_unique_mus.py b/tests/test_unique_mus.py index 4cc0695..db22c12 100644 --- a/tests/test_unique_mus.py +++ b/tests/test_unique_mus.py @@ -3,19 +3,26 @@ from pysat.formula import CNF, WCNF def test_unique_mus(): - cnf = CNF(from_clauses=[[-1, 2], [1, -2], [-1, -2], [1, 2]]) - wcnf = cnf.weighted() + def check_formula(wcnf): + # considering various parameter combinations + for booleans in itertools.product([False, True], repeat=3): + for trim in [0, 5]: + + with OptUx(wcnf, solver='g3', adapt=booleans[0], + exhaust=booleans[1], minz=booleans[2], + trim=trim, verbose=0) as optux: - # considering various parameter combinations - for booleans in itertools.product([False, True], repeat=3): - for trim in [0, 5]: + muses = [] + for mus in optux.enumerate(): + muses.append(mus) - with OptUx(wcnf, solver='g3', adapt=booleans[0], - exhaust=booleans[1], minz=booleans[2], - trim=trim, verbose=0) as optux: + assert len(muses) == 1, 'There should be a single MUS!' - muses = [] - for mus in optux.enumerate(): - muses.append(mus) + # first, test for unweighted formula + cnf = CNF(from_clauses=[[-1, 2], [1, -2], [-1, -2], [1, 2]]) + wcnf = cnf.weighted() + check_formula(wcnf) - assert len(muses) == 1, 'There should be a single MUS!' + # second, test for weighted formula + wcnf.wght = [10, 50, 1, 2] + check_formula(wcnf)