From 67ec86fc66ad06a0aa976bb4a00c79c56dce5d06 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Apr 2021 22:53:18 -0700
Subject: [PATCH] #5211

---
 src/ast/bv_decl_plugin.cpp     |  9 +++++++++
 src/ast/bv_decl_plugin.h       |  1 +
 src/sat/smt/bv_internalize.cpp | 13 +++++++++++++
 src/sat/smt/bv_solver.h        |  1 +
 4 files changed, 24 insertions(+)

diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 243e4273a..d01ed8b75 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -827,6 +827,15 @@ bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, ex
     return true;
 }
 
+bool bv_recognizers::is_repeat(expr const * e, expr*& arg, unsigned& n) const {
+    if (!is_app_of(e, get_fid(), OP_REPEAT))
+        return false;
+    arg = to_app(e)->get_arg(0);
+    n = to_app(e)->get_parameter(0).get_int();
+    return true;
+}
+
+
 bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const {
     if (!is_bv2int(e)) return false;
     r = to_app(e)->get_arg(0);
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index fc091f1f4..e780ad7a7 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -310,6 +310,7 @@ public:
     unsigned get_extract_high(expr const * n) const { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
     unsigned get_extract_low(expr const * n) const { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
     bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b) const;
+    bool is_repeat(expr const * e, expr*& arg, unsigned& n) const;
     bool is_bv2int(expr const * e, expr * & r) const;
     bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
     bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 81c9bd3bc..01e697d53 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -213,6 +213,7 @@ namespace bv {
         case OP_BSUB:             internalize_sub(a); break;
         case OP_CONCAT:           internalize_concat(a); break;
         case OP_EXTRACT:          internalize_extract(a); break;
+        case OP_REPEAT:           internalize_repeat(a); break;
         case OP_MKBV:             internalize_mkbv(a); break;
         case OP_INT2BV:           internalize_int2bv(a); break;
         case OP_BV2INT:           internalize_bv2int(a); break;
@@ -641,6 +642,18 @@ namespace bv {
         find_wpos(v);
     }
 
+    void solver::internalize_repeat(app* e) {
+        unsigned n = 0;
+        expr* arg = nullptr;
+        VERIFY(bv.is_repeat(e, arg, n));
+        expr_ref_vector conc(m);
+        for (unsigned i = 0; i < n; ++i)
+            conc.push_back(arg);
+        expr_ref r(bv.mk_concat(conc), m);
+        mk_bits(get_th_var(e));
+        add_unit(eq_internalize(e, r));
+    }
+
     void solver::internalize_bit2bool(app* n) {
         unsigned idx = 0;
         expr* arg = nullptr;
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index cf3d13751..94f0b03dc 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -249,6 +249,7 @@ namespace bv {
         void internalize_carry(app* n);
         void internalize_sub(app* n);
         void internalize_extract(app* n);
+        void internalize_repeat(app* n);
         void internalize_bit2bool(app* n);
         void internalize_udiv_i(app* n);
         template<bool Signed, bool Reverse, bool Negated>