handling overflows

yoni206 · Aug 2, 2024 · 9c45467 · 9c45467
1 parent df3dc90
commit 9c45467
Showing 1 changed file with 52 additions and 0 deletions.
diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
@@ -541,6 +541,58 @@ Node IntBlaster::translateWithChildren(
           d_zero);
       break;
     }
+    case Kind::BITVECTOR_UADDO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node sum = d_nm->mkNode(Kind::ADD, translated_children[0], translated_children[1]);
+      returnNode = d_nm->mkNode(Kind::GEQ, sum, pow2(bvsize));
+      break;
+    }
+    case Kind::BITVECTOR_SADDO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node signed0 = uts(translated_children[0], bvsize);
+      Node signed1 = uts(translated_children[1], bvsize);
+      Node sum = d_nm->mkNode(Kind::ADD, signed0, signed1);
+      Node disj1 = d_nm->mkNode(Kind::GEQ, sum, pow2(bvsize - 1));
+      Node disj2 = d_nm->mkNode(Kind::LT, sum, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
+      returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
+      break;
+    }
+    case Kind::BITVECTOR_UMULO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node mul = d_nm->mkNode(Kind::MULT, translated_children[0], translated_children[1]);
+      returnNode = d_nm->mkNode(Kind::GEQ, mul, pow2(bvsize));
+      break;
+    }
+    case Kind::BITVECTOR_SMULO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node signed0 = uts(translated_children[0], bvsize);
+      Node signed1 = uts(translated_children[1], bvsize);
+      Node mul = d_nm->mkNode(Kind::MULT, signed0, signed1);
+      Node disj1 = d_nm->mkNode(Kind::GEQ, mul, pow2(bvsize - 1));
+      Node disj2 = d_nm->mkNode(Kind::LT, mul, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
+      returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
+      break;
+    }
+    case Kind::BITVECTOR_USUBO:
+    {
+      returnNode = d_nm->mkNode(Kind::LT, translated_children[0], translated_children[1]);
+      break;
+    }
+    case Kind::BITVECTOR_SSUBO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node signed0 = uts(translated_children[0], bvsize);
+      Node signed1 = uts(translated_children[1], bvsize);
+      Node sub = d_nm->mkNode(Kind::SUB, signed0, signed1);
+      Node disj1 = d_nm->mkNode(Kind::GEQ, sub, pow2(bvsize - 1));
+      Node disj2 = d_nm->mkNode(Kind::LT, sub, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
+      returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
+      break;
+    }
     case Kind::ITE:
     {
       returnNode = d_nm->mkNode(oldKind, translated_children);