Merge pull request #4810 from peterschrammel/minisat2-unit-test

satcheck_minisat2 assumptions bug fix and unit tests

Author: peterschrammel

src/solvers/sat/satcheck_minisat2.cpp

@@ -178,89 +178,80 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
     {
       log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
                    << messaget::eom;
+      status = statust::UNSAT;
+      return resultt::P_UNSATISFIABLE;
     }
-    else
-    {
-      // if assumptions contains false, we need this to be UNSAT
-      bool has_false=false;
-
-      forall_literals(it, assumptions)
-        if(it->is_false())
-          has_false=true;
 
-      if(has_false)
+    // if assumptions contains false, we need this to be UNSAT
+    for(const auto &assumption : assumptions)
+    {
+      if(assumption.is_false())
       {
         log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
                      << messaget::eom;
+        status = statust::UNSAT;
+        return resultt::P_UNSATISFIABLE;
       }
-      else
-      {
-        Minisat::vec<Minisat::Lit> solver_assumptions;
-        convert(assumptions, solver_assumptions);
+    }
 
-        using Minisat::lbool;
+    Minisat::vec<Minisat::Lit> solver_assumptions;
+    convert(assumptions, solver_assumptions);
+
+    using Minisat::lbool;
 
 #ifndef _WIN32
 
-        void (*old_handler)(int)=SIG_ERR;
+    void (*old_handler)(int) = SIG_ERR;
 
-        if(time_limit_seconds!=0)
-        {
-          solver_to_interrupt=solver;
-          old_handler=signal(SIGALRM, interrupt_solver);
-          if(old_handler==SIG_ERR)
-            log.warning() << "Failed to set solver time limit" << messaget::eom;
-          else
-            alarm(time_limit_seconds);
-        }
+    if(time_limit_seconds != 0)
+    {
+      solver_to_interrupt = solver;
+      old_handler = signal(SIGALRM, interrupt_solver);
+      if(old_handler == SIG_ERR)
+        log.warning() << "Failed to set solver time limit" << messaget::eom;
+      else
+        alarm(time_limit_seconds);
+    }
 
-        lbool solver_result=solver->solveLimited(solver_assumptions);
+    lbool solver_result = solver->solveLimited(solver_assumptions);
 
-        if(old_handler!=SIG_ERR)
-        {
-          alarm(0);
-          signal(SIGALRM, old_handler);
-          solver_to_interrupt=solver;
-        }
+    if(old_handler != SIG_ERR)
+    {
+      alarm(0);
+      signal(SIGALRM, old_handler);
+      solver_to_interrupt = solver;
+    }
 
 #else // _WIN32
 
-        if(time_limit_seconds!=0)
-        {
-          log.warning() << "Time limit ignored (not supported on Win32 yet)"
-                        << messaget::eom;
-        }
+    if(time_limit_seconds != 0)
+    {
+      log.warning() << "Time limit ignored (not supported on Win32 yet)"
+                    << messaget::eom;
+    }
 
-        lbool solver_result=
-          solver->solve(solver_assumptions) ? l_True : l_False;
+    lbool solver_result = solver->solve(solver_assumptions) ? l_True : l_False;
 
 #endif
 
-        if(solver_result==l_True)
-        {
-          log.status() << "SAT checker: instance is SATISFIABLE"
-                       << messaget::eom;
-          CHECK_RETURN(solver->model.size()>0);
-          status=statust::SAT;
-          return resultt::P_SATISFIABLE;
-        }
-        else if(solver_result==l_False)
-        {
-          log.status() << "SAT checker: instance is UNSATISFIABLE"
-                       << messaget::eom;
-        }
-        else
-        {
-          log.status() << "SAT checker: timed out or other error"
-                       << messaget::eom;
-          status=statust::ERROR;
-          return resultt::P_ERROR;
-        }
-      }
+    if(solver_result == l_True)
+    {
+      log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
+      CHECK_RETURN(solver->model.size() > 0);
+      status = statust::SAT;
+      return resultt::P_SATISFIABLE;
+    }
+
+    if(solver_result == l_False)
+    {
+      log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
+      status = statust::UNSAT;
+      return resultt::P_UNSATISFIABLE;
     }
 
-    status=statust::UNSAT;
-    return resultt::P_UNSATISFIABLE;
+    log.status() << "SAT checker: timed out or other error" << messaget::eom;
+    status = statust::ERROR;
+    return resultt::P_ERROR;
   }
   catch(const Minisat::OutOfMemoryException &)
   {
@@ -328,14 +319,16 @@ bool satcheck_minisat2_baset<T>::is_in_conflict(literalt a) const
 template<typename T>
 void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
 {
-  assumptions=bv;
-
-  forall_literals(it, assumptions)
-    if(it->is_true())
+  // We filter out 'true' assumptions which cause an assertion violation
+  // in Minisat2.
+  assumptions.clear();
+  for(const auto &assumption : bv)
+  {
+    if(!assumption.is_true())
     {
-      assumptions.clear();
-      break;
+      assumptions.push_back(assumption);
     }
+  }
 }
 
 satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(

unit/Makefile

@@ -45,6 +45,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/lowering/byte_operators.cpp \
        solvers/prop/bdd_expr.cpp \
+       solvers/sat/satcheck_minisat2.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \

unit/solvers/sat/module_dependencies.txt

@@ -0,0 +1,4 @@
+solvers/prop
+solvers/sat
+testing-utils
+util

unit/solvers/sat/satcheck_minisat2.cpp

@@ -0,0 +1,86 @@
+/*******************************************************************\
+
+Module: Unit tests for satcheck_minisat2
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for satcheck_minisat2
+
+#ifdef HAVE_MINISAT2
+
+#  include <testing-utils/use_catch.h>
+
+#  include <solvers/prop/literal.h>
+#  include <solvers/sat/satcheck_minisat2.h>
+#  include <util/cout_message.h>
+
+SCENARIO("satcheck_minisat2", "[core][solvers][sat][satcheck_minisat2]")
+{
+  console_message_handlert message_handler;
+
+  GIVEN("A satisfiable formula f")
+  {
+    satcheck_minisat_no_simplifiert satcheck(message_handler);
+    literalt f = satcheck.new_variable();
+    satcheck.l_set_to_true(f);
+
+    THEN("is indeed satisfiable")
+    {
+      REQUIRE(satcheck.prop_solve() == propt::resultt::P_SATISFIABLE);
+    }
+    THEN("is unsatisfiable under a false assumption")
+    {
+      bvt assumptions;
+      assumptions.push_back(const_literal(false));
+      satcheck.set_assumptions(assumptions);
+      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("An unsatisfiable formula f && !f")
+  {
+    satcheck_minisat_no_simplifiert satcheck(message_handler);
+    literalt f = satcheck.new_variable();
+    satcheck.l_set_to_true(satcheck.land(f, !f));
+
+    THEN("is indeed unsatisfiable")
+    {
+      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("An unsatisfiable formula false implied by a")
+  {
+    satcheck_minisat_no_simplifiert satcheck(message_handler);
+    literalt a = satcheck.new_variable();
+    literalt a_implies_false = satcheck.lor(!a, const_literal(false));
+    satcheck.l_set_to_true(a_implies_false);
+
+    THEN("is indeed unsatisfiable under assumption a")
+    {
+      bvt assumptions;
+      assumptions.push_back(a);
+      satcheck.set_assumptions(assumptions);
+      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+    }
+    THEN("is still unsatisfiable under assumption a and true")
+    {
+      bvt assumptions;
+      assumptions.push_back(const_literal(true));
+      assumptions.push_back(a);
+      satcheck.set_assumptions(assumptions);
+      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+    }
+    THEN("becomes satisfiable when assumption a is lifted")
+    {
+      bvt assumptions;
+      satcheck.set_assumptions(assumptions);
+      REQUIRE(satcheck.prop_solve() == propt::resultt::P_SATISFIABLE);
+    }
+  }
+}
+
+#endif