From ba6b21d7d4d5b3faa46696b707a59afb4a8c5ed6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Nov 2022 05:23:38 -0700
Subject: [PATCH] Create solve_eqs2_tactic.h

---
 src/tactic/core/solve_eqs2_tactic.h | 41 +++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 src/tactic/core/solve_eqs2_tactic.h

diff --git a/src/tactic/core/solve_eqs2_tactic.h b/src/tactic/core/solve_eqs2_tactic.h
new file mode 100644
index 000000000..91b3875ae
--- /dev/null
+++ b/src/tactic/core/solve_eqs2_tactic.h
@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    solve_eqs2_tactic.h
+
+Abstract:
+
+    Tactic for solving variables
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+#pragma once
+
+#include "util/params.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/solve_eqs.h"
+
+
+class solve_eqs2_tactic_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(euf::solve_eqs, m, s);
+    }
+};
+
+inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs2");
+}
+
+
+/*
+  ADD_TACTIC("solve-eqs2", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")
+*/
+
+