Adding unit tests to external sat solveR

Author: fbbotero-aws

src/solvers/sat/external_sat.cpp

@@ -70,6 +70,8 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
   std::string line;
   external_satt::resultt result = resultt::P_ERROR;
   std::vector<bool> assigned_variables(no_variables(), false);
+  assignment.insert(assignment.begin(), no_variables(), tvt(false));
+
   while(getline(response_istream, line))
   {
     if(line[0] == 's')
@@ -92,7 +94,6 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
       if(status == "SATISFIABLE")
       {
         result = resultt::P_SATISFIABLE;
-        assignment.insert(assignment.begin(), no_variables() - 1, tvt(false));
       }
       if(status == "TIMEOUT")
       {
@@ -101,7 +102,7 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
       }
     }
 
-    if(line[0] == 'v' && result == resultt::P_SATISFIABLE)
+    if(line[0] == 'v')
     {
       auto assignments = split_string(line, ' ');
 

unit/Makefile

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

unit/solvers/sat/external_sat.cpp

@@ -0,0 +1,130 @@
+/// \file
+/// Unit tests for calling external SAT solver
+/// \author Francis Botero <[email protected]>
+
+#include <solvers/prop/literal.h>
+#include <solvers/sat/external_sat.h>
+#include <solvers/sat/satcheck_minisat2.h>
+#include <testing-utils/use_catch.h>
+#include <util/cout_message.h>
+
+class external_sat_test : public external_satt
+{
+public:
+  external_sat_test(message_handlert &message_handler, std::string cmd)
+    : external_satt(message_handler, cmd)
+  {
+  }
+
+  resultt parse_result(std::string result)
+  {
+    return external_satt::parse_result(result);
+  }
+};
+
+SCENARIO("external_sat", "[core][solvers][sat][external_sat]")
+{
+  console_message_handlert message_handler;
+
+  GIVEN("External SAT solver is used")
+  {
+    external_sat_test satcheck(message_handler, "cmd");
+    AND_GIVEN("the output is malformed")
+    {
+      auto result = GENERATE(
+        as<std::string>(),
+        "c comment line\nc another comment\n",
+        "c no results but assignments present\nv 1 2 3 4\n",
+        "c too many assignments\ns SATISFIABLE\nv 1 2 3 4",
+        "v_starts the line but is malformed",
+        "s_starts the line but is malformed",
+        "s SOMETHING STRANGE",
+        "another result");
+      WHEN("the solver output contains:\n" << result)
+      {
+        THEN("the result is set to error")
+        {
+          REQUIRE(satcheck.parse_result(result) == propt::resultt::P_ERROR);
+        }
+      }
+    }
+
+    AND_GIVEN("the output is malformed")
+    {
+      auto result = "c too few assignments\ns SATISFIABLE\nv 1 2 3 4";
+      WHEN("the solver output contains:\n" << result)
+      {
+        THEN("the result is set to error")
+        {
+          satcheck.set_no_variables(100);
+          REQUIRE(satcheck.parse_result(result) == propt::resultt::P_ERROR);
+        }
+      }
+    }
+
+    AND_GIVEN("SAT instance is unsatisfiable")
+    {
+      std::string unsat_result = GENERATE(
+        as<std::string>(),
+        "s UNSATISFIABLE",
+        "s UNSATISFIABLE\ns SATISFIABLE",
+        "s SATISFIABLE\ns UNSATISFIABLE");
+      WHEN("the solver output contains:\n" << unsat_result)
+      {
+        THEN("the result is set to unsatisfiable")
+        {
+          REQUIRE(
+            satcheck.parse_result(unsat_result) ==
+            propt::resultt::P_UNSATISFIABLE);
+        }
+      }
+    }
+
+    AND_GIVEN("SAT instance is satisfiable")
+    {
+      auto gen = GENERATE(
+        std::make_tuple(
+          "s SATISFIABLE\nv 1 2 3 4",
+          std::vector<bool>{true, true, true, true}),
+        std::make_tuple(
+          "s SATISFIABLE\nv 1 2 -3 -4",
+          std::vector<bool>{true, true, false, false}),
+        std::make_tuple(
+          "s SATISFIABLE\nv 1 -2 3 -4",
+          std::vector<bool>{true, false, true, false}),
+        std::make_tuple(
+          "s SATISFIABLE\nv -1 2 -3 4",
+          std::vector<bool>{false, true, false, true}),
+        std::make_tuple(
+          "s SATISFIABLE\nv -1 -2 -3 -4",
+          std::vector<bool>{false, false, false, false}),
+        std::make_tuple(
+          "v 4\ns SATISFIABLE\nv -1\nv 2\nv -3\n",
+          std::vector<bool>{false, true, false, true}));
+      WHEN("the solver output contains:\n" << std::get<0>(gen))
+      {
+        THEN("the result is set to satisfiable")
+        {
+          auto arr = std::get<1>(gen);
+          // add false to the start for element at 0
+          arr.insert(arr.begin(), false);
+          satcheck.set_no_variables(arr.size());
+          auto results_vector =
+            std::vector<bool>(satcheck.no_variables(), false);
+          REQUIRE(
+            satcheck.parse_result(std::get<0>(gen)) ==
+            propt::resultt::P_SATISFIABLE);
+          AND_THEN("has correct assignments")
+          {
+            auto assignments = satcheck.get_assignment();
+            for(size_t i = 1; i < satcheck.no_variables(); i++)
+            {
+              results_vector[i] = assignments[i].is_true();
+            }
+            REQUIRE_THAT(results_vector, Catch::Equals(arr));
+          }
+        }
+      }
+    }
+  }
+}