Add support for MergeSat

conp-solutions · tautschnig · commit 72d73e820a08 · 2021-11-04T12:42:52.000Z
MergeSat is a recent SAT solver that fits the MiniSat2 interface.

To use MergeSat as a proper SAT backend, some extensions might be dropped.
Especially being able to print memory usage is not helpful for CBMC, but
requires pulling in a new dependency.

Signed-off-by: Norbert Manthey &lt;nmanthey@conp-solutions.com&gt;
diff --git a/scripts/mergesat.patch b/scripts/mergesat.patch
@@ -0,0 +1,140 @@
+diff -urN mergesat-3.0.orig/core/OnlineProofChecker.h mergesat-3.0/core/OnlineProofChecker.h
+--- mergesat-3.0.orig/core/OnlineProofChecker.h	2021-03-25 07:15:00.000000000 +0000
++++ mergesat-3.0/core/OnlineProofChecker.h	2021-11-04 09:43:19.934897933 +0000
+@@ -832,6 +832,6 @@
+     }
+ }
+ 
+-}; // namespace MERGESAT_NSPACE
++} // namespace MERGESAT_NSPACE
+ 
+ #endif
+diff -urN mergesat-3.0.orig/core/Solver.cc mergesat-3.0/core/Solver.cc
+--- mergesat-3.0.orig/core/Solver.cc	2021-03-25 07:15:00.000000000 +0000
++++ mergesat-3.0/core/Solver.cc	2021-11-04 10:04:45.252778350 +0000
+@@ -215,22 +215,22 @@
+     if (!args) return false;
+     char *original_args = args;
+ 
+-    const size_t len = strlen(args);
++    std::vector<char *> argv;
++    argv.push_back(strdup("mergesat"));
+ 
+-    char *argv[len + 2];
+-    int count = 1;
+-
+-    argv[0] = "mergesat";
+     while (isspace(*args)) ++args;
+     while (*args) {
+-        argv[count++] = args;                    // store current argument
++        argv.push_back(args);                    // store current argument
+         while (*args && !isspace(*args)) ++args; // skip current token
+         if (!*args) break;
+         *args = (char)0; // separate current token
+         ++args;
+     }
+ 
+-    parseOptions(count, argv, false);
++    argv.push_back(NULL);
++
++    int count = argv.size() - 1;
++    parseOptions(count, argv.data(), false);
+     free(original_args);
+     return false;
+ }
+@@ -2601,7 +2601,7 @@
+ 
+         /* grow limit after each rephasing */
+         state_change_time = state_change_time + state_change_time_inc;
+-        state_change_time_inc = state_change_time_inc *= state_change_time_inc_inc;
++        state_change_time_inc *= state_change_time_inc_inc;
+ 
+         /* actually rephase */
+         if (rand() % 100 < 50)
+@@ -3042,7 +3042,8 @@
+         order_heap_CHB.build(order_heap_DISTANCE.elements());
+         order_heap = &order_heap_CHB;
+         break;
+-    default:
++    case VSIDS_CHB:
++    case CHB:
+         break;
+     }
+     assert(!considersDISTANCE() && "we should have disabled DISTANCE heuristic");
+@@ -3062,7 +3063,8 @@
+         order_heap_DISTANCE.build(order_heap_CHB.elements());
+         order_heap = &order_heap_DISTANCE;
+         break;
+-    default:
++    case VSIDS_DISTANCE:
++    case DISTANCE:
+         break;
+     }
+     assert(considersDISTANCE() && "we should have enabled DISTANCE heuristic");
+diff -urN mergesat-3.0.orig/core/SolverTypes.h mergesat-3.0/core/SolverTypes.h
+--- mergesat-3.0.orig/core/SolverTypes.h	2021-03-25 07:15:00.000000000 +0000
++++ mergesat-3.0/core/SolverTypes.h	2021-11-04 09:47:03.613323317 +0000
+@@ -187,6 +187,16 @@
+         unsigned onQueue : 1;
+         unsigned size : 30;
+     } header;
++#if defined __clang__
++  #pragma clang diagnostic push
++  #pragma clang diagnostic ignored "-Wzero-length-array"
++#elif defined __GNUC__
++  #pragma GCC diagnostic push
++  #pragma GCC diagnostic ignored "-Wpedantic" // no specific ZLA warning in GCC
++#elif defined _MSC_VER
++  #pragma warning(push)
++  #pragma warning(disable:4200)
++#endif
+     union {
+         Lit lit;
+         float act;
+@@ -194,6 +204,13 @@
+         uint32_t touched;
+         CRef rel;
+     } data[0];
++#if defined __clang__
++  #pragma clang diagnostic pop
++#elif defined __GNUC__
++  #pragma GCC diagnostic pop
++#elif defined _MSC_VER
++  #pragma warning(pop)
++#endif
+ 
+     friend class ClauseAllocator;
+ 
+diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h
+--- a/minisat/mtl/Vec.h
++++ b/minisat/mtl/Vec.h
+@@ -159,8 +159,7 @@
+     int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
+     if (add > INT_MAX - cap) throw OutOfMemoryException();
+ 
+-    T *newdata = (T *)::realloc(data, (cap + add) * sizeof(T));
++    T *newdata = (T *)xrealloc(data, (cap + add) * sizeof(T));
+-    if (newdata == NULL && errno == ENOMEM) throw OutOfMemoryException();
+ 
+     cap += add;
+     data = newdata;
+diff --git a/minisat/mtl/XAlloc.h b/minisat/mtl/XAlloc.h
+--- a/minisat/mtl/XAlloc.h
++++ b/minisat/mtl/XAlloc.h
+@@ -21,7 +21,6 @@
+ #ifndef MergeSat_XAlloc_h
+ #define MergeSat_XAlloc_h
+ 
+-#include <errno.h>
+ #include <stdlib.h>
+ 
+ // To not introduce this multiple times, use this header, as it's rather central
+@@ -41,7 +40,7 @@
+ static inline void *xrealloc(void *ptr, size_t size)
+ {
+     void *mem = realloc(ptr, size);
+-    if (mem == NULL && errno == ENOMEM) {
++    if (mem == NULL) {
+         throw OutOfMemoryException();
+     } else
+         return mem;
diff --git a/src/Makefile b/src/Makefile
@@ -133,6 +133,21 @@ minisat2-download:
 	@(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
 	@rm minisat2_2.2.1.orig.tar.gz
 
+mergesat-download:
+	@echo "Downloading MergeSat (replacing Minisat 2.2.1)"
+	@for i in $$(seq 1 3) ; do \
+	  $(DOWNLOADER) \
+	    https://github.com/conp-solutions/mergesat/archive/refs/tags/v3.0.tar.gz && \
+	    exit 0 ; \
+		$(RM) v3.0.tar.gz ; \
+	  if [ $$i -lt 3 ] ; then echo "Re-trying in 10 seconds" 1>&2 ; sleep 10 ; fi ; \
+	done ; exit 1
+	@$(TAR) xfz v3.0.tar.gz # will create mergesat-3.0
+	@rm -Rf ../mergesat-3.0
+	@mv mergesat-3.0 ../
+	@(cd ../mergesat-3.0; patch -p1 < ../scripts/mergesat.patch)
+	@rm v3.0.tar.gz
+
 cudd-download:
 	@echo "Downloading Cudd 3.0.0"
 	@$(DOWNLOADER) https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download cudd-3.0.0.tar.gz
diff --git a/src/config.inc b/src/config.inc
@@ -30,12 +30,13 @@ endif
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
 #MINISAT2 = ../../minisat-2.2.1
+#MERGESAT = ../../mergesat-3.0
 #IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
 #CADICAL = ../../cadical
 
 # select default solver to be minisat2 if no other is specified
-ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),)
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(MERGESAT)$(PICOSAT)$(CADICAL),)
   MINISAT2 = ../../minisat-2.2.1
 endif
 
