From dee35fc1a55e21e2c53bba75c64ab3ef38d46248 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 Apr 2026 09:55:56 -0700
Subject: [PATCH] really add fold-unfold as option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/CMakeLists.txt       |  1 +
 src/tactic/core/fold_unfold_tactic.h | 47 ++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 src/tactic/core/fold_unfold_tactic.h

diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt
index 8ab41f155..02e62aec0 100644
--- a/src/tactic/core/CMakeLists.txt
+++ b/src/tactic/core/CMakeLists.txt
@@ -34,6 +34,7 @@ z3_add_component(core_tactics
     elim_uncnstr_tactic.h
     elim_uncnstr2_tactic.h
     eliminate_predicates_tactic.h
+    fold_unfold_tactic.h
     injectivity_tactic.h
     nnf_tactic.h
     occf_tactic.h
diff --git a/src/tactic/core/fold_unfold_tactic.h b/src/tactic/core/fold_unfold_tactic.h
new file mode 100644
index 000000000..6fa3e5505
--- /dev/null
+++ b/src/tactic/core/fold_unfold_tactic.h
@@ -0,0 +1,47 @@
+
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    fold_unfold_tactic.h
+
+Abstract:
+
+    Tactic for solving variables
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-4-30
+
+Tactic Documentation:
+
+## Tactic fold-unfold
+
+### Short Description
+
+Solve for variables using fold-unfold transformations.
+
+### Notes
+
+* supports unsat cores
+* does not support fine-grained proofs
+* alternative to solve-eqs
+
+--*/
+
+#pragma once
+#include "util/params.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/fold_unfold.h"
+
+inline tactic *mk_fold_unfold_tactic(ast_manager &m, params_ref const &p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p,
+                 [](auto &m, auto &p, auto &s) -> dependent_expr_simplifier * { return alloc(euf::fold_unfold, m, s); });
+}
+
+/*
+  ADD_TACTIC("fold-unfold", "solve for variables.", "mk_fold_unfold_tactic(m, p)")
+  ADD_SIMPLIFIER("fold-unfold", "solve for variables.", "alloc(euf::fold_unfold, m, s)")
+*/