Fixings bugs discovered in the fuzzy testing of the paper 'Uncovering…

… and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging' by Tobias Paxian and Armin Biere

ADTs/Int.h

@@ -98,6 +98,7 @@ class Int {
     friend char* toString(Int num) { char buf[32]; sprintf(buf, "%lld", num.data); return xstrdup(buf); }   // Caller must free string.
     friend int   toint   (Int num) { if (num > INT_MAX || num < INT_MIN) throw Exception_IntOverflow(xstrdup("toint")); return (int)num.data; }
     friend long  tolong  (Int num) { if (num > LONG_MAX || num < LONG_MIN) throw Exception_IntOverflow(xstrdup("tolong")); return (long int)num.data; }
+    friend unsigned long  toulong (Int num) { if (num > ULONG_MAX || num < ULONG_MIN) throw Exception_IntOverflow(xstrdup("toulong")); return (unsigned long int)num.data; }
 };
 
 
@@ -294,6 +295,12 @@ class Int {
         return (long int)mpz_get_si(*num.data);
     }
 
+    friend unsigned long toulong (Int num) {
+        if (num.small() || !mpz_fits_ulong_p(*num.data))
+            throw Exception_IntOverflow(xstrdup("toulong"));
+        return (unsigned long int)mpz_get_ui(*num.data);
+    }
+
     explicit operator double () {
         if (this->small())
             throw Exception_IntOverflow(xstrdup("double"));

Main_utils.cc

@@ -157,6 +157,24 @@ void outputResult(const PbSolver& S, bool optimum)
 #endif
     if (!opt_satlive || resultsPrinted) return;
 
+    if (opt_output_top < 0) {
+        if (optimum){
+            if (S.best_goalvalue == Int_MAX) printf("s UNSATISFIABLE\n");
+            else {
+                if (!opt_satisfiable_out) {
+                    char* tmp = toString(S.best_goalvalue);
+                    printf("o %s\n", tmp);
+                    xfree(tmp);
+                }
+                printf("s OPTIMUM FOUND\n");
+            }
+        }else{
+            if (S.best_goalvalue == Int_MAX) printf("s UNKNOWN\n");
+            else                             printf("%c SATISFIABLE\n", (opt_satisfiable_out ? 's' : 'c'));
+        }
+        resultsPrinted = true;
+    } else if (opt_output_top == 1) resultsPrinted = true;
+
     if (opt_model_out && S.best_goalvalue != Int_MAX){
 #ifdef MAXPRE
         if (opt_use_maxpre) {
@@ -204,23 +222,6 @@ void outputResult(const PbSolver& S, bool optimum)
         }
         printf("\n");
     }
-    if (opt_output_top < 0) {
-        if (optimum){
-            if (S.best_goalvalue == Int_MAX) printf("s UNSATISFIABLE\n");
-            else {
-                if (!opt_satisfiable_out) {
-                    char* tmp = toString(S.best_goalvalue);
-                    printf("o %s\n", tmp);
-                    xfree(tmp);
-                }
-                printf("s OPTIMUM FOUND\n");
-            }
-        }else{
-            if (S.best_goalvalue == Int_MAX) printf("s UNKNOWN\n");
-            else                             printf("%c SATISFIABLE\n", (opt_satisfiable_out ? 's' : 'c'));
-        }
-        resultsPrinted = true;
-    } else if (opt_output_top == 1) resultsPrinted = true;
     fflush(stdout);
 }
 

MsSolver.cc