@@ -63,6 +64,10 @@ ifneq ($(MINISAT2),)
   CP_CXXFLAGS += -DSATCHECK_MINISAT2
 endif
 
+ifneq ($(MERGESAT),)
+  CP_CXXFLAGS += -DSATCHECK_MERGESAT
+endif
+
 ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DSATCHECK_GLUCOSE
 endif
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -22,6 +22,14 @@ ifneq ($(MINISAT2),)
   CLEANFILES += $(MINISAT2_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MINISAT2_LIB))
 endif
 
+ifneq ($(MERGESAT),)
+  MERGESAT_SRC=sat/satcheck_minisat2.cpp
+  MERGESAT_INCLUDE=-I $(MERGESAT)
+  MERGESAT_LIB=$(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT) $(MERGESAT)/minisat/core/Solver$(OBJEXT) $(MERGESAT)/minisat/utils/ccnr$(OBJEXT) $(MERGESAT)/minisat/utils/Options$(OBJEXT) $(MERGESAT)/minisat/utils/System$(OBJEXT)
+  CP_CXXFLAGS += -DHAVE_MERGESAT -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
+  CLEANFILES += $(MERGESAT_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MERGESAT_LIB))
+endif
+
 ifneq ($(IPASIR),)
   IPASIR_SRC=sat/satcheck_ipasir.cpp
   IPASIR_INCLUDE=-I $(IPASIR)
