Mergesat: get latest version from github

Signed-off-by: Norbert Manthey <[email protected]>

Author: conp-solutions

scripts/mergesat.patch

@@ -1,18 +1,32 @@
-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 @@
+diff --git a/minisat/core/OnlineProofChecker.h b/minisat/core/OnlineProofChecker.h
+index 6bd9ff9..e642781 100644
+--- a/minisat/core/OnlineProofChecker.h
++++ b/minisat/core/OnlineProofChecker.h
+@@ -833,6 +833,6 @@ inline void OnlineProofChecker::fullCheck()
      }
  }
 
 -}; // 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 @@
+diff --git a/minisat/core/Proofs.h b/minisat/core/Proofs.h
+index b835924..08c31f0 100644
+--- a/minisat/core/Proofs.h
++++ b/minisat/core/Proofs.h
+@@ -329,6 +329,6 @@ inline void Proof::flushToFile()
+ inline void Proof::setVerbosity(int v) { verbosity = v; }
+ 
+ 
+-}; // namespace MERGESAT_NSPACE
++} // namespace MERGESAT_NSPACE
+ 
+ #endif
+diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
+index b708a48..eec8d36 100644
+--- a/minisat/core/Solver.cc
++++ b/minisat/core/Solver.cc
+@@ -224,22 +224,22 @@ bool MERGESAT_NSPACE::updateOptions()
      if (!args) return false;
      char *original_args = args;
 
@@ -42,7 +56,7 @@ diff -urN mergesat-3.0.orig/core/Solver.cc mergesat-3.0/core/Solver.cc
      free(original_args);
      return false;
  }
-@@ -2601,7 +2601,7 @@
+@@ -2599,7 +2599,7 @@ lbool Solver::search(int &nof_conflicts)
 
          /* grow limit after each rephasing */
          state_change_time = state_change_time + state_change_time_inc;
@@ -51,7 +65,16 @@ diff -urN mergesat-3.0.orig/core/Solver.cc mergesat-3.0/core/Solver.cc
 
          /* actually rephase */
          if (rand() % 100 < 50)
-@@ -3042,7 +3042,8 @@
+@@ -2755,7 +2755,7 @@ lbool Solver::search(int &nof_conflicts)
+ 
+             if (verbosity >= 1 && (conflicts % status_every) == 0)
+                 printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)conflicts,
+-                       (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
++                       (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), (int)nClauses(), (int)clauses_literals,
+                        (int)max_learnts, nLearnts(), (double)learnts_literals / nLearnts(), progressEstimate() * 100);
+ 
+             // the top_trail_soln should be update after each conflict
+@@ -3013,7 +3013,8 @@ void Solver::disableDISTANCEheuristic()
          order_heap_CHB.build(order_heap_DISTANCE.elements());
          order_heap = &order_heap_CHB;
          break;
@@ -61,7 +84,7 @@ diff -urN mergesat-3.0.orig/core/Solver.cc mergesat-3.0/core/Solver.cc
          break;
      }
      assert(!considersDISTANCE() && "we should have disabled DISTANCE heuristic");
-@@ -3062,7 +3063,8 @@
+@@ -3033,7 +3034,8 @@ void Solver::enableDISTANCEheuristic()
          order_heap_DISTANCE.build(order_heap_CHB.elements());
          order_heap = &order_heap_DISTANCE;
          break;
@@ -71,10 +94,47 @@ diff -urN mergesat-3.0.orig/core/Solver.cc mergesat-3.0/core/Solver.cc
          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 @@
