A bugfix in RC2's model enumerator. Minor changes in the patch for Ca…

…DiCaL.

examples/rc2.py

@@ -206,7 +206,7 @@ def __init__(self, formula, solver='g3', adapt=False, exhaust=False,
         self.trim = trim
 
         # clause selectors and mapping from selectors to clause ids
-        self.sels, self.smap, self.sall, self.s2cl = [], {}, [], {}
+        self.sels, self.smap, self.sall, self.s2cl, self.sneg = [], {}, [], {}, set([])
 
         # other MaxSAT related stuff
         self.topv = formula.nv
@@ -529,6 +529,15 @@ def enumerate(self, block=0):
                         if selv in m:
                             # clause is satisfied
                             cl.append(-selv)
+
+                            # next time we want to falsify one of these
+                            # clauses, i.e. we should encode the negation
+                            # of each of these selectors
+                            if selv in self.s2cl and not selv in self.sneg:
+                                self.sneg.add(selv)
+                                for il in self.s2cl[selv]:
+                                    self.oracle.add_clause([selv, -il])
+
                         elif selv in self.s2cl:
                             # clause is falsified and it is not unit size
                             for il in self.s2cl[selv]:
@@ -1706,10 +1715,10 @@ def usage():
 
                 if i == to_enum:
                     break
-
-            # needed for MSE'20
-            if to_enum != 1 and block == 1:
-                print('v')
+            else:
+                # needed for MSE'20
+                if verbose > 2 and vnew and to_enum != 1 and block == 1:
+                    print('v')
 
             if verbose:
                 if not optimum_found:

pysat/__init__.py

@@ -10,7 +10,7 @@
 
 # current version
 #==============================================================================
-VERSION = (0, 1, 6, "dev", 2)
+VERSION = (0, 1, 6, "dev", 3)
 
 
 # PEP440 Format

solvers/patches/cadical.patch

@@ -15,7 +15,7 @@ diff -Naur build/solvers/cadical/Makefile solvers/cadical/Makefile
 +CXXPROF  := -O3 -g3 -fno-inline -fno-omit-frame-pointer -pg -DNDEBUG
 +INCLUDES := -I.
 +LIBS     := -L.
-+SOURCES  := analyze.cpp arena.cpp assume.cpp averages.cpp backtrack.cpp backward.cpp bins.cpp block.cpp ccadical.cpp checker.cpp clause.cpp collect.cpp compact.cpp config.cpp cover.cpp decide.cpp decompose.cpp deduplicate.cpp elim.cpp ema.cpp extend.cpp external.cpp file.cpp flags.cpp format.cpp gates.cpp instantiate.cpp internal.cpp ipasir.cpp limit.cpp logging.cpp lucky.cpp message.cpp minimize.cpp occs.cpp options.cpp parse.cpp phases.cpp probe.cpp profile.cpp proof.cpp propagate.cpp queue.cpp random.cpp reduce.cpp rephase.cpp report.cpp resources.cpp restart.cpp restore.cpp score.cpp signal.cpp solution.cpp solver.cpp stats.cpp subsume.cpp terminal.cpp ternary.cpp tracer.cpp transred.cpp util.cpp var.cpp version.cpp vivify.cpp walk.cpp watch.cpp
++SOURCES  := analyze.cpp arena.cpp assume.cpp averages.cpp backtrack.cpp backward.cpp bins.cpp block.cpp ccadical.cpp checker.cpp clause.cpp collect.cpp compact.cpp config.cpp cover.cpp decide.cpp decompose.cpp deduplicate.cpp elim.cpp ema.cpp extend.cpp external.cpp file0.cpp flags.cpp format.cpp gates.cpp instantiate.cpp internal.cpp ipasir.cpp limit.cpp logging.cpp lucky.cpp message.cpp minimize.cpp occs.cpp options.cpp parse.cpp phases.cpp probe.cpp profile.cpp proof.cpp propagate.cpp queue.cpp random.cpp reduce.cpp rephase.cpp report.cpp resources.cpp restart.cpp restore.cpp score.cpp signal.cpp solution.cpp solver.cpp stats.cpp subsume.cpp terminal.cpp ternary.cpp tracer.cpp transred.cpp util.cpp var.cpp version.cpp vivify.cpp walk.cpp watch.cpp
 +OBJECTS  := $(SOURCES:.cpp=.o)
 +TRGT     := cadical
 +
@@ -65,9 +65,9 @@ diff -Naur build/solvers/cadical/contract.hpp solvers/cadical/contract.hpp
  /*------------------------------------------------------------------------*/
 
  // If the user violates API contracts while calling functions declared in
-diff -Naur build/solvers/cadical/file.cpp solvers/cadical/file.cpp
---- build/solvers/cadical/file.cpp	2019-07-12 22:22:02.000000000 +0200
-+++ solvers/cadical/file.cpp	2019-12-02 08:41:16.375326400 +0100
+diff -Naur build/solvers/cadical/file0.cpp solvers/cadical/file0.cpp
+--- build/solvers/cadical/file0.cpp	2019-07-12 22:22:02.000000000 +0200
++++ solvers/cadical/file0.cpp	2019-12-02 08:41:16.375326400 +0100
 @@ -19,6 +19,19 @@
 
  /*------------------------------------------------------------------------*/

solvers/prepare.py

@@ -129,7 +129,7 @@
         ('src/extend.cpp', 'extend.cpp'),
         ('src/external.cpp', 'external.cpp'),
         ('src/external.hpp', 'external.hpp'),
-        ('src/file.cpp', 'file.cpp'),
+        ('src/file.cpp', 'file0.cpp'),
         ('src/file.hpp', 'file.hpp'),
         ('src/flags.cpp', 'flags.cpp'),
         ('src/flags.hpp', 'flags.hpp'),

web/news.rst

@@ -11,6 +11,12 @@ to date and then is good idea.
 Changelog and more
 ------------------
 
+07.07.2020 (*0.1.6.dev3*)
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+- Fixed RC2's enumeration of MSSes.
+- Minor changes to the patch for CaDiCaL
+
 06.07.2020 (*0.1.6.dev2*)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~