@@ -263,8 +263,8 @@ void MsSolver::harden_soft_cls(Minisat::vec<Lit>& assump_ps, vec<Int>& assump_Cs
 {
     int cnt_unit = 0, cnt_assump = 0, sz = 0;
     Int Ibound = UB_goalvalue - LB_goalvalue, WMAX = Int(WEIGHT_MAX);
-    weight_t       wbound = (Ibound >= WMAX ? WEIGHT_MAX : tolong(Ibound));
-    weight_t ub_goalvalue = (UB_goalvalue >= WMAX ? WEIGHT_MAX : tolong(UB_goalvalue - fixed_goalval));
+    weight_t       wbound = (Ibound >= WMAX ? WEIGHT_MAX : toweight(Ibound));
+    weight_t ub_goalvalue = (UB_goalvalue >= WMAX ? WEIGHT_MAX : toweight(UB_goalvalue - fixed_goalval));
     for (int i = top_for_hard - 1; i >= 0 && soft_cls[i].fst > wbound; i--) { // hardening soft clauses with weights > the current goal interval length 
         if (soft_cls[i].fst > ub_goalvalue) sz++;
         Lit p = soft_cls[i].snd->last(); if (soft_cls[i].snd->size() > 1) p = ~p;
@@ -616,7 +616,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
     if (ipamir_used) SCIP_found_opt.store(false);
     extern bool opt_use_scip_slvr;
     int sat_orig_vars = sat_solver.nVars(), sat_orig_cls = sat_solver.nClauses();
-    if (opt_use_scip_slvr && l_True == 
+    if (opt_use_scip_slvr && UB_goalval < Int(2L << std::numeric_limits<double>::digits) && l_True == 
       scip_solve(&assump_ps, &assump_Cs, &delayed_assump, weighted_instance, sat_orig_vars, sat_orig_cls)) {
         if (ipamir_used) reset_soft_cls(soft_cls, fixed_soft_cls, modified_soft_cls, goal_gcd);
         return;

PbParser.cc

@@ -425,7 +425,7 @@ static bool parse_wcnfs(B& in, S& solver, bool wcnf_format, Int hard_bound)
         reportf("Using MaxPre - an MaxSAT preprocessor by Tuukka Korhonen (2017) with techniques: %s\n", 
                 opt_maxpre_str);
         if (++weight_sum < hard_bound) hard_bound = weight_sum;
-        uint64_t topWeight = tolong(hard_bound);
+        uint64_t topWeight = toulong(hard_bound);
         for (auto &w : weights) 
             if (w == 0 || w > topWeight) w = topWeight;
         maxpre_ptr = new maxPreprocessor::PreprocessorInterface(clauses, weights, topWeight);

PbSolver.h

@@ -30,10 +30,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "StackAlloc.h"
 
 #ifdef BIG_WEIGHTS
-using weight_t = Int; 
+using weight_t = Int;
+#define toweight(x) (x)
 #define WEIGHT_MAX Int_MAX
 #else
 using weight_t = int64_t;
+#define toweight(x) tolong(x)
 static inline const char *toString(weight_t x) { static char buf[30]; sprintf(buf, "%" PRId64, x); return buf;  }
 #define WEIGHT_MAX std::numeric_limits<weight_t>::max()
 #endif

Pre_separator.cc

@@ -32,9 +32,9 @@ static weight_t gcd(weight_t n, weight_t m)
     return n;
 }
 
-static char isSeparating(const vec<weight_t>& cs, int idx, weight_t bound) {
+static char isSeparating(const vec<weight_t>& cs, int idx, Int bound) {
   int i, in_size = cs.size(), max_operations = 100000000;
-  vec<weight_t> weight_sums, shifted_weight_sums; 
+  vec<Int> weight_sums, shifted_weight_sums; 
   weight_sums.push(0);
 
   for (i = idx; i < in_size && max_operations > 0; i++) {
@@ -46,13 +46,13 @@ static char isSeparating(const vec<weight_t>& cs, int idx, weight_t bound) {
       shifted_weight_sums[j] += cs[i];
 
     // merge both lists removing duplicates to get new weight_sums
-    vec<weight_t> new_weight_sums;
+    vec<Int> new_weight_sums;
     int k, l, n, m;
     n = weight_sums.size();
     m = shifted_weight_sums.size();
 
     new_weight_sums.push(0);
-    weight_t last = 0, curr;
+    Int last = 0, curr;
     for (k = 1, l = 0; k < n && l < m; ) {
       if (weight_sums[k] <= shifted_weight_sums[l]) {
         if (weight_sums[k] == shifted_weight_sums[l]) l++; // remove a duplicate
@@ -82,12 +82,12 @@ void separationIndex(const vec<weight_t>& cs, vec<int>& separation_points) {
 
   if (cs.size() <= 2) return;
 
-  vec<weight_t> lw;
+  vec<Int> lw;
   separation_points.clear();
 
   // calculate prefix sums of weights
   lw.push(cs[0]);
-  for(int i=1; i<cs.size(); i++) { lw.push(cs[i] + lw[i-1]); }
+  for(int i=1; i<cs.size(); i++) { lw.push(Int(cs[i]) + lw[i-1]); }
 
   weight_t rdiff = WEIGHT_MAX, rgcd = cs[cs.size()-1];
 

SatSolver.cc

@@ -41,12 +41,14 @@ const Minisat::Clause& ExtSimpSolver::getClause  (int i, bool &is_satisfied) con
 }
 #endif
 
-void ExtSimpSolver::reduceProblem()
+bool ExtSimpSolver::reduceProblem()
 {
+    bool res = true;
 #if !defined(CADICAL) && !defined(CRYPTOMS)
-    if (use_simplification) eliminate();
+    if (use_simplification) res = eliminate();
     elimclauses.copyTo(elimClauses);
 #endif
+    return res;
 }
 
 #if !defined(CADICAL) && !defined(CRYPTOMS)

SatSolver.h

@@ -100,7 +100,7 @@ class ExtSimpSolver: public SimpSolver {
 #if !defined(CADICAL) && !defined(CRYPTOMS)
     const Minisat::Clause& getClause  (int i, bool &is_satisfied) const;
 #endif
-    void reduceProblem();
+    bool reduceProblem();
     void extendGivenModel(vec<lbool> &model);
     void printVarsCls(bool encoding = true, const vec<Pair<weight_t, Minisat::vec<Lit>* > > *soft_cls = NULL, int soft_cls_sz = 0);
     // compute a list of propagated literals for a given literal lit under some possible global assumptions

ScipSolver.cc

@@ -102,7 +102,7 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
         // MY_SCIP_CALL(SCIPprintSol(scip, sol, nullptr, FALSE));
         solver->best_goalvalue = obj_offset + long(round(SCIPgetSolOrigObj(scip, sol)));
         if (!solver->ipamir_used || opt_verbosity > 0) 
-            reportf("SCIP optimum: %ld\n", tolong(solver->best_goalvalue));
+            reportf("SCIP optimum (rounded): %ld\n", tolong(solver->best_goalvalue));
         for (Var x = 0; x < (int)vars.size(); x++)
         {
             if (vars[x] != nullptr) {
@@ -138,6 +138,8 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
             solver->sat_solver.extendGivenModel(opt_model);
             solver->best_model.clear();
             for (int x = 0; x < solver->pb_n_vars; x++) solver->best_model.push(opt_model[x] != l_False);
+            Minisat::vec<Lit> soft_unsat; // Not used in this context
+            solver->best_goalvalue = (solver->fixed_goalval + evalGoal(solver->soft_cls, solver->best_model, soft_unsat)) * solver->goal_gcd;
 
             if (opt_verbosity >= 1) {
                 SCIP_MESSAGEHDLR *mh = SCIPgetMessagehdlr(scip);
@@ -189,9 +191,10 @@ lbool MsSolver::scip_solve(const Minisat::vec<Lit> *assump_ps,
                                   int sat_orig_vars,
                                   int sat_orig_cls)
 {
-    sat_solver.reduceProblem(); sat_orig_cls = sat_solver.nClauses();
+    bool res = sat_solver.reduceProblem(); sat_orig_cls = sat_solver.nClauses();
 
-    if (sat_solver.nFreeVars() >= 100000 || sat_orig_cls >= 150000 || soft_cls.size() >=  100000) return l_Undef;
+    if (!res || sat_solver.nFreeVars() >= 100000 || sat_orig_cls >= 150000 || soft_cls.size() >=  100000) 
+        return l_Undef;
 
     extern double opt_scip_cpu;
     extern bool opt_scip_parallel;