+@@ -3081,7 +3083,7 @@ lbool Solver::solve_()
+     if (assumptions.size() > 0) solved_by_ls = false;
+ 
+     /* allow to disable SLS for larger clauses */
+-    if ((sls_var_lim != -1 && nVars() > sls_var_lim) || (sls_clause_lim != -1 && nClauses() > sls_clause_lim)) {
++    if ((sls_var_lim != -1 && nVars() > sls_var_lim) || (sls_clause_lim != -1 && nClauses() > (size_t)sls_clause_lim)) {
+         use_ccnr = false;
+     }
+ 
+diff --git a/minisat/core/Solver.h b/minisat/core/Solver.h
+index ed63db4..fc3b648 100644
+--- a/minisat/core/Solver.h
++++ b/minisat/core/Solver.h
+@@ -198,9 +198,9 @@ class Solver
+     lbool modelValue(Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
+     lbool modelValue(Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
+     int nAssigns() const;                          // The current number of assigned literals.
+-    int nClauses() const;                          // The current number of original clauses.
++    size_t nClauses() const;                       // The current number of original clauses.
+     int nLearnts() const;                          // The current number of learnt clauses.
+-    int nUnits() const;                            // The current number of unit clauses.
++    size_t nUnits() const;                         // The current number of unit clauses.
+     const Lit getUnit(size_t unit_idx) const;      // The clause with a given index;
+     const Clause &getClause(size_t cls_idx) const; // The clause with a given index;
+     int nVars() const;                             // The current number of variables.
+@@ -895,8 +895,8 @@ inline lbool Solver::value(Lit p) const { return assigns[var(p)] ^ sign(p); }
+ inline lbool Solver::modelValue(Var x) const { return model[x]; }
+ inline lbool Solver::modelValue(Lit p) const { return model[var(p)] ^ sign(p); }
+ inline int Solver::nAssigns() const { return trail.size(); }
+-inline int Solver::nClauses() const { return clauses.size(); }
+-inline int Solver::nUnits() const { return trail_lim.size() < 1 ? trail.size() : trail_lim[0]; }
++inline size_t Solver::nClauses() const { return clauses.size(); }
++inline size_t Solver::nUnits() const { return trail_lim.size() < 1 ? trail.size() : trail_lim[0]; }
+ inline const Lit Solver::getUnit(size_t unit_idx) const
+ {
+     assert(unit_idx < nUnits() && "can only access valid unit clauses");
+diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h
+index 4e366ac..3a150dd 100644
+--- a/minisat/core/SolverTypes.h
++++ b/minisat/core/SolverTypes.h
+@@ -189,6 +189,16 @@ class Clause
          unsigned onQueue : 1;
          unsigned size : 30;
      } header;
@@ -91,7 +151,7 @@ diff -urN mergesat-3.0.orig/core/SolverTypes.h mergesat-3.0/core/SolverTypes.h
      union {
          Lit lit;
          float act;
-@@ -194,6 +204,13 @@
+@@ -196,6 +206,13 @@ class Clause
          uint32_t touched;
          CRef rel;
      } data[0];
@@ -106,30 +166,32 @@ diff -urN mergesat-3.0.orig/core/SolverTypes.h mergesat-3.0/core/SolverTypes.h
      friend class ClauseAllocator;
 
 diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h
+index 4abb5db..e9c0d93 100644
 --- a/minisat/mtl/Vec.h
 +++ b/minisat/mtl/Vec.h
-@@ -159,8 +159,7 @@
+@@ -167,8 +167,7 @@ template <class T> void vec<T>::capacity(int min_cap)
      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();
++    T *newdata = (T *)xrealloc(data, (cap + add) * sizeof(T));
 
      cap += add;
      data = newdata;
 diff --git a/minisat/mtl/XAlloc.h b/minisat/mtl/XAlloc.h
+index 1f43745..50809cb 100644
 --- a/minisat/mtl/XAlloc.h
 +++ b/minisat/mtl/XAlloc.h
-@@ -21,7 +21,6 @@
+@@ -21,7 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
  #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 @@
+@@ -41,7 +40,7 @@ class OutOfMemoryException
  static inline void *xrealloc(void *ptr, size_t size)
  {
      void *mem = realloc(ptr, size);
@@ -138,3 +200,29 @@ diff --git a/minisat/mtl/XAlloc.h b/minisat/mtl/XAlloc.h
          throw OutOfMemoryException();
      } else
          return mem;
+diff --git a/minisat/parallel/ParSolver.cc b/minisat/parallel/ParSolver.cc
+index ad4c235..b76566b 100644
+--- a/minisat/parallel/ParSolver.cc
++++ b/minisat/parallel/ParSolver.cc
+@@ -44,7 +44,7 @@ ParSolver::ParSolver()
+   : par_reparsed_options(updateOptions())
+   , parsing(false)
+   , verbosity(0)
+-  , use_simplification(true)
++  , use_simplification(false)
+   , sync_mode(opt_sync_mode == 0 ? NON_DETERMINISTIC : (opt_sync_mode == 1 ? DETERMINISTIC_STATIC : DETERMINISTIC_DYNAMIC))
+   , cores(opt_cores)
+   , initialized(false)
+diff --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc
+index a5d9581..3c8d2bf 100644
+--- a/minisat/simp/SimpSolver.cc
++++ b/minisat/simp/SimpSolver.cc
+@@ -45,7 +45,7 @@ static BoolOption opt_use_asymm(_cat, "asymm", "Shrink clauses by asymmetric bra
+ static BoolOption opt_use_rcheck(_cat, "rcheck", "Check if a clause is already implied. (costly)", false, false);
+ static BoolOption opt_use_elim(_cat, "elim", "Perform variable elimination.", true);
+ static IntOption opt_grow(_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
+-static BoolOption opt_grow_iterations(_cat, "grow-iter", "Run iterative eliminations with growing.", true);
++static BoolOption opt_grow_iterations(_cat, "grow-iter", "Run iterative eliminations with growing.", false);
+ static IntOption opt_clause_lim(_cat,
+                                 "cl-lim",
+                                 "Variables are not eliminated if it produces a resolvent with a length above this "

src/Makefile

@@ -135,18 +135,11 @@ minisat2-download:
 
 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 ../
+	@git clone https://github.com/conp-solutions/mergesat.git ../mergesat-3.0
 	@(cd ../mergesat-3.0; patch -p1 < ../scripts/mergesat.patch)
-	@rm v3.0.tar.gz
+	@sed -i 's:eliminations with growing.", true);:eliminations with growing.", false);:g' ../mergesat-3.0/minisat/simp/SimpSolver.cc
+	@sed -i 's:use_simplification(true):use_simplification(false):g' ../mergesat-3.0/minisat/parallel/ParSolver.cc
 
 cudd-download:
 	@echo "Downloading Cudd 3.0.0"

src/solvers/sat/satcheck_minisat2.cpp

@@ -106,7 +106,7 @@ 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";
+  return "Mergesat (latest) without simplifier";
 #else
   return "MiniSAT 2.2.1 without simplifier";
 #endif
@@ -115,7 +115,7 @@ const std::string satcheck_minisat_no_simplifiert::solver_text()
 const std::string satcheck_minisat_simplifiert::solver_text()
 {
 #ifdef HAVE_MERGESAT
-  return "Mergesat 3.0 with simplifier";
+  return "Mergesat (latest) with simplifier";
 #else
   return "MiniSAT 2.2.1 with simplifier";
 #endif