@@ -74,6 +82,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(GLUCOSE_SRC) \
       $(LINGELING_SRC) \
       $(MINISAT2_SRC) \
+      $(MERGESAT_SRC) \
       $(IPASIR_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
@@ -222,6 +231,28 @@ $(MINISAT2)/minisat/core/Solver$(OBJEXT): $(MINISAT2)/minisat/core/Solver.cc
 endif
 endif
 
+ifneq ($(MERGESAT),)
+ifeq ($(BUILD_ENV_),MSVC)
+sat/satcheck_minisat2$(OBJEXT): sat/satcheck_minisat2.cpp
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/utils/ccnr$(OBJEXT): $(MERGESAT)/minisat/utils/ccnr.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/utils/Options$(OBJEXT): $(MERGESAT)/minisat/utils/Options.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/utils/System$(OBJEXT): $(MERGESAT)/minisat/utils/System.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT): $(MERGESAT)/minisat/simp/SimpSolver.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/core/Solver$(OBJEXT): $(MERGESAT)/minisat/core/Solver.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+endif
+endif
+
 ifneq ($(GLUCOSE),)
 ifeq ($(BUILD_ENV_),MSVC)
 sat/satcheck_glucose$(OBJEXT): sat/satcheck_glucose.cpp
@@ -237,6 +268,7 @@ endif
 
 INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
+  $(MERGESAT_INCLUDE) \
   $(IPASIR_INCLUDE) \
   $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) $(CADICAL_INCLUDE)
@@ -255,7 +287,7 @@ endif
 endif
 
 SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
