Merge pull request #8998 from diffblue/feature/1bit-signed-bv-compare

Support 1-bit signed bitvectors in `bv_utilst::lt_or_le`

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -1409,6 +1409,7 @@ literalt bv_utilst::lt_or_le(
   representationt rep)
 {
   PRECONDITION(bv0.size() == bv1.size());
+  PRECONDITION(!bv0.empty());
 
 #ifdef COMPACT_LT_OR_LE
   if(prop.has_set_to() && prop.cnf_handled_well())
@@ -1422,8 +1423,18 @@ literalt bv_utilst::lt_or_le(
       else if(top0.is_true() && top1.is_false())
         return const_literal(true);
 
+      // 1-bit signed: the sign bit is the only bit
+      if(bv0.size() == 1)
+      {
+        if(or_equal)
+          return prop.lor(top0, !top1);
+        else
+          return prop.land(top0, !top1);
+      }
+
       INVARIANT(
-        bv0.size() >= 2, "signed bitvectors should have at least two bits");
+        bv0.size() >= 2,
+        "the compact signed comparison encoding requires at least two bits");
       // 1 if a compare is needed below this bit
       bvt compareBelow = prop.new_variables(bv0.size() - 1);
       size_t start = compareBelow.size() - 1;

unit/Makefile

@@ -104,6 +104,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/flattening/boolbv_enumeration.cpp \
        solvers/flattening/boolbv_onehot.cpp \
        solvers/flattening/boolbv_update_bit.cpp \
+       solvers/flattening/bv_utils.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/prop/bdd_expr.cpp \
        solvers/sat/external_sat.cpp \

unit/solvers/flattening/bv_utils.cpp

@@ -0,0 +1,84 @@
+/*******************************************************************\
+
+Module: Unit tests for bv_utilst
+
+Author: Daniel Kroening
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for bv_utilst
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/cout_message.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO("1-bit signed less-than", "[core][solvers][flattening][bv_utils]")
+{
+  console_message_handlert message_handler;
+  message_handler.set_verbosity(0);
+
+  GIVEN("Two 1-bit signed bitvector symbols")
+  {
+    satcheckt satcheck(message_handler);
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    boolbvt boolbv(ns, satcheck, message_handler);
+
+    signedbv_typet s1(1);
+    auto x = symbol_exprt("x", s1);
+    auto y = symbol_exprt("y", s1);
+
+    THEN("-1 < 0 is satisfiable")
+    {
+      // x = -1, y = 0, x < y
+      boolbv << equal_exprt(x, from_integer(-1, s1));
+      boolbv << equal_exprt(y, from_integer(0, s1));
+      boolbv << less_than_exprt(x, y);
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+
+    THEN("0 < -1 is unsatisfiable")
+    {
+      boolbv << equal_exprt(x, from_integer(0, s1));
+      boolbv << equal_exprt(y, from_integer(-1, s1));
+      boolbv << less_than_exprt(x, y);
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+
+    THEN("-1 <= -1 is satisfiable")
+    {
+      boolbv << equal_exprt(x, from_integer(-1, s1));
+      boolbv << equal_exprt(y, from_integer(-1, s1));
+      boolbv << less_than_or_equal_exprt(x, y);
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+
+    THEN("-1 < -1 is unsatisfiable")
+    {
+      boolbv << equal_exprt(x, from_integer(-1, s1));
+      boolbv << equal_exprt(y, from_integer(-1, s1));
+      boolbv << less_than_exprt(x, y);
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+
+    THEN("x < y is satisfiable for symbolic 1-bit signed values")
+    {
+      boolbv << less_than_exprt(x, y);
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+
+    THEN("x <= y is satisfiable for symbolic 1-bit signed values")
+    {
+      boolbv << less_than_or_equal_exprt(x, y);
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+  }
+}