From eb7fd9efaae5b235f7792702edc9d6de5a35ef17 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 14 Aug 2025 11:54:34 -0700
Subject: [PATCH] Add virtual translate method to solver_factory class (#7780)

* Initial plan

* Add virtual translate method to solver_factory base class and all implementations

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add documentation for the translate method in solver_factory

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/smt_solver.cpp                        | 4 ++++
 src/solver/combined_solver.cpp                | 6 ++++++
 src/solver/solver.h                           | 5 +++++
 src/solver/tactic2solver.cpp                  | 9 +++++++++
 src/tactic/portfolio/smt_strategic_solver.cpp | 8 ++++++++
 5 files changed, 32 insertions(+)

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 05bcc00ba..1d38c0685 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -527,6 +527,10 @@ public:
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         return mk_smt_solver(m, p, logic);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(smt_solver_factory);
+    }
 };
 }
 
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index aacb2b1cc..9f489124f 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -424,6 +424,12 @@ public:
                                   (*m_f2)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic),
                                   p);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        solver_factory* translated_f1 = m_f1->translate(m);
+        solver_factory* translated_f2 = m_f2->translate(m);
+        return alloc(combined_solver_factory, translated_f1, translated_f2);
+    }
 };
 
 solver_factory * mk_combined_solver_factory(solver_factory * f1, solver_factory * f2) {
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 3ddd0b11f..b45f4f347 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -32,6 +32,11 @@ class solver_factory {
 public:
     virtual ~solver_factory() = default;
     virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0;
+    /**
+       \brief Create a clone of the solver factory for the given ast_manager.
+       The clone should be functionally equivalent but associated with the target manager.
+    */
+    virtual solver_factory* translate(ast_manager& m) = 0;
 };
 
 solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null);
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 7c4542451..af5442b77 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -390,6 +390,11 @@ public:
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         return mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        tactic* translated_tactic = m_tactic->translate(m);
+        return alloc(tactic2solver_factory, translated_tactic);
+    }
 };
 
 class tactic_factory2solver_factory : public solver_factory {
@@ -402,6 +407,10 @@ public:
         tactic * t = (*m_factory)(m, p);
         return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(tactic_factory2solver_factory, m_factory);
+    }
 };
 }
 
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 5257a70b5..ffd6450b3 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -60,6 +60,10 @@ public:
         auto s = mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
         return s;
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(smt_nested_solver_factory);
+    }
 };
 
 tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
@@ -185,6 +189,10 @@ public:
                                   mk_solver_for_logic(m, p, l), 
                                   p);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(smt_strategic_solver_factory, m_logic);
+    }
 };
 
 solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) {