-        $(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
+        $(MINISAT2_LIB) $(MERGESAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
         $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) $(CADICAL_LIB)
 
 SOLVER_OBJS = $(filter %$(OBJEXT), $(SOLVER_LIB))
diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 // #define SATCHECK_ZCHAFF
 // #define SATCHECK_MINISAT1
 // #define SATCHECK_MINISAT2
+// #define SATCHECK_MERGESAT
 // #define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
 // #define SATCHECK_PICOSAT
@@ -39,6 +40,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #define SATCHECK_MINISAT2
 #endif
 
+#if defined(HAVE_MERGESAT) && !defined(SATCHECK_MERGESAT)
+#define SATCHECK_MERGESAT
+#endif
+
 #if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE)
 #define SATCHECK_GLUCOSE
 #endif
@@ -80,7 +85,7 @@ typedef satcheck_booleforcet satcheck_no_simplifiert;
 typedef satcheck_minisat1t satcheckt;
 typedef satcheck_minisat1t satcheck_no_simplifiert;
 
-#elif defined SATCHECK_MINISAT2
+#elif defined SATCHECK_MINISAT2 || defined SATCHECK_MERGESAT
 
 #include "satcheck_minisat2.h"
 
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
@@ -22,8 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <minisat/core/Solver.h>
 #include <minisat/simp/SimpSolver.h>
 
-#ifndef HAVE_MINISAT2
-#error "Expected HAVE_MINISAT2"
+#if !defined(HAVE_MINISAT2) && !defined(HAVE_MERGESAT)
+#error "Expected HAVE_MINISAT2 or HAVE_MERGESAT"
 #endif
 
 void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
@@ -77,7 +77,11 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
   try
   {
     add_variables();
+#ifdef HAVE_MERGESAT
+    solver->setPolarity(a.var_no(), value);
+#else
     solver->setPolarity(a.var_no(), value ? l_True : l_False);
+#endif
   }
   catch(Minisat::OutOfMemoryException)
   {
@@ -101,12 +105,20 @@ void satcheck_minisat2_baset<T>::clear_interrupt()
 
 const std::string satcheck_minisat_no_simplifiert::solver_text()
 {
+#ifdef HAVE_MERGESAT
+  return "Mergesat 3.0 without simplifier";
+#else
   return "MiniSAT 2.2.1 without simplifier";
+#endif
 }
 
 const std::string satcheck_minisat_simplifiert::solver_text()
 {
+#ifdef HAVE_MERGESAT
+  return "Mergesat 3.0 with simplifier";
+#else
   return "MiniSAT 2.2.1 with simplifier";
+#endif
 }
 
 template<typename T>

Original file line number	Diff line number	Diff line change
`@@ -22,8 +22,8 @@ Author: Daniel Kroening, [email protected]`
`22`	`22`	`#include <minisat/core/Solver.h>`
`23`	`23`	`#include <minisat/simp/SimpSolver.h>`
`24`	`24`
`25`		`-#ifndef HAVE_MINISAT2`
`26`		`-#error "Expected HAVE_MINISAT2"`
	`25`	`+#if !defined(HAVE_MINISAT2) && !defined(HAVE_MERGESAT)`
	`26`	`+#error "Expected HAVE_MINISAT2 or HAVE_MERGESAT"`
`27`	`27`	`#endif`
`28`	`28`
`29`	`29`	`void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)`
`@@ -77,7 +77,11 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)`
`77`	`77`	`try`
`78`	`78`	`{`
`79`	`79`	`add_variables();`
	`80`	`+#ifdef HAVE_MERGESAT`
	`81`	`+ solver->setPolarity(a.var_no(), value);`
	`82`	`+#else`
`80`	`83`	`solver->setPolarity(a.var_no(), value ? l_True : l_False);`
	`84`	`+#endif`
`81`	`85`	`}`
`82`	`86`	`catch(Minisat::OutOfMemoryException)`
`83`	`87`	`{`
`@@ -101,12 +105,20 @@ void satcheck_minisat2_baset<T>::clear_interrupt()`
`101`	`105`
`102`	`106`	`const std::string satcheck_minisat_no_simplifiert::solver_text()`
`103`	`107`	`{`
	`108`	`+#ifdef HAVE_MERGESAT`
	`109`	`+ return "Mergesat 3.0 without simplifier";`
	`110`	`+#else`
`104`	`111`	`return "MiniSAT 2.2.1 without simplifier";`
	`112`	`+#endif`
`105`	`113`	`}`
`106`	`114`
`107`	`115`	`const std::string satcheck_minisat_simplifiert::solver_text()`
`108`	`116`	`{`
	`117`	`+#ifdef HAVE_MERGESAT`
	`118`	`+ return "Mergesat 3.0 with simplifier";`
	`119`	`+#else`
`109`	`120`	`return "MiniSAT 2.2.1 with simplifier";`
	`121`	`+#endif`
`110`	`122`	`}`
`111`	`123`
`112`	`124`	`template<typename T>`