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 <[email protected]>

* Add documentation for the translate method in solver_factory

Co-authored-by: NikolajBjorner <[email protected]>

---------

Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: NikolajBjorner <[email protected]>

Author: Copilot

src/smt/smt_solver.cpp

@@ -527,6 +527,10 @@ class smt_solver_factory : public solver_factory {
     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);
+    }
 };
 }
 

src/solver/combined_solver.cpp

@@ -424,6 +424,12 @@ class combined_solver_factory : public solver_factory {
                                   (*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) {

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);

src/solver/tactic2solver.cpp

@@ -390,6 +390,11 @@ class tactic2solver_factory : public solver_factory {
     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 @@ class tactic_factory2solver_factory : public solver_factory {
         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);
+    }
 };
 }
 

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -60,6 +60,10 @@ class smt_nested_solver_factory : public solver_factory {
         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 @@ class smt_strategic_solver_factory : public solver_factory {
                                   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) {