From 41b87b4c42382eedd96cc757a6bfcb9b6e3363f4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 2 Nov 2022 08:51:43 -0700
Subject: [PATCH] Create bv_slice_tactic.cpp

missing file
---
 src/tactic/bv/bv_slice_tactic.cpp | 33 +++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 src/tactic/bv/bv_slice_tactic.cpp

diff --git a/src/tactic/bv/bv_slice_tactic.cpp b/src/tactic/bv/bv_slice_tactic.cpp
new file mode 100644
index 000000000..040068e39
--- /dev/null
+++ b/src/tactic/bv/bv_slice_tactic.cpp
@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_slice_tactic.cpp
+
+Abstract:
+
+    Tactic for simplifying with bit-vector slices
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+
+#include "ast/simplifiers/bv_slice.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "tactic/bv/bv_slice_tactic.h"
+
+
+class bv_slice_factory : public dependent_expr_simplifier_factory {
+public:
+    dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
+        return alloc(bv::slice, m, s);
+    }
+};
+
+tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(bv_slice_factory), "bv-slice");
+}