Add mkZero, mkOne and mkUmulo to bv utils. (#1200)

This adds several utility functions for the theory BV. Function mkUmulo encodes an unsigned multiplication overflow detection operation, which we need for CBQI BV. In the future, we will introduce a Umulo node kind (and a corresponding bit-blasting strategy based on the encoding implemented in mkUmulo).

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 6697f9060ff0019710c9092e3b32d7801e1bd42b..aa318060484b8b657fe6575bbe432a113f220b17 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -16,6 +16,9 @@
  **/
 
 #include "theory/bv/theory_bv_utils.h"
+
+#include <vector>
+
 #include "theory/theory.h"
 
 namespace CVC4 {
@@ -23,6 +26,26 @@ namespace theory {
 namespace bv {
 namespace utils {
 
+Node mkUmulo(TNode t1, TNode t2) {
+  unsigned w = getSize(t1);
+  if (w == 1) return mkFalse();
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node uppc;
+  std::vector<Node> tmp;
+
+  uppc = mkExtract(t1, w - 1, w - 1);
+  for (size_t i = 1; i < w; ++i) {
+    tmp.push_back(nm->mkNode(kind::BITVECTOR_AND, mkExtract(t2, i, i), uppc));
+    uppc = nm->mkNode(kind::BITVECTOR_OR, mkExtract(t1, w-1-i, w-1-i), uppc);
+  }
+  Node zext_t1 = mkConcat(mkZero(1), t1);
+  Node zext_t2 = mkConcat(mkZero(1), t2);
+  Node mul = nm->mkNode(kind::BITVECTOR_MULT, zext_t1, zext_t2);
+  tmp.push_back(mkExtract(mul, w, w));
+  return nm->mkNode(kind::EQUAL, nm->mkNode(kind::BITVECTOR_OR, tmp), mkOne(1));
+}
+
 bool isCoreTerm(TNode term, TNodeBoolMap& cache) {
   term = term.getKind() == kind::NOT ? term[0] : term;
   TNodeBoolMap::const_iterator it = cache.find(term);

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 8b8d5e00319f71065048a763a9ba5230144ad884..6be0af4a0b9f8da5df2f9ee483fbb6dc2f67abae 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -204,6 +204,16 @@ inline Node mkConst(const BitVector& value) {
   return NodeManager::currentNM()->mkConst<BitVector>(value);
 }
 
+inline Node mkZero(unsigned size) { return mkConst(size, 0u); }
+
+inline Node mkOne(unsigned size) { return mkConst(size, 1u); }
+
+/* Unsigned multiplication overflow detection.
+ * See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
+ * overflow detection circuits", 2001.
+ * http://ieeexplore.ieee.org/document/987767 */
+Node mkUmulo(TNode t1, TNode t2);
+
 inline void getConjuncts(TNode node, std::set<TNode>& conjuncts) {
   if (node.getKind() != kind::AND) {
     conjuncts.insert(node);

diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index 19b715f762e53592303c02bbaad4bba594382652..5721957ec1b81208e2e25a0fe457fd4aef787316 100644 (file)
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -47,7 +47,6 @@ class TheoryBVWhite : public CxxTest::TestSuite {
   NodeManager* d_nm;
   SmtEngine* d_smt;
   SmtScope* d_scope;
-  EagerBitblaster* d_bb;
 
 public:
 
@@ -58,18 +57,18 @@ public:
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
-    d_smt->setOption("bitblast", SExpr("eager"));
-    d_bb = new EagerBitblaster(dynamic_cast<TheoryBV*>(d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]));
   }
 
   void tearDown() {
-    delete d_bb;
     delete d_scope;
     delete d_smt;
     delete d_em;
   }
  
   void testBitblasterCore() {
+    d_smt->setOption("bitblast", SExpr("eager"));
+    EagerBitblaster* bb = new EagerBitblaster(dynamic_cast<TheoryBV*>(
+        d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]));
     Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
     Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
     Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y);
@@ -77,11 +76,33 @@ public:
     Node x_shl_one = d_nm->mkNode(kind::BITVECTOR_SHL, x, one);
     Node eq = d_nm->mkNode(kind::EQUAL, x_plus_y, x_shl_one);
     Node not_x_eq_y = d_nm->mkNode(kind::NOT, d_nm->mkNode(kind::EQUAL, x, y));
-    
-    d_bb->bbFormula(eq);
-    d_bb->bbFormula(not_x_eq_y);
 
-    bool res = d_bb->solve(); 
+    bb->bbFormula(eq);
+    bb->bbFormula(not_x_eq_y);
+
+    bool res = bb->solve();
     TS_ASSERT (res == false);
+    delete bb;
+  }
+
+  void testMkUmulo() {
+    d_smt->setOption("incremental", SExpr("true"));
+    for (size_t w = 1; w < 16; ++w) {
+      d_smt->push();
+      Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(w));
+      Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(w));
+
+      Node zx = mkConcat(mkZero(w), x);
+      Node zy = mkConcat(mkZero(w), y);
+      Node mul = d_nm->mkNode(kind::BITVECTOR_MULT, zx, zy);
+      Node lhs =
+          d_nm->mkNode(kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w));
+      Node rhs = mkUmulo(x, y);
+      Node eq = d_nm->mkNode(kind::DISTINCT, lhs, rhs);
+      d_smt->assertFormula(eq.toExpr());
+      Result res = d_smt->checkSat();
+      TS_ASSERT(res.isSat() == Result::UNSAT);
+      d_smt->pop();
+    }
   }
 };/* class TheoryBVWhite */