diff options
Diffstat (limited to 'examples/hashsmt/word.cpp')
-rw-r--r-- | examples/hashsmt/word.cpp | 10 |
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; } |