Adding encoding of sha1 collision for the hashing example

1 files changed, 10 insertions, 0 deletions

diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index ac9cfbcff..3035983d9 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -24,6 +24,8 @@
 
 #include "word.h"
 
+#include <vector>
+
 using namespace std;
 using namespace hashsmt;
 using namespace CVC4;
@@ -55,6 +57,14 @@ Expr Word::operator == (const Word& b) const {
   return em()->mkExpr(kind::EQUAL, d_expr, b.getExpr());
 }
 
+Word Word::concat(const Word words[], unsigned size) {
+  Expr concat = words[0].d_expr;
+  for(unsigned i = 1; i < size; ++i) {
+      concat = em()->mkExpr(kind::BITVECTOR_CONCAT, concat, words[i].d_expr);
+  }
+  return Word(concat);
+}
+
 void Word::print(ostream& out) const {
   out << CVC4::Expr::setdepth(-1) << d_expr;
 }