fix Z3Prover#7404, relates to Z3Prover#7400.

Author: NikolajBjorner

src/tactic/core/simplify_tactic.cpp

@@ -98,6 +98,7 @@ void simplify_tactic::operator()(goal_ref const & in,
         (*m_imp)(*(in.get()));
         in->inc_depth();
         result.push_back(in.get());
+        m_clean = false;
     }
     catch (rewriter_exception & ex) {
         throw tactic_exception(ex.msg());
@@ -106,10 +107,13 @@ void simplify_tactic::operator()(goal_ref const & in,
 
 
 void simplify_tactic::cleanup() {
+    if (m_clean)
+        return;
     ast_manager & m = m_imp->m();
     params_ref p = std::move(m_params);
     m_imp->~imp();
     new (m_imp) imp(m, p);
+    m_clean = true;
 }
 
 void simplify_tactic::collect_statistics(statistics& st) const {

src/tactic/core/simplify_tactic.h

@@ -69,6 +69,7 @@ There are several options to control its behavior.
 #include "tactic/tactical.h"
 
 class simplify_tactic : public tactic {
+    bool       m_clean = true;
     struct     imp;
     imp *      m_imp;
     params_ref m_params;

src/tactic/smtlogics/qfnra_tactic.cpp

@@ -89,7 +89,7 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) {
         p_i.set_bool("shuffle_vars", true);
         // if ((i & 1) == 0)
         //     p_i.set_bool("randomize", false);
-        ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 3 * 1000));
+        ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p_i), 3 * 1000); }));
     }
     {
         ts.push_back(mk_qfnra_nlsat_tactic(m, p));
@@ -147,7 +147,7 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) {
         p_i.set_bool("shuffle_vars", true);
         // if ((i & 1) == 0)
         //     p_i.set_bool("randomize", false);
-        ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 5 * 1000));
+        ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p_i), 5 * 1000); }));
     }
     {
         ts.push_back(mk_qfnra_nlsat_tactic(m, p));
@@ -308,15 +308,20 @@ const double SMALL_THRESHOLD = 80.0;
 const double MIDDLE_THRESHOLD = 300.0;
 const double LARGE_THRESHOLD = 600.0;
 tactic * mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) {
+    auto very_small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_small_solver(m, p); });
+    auto small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_small_solver(m, p); });
+    auto middle_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_middle_solver(m, p); });
+    auto large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_large_solver(m, p); });
+    auto very_large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_large_solver(m, p); });
     return cond(mk_lt(mk_memory_probe(), mk_const_probe(VERY_SMALL_THRESHOLD)), 
-                mk_qfnra_very_small_solver(m, p),
+        very_small_t,
                 cond(mk_lt(mk_memory_probe(), mk_const_probe(SMALL_THRESHOLD)), 
-                     mk_qfnra_small_solver(m, p),
+                    small_t,
                      cond(mk_lt(mk_memory_probe(), mk_const_probe(MIDDLE_THRESHOLD)),
-                          mk_qfnra_middle_solver(m, p),
+                         middle_t,
                           cond(mk_lt(mk_memory_probe(), mk_const_probe(LARGE_THRESHOLD)),
-                               mk_qfnra_large_solver(m, p),
-                               mk_qfnra_very_large_solver(m, p)
+                             large_t,
+                             very_large_t
                         )
                     )
                 )

src/tactic/tactic.cpp

@@ -95,6 +95,32 @@ tactic * mk_skip_tactic() {
     return alloc(skip_tactic);
 }
 
+class lazy_tactic : public tactic {
+    ast_manager& m;
+    params_ref p;
+    std::function<tactic* (ast_manager& m, params_ref const& p)> m_mk_tactic;
+    tactic* m_tactic = nullptr;
+    void ensure_tactic() { if (!m_tactic) m_tactic = m_mk_tactic(m, p); }
+public:
+    lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic* (ast_manager&, params_ref const&)> mk_tactic) : m(m), p(p), m_mk_tactic(mk_tactic) {}
+    ~lazy_tactic() override { dealloc(m_tactic); }
+    void operator()(goal_ref const& in, goal_ref_buffer& result) override {
+        ensure_tactic();
+        (*m_tactic)(in, result);
+    }
+    void cleanup() override { if (m_tactic) m_tactic->cleanup(); }
+    char const* name() const override { return "lazy tactic"; }
+    void collect_statistics(statistics& st) const override { if (m_tactic) m_tactic->collect_statistics(st); }
+    void user_propagate_initialize_value(expr* var, expr* value) override { if (m_tactic) m_tactic->user_propagate_initialize_value(var, value); }
+    tactic* translate(ast_manager& m) override { ensure_tactic(); return m_tactic->translate(m); }
+    void reset() override { if (m_tactic) m_tactic->reset(); }
+};
+
+
+tactic* mk_lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic*(ast_manager& m, params_ref const& p)> mkt) {
+    return alloc(lazy_tactic, m, p, mkt);
+}
+
 class fail_tactic : public tactic {
 public:
     void operator()(goal_ref const & in, goal_ref_buffer & result) override {

src/tactic/tactic.h

@@ -135,6 +135,7 @@ class skip_tactic : public tactic {
 tactic * mk_skip_tactic();
 tactic * mk_fail_tactic();
 tactic * mk_fail_if_undecided_tactic();
+tactic*  mk_lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic*(ast_manager& m, params_ref const& p)>);
 
 /*
   ADD_TACTIC("skip", "do nothing tactic.", "mk_skip_tactic()")

src/tactic/tactical.cpp

@@ -30,6 +30,7 @@ class binary_tactical : public tactic {
 protected:
     tactic_ref      m_t1;
     tactic_ref      m_t2;
+    bool            m_clean = true;
 
 public:
 
@@ -61,8 +62,11 @@ class binary_tactical : public tactic {
     }
 
     void cleanup() override {
+        if (m_clean)
+            return;
         m_t1->cleanup();
         m_t2->cleanup();
+        m_clean = true;
     }
 
     void reset() override {
@@ -103,7 +107,8 @@ class and_then_tactical : public binary_tactical {
 
     char const* name() const override { return "and_then"; }
 
-    void operator()(goal_ref const & in, goal_ref_buffer& result) override { 
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
+        m_clean = false;
 
         bool proofs_enabled = in->proofs_enabled();
         bool cores_enabled  = in->unsat_core_enabled();
@@ -872,6 +877,7 @@ tactic * par_and_then(unsigned num, tactic * const * ts) {
 class unary_tactical : public tactic {
 protected:
     tactic_ref m_t;
+    bool m_clean = true;
 
 
 public:
@@ -880,11 +886,12 @@ class unary_tactical : public tactic {
         SASSERT(t);  
     }
 
-    void operator()(goal_ref const & in, goal_ref_buffer& result) override { 
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
+        m_clean = false;
         m_t->operator()(in, result);
     }
 
-    void cleanup(void) override { m_t->cleanup(); }
+    void cleanup(void) override { if (!m_clean) m_t->cleanup(); m_clean = true; }
     void collect_statistics(statistics & st) const override { m_t->collect_statistics(st); }
     void reset_statistics() override { m_t->reset_statistics(); }    
     void updt_params(params_ref const & p) override { m_t->updt_params(p); }
@@ -1158,6 +1165,7 @@ class cond_tactical : public binary_tactical {
     char const* name() const override { return "cond"; }
 
     void operator()(goal_ref const & in, goal_ref_buffer & result) override {
+        m_clean = false;
         if (m_p->operator()(*(in.get())).is_true()) 
             m_t1->operator()(in, result);
         else