really add fold-unfold as option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

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)")
+*/