From 01cf0427b4f788e854005f15fcbe3db6f6a6155b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Sep 2024 11:36:10 +0100
Subject: [PATCH] fix #7404, relates to #7400.
---
src/tactic/core/simplify_tactic.cpp | 4 ++++
src/tactic/core/simplify_tactic.h | 1 +
src/tactic/smtlogics/qfnra_tactic.cpp | 19 ++++++++++++-------
src/tactic/tactic.cpp | 26 ++++++++++++++++++++++++++
src/tactic/tactic.h | 1 +
src/tactic/tactical.cpp | 14 +++++++++++---
6 files changed, 55 insertions(+), 10 deletions(-)
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index f05b4c4fc62..ee5cd0f73c9 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/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 {
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index 7baabb8d6e8..af0806162b1 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/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;
diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp
index f95ae8a8c05..ab28ffab72b 100644
--- a/src/tactic/smtlogics/qfnra_tactic.cpp
+++ b/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
)
)
)
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index e4e7b246aef..19a370caa9f 100644
--- a/src/tactic/tactic.cpp
+++ b/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 {
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index c6927642476..698146c0d3d 100644
--- a/src/tactic/tactic.h
+++ b/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()")
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index db0a6d44d76..78e15aef7a7 100644
--- a/src/tactic/tactical.cpp
+++ b/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