mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 13:26:10 +00:00
Code Activity

update print and cancelation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-15 20:43:49 -07:00
parent 7dea14f732
commit db8a2f4f9e
3 changed files with 3 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/seq/seq_nielsen.cpp
View file

@ -2109,10 +2109,11 @@ namespace seq {
// m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it. // m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it.
m_depth_bound = 10; m_depth_bound = 10;
while (true) { while (true) {
if (m_cancel_fn && m_cancel_fn()) { if (!m().inc()) {
#ifdef Z3DEBUG #ifdef Z3DEBUG
// Examining the Nielsen graph is probably the best way of debugging // Examining the Nielsen graph is probably the best way of debugging
std::string dot = to_dot(); std::string dot = to_dot();
IF_VERBOSE(1, verbose_stream() << dot << "\n";);
#endif #endif
break; break;
} }
@ -2156,7 +2157,7 @@ namespace seq {
m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth); m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
// check for external cancellation (timeout, user interrupt) // check for external cancellation (timeout, user interrupt)
if (m_cancel_fn && m_cancel_fn()) if (!m().inc())
return search_result::unknown; return search_result::unknown;
// check DFS node budget (0 = unlimited) // check DFS node budget (0 = unlimited)

5
src/smt/seq/seq_nielsen.h
View file

@ -744,8 +744,6 @@ namespace seq {
unsigned m_num_input_mems = 0; unsigned m_num_input_mems = 0;
nielsen_stats m_stats; nielsen_stats m_stats;
// external cancellation callback: returns true if solving should abort
std::function<bool()> m_cancel_fn;
// ----------------------------------------------- // -----------------------------------------------
// Integer subsolver (abstract interface) // Integer subsolver (abstract interface)
@ -835,9 +833,6 @@ namespace seq {
// enable/disable Parikh image verification constraints // enable/disable Parikh image verification constraints
void set_parikh_enabled(bool e) { m_parikh_enabled = e; } void set_parikh_enabled(bool e) { m_parikh_enabled = e; }
// set a cancellation callback; solve() checks this periodically
void set_cancel_fn(std::function<bool()> fn) { m_cancel_fn = std::move(fn); }
// generate next unique regex membership id // generate next unique regex membership id
unsigned next_mem_id() { return m_next_mem_id++; } unsigned next_mem_id() { return m_next_mem_id++; }

1
src/smt/theory_nseq.cpp
View file

@ -48,7 +48,6 @@ namespace smt {
void theory_nseq::init() { void theory_nseq::init() {
m_arith_value.init(&get_context()); m_arith_value.init(&get_context());
m_nielsen.set_cancel_fn([this]() { return get_context().get_cancel_flag(); });
} }
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------